Time, Fences and the Ordering of Events in TSO

TL;DR

This paper develops a semantic framework for understanding when synchronization primitives are necessary under the TSO memory model, using a novel occurs-before relation to analyze event ordering and causality.

Contribution

It introduces a TSO-specific occurs-before relation and proves that creating such chains is essential for event ordering, generalizing prior lower bounds for shared memory implementations.

Findings

Characterizes when fences and RMWs are necessary in TSO

Proves that event ordering requires occurs-before chains

Extends reasoning from asynchronous systems to 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.