So, who hasn’t had an application or device driver lock up on their computer? Everyone knows that frustration.
To counter this, researchers at Microsoft have come up with a mathematical solution to lockups that examines your code and asks the same question: “Sarah Connor?”
The program from Microsoft Research is called the TERMINATOR software verification project. Instead of running for governor of California, this tool examines your software code and applies mathematical principles to all of the loops to insure they won’t hang.
A common misconception is that when software hangs, it’s frozen. It hasn’t ceased to execute, what has happened is it’s gotten caught in an infinite loop from which it cannot break, according to Microsoft researcher Byron Cook.
Examples include a device driver that continuously tries to reinitialize a piece of unresponsive hardware without a hard-coded timeout or an application that attempts to connect to the network when there is no connection, and it doesn’t know when to stop trying.
“When you’re in IE or Firefox, when it’s locked up, you’re always wondering if it will stop. So it’s always impossible to know,” said Cook. Since we have no way of knowing if the application is busy or locked up, most people err on the side of ending the application.
This is known as The Halting Problem, first identified by computing pioneer Alan Turing, who proved it is impossible to create a way of proving that all applications will always run to completion. “What you would like to do is just for once and for all know the loop won’t lock up in this case,” said Cook.
To that end, he devised a mathematical solution that applies a logical test to applications to see if they eventually return control to the person. TERMINATOR is accompanied by a second program, SLAM, which is designed specifically for device drivers.
A programmer runs these tools, perhaps overnight, and the results prove mathematically that your loops won’t go into a lock, or it shows where you are getting stuck, such as creating conditions that can never be met (they forget to add counters, or forget to add an increment to the counter).
Cook couldn’t speak for when this technology will be made available in Visual Studio or other Microsoft developer tools, but he said “it’s safe to say that these new proof-based tools that find proof of correctness will affect the quality of software. We’re seeing that in device drivers.”
Microsoft is using TERMINATOR and SLAM internally in its Vista testing and it’s resulting in better-quality drivers, Cook said.
He also expects future operating systems to be less prone to hangs, and that embedded applications will become more comprehensive. Embedded, vertical applications, such as those used in hospitals, use a minimum of loops because the last thing they need is to get caught in an infinite loop.
The result will be embedded devices able to handle more functionality, because developers of embedded devices won’t have to fear a lock-up.
“Microsoft claims that many Windows lockups come from third-party software, with device drivers being one annoying culprit,” said Joe Wilcox, senior analyst with JupiterKagan.
“If Microsoft’s claim is true, clean drivers would go a long way to improving Windows performance and stability.”
