The Taub Faculty of Computer Science Events and Talks

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.