A Load-Buffer Semantics for Total Store Ordering

We address the problem of verifying safety properties of concurrent programsrunning over the Total Store Order (TSO) memory model. Known decisionprocedures for this model are based on complex encodings of store buffers aslossy channels. These procedures assume that the number of processes is fixed.However, it is important in general to prove the correctness of asystem/algorithm in a parametric way with an arbitrarily large number ofprocesses. In this paper, we introduce an alternative (yet equivalent) semantics to theclassical one for the TSO semantics that is more amenable to efficientalgorithmic verification and for the extension to parametric verification. Forthat, we adopt a dual view where load buffers are used instead of storebuffers. The flow of information is now from the memory to load buffers. Weshow that this new semantics allows (1) to simplify drastically the safetyanalysis under TSO, (2) to obtain a spectacular gain in efficiency andscalability compared to existing procedures, and (3) to extend easily thedecision procedure to the parametric case, which allows obtaining a newdecidability result, and more importantly, a verification algorithm that ismore general and more efficient in practice than the one for bounded instances.Comment: Logic in computer scienc