A team of researchers have devised a method called Armada that verifies that a class of complex programs is bug-free without the need for traditional software testing.
The system makes use of a technique called formal verification to prove whether a piece of software will provide the desired output. It targets software that runs using concurrent execution, a widespread method for boosting performance, which has been a particularly challenging feature to which to apply this technique.
The collaborative effort between Microsoft Research, Carnegie Mellon, and the University of Michigan, was recognized at ACM’s 2020 Programming Language Design and Implementation conference with a Distinguished Paper Award.
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 Manos Kapritsos, assistant professor of computer science and engineering at U-M and 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.”