GPU Enabled Automated Reasoning

The development of complex hardware and software systems is error-prone and costly. Testing can be effective to detect the presence of bugs in these designs, but it cannot prove their absence. One technique that can provide worthful feedback on the correctness of system designs is Model Checking (MC). MC is an automated reasoning technique to find flaws in hardware and software systems. Successful examples include verifying CERN controllers, railway interlockings, nuclear control systems, and medical imaging. Companies such as Amazon, Microsoft, and Facebook use and develop MC technology to ensure their products behave functionally correct. MC is used to catch potential bugs as early as possibleópreferably at the design phaseóto make the necessary modifications quickly and cost-effectively. Industry reliance on MC is thus not only for safety but also for economic reasons. However, MC is computationally very demanding. It involves exhaustively analyzing a system design to determine whether it satisfies desirable functional specifications. Bounded Model Checking (BMC) is currently a contemporary symbolic technique that can analyze large designs in reasonable time. BMC determines whether a model satisfies a certain property expressed in temporal logic, by translating the model checking problem to a propositional Satisfiability (SAT) problem, for instance.

In this thesis, we investigate how Graphics Processing Units (GPUs) can be employed effectively for BMC, narrowing our focus to the reasoning on Satisfiability. GPUs offer great potential for parallel computation, while keeping power consumption low. However, not all types of computation can trivially be performed on GPUs, in most applications, the algorithms need to be entirely redesigned.

We focus on the simplifications of SAT formulas prior to the solving process (i.e. preprocessing); a strategy that leads to a drastic prune of the formula size, and the search space. Next, we present a new SAT solver which rigorously interleaves the search with simplifications (i.e. inprocessing). Inprocessing has proven to be powerful in modern SAT solvers, particularly when applied on SAT formulas encoding software and hardware verification problems. The new solver is hybrid, capable of running the parallel part on the GPU while the actual solving will run sequentially on the Central Processing Unit (CPU). Further, we discuss the design aspects of the data structures and the memory management of our parallel implementations, leading to substantial improvements in execution performance.

Concerning the solving part, we extend the Conflict-Driven Clause Learning (CDCL) search algorithm with Multiple Decision Making (MDM). The MDM procedure has the ability to make and propagate multiple decisions at once. Moreover, it is augmented with local search to improve the accuracy in assigning truth values to these decisions.

Finally, we describe the integration of our solver to a state-of-the-art bounded model checker. After optimizing further the inprocessing engine and making the solving process incremental, we study the impact of GPU-enabled BMC on software verification using Amazon Web Services (AWS) C99 library.