Abstract :
[en] Model-checking tools classicaly verify concurrent programs under the traditional Sequential Consistency
(SC) memory model, in which all accesses to the shared memory are immediately visible globally. However, modern multiprocessor architectures implement relaxed memory models, such as Total Store Order (TSO) (or its extension with locks x86-TSO), which allow many more possible executions and thus can introduce errors that were not present in SC. Of course, one can force a program executed in the context of TSO 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, rather than 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 (i.e. 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 model 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 check even designs that exploit the relaxed memory model in unusual
ways, and that may contain cycles.
We have also proposed a memory fence insertion algorithm that finds how to preserve the correctness of a program when it is moved from SC to TSO. Its starting point is a program that is correct for the usual sequential
consistency memory model (with respect to a given safety property), but that might be incorrect under x86-TSO. This program is then analyzed for this relaxed memory model and when errors are found (a broken 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.
In future work, we will investigate how to adapt our techniques to other common memory models, such as Partial Store Order (PSO), as well as how to optimally use the partial order reduction techniques.
