Scope: committed results of small litmus tests under a named model (SC, TSO, or a weak model where stated), debugged against the course model.
Begin with a minimal litmus test, its initial values and the named model. Record whether each value was tentative or committed. Two different values in a trace do not by themselves distinguish a legal execution from a cache bug or a missing fence.
Model, initial X=Y=0 unless noted | Observation | Classification |
|---|---|---|
SC, SB | Committed r1=0, r2=0 | Forbidden by SC. |
TSO, SB | Committed r1=0, r2=0 | Allowed: the store buffer delays each store past the later load. |
SC or TSO, MP | Committed flag=1, payload=0 | Forbidden. |
SC, MP | Payload load performs with 0 before the flag load | Not a violation by itself: check what commits. |
Any model, one location X: X initially 0, a write of 1, then a write of 2, no later write | A later read receives 1 (the overwritten value) | Data-value failure: the newest value was lost, whatever the ordering rules. |
Bug class | Symptom litmus | First evidence to collect |
|---|---|---|
Illustrative bug class: load queue does not check own evictions, or the cache drops clean lines silently without telling the load queue | MP commits (1, 0) under TSO | Eviction of X between the early payload load and its commit, and no squash recorded |
Illustrative bug class: load-queue match on too few address bits, or at word granularity while Inv is per line | Missed replay: MP (1, 0) when the Inv names another word of the line | The Inv's line address against the load-queue entry's stored address and compare mask |
Illustrative bug class: same-address read-read reordering in a weak core | CoRR: a later read of X returns an older value than an earlier read | The two loads' perform order and the Inv or Fwd-GetM for X between them |
Illustrative bug class: store-to-load forwarding from the wrong store (age compare bug) | A load returns a younger store's value, or an older one than its own core's latest store | Store-queue ages and the forwarding select at the load's perform cycle |
Illustrative bug class: store buffer drains out of order under TSO, for example by coalescing | MP commits (1, 0): Y=1 visible before X=1 | Order of the writer's GetM grants for X and Y and the store-buffer drain log |
Illustrative bug class: reservation not cleared on Inv, Fwd-GetM or eviction | Lost update: two harts' LR/SC increments both succeed from the same old value | Reservation register and the Inv or Fwd-GetM for its line between LR and SC |
Illustrative bug class: a squash also drops the MSHR fill | Orphan Data at C0, directory still lists C0, later Inv gets no matching entry or a hang | The MSHR entry for the line before and after the squash, and H's pending entry |
The last class is the controller side of a squash: see MSHRs and pending entries. A squash discards instruction results; it must not free the miss entry that will receive H's Data.
For an MP failure, preserve the writer's X-before-Y order, the reader's Y-before-X order, which write the flag load read, and the payload result at commit. Then check whether the payload load performed early, which Inv or Fwd-GetM for X arrived or which eviction of X happened before commit, whether a replay was marked, and whether younger work was actually discarded.
For a data-value failure during a dirty transfer, start instead with the line's serialized history and the chain of buffers holding the newest data. A fence does not repair a lost value, and replaying forever does not fix wrong source selection or response matching.
No. That loses the newest value for one location. Ordering constrains when accesses happen; it cannot restore data the coherence implementation destroyed.