Abstract :
[en] Classical model-checking tools verify concurrent programs under the
traditional "Sequential Consistency" (SC) memory model, in which all
accesses to the shared memory are immediately visible globally, and where
model-checking consists in verifying a given property when exploring the
state space of a program. However, modern
multi-core processor architectures implement relaxed memory models, such as
"Total Store Order" (TSO), "Partial Store Order" (PSO), or
an extension with locks such as "x86-TSO", which allow stores to be delayed
in various ways and thus introduce many more possible executions, and hence
errors, than those present in SC. Of course, one can force a program executed
in the context of a relaxed memory system to behave exactly as in SC by adding
synchronization operations after every memory access. But this totally defeats
the performance advantage that is precisely the motivation for implementing
relaxed memory models instead of SC. Thus, when moving a program to an
architecture implementing a relaxed memory model (which includes most current
multi-core processors), it is essential to have tools to help the programmer
check if correctness (e.g. a safety property) is preserved and, if not, to
minimally introduce the necessary synchronization operations.
The proposed verification approach uses an operational store-buffer-based
semantics of the chosen relaxed memory models and proceeds by using finite
automata for symbolically representing the possible contents of the buffers.
Store, load, commit and other synchronization operations then correspond to
operations on these finite automata.
The advantage of this approach is that it operates on (potentially infinite)
sets of buffer contents, rather than on individual buffer configurations, and
that it is compatible with partial-order reduction techniques. This
provides a way to tame the explosion of the number of possible buffer
configurations, while preserving the full generality of the analysis. It is thus
possible to even check designs that may contain cycles.
This verification approach then serves as a basis to a memory fence insertion
algorithm that finds how to preserve the correctness of a program when it is
moved from SC to TSO or PSO. Its starting point is a program that is correct for
the sequential consistency memory model (with respect to a given safety
property), but that might be incorrect under TSO or PSO. This program is then
analyzed for the chosen relaxed memory model and when errors are found (a
violated safety property), 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.
