Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People

The Taub Faculty of Computer Science Events and Talks

Preserving Correctness Under Relaxed Memory Models
event speaker icon
Michael Kuperstein (M.Sc. Thesis Seminar)
event date icon
Wednesday, 25.05.2011, 12:30
event location icon
Taub 601
event speaker icon
Advisor: Dr. Martin Vechev and Dr. Eran Yahav
We present an approach for automatic verification of concurrent programs running under relaxed memory models. Verification under relaxed memory models is a hard problem. Given a finite state program and a safety specification, verifying that the program satisfies the specification under a sufficiently relaxed memory model is undecidable. For somewhat stronger memory models, the problem is decidable but has non-primitive recursive complexity. We use abstract interpretation to provide a verification procedure for programs running under relaxed memory models. Our main contributions are: -- A family of partial-coherence abstractions, which partially preserve information required for memory coherence and consistency, while allowing effective verification. -- A framework for automatic repair of programs. Given a program, a specification and a description of the memory model, our framework computes a set of constraints that guarantee the correctness of the program under the memory model. The framework then realizes those constraints syntactically as "memory fences", hardware instructions that ensure the constraints are never violated. We implemented our approach in a tool called BLENDER and used it to infer correct and efficient placements of memory fences for several nontrivial algorithms, including practical concurrent data structures and mutual exclusion primitives.