Use an abstract store-buffering machine with X=0 and Y=0 initially, atomic indivisible accesses, no other agents and no fences. P0 executes X=1 then reads Y into r0. P1 executes Y=1 then reads X into r1. These are abstract hardware events, not non-atomic C/C++ code.
Under sequential consistency (SC), one global order respects each processor’s program order, so r0=r1=0 would require a cycle. Under the x86-TSO store-buffer model, each store can remain in its local buffer while the other-address load reads memory, allowing both zeros. Coherence for X and Y separately does not remove that possibility.
Litmus: coherence is not a cross-address memory model — worked trace
Illustrative isolated example; not measured silicon behaviour.
Model / outcome | Reason |
|---|---|
SC: (0,0) forbidden | X write < P0 read Y < Y write < P1 read X < X write would be required |
SC: (1,0), (0,1), (1,1) allowed | A consistent interleaving can produce each |
TSO store-buffer model: (0,0) allowed | Both loads can precede the other core’s store-buffer drain |
A fence experiment | Use the named model’s store-to-load ordering fence on both cores; do not substitute a cache flush |
No. Per-address coherence and cross-address ordering answer different questions. Both cores can read the other location’s initial value before the buffered stores become globally visible.
Isolated generic line model: C0 and C1 both request write permission for X; initially both have clean shared X=0. Assume a home serialises the line, chooses C0 first and queues C1. Invalidation/data acknowledgements are delivered eventually. This is an explicit arbitration choice, not a claim that ACE or CHI always favours C0.
C1 waits because its permission conflicts with the earlier transaction. After C0’s permission completes, C0 writes 7 before the home serves C1. The later transfer must resolve C0’s dirty 7; returning memory’s old 0 loses a completed write. A retry implementation could instead reject C1 and require a later re-request, but must not grant both exclusive writers.
A race needs a winner, not two guessed timelines — worked trace
Illustrative isolated example; not measured silicon behaviour.
Order | C0 | C1 | Required safety evidence |
|---|---|---|---|
Both request | Waiting | Waiting | Neither writes with a merely pending request |
Home chooses C0 | Waits for conflicting copy removal | Waits / relinquishes conflicting copy | C0 gains permission only after required conflicts resolve |
C0 completes and writes | Exclusive dirty X=7 | Still waiting | Memory may still contain 0 |
Home then serves C1 | Relinquishes its conflicting copy and supplies 7 | Receives X=7 with write permission | Only one writer; newest value preserved |
C1 waits behind the home’s chosen C0 transaction. It must receive 7, with the required permission transfer complete, before it can perform its own write.
Coherency bugs require correlating three views: the initiating transaction (ID, address), the snoop responses (which caches responded, what state), and the final data delivery (who provided data, from cache or memory).
Use litmus tests with explicit initial values, operation semantics and a named memory model. A forbidden observed outcome is useful counterexample evidence only if the test and observation are valid; passing sampled executions is not a general proof. Do not use undefined non-atomic C/C++ races as hardware memory-model evidence.
Log format: timestamp, txn ID, address[addr_bits:line_bits], snoop type, responder, final state.
Deadlock: build a wait-for graph using held/requested buffers, credits, transaction slots and message dependencies; channel names alone are not resources.
False sharing can raise line-ownership traffic; correlate line addresses, writers and performance before naming it.
Reuse the ACE ReadUnique setup: C0 alone holds dirty X=7, C1 is invalid and memory contains 0. No later write or reset occurs. The monitor sees C1's request accepted, a snoop response from C0 promising data, and C1 later receiving 0. This is a value-preservation failure under the stated initial state; it does not require an across-location memory-model argument. The table lists competing explanations, not preselected root causes.
Discriminate at the first boundary that loses 7
Hypothesis | Evidence to capture | What would distinguish it? |
|---|---|---|
C0 returned the wrong bytes | Accepted CD beats, byte position and line context | CD already contains 0 for X despite C0's recorded newest value 7. |
IC selected stale memory | Peer data, memory data and final R selection for this request | CD contains 7, while the output uses memory's 0. |
Response matched to another access | Node/port, ID, sequence and line at each boundary | Correct data is associated with the wrong live request. |
Monitor or initial-state error | Cache initialisation, intervening writes and accepted-event capture | A write/reset or missed handshake invalidates the claimed counterexample. |
No. It narrows the search past that observation, but routing, request correlation, buffering and monitor errors remain possible. Follow the same line and live transaction to locate the earliest boundary where the expected value or association changes.
Correlate node plus transaction context, line, data source and permission evidence; one ID or counter is insufficient.
A data-value counterexample, a forbidden memory-model outcome and a wait cycle answer different questions.
A quiet trace proves neither deadlock nor a particular root cause without outstanding obligations and service assumptions.