Sequence Diagrams — Message Path and Ownership Changes
How messages and partition ownership actually move between named participants. Two scenarios, both sequenceDiagram with autonumber.
Relationship to Use cases and flows: Scenario A's steady-state path below is the same link that page draws as an activity flowchart. Read that page for branch conditions and conservation formulas, this one for participant order and message contents.
Publish Persistence + Consume Delivery (main success path)
Exception Branches (summary of the failure paths of the same interaction)
| Failure point | Behavior | Error / state |
|---|---|---|
| Invalid token | Reject the connection's first frame | ERR AUTH_FAILED (generic + 100 ms) |
| Both followers lagging | Ack timeout → enter ReadOnly | ERR QUORUM_LOST / READ_ONLY_DEGRADED |
| Old leader rejoins | Epoch fencing: append rejected | STALE_LEADER_EPOCH (internal) |
| Consumer without credit | MSG scheduling pauses (no mid-frame read stalls) | Credit wait (not an error) |
| PUB replay (client retry) | Producer dedup on (producer_id, producer_seq); delivery_id only fences the consume side | Idempotent, no duplicate delivery |
Relation to simulation and model checking
- This action sequence is one of the simulation's "golden traces" (the harness injects
kill -9between steps 3–5). - "Quorum flushed before commit" is the protocol projection of the
lease.qntinvariantvisibleImpliesQuorumFlushed.
Scenario A: Consumer-Group Membership Change (incremental rebalance)
Scenario B: Lease-Timeout Degraded Election (Prepare/Install)
Semantic Anchors
| Interaction | Guarantee | Verification |
|---|---|---|
| All of scenario A | Incrementality / safety / liveness | CB1–CB4; slow-consumer / partition injection |
| Scenario B: majority promise before Install | No split brain | inv_installNeedsQuorumPromise |
| Scenario B: fencing | Visible log never regresses | visibleMonotonic |
| Shared constraint | Metadata mutations go through the single-writer metadata log | DECLARE/NOTICE idempotency |