Brief Announcement: Time, Fences and the Ordering of Events in TSO

Modern multiprocessors rely on relaxed memory models to improve performance through techniques such as store buffering and out-of-order execution. Among these, Total Store Order (TSO) – used in Intel’s x86 and x64 architectures – is one of the most widely deployed. TSO increases efficiency by allowing writes to be held temporarily in per-process store buffers, deferring their visibility to other processors. However, this optimization breaks sequential consistency (SC) [11], making reasoning about correctness more difficult: a program correct under SC may fail under TSO due to delayed write visibility. To ensure correct behavior under TSO, programmers can use synchronization primitives such as memory fences ($𝙵$) and read-modify-write ($\mathrm{𝚁𝙼𝚆}$) operations. These enforce memory ordering by flushing buffers or performing atomic accesses. While effective, they limit concurrency and reduce performance [4, 9, 17]. Determining when such synchronization is truly necessary is therefore a central question in the study of weak memory models such as TSO.

Lamport’s happens-before relation [10] is central in asynchronous computing, underlying vector clocks, race detection, causal memory [12, 7, 1], and more. Happens-before was originally defined in asynchronous message-passing models, and it captures all of the information about timing that processes can obtain in such settings. In a recent paper, we proved a theorem called Delaying the Future (DtF) that provides a close formal connection between happens-before and the ability to reorder actions and events in asynchronous message-passing systems [14]. Roughly speaking, DtF implies that if there is no message chain between an operation $A$ and an operation $B$ in a given run $r$, then there is a run $r^{\prime }$ that is indistinguishable to all processes from $r$ in which $A$ takes place after $B$ does in real-time. This is of importance, for example, when considering linearizable implementations of concurrent objects, since the real-time order of event invocations and completions plays a central role in the definition of Linearizability [8]. The happens-before relation has been considered in different models, including TSO [3]. In this work, we introduce a new definition for the analogue of happens-before in TSO, which we call the occurs-before relation. One of the differences is that our definition stems from an operational model of TSO, whereas previous definitions such as in [3] are formulated using declarative models. As a result, our approach employs a lower level of abstraction, making it easier to derive concrete implementation constraints. We demonstrate the analogy between the classical happens-before relation of message chains to our occurs-before relation by proving a version of the DtF theorem for TSO, which is obtained by replacing “happens before” by “occurs before.” This makes it possible to prove necessary conditions on the use of synchronization in linearizable TSO implementations, much in the spirit and style that [14] does for linearizable register implementations in asynchronous message passing.

This section outlines the main features of our model; the reader should consult the full version [15] for additional details. The model is based on the operational definition of TSO given in [6]. (Similar, though slightly different, operational models for TSO have appeared, e.g., in [16, 5].) It consists of a set $\mathrm{\Pi }=\{1,\mathrm{\dots },n\}$ of $n$ processes and a finite set $\mathrm{𝖵𝖺𝗋}$ of variables. A basic TSO state is a pair $\sigma =⟨𝗆,\mathrm{𝖻𝗎𝖿}⟩$, where $𝗆\in \mathrm{𝖵𝖺𝗋}\to \mathrm{𝖵𝖺𝗅}$ describes the main memory and $\mathrm{𝖻𝗎𝖿}\in \mathrm{\Pi }\to {(\mathrm{𝖵𝖺𝗋}\times \mathrm{𝖵𝖺𝗅})}^{\ast }$ assigns a queue called a store buffer to every process. Processes can perform actions from the set $\{𝚁[x],𝚆[x,v],𝙵,\mathrm{𝚁𝙼𝚆}[x,v_{\text{exp}},v_{\text{new}}],\perp \}$. These correspond, respectively, to reading the value of $x$ (from local buffer if it contains an unexecuted write to $x$ and from the physical variable $x$ in memory otherwise), writing the value $v$ in $x$ ($v$ is appended to the local buffer), performing a fence (which occurs only when the local buffer is empty), performing a read-modify-write action $\mathrm{𝚁𝙼𝚆}[x,v_{\text{exp}},v_{\text{new}}]$ (which occurs only if the buffer is empty and the value of $x$ in the memory is $v_{\text{exp}}$. Its effect is to write $v_{\text{new}}$ directly to the memory). To account for propagating values from the store buffer to variables in memory, we associate with each $i\in \mathrm{\Pi }$ a “local dispatcher” component $d_i$ with a single action $\mathrm{𝚙𝚛𝚘𝚙}$, whose impact is to propagate a write command from the buffer queue to the memory. We denote $\mathrm{Ag}\triangleq \mathrm{\Pi }\cup {\{d_i\}}_{i\in \mathrm{\Pi }}$ and call its elements agents. Reads and writes are always enabled, while fences, $\mathrm{𝚁𝙼𝚆}$ and $\mathrm{𝚙𝚛𝚘𝚙}$ actions can take place only if specific preconditions hold.

We think of an action taking place as being an event. It is convenient to consider two types of read events: $\mathrm{𝚁𝚏𝙱}(x,v)$ and $\mathrm{𝚁𝚏𝙼}(x,v)$. The former is when the value of $x$ is read from the store buffer, and the latter is when the value of $x$ is read from the variable $x\in 𝗆$ in memory. In both instances, the value returned by the read action is $v\in \mathrm{𝖵𝖺𝗅}$. Using ${\beta |}_x$ to denote the restriction of a store buffer $\beta$ to pairs of the form $⟨x,\mathrm{\_}⟩$ involving writes to $x\in 𝗆$, the preconditions and effects of the event of a single action being performed in a TSO state $\sigma =⟨𝗆,\mathrm{𝖻𝗎𝖿}⟩$ are defined as follows:

A TSO action is considered a memory access of the variable $x$ if it is either a $\mathrm{𝚁𝙼𝚆}[x,\cdot ]$, a $\mathrm{𝚙𝚛𝚘𝚙}$ action resulting in $\mathrm{𝚙𝚛𝚘𝚙}(x,\cdot )$, or a read action $𝚁[x]$ resulting in $\mathrm{𝚁𝚏𝙼}(x,\cdot )$.

In asynchronous message-passing systems, the only way that a protocol can ensure that an action takes place later than a specific event at another process, is by forcing the action to be delayed until a message chain from the second process has been constructed. This is Lamport’s happens-before relation ([10]). We now define an analogous relation for TSO, where scheduling and propagation are asynchronous and processes lack direct knowledge of event timing. Complicating matters is the fact that distinct processes can read different values of a variable $x$ at the same time. Our occurs-before relation, also builds chains across process timelines,¹¹1We do not call this relation “happens-before” because the latter has become synonymous with message chains over the last five decades, and the new relation in TSO has a different flavor. and is defined as follows:

What makes ${\stackrel{ob}{\rightsquigarrow }}_r$ interesting and useful is the fact that, in a precise sense, it covers all the information that may be available to the processes regarding the ordering of events. We will show that, roughly speaking, if an event $e$ in $r$ is not related by ${\stackrel{ob}{\rightsquigarrow }}_r$ to another event $e^{\prime }$ in $r$, then there is a run $r^{\prime }$ that is indistinguishable from $r$ in which $e^{\prime }$ takes place strictly before $e$ does. We now turn to prove a more general result which will imply this fact.

Our goal is to use the occurs-before relation to prove lower bounds and necessary conditions on protocol structure. First, we show that processes cannot guarantee a specific event order without an occurs-before chain. If a process has the same local state at two execution points where it moves, it will take the same action at both points; events that did not modify its state cannot affect its behavior. This motivates the definitions of ${\mathrm{𝙿𝚊𝚜𝚝}}_r(S)$, the set of nodes in the causal past of $S$ and of runs local equivalence.

We can now show:

Intuitively, Theorem 4 implies that everything outside the ${\mathrm{𝙿𝚊𝚜𝚝}}_r$ of a node (or set of nodes) can be moved forward in time by an arbitrary amount, while preserving the timing of events in this past. This implies that without an $\stackrel{ob}{\rightsquigarrow }$ connection, events and operations preceding a given operation can be shifted to no longer precede it, without changing its outcome. If changing the real-time order of two operations can affect the correctness of a given execution, as it typically does when linearizability is required, then implementations must ensure that operations whose order should not be changed are related by $\stackrel{ob}{\rightsquigarrow }$. In some cases, e.g., when a process runs solo, it is possible to show that establishing $\stackrel{ob}{\rightsquigarrow }$ requires a process to perform explicit synchronization operations. This is the subject of the next section.

Roughly speaking, an implementation $ℐ$ of an object is a protocol satisfying the object’s specification. It is said to be linearizable if in every execution of $ℐ$, operations appear to occur instantaneously in a way that is consistent with the original execution and that satisfy the sequential specification of the object. See [8] for a formal definition.

While we focus in this BA on registers, the full version [15] also covers snapshots, and extending the approach to the study of linearizable implementations of other shared objects appears promising. The register results of [6] exploit the fact that $\mathrm{𝖱𝖾𝖺𝖽}$ operations are one-sided non-commutative with respect to $\mathrm{𝖶𝗋𝗂𝗍𝖾}$ operations, yielding (roughly) that there exist runs where at least one of two adjacent write–read operations must contain a $𝙵$ or $\mathrm{𝚁𝙼𝚆}$. Our framework strengthens this: we prove that there exist runs where in fact $\mathrm{𝖶𝗋𝗂𝗍𝖾}$s must contain a $𝙵$ or $\mathrm{𝚁𝙼𝚆}$. In typical register implementations, $\mathrm{𝖶𝗋𝗂𝗍𝖾}$s complete with an acknowledgment independently of preceding $\mathrm{𝖶𝗋𝗂𝗍𝖾}$s, meaning they are not one-sided non-commutative. Nevertheless, our tools show that there are runs where $\mathrm{𝖶𝗋𝗂𝗍𝖾}$s must contain $𝙵$ or $\mathrm{𝚁𝙼𝚆}$. In addition, the DtF theorem and its uses, both in the TSO setting and in [14], raise the question of whether similar results hold in other memory models. Finally, we observe that although our $\stackrel{ob}{\rightsquigarrow }$ relation in TSO is analogous to happens-before in message passing, it differs in that $\stackrel{ob}{\rightsquigarrow }$ does not necessarily convey information, even under full information, whereas happens-before does. Nevertheless, like happens-before, the $\stackrel{ob}{\rightsquigarrow }$ relation remains a necessary condition for ordering in many cases. This fundamental difference is both interesting and worth deeper investigation.