Concurrency libraries can facilitate the development of multi-threaded

programs by providing concurrent implementations of familiar data

types such as queues or sets. There exist many optimized algorithms

that can achieve superior performance on multiprocessors by allowing

concurrent data accesses without using locks. Unfortunately, such

algorithms can harbor subtle concurrency bugs. Moreover, they require

memory ordering fences to function correctly on relaxed memory models.

To address these difficulties, we propose a verification approach that

can exhaustively check all concurrent executions of a given test

program on a relaxed memory model and can verify that they are

observationally equivalent to a sequential execution. Our

CheckFence prototype automatically translates the C

implementation code and the test program into a SAT formula, hands the

latter to a standard SAT solver, and constructs counterexample traces

if there exist incorrect executions. Applying CheckFence to

five previously published algorithms, we were able to (1) find several

bugs (some not previously known), and (2) determine how to place

memory ordering fences for relaxed memory models.

PDF file

PowerPoint presentation

In  Programming Language Design and Implementation (PLDI)

Details