Every earlier part taught one mechanism at a time. The capstone puts them in one place: you write a small coherence protocol that runs, a checker that judges it after every event, and you then hunt three races that a reviewer would expect a careful designer to have thought about. The output is the kind of evidence a design review asks for: a model, failing traces, fixes, numbers and a memo.
The course model with two stated extensions: three cores, and finite input buffers at H. The cores are C0, C1 and C2. With two request slots, three cores are the minimum (with one slot, two cores deadlock too): the third planted race needs two requests waiting at H while a third cache owes H a response. One line X, which starts at 0 in memory and in no cache.
Choice | This capstone | Where it was taught |
|---|---|---|
Protocol | MESI: E (MESI, MOESI) is granted to a GetS when no cache holds X, and E to M is silent | |
Directory | U, S{...} or exclusive(Cn) at H, with one pending entry for X | |
Acknowledgements | Inv-Acks are collected at H, so requesters wait only for Data (IS^D, IM^D, SM^D) | |
Data from a holder | Four-hop: the holder sends Data to H, H sends Data to the requester | |
Evictions | Notified: PutS, PutE, PutM, each waiting for Put-Ack in SI^A, EI^A or MI^A; the WB entry answers forwards | |
Network | Reliable, unordered: no FIFO order between any two nodes or classes | Course model |
Home buffers | Finite: two request slots at H's input; responses have their own n - 1 reserved slots | |
Grant delivery | H starts no conflicting transaction for X until its Data grant has been delivered (the course-model assumption) | Course model |
MESI rather than MSI because E adds a real race surface (a silent E to M change that H cannot see, PutE, and EI^A answering a forward) while keeping the model small. MOESI appears only in the traffic comparison of step 4, where the question is what O saves.
Step | Deliverable | Done when |
|---|---|---|
A runnable MESI model with a golden checker: SWMR and the data-value invariant after every event, seeded unordered delivery, a progress check and end checks | Many seeded runs and one long run pass, and the run statistics show the races occurring | |
Three planted defects behind switches, each found by the right check, each failure reduced to a short trace | Each defect fails on the seeds you report; the correct model passes the same seeds | |
The three fixes, the passing directed traces, and a MESI versus MOESI traffic comparison on one trace | Fixed model passes; traffic numbers are asserted, not just printed | |
4. Design memo | A one to two page memo in the taught structure: problem, constraints, options, analysis, recommendation with its flip condition, risks, verification plan | A reviewer can act on it without asking you a question |
The planted defects are (a) an upgrade race that loses an invalidation, (b) an eviction-versus-forward race that returns stale data, and (c) a resource cycle that deadlocks when requests and responses share H's finite input buffer. (a) and (b) are safety bugs and must be caught by the value checker; (c) is a progress bug and must be caught by the progress check, because a deadlocked system never returns a wrong value.
Criterion | 0: missing | 2: partial | 4: strong |
|---|---|---|---|
Model fidelity | States or messages differ from the course model without saying so | Runs, but some rule (ack collection, late Put, WB entry) is implicit | Every rule is written down, matches the course model, and each extension is stated |
Checker strength | Checks only at the end, or checks states not values | Value checks on loads only | After every event: SWMR, every usable copy against golden, and the authority half (H's entry names each E or M holder, and memory is golden when H records U or S); unique store values, protocol legality, progress and end checks |
Evidence of coverage | Seeds pass, nothing more | Some race counts reported | Every race the defects need is shown to occur in the passing runs |
Bug finding | A defect is found by luck or not at all | Found, but trace not reduced | Each defect found by the intended check, on named seeds, with a minimal trace in course notation |
Fixes | Symptom patched (a seed now passes) | Correct fix, argued informally | Fix states the rule it restores and passes the directed trace in each arrival order you script |
Traffic and memo | Numbers without a trace or a routing | Numbers with assumptions | Assumptions, asserted numbers, a recommendation tied to the workload, risks and a verification plan |
Part 2: SWMR Precisely, The Data-Value Invariant, Stable Versus Transient States.
Part 3: Upgrade From Shared, Dirty Intervention, Dirty Writeback.
Part 4: Simultaneous Upgrades, Eviction Versus Intervention, MSHRs and Pending Entries.
Part 5: A Protocol Deadlock, Deadlock, Livelock, Starvation, Stating Progress Assumptions.
Part 11: Check Values, Not States, A Reference Model in Python, Random Traffic and Injected Bugs.
A deadlock stops events from happening; no load ever returns a value, so no value can be wrong. SWMR and the data-value invariant are safety properties and stay true in a frozen system. Only a check that notices pending work with no enabled move (or a drain that never finishes) reports it.