Improving Verification with Parallel Software Model Checking

Created September 2017

Scalability is a fundamental challenge in software model checking (SMC) because current methods take too much time. We are developing algorithms for SMC that execute many operations in parallel, thereby leveraging multiple cores available in modern processors to improve scalability.

A Slow but Promising Method for Verifying Software

As the U.S. Department of Defense (DoD) becomes more software reliant, rigorous techniques to assure the correct behavior of programs are in great demand. Software model checking (SMC), the algorithmic analysis of programs to prove the correctness of their execution, is promising because it can identify software errors that escape detection with conventional testing methods. But SMC does not scale effectively to the large size of today's distributed embedded systems. Scalability is a challenge in SMC because of the state-space explosion. Most SMC tools are sequential. They consist of a single thread of execution that performs a sequence of computation steps. The large code size of military and industrial software means that current SMC methods take too long.

Recently, high-performance computing technologies such as multicore processors and clusters have emerged. Yet few SMC tools are designed to use this cheap and abundant computing power. A key reason is that model checking is essentially a graph search—where the graph is the state space of the model, which is difficult to parallelize effectively. This means that model checking does not obtain reasonable speedups. The main challenge of leveraging the power of multicores and clusters is figuring out how to partition the model checker's search among the CPUs in a way that limits duplicated effort and communication bottlenecks.

Speeding up Software Model Checking with Parallel Processing

A promising approach is to start with a verification algorithm that maintains a "worklist." The algorithm can distribute elements of the worklist to different CPUs in a balanced manner. As CPUs process the elements, new elements are added to the worklist. This strategy was used successfully to parallelize the breadth-first search in the SPIN model checker. We explored this strategy to parallelize a different algorithm for SMC, known as Generalized Property-Directed Reachability (GPDR).

GPDR falls in the broad class of constraint-satisfaction algorithms in logic and computer science, which include propositional satisfiability, planning, linear programming, and integer linear programming. GPDR is an algorithm for finding a satisfying solution to a set of logical constraints. This problem is also known as HORN-SMT reachability (HSR), for reasons originating from the restricted structure of the logical constraints that are involved. We decided to parallelize GPDR in our project because a number of SMC tools that verify different types of software—such as sequential C code, periodic real-time software, and Simulink and Lustre programs—work by reducing their problems to HSR. An effective parallel solution to HSR will have a wide impact that benefits these projects.

Model Checking with Portfolios of Solvers

We pursued the following hypothesis: Could a portfolio of GPDR algorithms running in parallel speed up model checking? To test this potential, we focused on PDR, a restricted form of GPDR tuned for verifying hardware circuits. In recent years, the PDR variant called IC3 has emerged as a leading algorithm for model checking hardware and has all the essential elements and complexities of GPDR (e.g., worklists). Success in parallelizing IC3 would likely carry over to GPDR.

We implemented three variants of parallel IC3 with different solution strategies. The algorithms vary in degree of synchronization and the aggressiveness with which they check proofs. They represent tradeoffs of overhead and likeliness of proof detection. The key idea behind each variant is to run several copies of IC3 in parallel on different machines or cores. All the copies share a common pool of learned partial solutions. These partial solutions are also known as lemmas. When one of the copies finds a new set of lemmas, it checks whether the collection of inductive lemmas across all the copies forms an inductive invariant. In other words, they share lemmas to reduce duplicated effort. The first solver to succeed provides the solution. Using a portfolio of 20 parallel algorithms, we observed speedups of 6 times faster to more than 300 times faster. More details about this research and our empirical results can be found in our paper for the International Conference on Verification, Model Checking, and Abstract Interpretation 2016.

Software Engineering Institute