By Rob Knies
August 16, 2006 11:01 PM PT
It is May 28, 1936. A paper entitled On Computable Numbers With an Application to the Entscheidungsproblem is received by the London Mathematical Society for publication in its journal.
In the paper, the latest salvo in a mathematical debate that extends back to the dawn of the 20th century, Cambridge academic Alan Turing proves that a general algorithm to determine whether all possible combinations of programs and initial inputs will run to completion as intended is impossible to devise. Computer scientists refer to this as the “halting problem.”
Fast forward 70 years. Microsoft researcher Byron Cook, buttressed by his collaboration with a clutch of European computer scientists, prepares to deliver a series of lectures describing new automatic methods for proving program termination in most—and perhaps, someday, practically all—circumstances.
What’s going on here? Turing is popularly considered to be the father of modern computer science. The Association for Computing Machinery named its most prestigious technical honor the A.M. Turing Award. Is it possible that one of his enduring proofs is about to be upended?
Not quite. But someday, the impact of Turing’s result may be considered strictly academic. With the Terminator project, Cook, a researcher in the Programming Principles and Tools group within Microsoft Research’s Cambridge lab, is simply doing what researchers do: pursuing solutions to difficult problems and making scientific advances. In this case, Cook is challenging Turing’s result. In a sense, you could say he is whittling away at the impossible.
”Turing proved that, in general, proving program termination is ‘undecidable,’ ” Cook says. “However, this result does not preclude the existence of future program-termination proof tools that work 99.9 percent of the time on programs written by humans. This is the sort of tool that we’re aiming to make.”
Cook and his colleagues will present a series of lectures discussing these advances during the Federated Logic Conference, a mega-conference that combines all the top conferences that apply logic to computer science, which runs from Aug. 10-22 in Seattle.
What Cook and collaborators have set out to do is to create a tool that can automatically analyze software using mathematical techniques and confirm with a mathematical proof that the software will run as it is intended to run.
“Automatic formal verification tools are designed to algorithmically search for proofs of mathematically described properties,” Cook explains. “These properties can be divided into two categories. The first is ‘safety properties,’ which, roughly speaking, specify that bad things don’t happen. A number of tools now support the automatic proving of these safety properties.
“ ‘Liveness properties’ form the other category. They ensure that good things eventually happen. Termination is an example of a liveness property. Until now, no tool supported automatic methods for proving liveness properties. Terminator is designed to fill this gap.”
As the first known tool to break through this liveness-checking barrier, Terminator is being used to prove automatically termination and other liveness properties of commercial software.
“It’s being used, for example,” Cook says, “to automatically prove that Windows device-driver dispatch routines will always eventually stop trying to handle an event such as a mouse-click or an attempt to save a file.”
In fact, Terminator has been used to prove liveness properties of device drivers for Vista, the next version of Windows, and has helped the Vista product team iron out a number of significant wrinkles.
Work on the Terminator project began in the fall of 2004. Before starting the project, Cook had worked on the SLAM/Static Driver Verifier (SDV) project, which produced a tool designed to prove safety properties automatically and which has been used successfully to analyze Windows device drivers and to find bugs in flawed drivers.
“When SLAM/SDV reached a satisfying level of maturity,” Cook says, “I began to look for a bigger challenge. Proving termination and liveness is much harder than safety, so I began looking into this topic.”
“I am friends with Andreas Podelski and Andrey Rybalchenko at the Max-Planck-Institut in Saarbrücken [Germany]. In 2004, they had just proved a new theoretical result regarding well-founded mathematical relations using Ramsey's theorem,” he says. “This new result had implications in the area of proving program termination and liveness. I learned about this result while attending a weeklong meeting with Andreas and Andrey and others at Schloss Ringberg [a castle in the Bavarian Alps]. Their result was very exciting to me!
“A month after Schloss Ringberg, I traveled to Saarbrücken and worked with Andreas and Andrey for two or three additional days. We discussed ways to use the new result as the basis for automatic termination provers. These were terrifically chaotic meetings, Fog of War sort of stuff. And the dust only settled about an hour before I was due to take a train to Zürich [Switzerland] to visit ETH [Eidgenössische Technische Hochschule Zürich]. We finally got the Terminator algorithm right while sitting in Andreas’ kitchen. It was written on a bag from the pastry shop where we’d bought cakes that morning.”
That didn’t mean their work was done, though—far from it.
“Once we implemented that original algorithm and used it on real programs,” Cook recalls, “we found that it was less accurate that we’d hoped. In particular, our initial implementation was quite imprecise when it was applied to programs that make heavy use of data structures.”
Over the past year,” Cook recounts, “we’ve been working on methods that provide greater accuracy for programs that modify the shape of the data structures in their heap. This was work with the East London Massive [a collective of computer scientists and logicians from London and Cambridge]. For some time, we had a technique that seemed to work in practice, but the manual proof of the algorithm’s correctness was very tricky and took three or four tries. It required expertise in at least three different areas of research, and several of us lost many months on this proof. We finally finished the proof in June while working day and night together at Schloss Dagstuhl [another castle in the German countryside].”
Now that Terminator is being successfully used on real programs, what’s next? For Cook, the next step is to address concurrent programs.
“To date, Terminator only works for sequential programs,” he says. “The big challenge is liveness and termination for concurrent programs.”
Solving that would take him and his colleagues a long way toward their ultimate goal.
“Developers don’t want their code to break in the field,” Cook says. “Without automatic tools to prove program correctness, today, we must often make conservative design choices even though we know that we could develop better-performing but more complicated code. Imagine a future where this constraint no longer holds. To achieve this future, we need robust automatic formal verification tools that support the code that developers want to write and prove all of the properties that we need the code to obey.
“What I want is to make a program termination prover that can support all code written by industrial practitioners.”
“I am fortunate to be surrounded by smart researchers across Europe and the world who visit me often and invite me to their institutions,” he says, citing Daniel Kröning, Moshe Vardi, and others, in addition to Podelski, Rybalchenko, and his East London Massive cohorts.
“In London and Cambridge,” Cook says, “I’m surrounded by brilliant colleagues. And throughout Europe, I can draw on a rich pool of talent. I have ongoing collaborations and friendships with many of these people, meaning that I have a very varied and stimulating research environment to work in.”