Release-Acquire Memory Model

computer-architecture memory-models

Definition

Release-Acquire Memory Model

In the release-acquire memory model, an atomic release operation prevents earlier loads and stores in the same thread from moving after it, and an atomic acquire operation prevents later loads and stores from moving before it.

Formally:

• if $a$ is a release, then every operation $x$ with $x{<}_{p}a$ remains before $a$ in the visible order;
• if $b$ is an acquire, then every operation $y$ with $b{<}_{p}y$ remains after $b$ in the visible order.

Relaxed operations impose no such ordering.

Local Ordering Only

Release-acquire constrains reordering within a thread around the synchronising atomic operations. It does not make the whole program sequentially consistent.

The model is strong enough to communicate between threads through shared memory when one thread publishes data with release and another observes the publication with acquire.

Producer-consumer

Flag publication

Let $D$ be non-atomic data and $F$ be an atomic flag.

Producer:

$$\begin{array}{r}D:=42;F:=1\text{(release)}\end{array}$$

Consumer:

$$\text{while }F=0\text{ do skip};X:=D\text{(acquire)}$$

The release prevents $D:=42$ from moving after the flag store. The acquire prevents $X:=D$ from moving before the flag load. Hence the consumer reads the published data.

Limitation

Not sequential consistency

Release-acquire does not globally order all operations. Unrelated loads and stores may still be reordered, so correctness arguments must use the synchronisation relation explicitly.