Peter Seibel - Coders at Work - Reflections on the craft of programming

These were numbers about a hundred digits each and it really wasn’t feasible to trace through the entire thing by hand because the division routine was fairly complicated and these were big numbers. So I stared at the code and didn’t see anything obviously wrong. But one thing that caught my eye was a conditional step that I didn’t quite understand.

These routines were based on algorithms from Knuth, so I got Knuth off the shelf and read the specification and proceeded to map the steps of Knuth’s algorithm onto the assembly-language code. And what caught my eye in Knuth was a comment that this step happens rarely—with a probability of roughly only one in two to the size of the word. So we expected this to happen only once in every four billion times or something.

From that I reasoned to myself, “These routines are thought to be well shaken out, thus this must be a rare bug; therefore the problem is likely to be in the rarely executed code.” That was enough to focus my attention on that code and realize that a data structure wasn’t being properly copied. As a result, later down the line there was a side-effect bug where something was getting clobbered. And so I repaired that and then fed the numbers through and got the right answer and Gosper seemed to be satisfied.

A week later he came back with two somewhat larger numbers and said, “These don’t divide properly either.” This time, properly prepared, I returned to that same little stretch of ten instructions and discovered there was a second bug of the same kind in that code. So then I scoured the code thoroughly, made sure everything was copied in the right ways, and no errors were ever reported after that.

Seibel:That’s always the trick—that there’s going to be more than one.

Steele:So I guess there’s lessons there—the lesson I should have drawn is there may be more than one bug here and I should have looked harder the first time. But another lesson is that if a bug is thought to be rare, then looking at rarely executed paths may be fruitful. And a third thing is, having good documentation about what the algorithm is trying to do, namely a reference back to Knuth, was just great.

Seibel:When it’s not just a matter of waking up in the middle of the night and realizing what the problem is, what are your preferred debugging techniques? Do you use symbolic debuggers, print statements, assertions, formal proofs, all of the above?

Steele:I admit to being lazy—the first thing I will try is dropping in print statements to see if it will help me, even though that is probably the least effective for dealing with a complicated bug. But it does such a good job of grabbing the simple bugs that it’s worth a try. On the other hand, one of the great revelations in the evolution of my thinking about programming was when I was working on that one project in Haskell. Because it was a purely functional language, I couldn’t just drop in print statements.

This forced me to go 100 percent to a regimen of unit testing. So I proceeded to construct thorough unit tests for each of my subprocedures. And this turned out to be a very good discipline.

This has influenced the design of Fortress to try to include features that would encourage the construction of unit tests. And recording them alongside the program text, rather than in separate files. To that extent we borrowed some ideas of say, Eiffel’s Design by Contract and similar things where you can put preconditions and postconditions on procedures. There are places where you can declare test data and unit-test procedures, and then a test harness will take care of running those whenever you request.

Seibel:Since you just mentioned Design by Contract, how do you use assertions in your own code?

Steele:I have a tendency to drop in assertions, particularly at the beginnings of procedures and at important points along the way. And when trying to—maybe “prove” is too strong a word—trying to justify to myself the correctness of some code I will often think in terms of an invariant and then prove that the invariant is maintained. I think that’s a fruitful way to think about it.

Seibel:How about stepping through code in a debugger? Is that something you’ll do if all else fails?

Steele:It depends on the length of the program. And of course you can have tools that will help you to skip sections you don’t need to step through because you’re confident that those parts are OK. And of course Common Lisp has this very nice STEPfunction, which is very helpful. I’ve stepped through a lot of Common Lisp code. The ability to skip over particular subroutines whose details you trust, of course, buys you a lot. Also the ability to set traps and say, “I really don’t need to look at this until this particular loop has gone around for the seventeenth time.” And there were hardware tools to support that on the PDP-10, which was nice, at least at MIT. They tended to modify their machines in those days, to add features. And there’s a lot to be said for watching the actual execution of code in various ways.

Seibel:Do you ever try to formally prove your code correct?

Steele:Well, it depends on the code. If I’m writing code with some kind of tricky mathematical invariant I will go for a proof. I wouldn’t dream of writing a sorting routine without constructing some kind of invariant and proving it.

Seibel:Peter van der Linden in his book Expert C Programming has a sort of dismissive chapter about proofs in which he shows a proof of something, but then, ha ha, this proof has a bug in it.

Steele:Yes, indeed. Proofs can also have bugs.

Seibel:Are they at least less likely to have a bug than the code which they are proving?

Steele:I think so, because you come at it in a different way and you use different tools. You use proofs for the same reason you use data types, or for the same reason that mountain climbers use ropes. If all is well, you don’t need them. But they increase the chance of catching it if something does go wrong.

Seibel:I suppose the really bad case would be if you had a bug in your program and then a compensating bug in your proof. Hopefully that would be rare.

Steele:That can happen. I’m not even sure it’s necessarily rare, because you tend to construct the proof to match the structure of the code. Or conversely, if you’ve got a proof in mind as you’re writing the code, that tends to guide your construction of the program. So you really can’t say the code and the proof are totally independent, in the probabilistic sense. But you can bring different tools and different modes of thought to bear.

In particular, the details of the programming tend to take a local point of view and the invariants tend to focus on the global point of view. It’s in doing the proof that you cause those two things to interact. You look at how the local steps of the program affect the global invariant you’re trying to maintain.

One of the most interesting exercises in my career was the time I was asked to review a paper for CACM by David Gries on proving a garbage collector algorithm correct, a parallel garbage collector. Susan Owicki was a student of Gries’s and she developed some tools for proving parallel programs correct, and he decided to apply these techniques to a version of a parallel garbage collector that had been developed by Dijkstra. The whole piece of code fit on, I think, a half a page. And then the entire rest of the paper was the proof of correctness.

I cranked through the proof and tried to verify every step for myself. And what makes it tricky is, in effect, every statement in the program has the potential to violate any invariant because it’s a parallel program. So the Owicki technique involves cross-checking these at all points. And it took me about 25 hours to go through, and in the process I found a couple of steps I couldn’t push through. So I reported this and it turned out they did represent bugs in the algorithm.