Computer Architecture · Memory Consistency

Propagation, Cumulativity, and Why Weak Models Need Transitive Visibility

Messages that preserve ordering are not enough: a store already observed by one thread must be observed by every thread it reaches, and multi-copy atomicity is the property that says so.

A relay of threads is a common way to break a weak memory model, and it fails in a way that ordering alone does not explain. Thread 1 writes a value and a flag. Thread 2 reads the flag, then writes a second flag. Thread 3 reads the second flag, then reads the value. The intent is a chain: if thread 3 sees flag two, then thread 2 saw flag one, and therefore the value was already there. On models without cumulativity this chain does not hold, and the reason is not that any individual ordering was relaxed. It is that the write observed by thread 2 was not automatically made visible by thread 2’s own write.

The property that would guarantee the chain is transitive visibility of writes, and it is worth separating from the ordering properties that get more attention.

The relay pattern and what it exposes

Written out, the relay is three threads on three locations:

/* x = 0, y = 0, z = 0; barriers elided to keep the pattern visible */
void t1(void) { x = 1; /* write barrier */ y = 1; }    // data, then flag
void t2(void) { int r = y; if (r) z = 1; }             // read flag, set relay
void t3(void) { int s = z; int v = x; /* ... */ }      // read relay, then data

The question is whether thread 3 can observe s == 1 and v == 0. Thread 2 saw y == 1, which means thread 1’s store to y had reached thread 2. Since thread 1 ordered its store to x before its store to y with the write barrier, thread 2’s observation of y should imply x was already visible somewhere. Thread 2 then writes z, and thread 3 observes z. For thread 3 to miss x, the store to x must not have propagated to the component that serves thread 3’s load, even though it had propagated to the component that served thread 2’s load.

On PowerPC, this outcome was permitted. The model there gave write-read ordering only locally, and propagation was not transitive: a write that had reached one observer was not automatically visible to others through that observer. The mechanism is a store queue and a write-back cache hierarchy in which stores become visible at different levels of the tree at different times, and a write that has been seen by one core’s cache is not thereby flushed to the shared level.

This is the failure mode that cumulativity rules exist to forbid, and it is why the property is sometimes called cumulative memory order.

Multi-copy atomicity, stated precisely

The cleanest way to state the property is to name the atomicity of stores rather than the transitivity of their propagation. A system is multi-copy atomic if a store is made visible to all observers at the same instant, at the point at which it becomes visible to any observer other than the issuing processor. Before that instant, no other processor can see it. After it, all can.

The consequences are worth spelling out, because they are what a programmer relies on without noticing.

Once a store is observed by any thread, it is observed by every thread that executes a later synchronisation that orders it after that observation. The relay breaks because thread 2’s observation of y did not imply global visibility of x; under multi-copy atomicity it does.

Propagation has a single point of serialisation per store, which means the order in which stores become visible is a total order as far as observers are concerned. That is why multi-copy atomic systems give a single order over all stores even when loads and stores are otherwise relaxed, and why the IRIW test (independent reads of independent writes) is forbidden on them: two readers cannot disagree about the order of two stores, because there is one propagation order and both readers see it.

Store buffers are compatible with multi-copy atomicity. A store sitting in the issuing core’s buffer is not yet visible to anyone, including other cores. When it leaves the buffer and enters the coherence fabric, it becomes visible at one point. The buffer delays the visibility instant but does not make it gradual. This is why x86’s TSO, despite allowing loads to bypass stores, is multi-copy atomic.

Cumulativity in the axiomatic formulation

In the axiomatic style, the property is expressed as a rule about how ordering relations compose with visibility. The relations are usually named:

  • po — program order within a thread.
  • rf — the reads-from relation, mapping each load to the store whose value it returned.
  • co — the coherence order, a total order per location over writes to that location.
  • fr — from-read, the order from a load to writes that follow the one it read from in co.
  • ob — the ordering established by barriers and by acquires and releases.

A candidate execution is allowed if certain derived relations are acyclic. Multi-copy atomicity appears as the requirement that a write observed by a load is ordered before any write that the observer emits later, as seen by third parties. Formally, the store that a load read from must be ordered before any store that the loading thread subsequently emits, in the external view. Without this rule, a write can be visible to one observer and not to another, and the relay is permitted.

The practical formulation, and the way it appears in architecture manuals, is a constraint on the ordering primitives themselves. A barrier that is cumulative orders not only the operations of the thread executing it, but also the operations those operations depend on. A non-cumulative barrier orders only the thread’s own accesses. The distinction between a barrier that orders writes against writes and a barrier that additionally ensures prior propagation is complete is exactly the cumulativity distinction.

This is why the barrier vocabulary in weak-model architectures is larger than a single full fence. On PowerPC the sync and lwsync instructions differed in cumulativity, and on Arm the DMB family carries domain and direction qualifiers that determine which operations, and which prior observations, are ordered by it.

What a cumulative barrier costs

If cumulativity requires that prior stores have propagated to a point all observers will see, then the barrier must wait for acknowledgements from that point rather than from the local cache. The cost is the round trip to the shared level of the hierarchy, plus the invalidations of any sharers of the affected lines.

The wait is why cumulativity is optional in the instruction set rather than universal. A thread that is the only one that will ever read its data does not need the transitive guarantee, and a barrier that waits for global propagation is wasted latency. The instruction set exposes both, and the programmer chooses. A DMB ISH on Arm orders within the inner shareable domain, which is the coherence domain that ordinary threads share; a stronger domain orders further out.

The design constraint that forced this layering is scale. In a large system, “propagated everywhere” can mean propagated to sockets connected by a link with a round trip in the hundreds of nanoseconds. Making every barrier wait for that is untenable for code whose sharing is confined to one socket. The architecture therefore offers the guarantee at multiple scopes, and the model is parameterised by the scope at which each operation acts.

The scopes are not a performance hint. A barriered store that is only guaranteed within a domain is correct only for readers in that domain, and code that assumes otherwise fails when the readers are elsewhere. The general pattern is covered in Ordering Across the Device Boundary: DMA, MMIO, and Posted Writes, where scope matters for a different reason.

Why sequential consistency hides the problem

Sequential consistency implies multi-copy atomicity for free, because the single total order over all operations means a store occupies one position and all observers see it at that position. A program developed and tested under sequential consistency, or under a model close to it, never encounters the relay failure because the failure requires the relaxation. Moving such a program to a machine without multi-copy atomicity exposes an assumption the programmer did not know they were making.

This is the reason the property is discussed separately from the ordering table. A model defined only by which reorderings it permits can be stronger than the hardware it describes in one respect and weaker in another, and multi-copy atomicity is the respect where the historically weak models were weakest. The difference between x86-TSO and PowerPC is not mainly in the reorderings allowed for a single thread; it is in whether a store’s visibility is a single event or a gradual process.

The mechanism that produced gradual visibility on those machines was the combination of a store queue that forwards to the local cache immediately and a cache hierarchy in which data written to one level reaches the shared level later. A second core attached to the same level sees the store before a core attached to the shared level does. Nothing in the ordering of the issuing core’s operations was relaxed; the visibility itself was staged.

Designing for a model without it

The practical rules for code that must run on a model without multi-copy atomicity are a small set, and they are all about not relying on relays.

A chain of threads is safe only if each step uses a release-acquire pair with cumulative semantics, so that the observation at each step carries the earlier store forward. A non-cumulative barrier at an intermediate step does not, because it orders the intermediate thread’s own operations without guaranteeing that what it observed has spread.

The strongest available ordering at the relay point is the safe choice when the model is uncertain. A full sequentially consistent atomic operation at the relay carries everything an ordered fence carries and is specified in the language model in terms the compiler must honour. The narrower primitives are worth using only where the algorithm’s reasoning is explicit about which observations need to be carried forward.

Reading and writing the same flag is not a substitute for a relay. A second flag written by an intermediary thread is an ordinary store, and its visibility is subject to the same rules as the data it is meant to signal. The technique of having the intermediary write back what it read, so that the chain is a series of dependent accesses, is one that works on models with address-dependency ordering, which is the residual ordering property that survives even when cumulativity does not. The read-modify-write case is where this dependency is often exploited deliberately, as described in Read-Modify-Write Atomicity and the Ordering It Carries.

Where the property sits in a model

A complete model needs three separate statements: which orderings between a thread’s own operations are preserved, which ordering edges synchronisation establishes, and whether observed writes propagate transitively. The first two are what the ordering tables in architecture manuals state. The third is what separates models that look similar in a reordering table and behave very differently in a relay.

When comparing two machines, the reordering table is necessary and not sufficient. Two models that permit the same set of per-thread reorderings can differ in whether the relay is legal, and a program validated on one can fail on the other. The difference is not academic: it is the reason the ARM and PowerPC models needed a formal treatment separate from the earlier SC-based formulations, and the reason litmus suites include relay tests alongside the store-buffering and message-passing tests covered in Litmus Tests and How Allowed Outcomes Are Decided.

References

  1. Understanding POWER Multiprocessors — Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams, ACM PLDI 2011
  2. A Tutorial Introduction to the ARM and POWER Relaxed Memory Models — Jade Alglave, Luc Maranget, and Susmit Sarkar, technical report, 2010
  3. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory — Jade Alglave, Luc Maranget, and Michael Tautschnig, ACM TOPLAS 2014
  4. Arm Architecture Reference Manual for A-profile architecture — Arm Limited