M.Sc Thesis

M.Sc StudentKuperstein Michael
SubjectPreserving Correctness Under Relaxed Memory Models
DepartmentDepartment of Computer Science
Supervisors PROF. Eran Yahav
PROF. Martin Wechev
Full Thesis textFull thesis text - English Version


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:

(i) 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.

(ii) 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.