Modern CPUs and GPUs use many optimizations when executing code such as out-of-order execution, buffering/caching of memory accesses, and even speculation. While these optimizations are invisible to single-threaded programs, they can impact the behavior of concurrent one's and thus lead to bugs.
A classical example is the so-called message passing, where a producer stores new data and then sends a signal to a consumer who, after receiving the signal, tries to access the data.
If producer and consumer run on different CPUs, the aforementioned optimizations can break this communication in two ways. If the producer buffers its data store instead of sending it to main memory, the consumer may end up seeing old/stale data from the main memory. But even if the producer makes sure to flush its buffers before sending the signal, the consumer could speculatively access the data before it got the signal to do so, again seeing outdated values.
Therefore, to understand the behavior of a concurrent program it is not sufficient to just look at its code but also at the hardware that is executing it. Fortunately, rather than taking the concrete hardware into account, it is possible to reason over a more abstract description of the hardware known as its (weak memory) consistency model. We are interested in verification techniques that take these consistency models into account.
Dartagnan is a bug-finding tool for concurrent programs under weak memory consistency.
It takes as input a program (C/LLVM/Assembly/SPIRV), a memory consistency model (X86, AARCH64 v8-A, POWER, C11, Vulkan, etc., expressed in the CAT language), and a specification (assertions, data race freedom, deadlock freedom) and checks if the specification can be violated if the given program is executed under the given memory consistency model.
The underlying technique of Dartagnan is so-called bounded model checking (BMC).
The goal of BMC is to reduce the verification problem to a logical satisability problem such as SAT or SMT that is then solved by off-the-shelf solvers like Microsoft's Z3.
To make this reduction possible, Dartagnan bounds the loops of the program yielding a bounded verification instance. Bugs in the bounded program are bugs in the full program but the converse does not hold.
For this reason, Dartagnan can, in general, only prove the existence of bugs but not their absence.
Dartagnan is open-source and available on Github. Further information about the usage of Dartagnan, related publications, and won awards are also found on its github page.
Team: Thomas Haas, René Pascal Maseli
RAT is a tool for automatically proving properties of and between consistency models.
It takes as input a consistency model, a set of assumptions, and a set of assertions all of which are described in the relational algebra language CAT, and then tries to prove if the consistency model satisfies the assertions under the given assumptions.
The underlying proof technique is based on cyclic proof tableaus, a proof system that can naturally express proofs with repeating subproofs, that is, proofs by induction.
RAT is open-source and available on Github. The tool is still work-in-progress and bugs are expected.
Team: Jan Grünke, Thomas Haas