View article

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 …