A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems

Alexander Linden
ULG
Friday, 20 January, 2012 - 16:00
Room: NO5 Solvay

In this talk, we address the problem of verifying and correcting
programs when they are moved from a sequential consistency execution
environment to a relaxed memory context. Specifically, it considers the
TSO (Total Store Order) relaxation, which corresponds to the use of
store buffers, and its extension x86-TSO, which in addition allows
synchronization and lock operations.

The proposed approach uses a previously developed verification tool that
uses finite automata to symbolically represent the possible contents of
the store buffers. Its starting point is a program that is correct for
the usual sequential consistency memory model, but that might be
incorrect under x86-TSO. This program is then analyzed for this relaxed
memory model and when errors are found (with respect to safety
properties), memory fences are inserted in order to avoid these errors.
The approach proceeds iteratively and heuristically, inserting memory
fences until correctness is obtained, which is guaranteed to happen.

An advantage of our technique is that the underlying symbolic
verification tool makes a full exploration possible even for cyclic
programs, which makes our approach broadly applicable. The method has
been tested with an experimental implementation and can effectively
handle a series of classical examples.

Joint with Pierre Wolper.