|
| 1 | +/* Global invariant monitors for the manifest-replica lifecycle seam. |
| 2 | + |
| 3 | + ReplicaStateMatchesReaders (safety, INV: no leak / no premature loss). At a |
| 4 | + quiesce checkpoint, the set of streams the replica still holds state for must |
| 5 | + equal the set of streams with a live reader. Two directions, each tied to a |
| 6 | + guard: |
| 7 | + - held => live (no leak): a stranded entry for an exited reader trips this. |
| 8 | + Proves the member-DOWN cleanup (G1) load-bearing, and surfaces the |
| 9 | + sync-after-exit gap (a sync re-creates a row after cleanup released it). |
| 10 | + - live => held (no loss): evicting a live reader's state trips this. Proves |
| 11 | + the re-registration monitor repoint (G3) load-bearing. |
| 12 | +
|
| 13 | + NoStaleFloorServed (safety, INV: no stale floor). Read-side analogue of the |
| 14 | + ../gc-reset-multinode finding. The cache's applied (epoch, sn) must be |
| 15 | + monotonically non-decreasing and must only ever hold a committed floor, so a |
| 16 | + replica never serves a floor that a newer write already superseded. Proves |
| 17 | + is_stale_sync (G2) load-bearing. |
| 18 | + |
| 19 | + ReplicaConverges (liveness, hot state). Once the writer has committed a floor, |
| 20 | + a replica that keeps receiving syncs must eventually catch up to the latest |
| 21 | + committed (epoch, sn). A run that ends with the cache permanently behind is a |
| 22 | + liveness violation. */ |
| 23 | + |
| 24 | +/* held(stream) == (live readers for stream > 0), checked at quiesce. */ |
| 25 | +spec ReplicaStateMatchesReaders |
| 26 | + observes eReaderUp, eReaderDown, eQuiesceBegin, eHeld, eQuiesceEnd { |
| 27 | + var liveReaders: map[StreamId, int]; |
| 28 | + var held: set[StreamId]; |
| 29 | + |
| 30 | + start state Watching { |
| 31 | + on eReaderUp do (s: StreamId) { |
| 32 | + if (s in liveReaders) { |
| 33 | + liveReaders[s] = liveReaders[s] + 1; |
| 34 | + } else { |
| 35 | + liveReaders[s] = 1; |
| 36 | + } |
| 37 | + } |
| 38 | + on eReaderDown do (s: StreamId) { |
| 39 | + if (s in liveReaders) { |
| 40 | + liveReaders[s] = liveReaders[s] - 1; |
| 41 | + if (liveReaders[s] == 0) { |
| 42 | + liveReaders -= (s); |
| 43 | + } |
| 44 | + } |
| 45 | + } |
| 46 | + on eQuiesceBegin do { |
| 47 | + held = default(set[StreamId]); |
| 48 | + } |
| 49 | + on eHeld do (s: StreamId) { |
| 50 | + held += (s); |
| 51 | + } |
| 52 | + on eQuiesceEnd do { |
| 53 | + var s: StreamId; |
| 54 | + /* No leak: every held stream must still have a live reader. */ |
| 55 | + foreach (s in held) { |
| 56 | + assert s in liveReaders, |
| 57 | + format("NOLEAK violated: replica holds per-node state for stream {0} with no live reader (an exited reader was not cleaned up, or a sync re-stranded the row after cleanup)", |
| 58 | + s); |
| 59 | + } |
| 60 | + /* No loss: every live reader's stream must still be held. */ |
| 61 | + foreach (s in keys(liveReaders)) { |
| 62 | + assert s in held, |
| 63 | + format("RETAIN violated: replica dropped per-node state for stream {0} that still has a live reader (a superseded member DOWN evicted the live context)", |
| 64 | + s); |
| 65 | + } |
| 66 | + } |
| 67 | + } |
| 68 | +} |
| 69 | +
|
| 70 | +/* The cache may only ever hold a committed floor, and its applied (epoch, sn) |
| 71 | + must never regress - the read-side stale-floor guard. */ |
| 72 | +spec NoStaleFloorServed observes eFloorCommitted, eCacheUpdated { |
| 73 | + var committed: set[(floor: int, epoch: int, sn: int)]; |
| 74 | + var maxApplied: map[StreamId, (epoch: int, sn: int)]; |
| 75 | +
|
| 76 | + start state Watching { |
| 77 | + on eFloorCommitted do (p: (floor: int, epoch: int, sn: int)) { |
| 78 | + committed += ((floor = p.floor, epoch = p.epoch, sn = p.sn)); |
| 79 | + } |
| 80 | + on eCacheUpdated do (p: (stream: StreamId, floor: int, epoch: int, sn: int)) { |
| 81 | + var prev: (epoch: int, sn: int); |
| 82 | + assert (floor = p.floor, epoch = p.epoch, sn = p.sn) in committed, |
| 83 | + format("STALEFLOOR violated: replica cached an uncommitted floor for stream {0} (floor={1}, epoch={2}, sn={3})", |
| 84 | + p.stream, p.floor, p.epoch, p.sn); |
| 85 | + if (p.stream in maxApplied) { |
| 86 | + prev = maxApplied[p.stream]; |
| 87 | + assert !StaleLex(p.epoch, p.sn, prev.epoch, prev.sn), |
| 88 | + format("STALEFLOOR violated: cache for stream {0} regressed to (epoch={1}, sn={2}) below already-applied (epoch={3}, sn={4}) - a stale sync rolled the floor backward", |
| 89 | + p.stream, p.epoch, p.sn, prev.epoch, prev.sn); |
| 90 | + } |
| 91 | + maxApplied[p.stream] = (epoch = p.epoch, sn = p.sn); |
| 92 | + } |
| 93 | + } |
| 94 | +} |
| 95 | +
|
| 96 | +/* Liveness: a single tracked stream's cache must eventually reach the latest |
| 97 | + committed (epoch, sn). Lagging is hot: a terminal state with the cache behind |
| 98 | + the committed floor is a violation. */ |
| 99 | +spec ReplicaConverges observes eFloorCommitted, eCacheUpdated { |
| 100 | + var committedEpoch: int; |
| 101 | + var committedSeq: int; |
| 102 | + var cacheEpoch: int; |
| 103 | + var cacheSeq: int; |
| 104 | + |
| 105 | + start state Caught { |
| 106 | + on eFloorCommitted do (p: (floor: int, epoch: int, sn: int)) { |
| 107 | + committedEpoch = p.epoch; |
| 108 | + committedSeq = p.sn; |
| 109 | + if (StaleLex(cacheEpoch, cacheSeq, committedEpoch, committedSeq)) { |
| 110 | + goto Lagging; |
| 111 | + } |
| 112 | + } |
| 113 | + on eCacheUpdated do (p: (stream: StreamId, floor: int, epoch: int, sn: int)) { |
| 114 | + cacheEpoch = p.epoch; |
| 115 | + cacheSeq = p.sn; |
| 116 | + } |
| 117 | + } |
| 118 | + |
| 119 | + hot state Lagging { |
| 120 | + on eFloorCommitted do (p: (floor: int, epoch: int, sn: int)) { |
| 121 | + committedEpoch = p.epoch; |
| 122 | + committedSeq = p.sn; |
| 123 | + } |
| 124 | + on eCacheUpdated do (p: (stream: StreamId, floor: int, epoch: int, sn: int)) { |
| 125 | + cacheEpoch = p.epoch; |
| 126 | + cacheSeq = p.sn; |
| 127 | + if (!StaleLex(cacheEpoch, cacheSeq, committedEpoch, committedSeq)) { |
| 128 | + goto Caught; |
| 129 | + } |
| 130 | + } |
| 131 | + } |
| 132 | +} |
0 commit comments