Time, Fences and the Ordering of Events in TSO

Abstract

The Total Store Order (TSO) is arguably the most widely used relaxed memory model in multiprocessor architectures, widely implemented, for example in Intel's x86 and x64 platforms. It allows processes to delay the visibility of writes through store buffering. While this supports hardware-level optimizations and makes a significant contribution to multiprocessor efficiency, it complicates reasoning about correctness, as executions may violate sequential consistency. Ensuring correct behavior often requires inserting synchronization primitives such as memory fences ($F$) or atomic read-modify-write ($RMW$) operations, but this approach can incur significant performance costs. In this work, we develop a semantic framework that precisely characterizes when such synchronization is necessary under TSO. We introduce a novel TSO-specific occurs-before relation, which adapts Lamport's celebrated happens-before relation from asynchronous message-passing systems to the TSO setting. Our main result is a theorem that proves that the only way to ensure that two events that take place at different sites are temporally ordered is by having the execution create an occurs-before chain between the events. By studying the role of fences and $RMW$s in creating occurs-before chains, we are then able to capture cases in which these costly synchronization operations are unavoidable. Since proper real-time ordering of events is a fundamental aspect of consistency conditions such as Linearizability, our analysis provides a sound theoretical understanding of essential aspects of the TSO model. In particular, we are able to generalize prior lower bounds for linearizable implementations of shared memory objects. Our results capture the structure of information flow and causality in the TSO model by extending the standard communication-based reasoning from asynchronous systems to the TSO memory model.