Checking Consistency of Concurrent Data Types on Relaxed Memory Models

Concurrency libraries can facilitate the development of multi-threaded programs by providing concurrent implementations of familiar data types such as queues or sets. On multiprocessors, optimized algorithms can achieve superior performance by allowing concurrent data accesses without using locks for mutual exclusion. Unfortunately, such implementations often harbor subtle concurrency bugs and are susceptible to relaxations in the memory model. Moreover, state-of-the-art verification tools are not directly applicable, because they assume a sequentially consistent memory model or race-free programs.
We present a novel verification approach for this domain (realized in our tool CheckFence) that helps the algorithm designer or library implementor by exhaustively checking all concurrent executions of a given symbolic test program on the chosen memory model and verifying that they are observationally equivalent to some serial execution. CheckFence automatically translates the C implementation code (including memory ordering fences) and the test program into a SAT formula, hands the latter to a standard SAT solver, and presents formatted counterexample traces if there exist incorrect executions. We applied CheckFence to seven previously published algorithms and were able to (a) confirm correct behavior for sequentially consistent platforms or find bugs in some cases, and (b) determine how to insert memory ordering fences for correct execution on architectures with relaxed memory models.