Dynamic Synthesis for Relaxed Memory Models [abstract] (ACM DL, PDF)
Feng Liu, Nayden Nedev, Nedyalko Prisadnikov, Martin Vechev, and Eran Yahav
Proceedings of the 33nd ACM SIGPLAN Conference on Programming
Language Design and Implementation (PLDI), June 2012.
Modern architectures implement relaxed memory models which may reorder memory
operations or execute them non-atomically. Special instructions called memory
fences are provided, allowing control of this behavior.
To implement a concurrent algorithm for a modern architecture, the programmer
is forced to manually reason about subtle relaxed behaviors and figure out ways
to control these behaviors by adding fences to the program. Not only is this
process time consuming and error-prone, but it has to be repeated every time
the implementation is ported to a different architecture.
In this paper, we present the first scalable framework for handling real-world
concurrent algorithms running on relaxed architectures. Given a concurrent C
program, a safety specification, and a description of the memory model, our
framework tests the program on the memory model to expose violations of the
specification, and synthesizes a set of necessary ordering constraints that
prevent these violations. The ordering constraints are then realized as
additional fences in the program.
We implemented our approach in a tool called DFENCE based on LLVM and used it
to infer fences in a number of concurrent algorithms. Using DFENCE, we perform
the first in-depth study of the interaction between fences in real-world
concurrent C programs, correctness criteria such as sequential consistency and
linearizability, and memory models such as TSO and PSO, yielding many
interesting observations. We believe that this is the first tool that can
handle programs at the scale and complexity of a lock-free memory allocator.