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

This paper addresses 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 PSO (Partial Store Order)
memory model, which corresponds to the use of a store buffer for each shared
variable and each process. We also will consider, as an intermediate step, the
TSO (Total Store Order) memory model, which corresponds to the use of one store
buffer per process.

The proposed approach extends 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 (SC) memory model, but that might be incorrect under PSO with
respect to safety properties.
This program is then first analyzed and corrected for the TSO memory model, and
then this TSO-safe program is analyzed and corrected under PSO, producing a
PSO-safe program. To obtain a TSO-safe program, only store-load fences (TSO
only allows store-load relaxations) are introduced into the program. Finaly, to
produce a PSO-safe program, only store-store fences (PSO
additionally allows store-store relaxations) are introduced.

An advantage of our technique is that the underlying symbolic verification tool
makes a full exploration of program behaviors 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.