The development of complex hard- and software systems is very complicated and prone to introducing errors. One technique to use a computer to systematically analyse the design (high-level description) of such a system is called model checking. A model checking tool checks whether a design meets desired functional requirements. Although successful, the use of model checking in software development projects is not very common (yet), due to its high resource requirements; its calculations are time consuming, and it needs lots of computer memory.
In the GEARS project, we investigate how a state-of-the-art model checking technique, called IC3, can be accelerated by using General Purpose Graphics Processing Units (GPGPUs, or GPUs for short). GPUs were originally designed for the fast processing of video related tasks, but nowadays they can also be used for other, computationally intensive tasks. IC3 intensively uses methods to solve the so-called propositional satisfiability problem. Therefore, in the GEARS project, we first of all focus on solving this type of problem using GPUs. Our project is the first to investigate whether model checking problems expressed as propositional satisfiability problems and IC3 can be efficiently solved with the use of GPUs.
The propositional satisfiability problem is a fundamental mathematical problem that is the foundation of many practical decision and optimisation problems in various domains of computer science, such as artificial intelligence, operational research, the design of hardware, and the verification of hard- and software. Problems such as the planning of tasks and the colouring of graphs can be expressed as propositional satisfiability problems. The propositional satisfiability problem has as input a logical proposition, and the question whether the atomic formulas in the proposition can be assigned the value TRUE or FALSE, such that the proposition evaluates to TRUE. For instance, consider the following proposition:
(p1 or p2) and ((not p1) or p3)
This proposition is satisfiable, because if we assign TRUE to both p2 and p3, then the proposition evaluates to TRUE. No methods are known to exist to efficiently solve the propositional satisfiability problem, but various methods have been developed that use heuristics to solve particular problems derived from real applications in reasonable time.
In previous work, one has already investigated the potential to apply GPUs to accelerate the solving of propositional satisfiability problems. However, in those cases, one has always focussed on solving such problems in general, and it is known that when one focusses on particular variants of the problem, such as problems stemming from model checking, that particular heuristics will not work well, while others will. In the GEARS project, we focus specifically on model checking problems. Besides this, it is known that IC3 can be performed in parallel. During the execution of IC3, many propositional satisfiability problems are generated, which can be solved independently of each other. This offers an extra potential for parallel computing. Contrary to multi-core processors, that allow to perform tens of computations in parallel, one can use GPUs to conduct thousands of computations simultaneously. Therefore, there is a large potential for the efficient acceleration of model checking with GPUs.