What does running MP a billion times tell you?

Part 6 enumerated every execution of SB and MP on small models. Silicon cannot be enumerated: you run the test many times and count what you see. The rule for reading the counts is asymmetric. An outcome the architecture forbids, seen even once, is a bug. An outcome the architecture allows but never seen proves nothing: the implementation may simply be stronger than the model, or the harness may never have created the timing.

The four standard tests

X and Y are in different 64-byte lines, both 0 initially, plain aligned loads and stores. IRIW needs four agents: it extends the course model to C0..C3, and says so.

Models named in the table: TSO is x86-TSO as formalised by Owens, Sarkar and Sewell (University of Cambridge technical report UCAM-CL-TR-745). Armv8-A is the AArch64 memory model of the Arm Architecture Reference Manual for A-profile architecture (DDI 0487). RVWMO is the memory model of the RISC-V Unprivileged ISA specification.

The verdict depends on the named model, as in Weak Models: Arm and RISC-V. Run MP with plain accesses on an Armv8-A part and see (1,0): that is a legal result, not a bug. CoRR and the fenced variants are the tests whose forbidden outcomes indict the implementation on any architecture: the core's ordering logic or the coherence protocol. Triage decides which (see Ordering Bugs in Out-of-Order Cores).

How a silicon harness creates the rare timings

Litmus testing tools exist for exactly this. The herdtools7 suite by Jade Alglave and Luc Maranget includes diy7 (generates litmus tests from concise specifications), litmus7 (runs litmus tests written in assembly on the machine and reports which outcomes occurred) and herd7 (a simulator that computes the outcomes a memory model allows). The usual flow: generate the tests, compute the allowed set with the model simulator, run them on silicon, and flag any observed outcome outside the allowed set.

A buggy store buffer under stress

The model below is TSO, so MP's (1,0) is forbidden. The correct store buffer drains in FIFO order. The buggy one lets a younger store that hits in C0's cache (Y) drain past an older store that misses (X): a plausible optimisation gone wrong. The harness flushes X before each run, so its store misses with a random latency; without that preconditioning the same bug is invisible.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

import random

def mp_once(rng, fifo, stress):
    # C0: W(X)=1 then W(Y)=1 into its store buffer at t=0 and t=1.
    # stress=True: X was flushed before the iteration, so its store misses.
    lat_x = rng.randint(1, 20) if stress else 1
    lat_y = 1                       # Y stays hot in C0's cache: a hit
    t_x = 0 + lat_x                 # X becomes globally visible
    if fifo:
        t_y = max(t_x, 1) + lat_y   # Y may not drain past the older X
    else:
        t_y = 1 + lat_y             # bug: a hit drains past an older miss
    # C1: r1 = R(Y), then r2 = R(X), in order, after a random start delay.
    start = rng.randint(0, 25)
    gap = rng.randint(1, 3)
    r1 = 1 if start >= t_y else 0
    r2 = 1 if start + gap >= t_x else 0
    return (r1, r2)

def histogram(fifo, stress, runs=20000, seed=7):
    rng = random.Random(seed)
    counts = {}
    for _ in range(runs):
        outcome = mp_once(rng, fifo, stress)
        counts[outcome] = counts.get(outcome, 0) + 1
    return counts

FORBIDDEN = (1, 0)                  # MP under TSO, plain loads and stores
ALLOWED = {(0, 0), (0, 1), (1, 1)}

good = histogram(fifo=True, stress=True)
bad = histogram(fifo=False, stress=True)
bad_quiet = histogram(fifo=False, stress=False)

assert FORBIDDEN not in good                 # correct design: never seen
assert set(good) == ALLOWED                  # and stress reached every allowed outcome
assert bad.get(FORBIDDEN, 0) > 0             # buggy design: seen under stress
assert set(bad) <= ALLOWED | {FORBIDDEN}
assert FORBIDDEN not in bad_quiet            # same bug, no flush: never seen
for seed in range(1, 6):                     # not a lucky seed
    assert FORBIDDEN not in histogram(True, True, 5000, seed)
    assert histogram(False, True, 5000, seed).get(FORBIDDEN, 0) > 0
print("PASS: forbidden MP outcome appears only for the non-FIFO buffer, and only under stress")

Three results matter. The correct buffer never produces (1,0) under any seed. The buggy buffer does, but only when the harness flushes X; with warm caches its histogram looks identical to a correct part's. And the correct run shows all three allowed outcomes, which tells you the stress is reaching the corners. Real rates are far lower than this toy's, which is why iteration counts run into billions.

Related topics

• Shared course model

• Enumerated SC and TSO outcome sets

• Arm and RISC-V verdicts

• Post-silicon validation (Verification course)