Technical Report MSC-2012-14

TR#:MSC-2012-14
Class:MSC
Title: Preserving Correctness Under Relaxed Memory Models
Authors: Michael Kuperstein
Supervisors: Eran Yahav, Martin Vechev
PDFMSC-2012-14.pdf
Abstract: This thesis addresses the problem of automatic verification and fence inference in concurrent programs running under relaxed memory models. Modern architectures implement relaxed memory models in which memory operations may be reordered and executed non-atomically. Instructions called memory fences are provided to the programmer, allowing control of this behavior. To ensure correctness of many algorithms, the programmer is often required to explicitly insert memory fences into her program. However, she must use as few fences as possible, or the benefits of the relaxed architecture may be lost. It is our goal to help automate the fence insertion process.

We present a framework for automatic inference of memory fences in concurrent programs, relieving the programmer from this complex task. The framework consists of two parts: * An algorithm that given a finite-state program, a safety specification and a description of the memory model computes a set of ordering constraints that guarantee the correctness of the program under the memory model. The computed constraints are maximally permissive: removing any constraint from the solution would permit an execution violating the specification. These constraints are then realized as additional fences in the input program. * A family of novel partial-coherence abstractions, specialized for relaxed memory models. These abstractions allow us to extend the applicability of the algorithm to programs that are infinite-state under the relaxed memory model, even when they were finite-state under the "standard" sequentially consistent model.

We implemented our approach in a pair of tools called Fender and Blender and used them to infer correct and efficient placements of fences for several non-trivial algorithms, including practical mutual exclusion primitives and concurrent data structures.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2012/MSC/MSC-2012-14), rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the MSC technical reports of 2012
To the main CS technical reports page

Computer science department, Technion
admin