Dynamic synthesis for relaxed memory models

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...

• Type: Journal
• Year: 2012
• Where: PLDI
• Authors: Feng Liu, Nayden Nedev, Nedyalko Prisadnikov, Martin T. Vechev, Eran Yahav
• Keywords: Concurrent Algorithms, Correctness Criteria, Memory Allocator, PLDI 2012, Programming Languages