DMC Model Checker - Delta-Driven Variable-Length Next-State Generation via Recursive Compression
Freark van der Berg is a PhD student in the Department of Formal Methods and Tools. Promotor is prof.dr. J.C. van der Pol from the Faculty of Electrical Engineering, Mathematics and Computer Science.
In today's society, software and hardware systems are involved in our every day lives, ranging from control systems in planes, trains and automobiles to financial systems, to communication networks. The reliability of these systems is critical: one small error can lead to the loss of lives, catastrophic financial loss or disruption of essential infrastructure. Designing such systems correctly is notoriously difficult.
Computers have become increasingly complex over the years to cater for the ever-growing thirst for performance. Various innovations have led to great improvements, but to harness this power, the software running on said hardware has increased in complexity as well. A compiler today is not just a translator, but also a performance engineer, security guard, and portability layer between humans and increasingly diverse and complex hardware.
Due to physical limitations, the increase in performance the past two decades has predominantly been achieved by adding more computational cores to CPUs, with shared access to main memory. To use these multi-core CPUs, multi-threaded software has increased in popularity, such that threads can be spread evenly over the computational cores to distribute work. To communicate to each other, these threads perform write and read operations to the shared memory.
This manner of communication is notoriously difficult to design and implement correctly: because the threads execute seemingly independently, there are a vast number of possible interleavings of the memory operations of all the threads. This can cause very subtle and hard to debug errors, potentially leading to system failures which can have great consequences.
Correct communication between threads is paramount. One way to aid in writing correct software is by using model checking. Model checking is a technique that can be used to check for violations in all possible states a program can be in. In this manner, all possible interleavings of the memory operations of all independently running threads can be checked automatically.
In this thesis, we aim to advance the application of model checking to software.
At a high-level, our approach to achieve this is by introducing an improved method of storing the variable-length states a program can be in, in a losslessly compressed manner (Recursive Compression). Then, using this particular lossless compression, we introduce a method of exhaustive search that does not need to consider complete states: only changes between states are enough (Delta-Driven Variable-Length Next-State Generation).
We implement these techniques in the novel DMC Model Checker and show the efficacy of this approach by applying it to tests of concurrent data structures. We show that the techniques can lead to multiple orders of improvement, both in terms of exploration speed (states per second) and compression (bytes per state).
