A.3.5-8 PPO Rules 1–8: Overlaps, Fences & Synchronization, Explained

Each PPO rule exists to permit one microarchitecture and forbid another. This page walks rules 1–8 with the spec’s own examples.

Rules 1–3: overlapping addresses

Rule 1 (…before a later overlapping store) is the easy direction: a speculatively visible store can’t be undone, so the model simply bans store reordering past anything overlapping. The missing converse — store before later same-address load — is deliberate: that’s forwarding, legalized by the Load Value Axiom instead.

Rule 2 is CoRR with two famous carve-outs, the fri-rfi and RSW patterns :

MP+fence.w.w+fre-rfi-addr (Table 80)Initially: x = 0, y = 0

Hart 0

li t1, 1
(a) sw t1,0(s0)
(b) fence w,w
(c) sw t1,0(s1)

Hart 1

li t2, 2
(d) lw a0,0(s1)
(e) sw t2,0(s1)
(f) lw a1,0(s1)
xor t3,a1,a1
add s0,s0,t3
(i) lw a2,0(s0)

a0=1, a1=2, a2=0 — ALLOWEDLegal: (f) performed before (d), but returned a NEWER value (own forwarded store). Rule 2 fires only when two loads return values from different stores with no intervening same-address store — value-staleness, not performing order, is what CoRR protects.

RSW: two same-address loads that return values from the same store may also reorder (a snoop-verified speculation real cores do). If they return different stores’ values, rule 2 bites. Rule 3: nothing may consume an AMO/SC’s value until it performs globally — even AMOSWAP’s semantically independent store value. No forwarding out of atomics, uniformly. All three rules apply to partial overlaps, and per-component for misaligned accesses.

Rule 4: fences

PR/PW/SR/SW subset the predecessor/successor sets. Ten non-trivial combinations exist; six do all the real work: RW,RW, FENCE.TSO, RW,W, R,RW, R,R, W,W. And because RISC-V is multi-copy atomic, fences are thread-local — no cumulativity reasoning (unlike POWER).

Rules 5–8: acquire, release, RCsc, pairing

The spinlock, annotated two ways (Listings 11/12):

aq/rl annotations vs fences: same lock, different collateral ordering
	amoswap.w.aq / .rl (Listing 11)	plain amoswap + fences (Listing 12)
Acquire ordering	Critical section after the lock AMO — and only that	fence r,rw after the AMO
Release ordering	Critical section before the unlock AMO — and only that	fence rw,w before the AMO — also orders the section before arbitrary later stores
Cost model	Ordering scoped to the sync variable: max reordering freedom elsewhere	Correct but coarser; the fence version is also what aq/rl-less cores emulate

Dotted-underlined cells have explanations — click one.

RCpc vs RCsc (rule 7): with RCpc annotations alone, store-release → load-acquire is not ordered — a deliberate gift to TSO/RCpc code porting. RCsc annotations (what aq/rl on atomics produce) order all sync operations among themselves. Rule 8 puts an SC after its paired LR even when the stored value has no syntactic dependency on the LR’s result. Annotations, like fences, are not cumulative.

Hardware Designer Notes

If your LSU keeps loads in order per address and drains stores in order, rules 1–3 hold by construction and rule 2’s subtleties never arise — the carve-outs only matter once you let same-address loads issue out of order with snoop-based repair. Choose that complexity knowingly; the appendix literally marks rule 2 “worth double checking carefully.”

Minimal Linux-boot hart MUST

Never reorder a store past an overlapping earlier access (rule 1) — no store-undo exists
Enforce rule 3 literally: no early forwarding out of AMOs/SCs, AMOSWAP included
Double-check rule 2 corners (the spec itself flags it as the subtle one): fri-rfi and RSW legal, stale-value CoRR violations not

MAY simplify / trap-and-emulate

Implement aq/rl as fences (r,rw / rw,w equivalents) on a simple core — coarser, correct
Enforce full same-address load-load ordering and skip the fri-rfi/RSW subtleties entirely
Treat every FENCE as RW,RW

Check yourself — PPO rules 1-8 rationale

1.Why does PPO order every access before a later overlapping STORE (rule 1), but not a store before a later overlapping load?

2.In the fri-rfi pattern, a younger same-address load performs BEFORE an older one yet the outcome is legal. What saves it from being a CoRR violation?

3.Rule 3 forbids forwarding an AMOSWAP's store value to a later load — even though that value doesn't depend on memory. Why so strict?

4.aq on an AMOSWAP vs FENCE R,RW after a plain AMOSWAP — what's the observable difference (spinlock acquire)?

5.Why isn't a store-release followed by a load-acquire (RCpc) ordered, and what restores the ordering?

5 questions