Find the Races

Part 14 · Capstone · All levels

On this page

Which check finds which bug, and on which seeds?

Each defect is one changed condition in the model of the previous lesson. Switched on, it must be found by the intended check: (a) and (b) by the value checker, (c) by the progress check. A random seed finds it; a directed script then reproduces the reduced trace shown here. All three traces use MESI, the three-core model, and acks collected at H.

Your task	Detail
Build	The three defect switches, each one changed condition; a directed script for each trace below
Interface	run(seed, defects=("lost-inv",)) and the same for "late-put" and "shared-queue"; script=[...] to replay a trace; log=[] to record a failing seed as a script
Done when	Each defect fails seeds 0 to 19 with its intended check while the correct model passes them, and each script fails with its own defect only

Plant and hunt the defects yourself before reading the traces: the tables below are the answers.

Defect	The changed condition	Bug class	Found by
a. lost-inv	When a GetM enters H's buffer, H clears the requester's sharer bit ('it is becoming the writer')	Safety: a reader survives a write	Value checker (SWMR fails at the same event)
b. late-put	H's Put handler checks only that X is exclusive, not that the sender is the recorded holder	Safety: memory overwritten with stale data	Value checker, authority half (H records U while C1 is in M)
c. shared-queue	Requests and responses share H's two input slots	Progress: resource cycle	Progress check

a. Upgrade race that loses an invalidation

Warm-up (from the script): C0 reads X and gets E, C1 reads X, H forwards to C0 and both end in S / 0, H S{C0,C1}, memory = 0. Then both cores store. C1's GetM B reaches H's buffer first; C0's GetM A is handled first. C2 stays I / - and is left out.

C1's GetM enters H's buffer and the defect clears C1's sharer bit; C0's GetM is handled with no sharer to invalidate, C0 gets M and writes 1 while C1 still holds a readable 0.

Defect a: H drops a queued upgrader from the sharer set, so the upgrade served first invalidates nobody.

Step	C0 state / value	C1 state / value	H directory	Newest data
Start	S / 0	S / 0	S{C0,C1}	C0, C1 and memory: 0
L. C1 store	S / 0	SM^D / 0	S{C0,C1}	C0, C1 and memory: 0
L. C0 store	SM^D / 0	SM^D / 0	S{C0,C1}	C0, C1 and memory: 0
1. GetM B in H's buffer	SM^D / 0	SM^D / 0	S{C0}, queued GetM C1 (defect)	C0, C1 and memory: 0
2. GetM A at H	SM^D / 0	SM^D / 0	S{C0}, pend GetM C0, acks 0/0, queued GetM C1	C0, C1 and memory: 0, Data (permission only) in flight to C0
3. Data at C0, store	M / 1	SM^D / 0	S{C0}, pend GetM C0, acks 0/0, queued GetM C1	C0: 1

At step 3 the checker reports 'value: C1 holds 0, golden 1; SWMR: writers [0], readers [1]': C1's SM^D copy is still readable and stale, and C0 in M beside a reader breaks SWMR at the same event. The correct H keeps C1 in S{C0,C1} at step 1, sends Inv to C1 at step 2 and waits for its Inv-Ack, exactly as Simultaneous Upgrades shows. Script A2 replays the other arrival order, C0's GetM entering first and C1's handled first: the defect then drops C0's bit, and the checker reports C0 holding a stale 0 beside C1 in M. Why it matters: the upgrade path is permission-only, so nothing else (no data transfer, no Fwd) would ever touch the stale copy; a missing Inv is silent until a load reads the stale value.

b. Eviction versus forward that returns stale data

Warm-up: C0 stores X = 1 (GetM from I, M / 1), H exclusive(C0), memory = 0. C0 then evicts while C1 wants to write. C2 stays I / - and is left out. Compare order B of Eviction Versus Intervention, which is the same race with a Fwd-GetS; here the forward is a Fwd-GetM. Unlike the design in An Illustrative Escape, this H does not use the 'from the WB entry' mark on a Fwd-GetM answer to flag the coming PutM, so the four-hop route does not hide the defect.

C0's PutM is overtaken by C1's GetM; C0 answers the forward from its writeback entry, C1 writes 2, then the late PutM makes the defective H write 1 to memory and record U, so C0's next read gets E with the stale 1.

Defect b: a late PutM from a cache that is no longer the holder overwrites memory and erases the real holder from the directory.

Step	C0 state / value	C1 state / value	H directory	Memory	Newest data
Start	M / 1	I / -	exclusive(C0)	0	C0: 1
L. C0 evicts	MI^A / 1 (in WB)	I / -	exclusive(C0)	0	C0 WB: 1, PutM(1) in flight to H
L. C1 store	MI^A / 1 (in WB)	IM^D / -	exclusive(C0)	0	C0 WB: 1, PutM(1) in flight to H
1. GetM at H	MI^A / 1 (in WB)	IM^D / -	exclusive(C0), pend GetM C1	0	C0 WB: 1, PutM(1) in flight to H
2. Fwd-GetM at C0	II^A / -	IM^D / -	exclusive(C0), pend GetM C1	0	Data(1) in flight to H, PutM(1) in flight to H
3. Data at H	II^A / -	IM^D / -	exclusive(C0), pend GetM C1	0	H buffer: 1, Data(1) in flight to C1, PutM(1) in flight to H
4. Data at C1, store	II^A / -	M / 2	exclusive(C0), pend GetM C1	0	C1: 2
(assumed) grant delivered	II^A / -	M / 2	exclusive(C1)	0	C1: 2
5. late PutM at H	II^A / -	M / 2	U (defect)	1	C1: 2
6. Put-Ack at C0	I / -	M / 2	U	1	C1: 2
L. C0 load	IS^D / -	M / 2	U	1	C1: 2
7. GetS at H	IS^D / -	M / 2	U, pend GetS C0	1	C1: 2
8. Data at C0	E / 1	M / 2	U, pend GetS C0	1	C1: 2

The bad step is 5: C0 is not the recorded holder, so its PutM is late and its data stale, but the defective H writes it to memory and forgets C1. The authority half of the data-value invariant fires there, before any load: 'value: dir U with C1 in M; value: dir U, memory 1, golden 2'. A checker with only the copy half sees nothing at step 5, because every cache copy is still correct; it fires only at step 8, when C0's load returns 1 against golden 2, and SWMR is also broken there (E beside M). The block below asserts both. Script B2 replays Part 4's order A, the PutM reaching H before the GetM: then C0 is still the holder, its PutM is a normal writeback, and even the defective model passes, so the bug needs the GetM to win. The correct rule, used throughout the course, is that a Put from a cache H no longer records as a holder gets Put-Ack with no directory or memory change. The cache-side twin of this bug, freeing the WB entry when PutM is sent instead of at Put-Ack, would fail at step 2 instead: the Fwd-GetM would find nothing to answer from. Why it matters: both writes and evictions are common, so this window opens in ordinary traffic, and without the authority check the symptom (old data from memory) appears long after the cause.

c. A resource cycle under finite buffers

Warm-up as in (a): C0 S / 0, C1 S / 0, C2 I / -, H S{C0,C1}, memory = 0. This trace needs the third core.

C0's GetM makes H busy and sends Inv to C1; C1's GetM and C2's GetS fill both shared buffer slots; C1's Inv-Ack has nowhere to go, and nothing can move.

Defect c: the Inv-Ack that A waits for cannot enter H's buffer, which is full of requests that wait for A.

Step	C0 state / value	C1 state / value	C2 state / value	H directory	Newest data
Start	S / 0	S / 0	I / -	S{C0,C1}	C0, C1 and memory: 0
L. C0 store	SM^D / 0	S / 0	I / -	S{C0,C1}	C0, C1 and memory: 0
1. GetM A at H	SM^D / 0	S / 0	I / -	S{C0,C1}, pend GetM C0, acks 0/1	C0, C1 and memory: 0
L. C1 store	SM^D / 0	SM^D / 0	I / -	S{C0,C1}, pend GetM C0, acks 0/1	C0, C1 and memory: 0
L. C2 load	SM^D / 0	SM^D / 0	IS^D / -	S{C0,C1}, pend GetM C0, acks 0/1	C0, C1 and memory: 0
2. GetM B in H's buffer	SM^D / 0	SM^D / 0	IS^D / -	S{C0,C1}, pend GetM C0, acks 0/1, queued GetM C1	C0, C1 and memory: 0
3. GetS R in H's buffer	SM^D / 0	SM^D / 0	IS^D / -	S{C0,C1}, pend GetM C0, acks 0/1, queued GetM C1, GetS C2	C0, C1 and memory: 0
4. Inv at C1	SM^D / 0	IM^D / -	IS^D / -	S{C0,C1}, pend GetM C0, acks 0/1, queued GetM C1, GetS C2	C0 and memory: 0

Dependency graph with three nodes: H's pending entry waits for C1's Inv-Ack, which waits for a slot in the shared buffer, whose slots are held by requests waiting for the pending entry.

The cycle: A's pending entry waits for the Inv-Ack, the Inv-Ack waits for a buffer slot, the slots wait for A to finish.

After step 4 nothing can move: no message is addressed to a cache, the Inv-Ack has no slot, and both buffered requests wait for A. The progress check reports 'deadlock: no enabled move, H busy True, buffer [GetM, GetS], waiting [Inv-Ack]'. Every value is still correct, so the value checker never fires. This is the cycle of A Protocol Deadlock appearing on one line with three cores instead of two lines. With two cores and the same two shared slots the cycle cannot close (the one other cache can queue one request and still leave a slot for its Inv-Ack); with one shared slot it closes with two cores too. Why it matters: it needs only ordinary contention (two caches asking while a third owes an ack), it is permanent, and it can stay hidden in tests whose buffers are large or whose traffic is light.

Finding them by seed, and proving the traces

The block runs the three defects on seeds 0 to 19, records the event of each first failure, checks short runs, replays the scripts, and turns one failing random seed into a script through its log.

example.py

import random
from collections import Counter
REQ = ("GetS", "GetM", "PutS", "PutE", "PutM")    # request class, everything else sent to H is a response
STABLE = ("I", "S", "E", "M")
def run(seed, defects=(), steps=4000, n=3, hq_size=2, resp_size=None, script=None, drain=False,
        seen=None, log=None, authority=True):
    """Three-core MESI directory model of one line X. Returns (first failure or None, traffic counts)."""
    rng, seen = random.Random(seed), Counter() if seen is None else seen
    resp_size, log = n - 1 if resp_size is None else resp_size, [] if log is None else log
    c = [{"st": "I", "v": None} for _ in range(n)]  # I S E M, IS IM SM (the ^D states), SI EI MI II (^A)
    H = {"dir": "U", "sh": set(), "own": None, "mem": 0, "busy": None, "tid": 0}   # dir U, S or X(own)
    to_c, link, hq = [], [], []    # to caches (always sink), waiting to enter H, H's input buffer
    gold, nxt, cnt, bad = [0], [0], Counter(), []
    def send(kind, src, dst, **kw):
        cnt["msgs"] += 1
        (link if dst == "H" else to_c).append(dict(kind=kind, src=src, dst=dst, **kw))
    def room(m):                                   # may m enter H's input buffer now?
        if "shared-queue" in defects: return len(hq) < hq_size          # defect c: one shared buffer
        if m["kind"] in REQ: return sum(x["kind"] in REQ for x in hq) < hq_size
        return sum(x["kind"] not in REQ for x in hq) < resp_size        # reserved response slots
    def enter(m):
        link.remove(m); hq.append(m)
        if m["kind"] == "GetM" and H["busy"]: seen["GetM queued behind busy"] += 1
        if "lost-inv" in defects and m["kind"] == "GetM": H["sh"].discard(m["src"])  # defect a
    def store(i): nxt[0] += 1; c[i]["v"] = gold[0] = nxt[0]   # unique values: a stale read is visible
    def load(i):
        if c[i]["v"] != gold[0]: bad.append(f"value: load at C{i} got {c[i]['v']}, golden {gold[0]}")
    def check():                                   # the golden checker, after EVERY event
        w = [i for i in range(n) if c[i]["st"] in ("E", "M")]
        r = [i for i in range(n) if c[i]["st"] in ("S", "SM")]
        err = bad + [f"value: C{i} holds {c[i]['v']}, golden {gold[0]}" for i in w + r if c[i]["v"] != gold[0]]
        if authority:                              # the authority half: H's record and memory
            rec = f"exclusive(C{H['own']})" if H["dir"] == "X" else H["dir"]
            err += [f"value: dir {rec} with C{i} in {c[i]['st']}" for i in w if rec != f"exclusive(C{i})"]
            if H["dir"] in ("U", "S") and H["mem"] != gold[0]:
                err.append(f"value: dir {rec}, memory {H['mem']}, golden {gold[0]}")
        if len(w) > 1 or (w and r): err.append(f"SWMR: writers {w}, readers {r}")
        if sum(x["kind"] not in REQ for x in hq) > resp_size: err.append("response slots exceeded")
        assert not err, "; ".join(err)
    def grant(dst, perm, v): send("Data", "H", dst, v=v, perm=perm)   # recorded when delivered
    def done(t):
        if not t.get("sent") and t["acks"] == 0: t["sent"] = True; grant(t["req"], "M", H["mem"])
    def home(m):                                   # H handles one message from its input buffer
        hq.remove(m); k, s, b = m["kind"], m["src"], H["busy"]
        if k == "GetS":
            H["busy"] = {"req": s, "op": k}
            if H["dir"] == "X": send("Fwd-GetS", "H", H["own"])
            else: grant(s, "E" if H["dir"] == "U" else "S", H["mem"])
        elif k == "GetM":
            assert not (H["dir"] == "X" and H["own"] == s), f"protocol: GetM from holder C{s}"
            H["tid"] += 1; t = H["busy"] = {"req": s, "op": k, "id": H["tid"], "acks": 0}
            if H["dir"] == "X": send("Fwd-GetM", "H", H["own"])
            else:
                for o in sorted(H["sh"] - {s}): t["acks"] += 1; send("Inv", "H", o, id=t["id"])
                done(t)                            # grants only when every Inv-Ack is in
        elif k == "Inv-Ack":
            assert b and b.get("id") == m["id"], f"protocol: unexpected Inv-Ack from C{s}"
            H["sh"].discard(s); b["acks"] -= 1; done(b)
        elif k == "Data":                          # newest data from the exclusive holder, after a Fwd
            assert b and b.get("op") in ("GetS", "GetM"), f"protocol: unexpected Data from C{s}"
            if b["op"] == "GetS":                  # MESI: a forwarded read also writes memory
                H["mem"] = m["v"]; cnt["memwr"] += 1
                H.update(dir="S", sh=set() if m["wb"] else {H["own"]}, own=None)
            grant(b["req"], "S" if b["op"] == "GetS" else "M", m["v"])
        else:                                      # PutS, PutE, PutM
            holder = H["dir"] == "X" and H["own"] == s
            if holder or ("late-put" in defects and k == "PutM" and H["dir"] == "X"):   # defect b
                if k == "PutM": H["mem"] = m["v"]; cnt["memwr"] += 1
                H.update(dir="U", own=None)
            else:                                  # a sharer, or a late Put from a non-holder
                if k != "PutS": seen["late " + k] += 1
                H["sh"].discard(s)
                if H["dir"] == "S" and not H["sh"]: H["dir"] = "U"
            send("Put-Ack", "H", s)
    def move(i, k, table):                         # protocol checker: is k legal in this state?
        assert c[i]["st"] in table, f"protocol: {k} at C{i} in {c[i]['st']}"
        seen[(k, c[i]["st"])] += 1; c[i]["st"] = table[c[i]["st"]]
    def cache(m):
        to_c.remove(m); i, k, x = m["dst"], m["kind"], c[m["dst"]]
        if k == "Data":                            # course-model assumption: H sees grant delivery,
            H["busy"] = None                       # and records the new holder or sharer then
            if m["perm"] == "S": H["dir"] = "S"; H["sh"].add(i)
            else: H.update(dir="X", own=i, sh=set())
            x["v"] = m["v"]; move(i, k, {"IS": m["perm"], "IM": "M", "SM": "M"})
            store(i) if x["st"] == "M" else load(i)    # the stalled access completes first
        elif k == "Inv":
            send("Inv-Ack", i, "H", id=m["id"]); move(i, k, {"S": "I", "SM": "IM", "SI": "II"})
        elif k in ("Fwd-GetS", "Fwd-GetM"):        # answered from the array or from the WB entry
            send("Data", i, "H", v=x["v"], wb=x["st"] in ("MI", "EI"))
            move(i, k, {"E": "S", "M": "S", "EI": "SI", "MI": "SI"} if k == "Fwd-GetS"
                 else {"E": "I", "M": "I", "EI": "II", "MI": "II"})
        else: move(i, k, {"MI": "I", "EI": "I", "SI": "I", "II": "I"})   # Put-Ack frees the WB entry
        if x["st"] in ("I", "IM", "II"): x["v"] = None
    def op(i, what=None):
        x = c[i]
        if x["st"] not in STABLE + ("SM",): return     # one outstanding request per cache
        if what is None:
            r = rng.random(); what = "load" if r < 0.45 else "store" if r < 0.8 else "evict"
        log.append((i, what))
        if x["st"] == "SM":                        # SM^D: loads hit, stores and evictions wait
            if what == "load": load(i); seen["load hit in SM^D"] += 1
        elif what == "load":
            if x["st"] == "I": x["st"] = "IS"; send("GetS", i, "H")
            else: load(i)
        elif what == "store":
            if x["st"] in ("E", "M"): x["st"] = "M"; store(i)     # E to M is silent
            else: x["st"] = "SM" if x["st"] == "S" else "IM"; send("GetM", i, "H")
        elif x["st"] != "I":                       # notified eviction: the WB entry keeps the value
            send({"S": "PutS", "E": "PutE", "M": "PutM"}[x["st"]], i, "H", v=x["v"]); x["st"] += "I"
    def moves():
        return ([("c", m) for m in to_c] + [("in", m) for m in link if room(m)]
                + [("h", m) for m in hq if m["kind"] not in REQ or not H["busy"]])
    def do(mv):                                    # one delivery, logged in script form
        m = mv[1]; log.append((m["kind"], m["src"], m["dst"]) + (("wait",) if mv[0] == "in" else ()))
        {"c": cache, "in": enter, "h": home}[mv[0]](m)
    step = None
    try:
        for e in script or ():                     # directed run: core ops and chosen deliveries
            if isinstance(e[0], int): op(*e)
            else:                                  # (kind, src, dst[, "wait"]): deliver that message
                mv = [x for x in moves() if (x[1]["kind"], x[1]["src"], x[1]["dst"]) == e[:3]]
                assert mv, f"script: {e} not enabled"
                do(mv[0]); check()
                if mv[0][0] == "in" and e[3:] != ("wait",):       # and let H handle it, if it can
                    mv = [x for x in moves() if x[0] == "h" and x[1] is mv[0][1]]
                    if mv: do(mv[0])
            while drain and moves(): do(moves()[0]); check()   # traffic mode: nothing overlaps
            check()
        if script is not None: steps = 0           # after a script: just drain, in seeded order
        for step in range(10 ** 6):
            mv, pending = moves(), to_c or link or hq
            if pending and not mv:                 # the progress check
                raise AssertionError(f"deadlock: no enabled move, H busy {bool(H['busy'])}, "
                                     f"buffer {[x['kind'] for x in hq]}, waiting {[x['kind'] for x in link]}")
            for w in {"request" if m["kind"] in REQ else "response" for m in link if not room(m)}:
                seen[w + " waits for buffer space"] += 1
            if step >= steps and not pending: break
            if mv and (step >= steps or rng.random() < 0.6): do(mv[rng.randrange(len(mv))])
            elif step < steps: op(rng.randrange(n))
            check()
        assert H["busy"] is None and all(x["st"] in STABLE for x in c), "end: not quiescent"
        holders = {i for i in range(n) if c[i]["st"] != "I"}
        recorded = H["sh"] if H["dir"] == "S" else {H["own"]} if H["dir"] == "X" else set()
        assert holders == recorded, f"end: directory records {recorded}, caches hold {holders}"
        dirty = [x["v"] for x in c if x["st"] == "M"]
        assert (dirty[0] if dirty else H["mem"]) == gold[0], "end: newest value lost"
    except AssertionError as e:
        return (str(e) if step is None else f"step {step}: {e}"), cnt
    return None, cnt
WARM = [(0, "load"), ("GetS", 0, "H"), ("Data", "H", 0), (1, "load"), ("GetS", 1, "H"),
        ("Fwd-GetS", "H", 0), ("Data", 0, "H"), ("Data", "H", 1)]          # warm-up: C0 S / 0, C1 S / 0
A = WARM + [(1, "store"), (0, "store"), ("GetM", 1, "H", "wait"), ("GetM", 0, "H")]
A2 = WARM + [(1, "store"), (0, "store"), ("GetM", 0, "H", "wait"), ("GetM", 1, "H")]
B0 = [(0, "store"), ("GetM", 0, "H"), ("Data", "H", 0), (0, "evict"), (1, "store")]
B = B0 + [("GetM", 1, "H"), ("Fwd-GetM", "H", 0), ("Data", 0, "H"), ("Data", "H", 1), ("PutM", 0, "H"),
          ("Put-Ack", "H", 0), (0, "load")]
B2 = B0 + [("PutM", 0, "H"), ("Put-Ack", "H", 0), ("GetM", 1, "H"), ("Data", "H", 1), (0, "load")]
C = WARM + [(0, "store"), ("GetM", 0, "H"), (1, "store"), (2, "load"), ("GetM", 1, "H", "wait"),
            ("GetS", 2, "H", "wait"), ("Inv", "H", 1)]
DEFECTS = {"lost-inv": "value", "late-put": "value", "shared-queue": "deadlock"}   # defect: expected check
first, weak = {d: [] for d in DEFECTS}, []
for seed in range(20):                             # full runs: the correct model passes, each defect fails
    assert run(seed)[0] is None, seed
    for d, check_name in DEFECTS.items():
        fail = run(seed, defects=(d,))[0]
        assert fail and fail.split(": ")[1] == check_name, (seed, d, fail)
        assert d != "lost-inv" or "SWMR" in fail, fail                  # (a): SWMR fails at the same event
        assert d != "late-put" or " with C" in fail.split("; ")[0], fail  # (b): the authority half fires
        first[d].append(int(fail.split()[1][:-1]))
    weak.append(int(run(seed, defects=("late-put",), authority=False)[0].split()[1][:-1]))
assert {d: (min(v), max(v)) for d, v in first.items()} == {
    "lost-inv": (27, 2122), "late-put": (41, 907), "shared-queue": (15, 429)}, first
assert (min(weak), max(weak)) == (48, 1029), weak  # copy half only: (b) is still found, but later
short = {d: [s for s in range(30) if run(s, defects=(d,), steps=200)[0]] for d in DEFECTS}
assert all(run(s, steps=200)[0] is None for s in range(30))
assert short == {"lost-inv": [3, 7, 8, 9, 13, 21, 23, 26],
                 "late-put": [0, 2, 4, 6, 7, 9, 10, 12, 20, 21, 23, 24, 26, 28, 29],
                 "shared-queue": [s for s in range(30) if s not in (1, 2, 5, 11, 13, 17, 20)]}, short
found = {d: run(0, defects=(d,), script=sc)[0] for d, sc in zip(DEFECTS, (A, B, C))}
assert found["lost-inv"].endswith("value: C1 holds 0, golden 1; SWMR: writers [0], readers [1]"), found
assert found["late-put"] == "value: dir U with C1 in M; value: dir U, memory 1, golden 2", found  # step 5
assert run(0, defects=("late-put",), script=B, authority=False)[0].endswith(      # step 8, SWMR too
    "value: load at C0 got 1, golden 2; value: C0 holds 1, golden 2; SWMR: writers [0, 1], readers []")
assert "deadlock" in found["shared-queue"] and "waiting ['Inv-Ack']" in found["shared-queue"], found
assert run(0, defects=("lost-inv",), script=A2)[0].endswith("value: C0 holds 0, golden 1; SWMR: writers [1], readers [0]")
assert run(0, defects=("late-put",), script=B2)[0] is None   # PutM first: a normal writeback, no bug
for d, sc in zip(DEFECTS, (A, B, C)):              # each directed trace exposes its own defect only
    assert all(run(0, defects=(o,), script=sc)[0] is None for o in DEFECTS if o != d), d
    assert run(0, script=sc)[0] is None, d
log = []                                           # a failing random seed, logged, replays as a script
fail = run(3, defects=("lost-inv",), log=log)[0]
assert len(log) == 29 and run(0, defects=("lost-inv",), script=log)[0] == fail.split(": ", 1)[1], (fail, log)
assert all(run(s, n=2, defects=("shared-queue",))[0] is None for s in range(20))          # 2 cores, 2 slots
assert all(run(s, n=2, hq_size=1, defects=("shared-queue",))[0] for s in range(5))        # 2 cores, 1 slot
print("PASS: every defect is caught on seeds 0-19 by the right check, short runs show which seeds, "
      f"latest first failures at events {[max(v) for v in first.values()]}, the traces and a seed log reproduce")

Defect	Full runs (4,000 events), seeds 0 to 19	First failure (event), measured	Short runs (200 events), seeds 0 to 29
a. lost-inv	All 20, value checker, SWMR at the same event	27 to 2,122	8 of 30: 3, 7, 8, 9, 13, 21, 23, 26
b. late-put	All 20, value checker (authority half)	41 to 907 (48 to 1,029 with the copy half only)	15 of 30: 0, 2, 4, 6, 7, 9, 10, 12, 20, 21, 23, 24, 26, 28, 29
c. shared-queue	All 20, progress check	15 to 429	23 of 30: all but 1, 2, 5, 11, 13, 17, 20

The correct model passes every one of these seeds. The scripts A, B and C replay the three tables above: each fails with its own defect and passes with either of the other two switched on, so each trace isolates one bug. The spread matters: (a) and (b) each need a specific overlap of two transactions, and a 200-event run finds (a) on only 8 of 30 seeds and (b) on half. A regression that ran short tests on a handful of seeds could miss both. The last checks show how a random failure becomes a trace: seed 3 of lost-inv fails at event 33, its log has 29 entries, and replaying the log as a script gives the same failure, ready to be cut down by hand.

Check yourself In trace (b), every cache copy is still correct after step 5. Why does the checker fire there, and what would a checker that judges only cache copies and loads report instead?

The authority half of the data-value invariant checks H's record and memory against the holders: an E or M holder must be the cache H records as exclusive, and memory must equal the golden value whenever H records U or S. At step 5 H records U while C1 is in M, and memory holds 1 against golden 2, so both fail. A copy-only checker sees nothing until step 8, when H serves C0's read from the stale memory; if nobody read X again, it would see nothing until an end-of-run check.

Check yourself Would defect (c) disappear if H's buffer had three slots?

Not in general. With three cores and three slots, C0's GetM plus requests from C1 and C2 no longer fill the buffer, but any bounded shared buffer can be filled when more caches or lines compete. The fix is a separate response class with its own reserved space, not a bigger shared buffer.

Navigate

Which check finds which bug, and on which seeds?

a. Upgrade race that loses an invalidation

b. Eviction versus forward that returns stale data

c. A resource cycle under finite buffers

Finding them by seed, and proving the traces

Related topics

Find the Races

Which check finds which bug, and on which seeds?

a. Upgrade race that loses an invalidation

b. Eviction versus forward that returns stale data

c. A resource cycle under finite buffers

Finding them by seed, and proving the traces

Related topics

Which check finds which bug, and on which seeds?

a. Upgrade race that loses an invalidation

b. Eviction versus forward that returns stale data

c. A resource cycle under finite buffers

Finding them by seed, and proving the traces

Related topics

Up next

Which check finds which bug, and on which seeds?

a. Upgrade race that loses an invalidation

b. Eviction versus forward that returns stale data

c. A resource cycle under finite buffers

Finding them by seed, and proving the traces

Related topics

Up next