Bug-free programsEnsuring Complex Programs Are Bug-Free without Testing

A team of researchers have devised a way to verify that a class of complex programs is bug-free without the need for traditional software testing. Called Armada, the system makes use of a technique called formal verification to prove whether a piece of software will output what it’s supposed to. It targets software that runs using concurrent execution, a widespread method for boosting performance, which has long been a particularly challenging feature to apply this technique to.

The collaborative effort between the University of Michigan, Microsoft Research, and Carnegie Mellon was recognized at ACM’s Programming Language Design and Implementation (PDLI 2020) with a Distinguished Paper Award.

Michigan notes that concurrent programs are known for their complexity, but have been a vital tool for increasing performance after the raw speed of processors began to plateau. Through a variety of different methods, the technique boils down to running multiple instructions in a program simultaneously. A common example of this is making use of multiple cores of a CPU at once.

Formal verification, on the other hand, is a means to demonstrate that a program will always output correct values without having to test it with a full range of possible inputs. By reasoning about the program as a mathematical proof, programmers can demonstrate that bugs or errors are impossible and that its execution is airtight. This overcomes the shortcoming common to all programs, even without concurrency, that testing something exhaustively can be either impractical or actually impossible.

“Fundamentally, unless you try all the possible inputs, you may miss something,” says Prof. Manos Kapritsos, co-author on the paper. “And in practice, people do miss things. The systems we’re talking about are very complex, there’s no way that they can exhaustively try all the behaviors of the system.”

Formal verification offers an alternative to this need for exhaustive testing. But the process of generating a satisfactory proof turns out to be very difficult and time-consuming, especially as you delve into programs with the added complexity of concurrency.

“The main challenge in concurrent programs comes from the need to coordinate many different threads of code together,” says Upamanyu Sharma, co-author who worked on the project as an undergraduate at U-M. “To verify that multi-threaded programs are correct, we have to reason about the huge number of interleavings that are possible when multiple methods run at the same time.”