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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193

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)]
SCRIPTS = {"lost-inv": (A, A2), "late-put": (B, B2), "shared-queue": (C,)}   # each race, each order
r_first = []
for d, scripts in SCRIPTS.items():
    for sc in scripts:
        runs = set()
        for seed in range(10):                               # fixed: the race completes on every seed
            log = []
            assert run(seed, script=sc, log=log)[0] is None, (d, seed)
            runs.add(tuple(log))
            served = [e for e in log if e in (("GetM", 1, "H"), ("GetS", 2, "H"))]
            if sc is C and served[0][0] == "GetS": r_first.append(seed)     # H served R before B
        assert (len(runs) == 1) == (sc is not C), (d, len(runs))   # A, A2, B, B2: one forced drain order
assert r_first == [0, 2, 3, 4, 5], r_first                   # C: both orders, B first on 1 and 6 to 9
assert all(run(0, defects=(d,), script=sc)[0] for d, sc in (("lost-inv", A), ("lost-inv", A2),
           ("late-put", B), ("shared-queue", C)))            # failing case: each defect still fails
for size in (1, 2, 3):                                       # request slots
    for slots in (1, None):                                  # response slots: 1, or n - 1 = 2
        seen = Counter()
        for seed in range(20):
            fail, _ = run(seed, hq_size=size, resp_size=slots, seen=seen)
            assert fail is None, (size, slots, seed, fail)
        assert (seen["response waits for buffer space"] > 0) == (slots == 1), (size, slots)
assert "deadlock" in run(0, resp_size=0)[0]                  # no response slot: the progress check fires
assert run(0, hq_size=1, defects=("shared-queue",))[0]       # one shared slot still deadlocks
def turn(w): return [(w, "load"), (w, "store")] + [(r, "load") for r in range(3) if r != w]
counter = [e for _ in range(2) for w in range(3) for e in turn(w)] + [(2, "evict")]
producer = [e for _ in range(3) for e in [(0, "store")] + [(1, "load"), (2, "load")] * 2] + [(0, "evict")]
mesi = {}
for name, tr in (("counter", counter), ("producer", producer)):
    fail, cnt = run(0, script=tr, drain=True)                # traffic mode: one operation at a time
    assert fail is None, (name, fail)
    mesi[name] = (cnt["msgs"], cnt["memwr"])
assert mesi == {"counter": (70, 6), "producer": (34, 3)}, mesi
print(f"PASS: the fixed model passes five race scripts on 10 seeds each and 120 seeded runs, MESI traffic {mesi}")

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
44
45
46

def count(proto, trace, broken=False):
    """One operation at a time (no races): data through H, acks at H, notified evictions."""
    st, val, mem, last, n = {}, {}, 0, 0, {"msgs": 0, "memwr": 0}
    for i, op in trace:
        s = st.get(i, "I")
        others = {k: x for k, x in st.items() if k != i and x != "I"}
        holder = next((k for k, x in others.items() if x in "EMO"), None)
        if op == "load" and s == "I":
            if holder is None:                               # GetS, Data from memory
                n["msgs"] += 2; val[i] = mem; st[i] = "S" if others else "E"
            else:                                            # GetS, Fwd-GetS, Data to H, Data
                n["msgs"] += 4; val[i] = val[holder]; st[i] = "S"
                if proto == "MOESI" and others[holder] in "MO":
                    st[holder] = "O" if not broken else "S"  # broken: dirty S, nobody responsible
                else:                                        # E or M holder in MESI, E in MOESI
                    st[holder] = "S"; mem = val[holder]; n["memwr"] += 1
        if op == "load":
            assert val[i] == last, f"{proto}: load at C{i} got {val[i]}, last store {last}"
        elif op == "store":
            if s not in "EM":                                # E to M is silent
                n["msgs"] += 2 + 2 * sum(x == "S" for x in others.values())   # GetM, Data, Inv, Inv-Ack
                if holder is not None: n["msgs"] += 2        # Fwd-GetM, Data to H
                for k in others: st[k] = "I"
            last += 1; st[i], val[i] = "M", last
        elif op == "evict" and s != "I":
            n["msgs"] += 2                                   # PutS, PutE or PutM, then Put-Ack
            if s in "MO": mem = val[i]; n["memwr"] += 1      # PutM writes memory
            st[i] = "I"
    if not any(x in "MO" for x in st.values()):
        assert mem == last, f"{proto}: memory {mem} after the last dirty copy left, last store {last}"
    return n["msgs"], n["memwr"]
def turn(w): return [(w, "load"), (w, "store")] + [(r, "load") for r in range(3) if r != w]
counter = [e for _ in range(2) for w in range(3) for e in turn(w)] + [(2, "evict")]
mesi, moesi = count("MESI", counter), count("MOESI", counter)
assert (mesi, moesi) == ((70, 6), (82, 1)), (mesi, moesi)   # MESI numbers equal the full model's
start, steady = turn(0), turn(1)                            # one steady turn, after C0's turn
d = {p: tuple(a - b for a, b in zip(count(p, start + steady), count(p, start))) for p in ("MESI", "MOESI")}
assert d == {"MESI": (12, 1), "MOESI": (14, 0)}, d          # O saves the write, costs 2 messages
private = [(0, "load"), (0, "store"), (0, "store"), (0, "evict")]
assert count("MESI", private) == count("MOESI", private) == (4, 1)   # no dirty sharing: no saving
try:
    count("MOESI", counter, broken=True)
    raise SystemExit("broken MOESI was not caught")
except AssertionError as e:
    assert str(e) == "MOESI: load at C2 got 0, last store 1", e
print(f"PASS: counter trace MESI {mesi} vs MOESI {moesi} (messages, memory writes), O saves one write per turn")