Detect deadlocks across shard boundaries

Use one vertex for each live transaction instance and a directed edge from a waiting transaction to the transaction whose incompatible lock prevents it from proceeding. For an AND-style nonpreemptive resource model, where each blocked operation needs its requested resource and locks are not spontaneously released, a directed wait-for cycle identifies a deadlock. Other waiting models need different reasoning: waiting for any one of several alternatives is not equivalent to requiring them all. State the model before applying a cycle rule.

A local shard sees only the dependencies involving resources it manages. The global cycle can be invisible in every local subgraph. Include transaction generation and resource identity in exported edges, especially when transaction identifiers or connections can be reused. Distinguish a transaction waiting for another lock owner from a transaction waiting for coordinator recovery or network delivery. Combining all these waits in one unlabeled graph can produce a plausible picture with no valid deadlock theorem behind it.

Edges appear and disappear while a detector gathers information. A union of old observations can contain a cycle that never existed at one instant. A detector therefore needs a protocol and correctness assumptions, such as validated current edges, transaction epochs, or a formally specified distributed detection algorithm. A slow request or a lock-wait timeout can justify a bounded-wait policy without proving deadlock. Record whether an abort was caused by policy, a validated deadlock, or a different failure so operators can interpret the evidence.

When a real cycle is found, choose a victim using the system’s policy and ensure its abort actually releases the relevant resources before expecting peers to advance. An already prepared participant may be constrained by atomic-commit promises, so a lock manager cannot freely override the transaction protocol. Victim choice can balance wasted work and starvation, but it is not a new commit decision. Retrying should rerun the logical transaction under a bounded policy, with consistent lock ordering where practical to prevent repeated cycles.

Test two- and three-shard cycles with deterministic barriers: arrange the initial locks, confirm the waits, then invoke the detector. Also test a near-cycle whose first edge disappears before the last is created. Check that the detector does not confuse a retried transaction with its previous generation. Recovery tests should verify both the chosen victim’s final abort and eventual progress by survivors when the environment permits it. A graph screenshot without those state transitions is incomplete evidence.

The modular lab supplies a small cycle analogy. Reset, set modulus to 3 and additive step to 1, predict a return to zero after three additions, then press Step three times. For a new run, Reset and set both modulus to 4 and additive step to 2, predict the period, then Step twice. This is an exact arithmetic orbit, not a wait-for graph or deadlock detector. Explain why seeing a cycle here says nothing about whether any transaction is blocked or whether the observations were simultaneous.