Replacing Store Buffers by Load Buffers in Total Store Ordering

We consider the verification of concurrent programs running under the classical TSO (Total Store Order) memory model. The model allows write to read relaxation corresponding to the addition of an unbounded store buffer (that contains pending store operations) between each processor and the main memory. In this talk, we introduce a novel semantics which we call the dual TSO semantics that replaces each store buffer with a load buffer that contains pending load operations. The flow of information is reversed, i.e., store operations are performed by the processes atomically on the main memory, while values of variables are propagated from the memory to the load buffers of the processes. We show that the two semantics are equivalent in the sense that a program will reach identical sets of states when running under the two semantics. Furthermore, we present a simple and effective reachability algorithm for checking safety properties of programs running under the dual semantics.