A flat latency counter cannot classify the failure. Inspect enabled transitions and resource ownership. Use the two-core model with a pending request for X, and add only the finite queues or arbitration policy each case describes.
Case | What happens | Classification | Evidence |
|---|---|---|---|
P_X and Q wait on each other | No permitted service can free either resource. | Deadlock in the modelled subsystem, which is closed: no outside event can free a resource. | A held/requested dependency cycle and no enabled escape. |
MSI: M passes back and forth | C0 receives Data(M) but answers C1's Fwd-GetM before its store performs. C1 then does the same. The line moves between them and no store completes. | Livelock. | Messages keep moving, no useful operation completes. Repair: the policy in Simultaneous Upgrades. |
C1's GetM is NACKed on every retry | H keeps admitting C0's requests for other lines into every freed slot, so C1's retry for X is always NACKed. | Starvation of C1. | The eligible request is bypassed without bound. Remedies: Retries, NACKs and Credits. |
Output temporarily full, then drains | The blocked sender resumes after capacity returns. | Backpressure, not by itself a progress failure. | A finite stall with a named capacity-return event. |
A reserved response path can remove the earlier P/Q deadlock. It does not make an unfair arbiter service C1. A fair arbiter does not repair a full resource cycle. Random backoff can reduce collisions but is not a deterministic proof that every operation eventually finishes.
Eventual completion after a backpressure stall holds under A1-A6 (assumptions), here chiefly A4: the downstream consumer eventually accepts. Without it, 'the queue will drain' is a wish rather than an argument.
A finite test can demonstrate a deadlock checkpoint for a closed modelled system, or detect an excessive wait under an assumed bound. It cannot establish an infinite execution from a timeout alone. Preserve state and dependencies when reporting a hang instead of only reporting elapsed cycles.
Not on that evidence. The system is making useful progress, but C1 may be starving. Review eligibility and fairness rather than trying to break a nonexistent global wait cycle.