If the results bear out, it could add yet another tool in the arsenal of software developers that supplements conventional QA tests with algorithmic computations on the likelihood that some faulty piece of code will cause a program to stall.
A paper delivered by Byron Cook, a programming languages and tools researcher at Microsoft’s Cambridge, England labs, proposes an algorithm that mathematically determines a program’s liveness properties and the likelihood that it will terminate operations at the right time and return control to the original command.
The paper was delivered at Federated Logic, a computer science conference wrapping up in Seattle today.
Although existence of the algorithm alone doesn’t mean that developers could apply it tomorrow as part of QA routines, eventually it could be applied in tooling that drills down to the offending code.
In general, to validate mathematically that a program behaves as designed, it is necessary to prove liveness and its flipside, safety. In plain English, safety is the assurance that the program won’t do anything bad or destructive, while liveness is the assurance that it will deliver the right result.
In turn, termination refers to the ability for a program or subroutine to stop executing when its and return control to the original program or routine when the task is done. Programs hang when they don’t terminate as planned, and that’s what Cook’s research addressed.
The origin of the research was an attempt to answer computing pioneer Alan Turing, who in 1936, anticipated that once electronic computing were invented, that there would be no way to mathematically prove that any program would behave absolutely properly. For 70 years, this has been known as The Halting Problem.
Cook’s research, aided by colleagues at several European universities, was to devise algorithms that would, in effect, be good enough.
The first hints came through earlier projects that dealt with prediction of safety properties that resulted in tools that debug, not through tests, but through mathematical analysis on a wide sampling of environmental variables. Over the past year, such tools were used to validate device drivers for Microsoft’s upcoming Vista operating system.
With apologies to Arnold Schwarzenegger, Cook named his project Terminator. The goal was developing algorithms that would mathematically prove whether code would or would not terminate properly.
We perform a symbolic proof, Cook said, explaining that the approach is meant to supplement, not replace traditional software QA and debugging efforts. Developers write code and hope that it will return control back to the caller [the routine that requested the task], but they’re not 100% sure it will hold. That could be fatal in situations like piloting aircraft or running medical devices.
Of course, Cook doesn’t claim that his team’s algorithms will provide such 100% assurance either, but in the long run they could provide another layer of defense in the software QA cycle.
While the tooling produced by Cook is Microsoft intellectual property, his findings will be freely available so others could devise their own tools.
