Memory Model Sensitive Analysis of Concurrent Data Types

Concurrency libraries can facilitate the development of multi-threaded programs by providing concurrent implementations of familiar data types such as queues and sets. Many optimized algorithms that use lock-free synchronization have been proposed for multiprocessors. Unfortunately, such algorithms are notoriously difficult to design and verify and may contain subtle concurrency bugs. Moreover, it is often difficult to place memory ordering fences in the implementation code. Such fences are required for correct function on relaxed memory models, which are common on contemporary multiprocessors. To address these difficulties, we describe an automated verification procedure based on bounded model checking that can exhaustively check all concurrent executions of a given test program on a relaxed memory model and can either (1) verify that the data type is sequentially consistent, or (2) construct a counterexample. Given C implementation code, a bounded test program, and an axiomatic memory model specification, our CheckFence prototype verifies operation-level sequential consistency by encoding the existence of inconsistent executions as solutions to a propositional formula and using a standard SAT solver to decide satisfiability. We applied CheckFence to five previously published algorithms and found several bugs (some not previously known). Furthermore, we determined where to place memory ordering fences in the implementations and verified their sufficiency on our test suite.