A litmus test is a short program plus the outcome in question. Allowed means some legal execution produces it; forbidden means none does.
Pattern | Program | Weak outcome | Fix on ARMv8 / RVWMO |
|---|---|---|---|
SB | A: St x, Ld y; B: St y, Ld x | r1 = 0, r2 = 0 | Full fence between each store and load. |
MP | A: St x, St y; B: Ld y, Ld x | r1 = 1, r2 = 0 | Release store with acquire load, or fences. |
LB | A: Ld x, St y; B: Ld y, St x | r1 = 1, r2 = 1 | Full fence between each load and store. |
WRC | A: St x; B: Ld x, St y; C: Ld y, Ld x | chain sees y = 1 yet x = 0 | Cumulative fence; forbidden on MCA models. |
IRIW | A: St x; C: St y; readers split | readers disagree on store order | Full cumulative fences; forbidden on MCA models. |
The harness below enumerates every execution of SB and MP under four machines. SC contributes 4-operation interleavings (6 orders each); the SB drain machine adds issue and drain events (80 orders satisfying issue-before-use), and the MP machines reuse that event set with ordered or relaxed load and drain rules.
module tb_litmus_enum;
int p0, p1, p2, p3, p4, p5;
int sc_sb_cnt, sc_sb_mask, sc_mp_cnt, sc_mp_mask;
int tso_cnt, tso_mask, ord_cnt, ord_mask, weak_mask;
int errors, r1, r2;
function automatic bit dup4(input int v0, input int v1, input int v2, input int v3);
if (v0 == v1 || v0 == v2 || v0 == v3 || v1 == v2 || v1 == v3 || v2 == v3) return 1;
return 0;
endfunction
function automatic bit dup6(input int v0, input int v1, input int v2, input int v3, input int v4, input int v5);
if (v0 == v1 || v0 == v2 || v0 == v3 || v0 == v4 || v0 == v5) return 1;
if (v1 == v2 || v1 == v3 || v1 == v4 || v1 == v5) return 1;
if (v2 == v3 || v2 == v4 || v2 == v5) return 1;
if (v3 == v4 || v3 == v5) return 1;
if (v4 == v5) return 1;
return 0;
endfunction
initial begin
errors = 0;
sc_sb_cnt = 0; sc_sb_mask = 0;
for (p0 = 0; p0 < 4; p0 = p0 + 1)
for (p1 = 0; p1 < 4; p1 = p1 + 1)
for (p2 = 0; p2 < 4; p2 = p2 + 1)
for (p3 = 0; p3 < 4; p3 = p3 + 1) begin
if (dup4(p0, p1, p2, p3) == 0 && p0 < p1 && p2 < p3) begin
sc_sb_cnt = sc_sb_cnt + 1;
r1 = (p2 < p1) ? 1 : 0;
r2 = (p0 < p3) ? 1 : 0;
sc_sb_mask = sc_sb_mask | (1 << (r1 * 2 + r2));
end
end
if (sc_sb_cnt != 6) errors = errors + 1;
if (sc_sb_mask != 14) errors = errors + 1;
sc_mp_cnt = 0; sc_mp_mask = 0;
for (p0 = 0; p0 < 4; p0 = p0 + 1)
for (p1 = 0; p1 < 4; p1 = p1 + 1)
for (p2 = 0; p2 < 4; p2 = p2 + 1)
for (p3 = 0; p3 < 4; p3 = p3 + 1) begin
if (dup4(p0, p1, p2, p3) == 0 && p0 < p1 && p2 < p3) begin
sc_mp_cnt = sc_mp_cnt + 1;
r1 = (p1 < p2) ? 1 : 0;
r2 = (p0 < p3) ? 1 : 0;
sc_mp_mask = sc_mp_mask | (1 << (r1 * 2 + r2));
end
end
if (sc_mp_cnt != 6) errors = errors + 1;
if (sc_mp_mask != 11) errors = errors + 1;
tso_cnt = 0; tso_mask = 0;
for (p0 = 0; p0 < 6; p0 = p0 + 1)
for (p1 = 0; p1 < 6; p1 = p1 + 1)
for (p2 = 0; p2 < 6; p2 = p2 + 1)
for (p3 = 0; p3 < 6; p3 = p3 + 1)
for (p4 = 0; p4 < 6; p4 = p4 + 1)
for (p5 = 0; p5 < 6; p5 = p5 + 1) begin
if (dup6(p0, p1, p2, p3, p4, p5) == 0 && p0 < p1 && p0 < p4 && p2 < p3 && p2 < p5) begin
tso_cnt = tso_cnt + 1;
r1 = (p5 < p1) ? 1 : 0;
r2 = (p4 < p3) ? 1 : 0;
tso_mask = tso_mask | (1 << (r1 * 2 + r2));
end
end
if (tso_cnt != 80) errors = errors + 1;
if (tso_mask != 15) errors = errors + 1;
ord_cnt = 0; ord_mask = 0;
for (p0 = 0; p0 < 6; p0 = p0 + 1)
for (p1 = 0; p1 < 6; p1 = p1 + 1)
for (p2 = 0; p2 < 6; p2 = p2 + 1)
for (p3 = 0; p3 < 6; p3 = p3 + 1)
for (p4 = 0; p4 < 6; p4 = p4 + 1)
for (p5 = 0; p5 < 6; p5 = p5 + 1) begin
if (dup6(p0, p1, p2, p3, p4, p5) == 0 && p0 < p1 && p0 < p4 && p1 < p5 && p2 < p3 && p4 < p5) begin
ord_cnt = ord_cnt + 1;
r1 = (p5 < p2) ? 1 : 0;
r2 = (p4 < p3) ? 1 : 0;
ord_mask = ord_mask | (1 << (r1 * 2 + r2));
end
end
if (ord_cnt == 0) errors = errors + 1;
if (ord_mask != 11) errors = errors + 1;
weak_mask = 0;
for (p0 = 0; p0 < 6; p0 = p0 + 1)
for (p1 = 0; p1 < 6; p1 = p1 + 1)
for (p2 = 0; p2 < 6; p2 = p2 + 1)
for (p3 = 0; p3 < 6; p3 = p3 + 1)
for (p4 = 0; p4 < 6; p4 = p4 + 1)
for (p5 = 0; p5 < 6; p5 = p5 + 1) begin
if (dup6(p0, p1, p2, p3, p4, p5) == 0 && p0 < p1 && p0 < p4 && p1 < p5 && p2 < p3) begin
r1 = (p5 < p2) ? 1 : 0;
r2 = (p4 < p3) ? 1 : 0;
weak_mask = weak_mask | (1 << (r1 * 2 + r2));
end
end
if ((weak_mask & 4) == 0) errors = errors + 1;
if (errors == 0) $display("PASS: SC holds 3 of 4 SB and MP outcomes, buffering adds SB 0,0, weak MP adds 1,0, ordered MP keeps 3, counts 6 and 80 check");
else $display("FAIL: %0d checks wrong", errors);
$finish;
end
endmoduleA lock needs acquire semantics and an unlock needs release semantics. Dekker-style mutual exclusion needs full fences on weak models instead.
ISA | Lock | Unlock |
|---|---|---|
x86-TSO | XCHG or LOCK-prefixed op (full barrier) | Plain store (StSt order holds). |
ARMv8 | LDAXR and STLXR loop (acquire) | STLR (release). |
RISC-V | AMOSWAP with AQ set | AMOSWAP with RL set. |
The listing below is not run. It is a fence-placement sketch with ISA annotations, not executable code.
// not-run: fence-placement sketch with ISA annotations, not executable SystemVerilog
// MP publication: writer stores data, then flag; reader polls flag, then reads data.
// x86-TSO : St data; St flag || Ld flag; Ld data (no fence needed)
// ARMv8 : St data; STLR flag || LDAR flag; Ld data (release plus acquire)
// RVWMO : St data; FENCE; St flag || Ld flag; FENCE; Ld data
// Spinlock: x86 XCHG locks (full barrier), plain store unlocks;
// ARMv8 LDAXR and STLXR loop locks (acquire), STLR unlocks (release);
// RISC-V AMOSWAP.AQ locks, AMOSWAP.RL unlocks.Map every ISA ordering claim to its microarchitectural mechanism first. Then validate fences under speculation and buffer pressure, not in idle traffic.
Reproduce the failing pattern with a deterministic seed.
Log pipeline reorder points and retirement order near the failure.
Confirm fence decode and retire semantics for the exact sequence.
Rerun with stricter fences to bound the culprit, then keep the minimal fence the model requires.
Pass both short litmus and long system synchronization stress before sign-off.
Compiler transformations reorder accesses too, so treat them as part of ordering validation. Use barrier intrinsics at synchronization points and review codegen assumptions with runtime teams.
An ordering miss passes most workloads yet corrupts lock-free paths in the field. That asymmetry is why the triage above starts from the litmus shape, not from performance knobs.
Tie the failure to a litmus shape, usually MP-style publication, and check the fence at that point before touching the hardware.
It bounds the culprit to ordering rather than values. The next step is the minimal fence the model requires.