|
1 | 1 | /* INV#4 (tier resolution total / correct): an offset held only by the remote |
2 | | - tier (covered by the remote extent, not by the local log) must route to the |
3 | | - remote tier. Routing it locally silently skips the remote data. An offset the |
4 | | - local tier also holds may route locally (osiris prefers the local reader), so |
5 | | - the obligation is only on offsets the local tier does NOT cover. */ |
6 | | -spec TierRoutingCorrect observes eResolution { |
| 2 | + tier (covered by the remote extent, not by the local log) must not route to |
| 3 | + the local tier. Routing it locally silently skips the remote data. RETRY is |
| 4 | + acceptable there (fail closed, the consumer retries); LOCAL is not. An |
| 5 | + offset the local tier also holds may route locally (osiris prefers the local |
| 6 | + reader), so the obligation is only on offsets the local tier does NOT cover. |
| 7 | + |
| 8 | + Independent oracle: coverage is re-derived here from the ground-truth extent |
| 9 | + the DRIVER announced, never from anything the Reader or the cache reported. |
| 10 | + The previous version of this spec computed remoteCovers from the |
| 11 | + ManifestStore's reply, which made the cache simultaneously the component's |
| 12 | + input and the monitor's oracle: a reader that believed an empty or missing |
| 13 | + cache could not be flagged, and the boot-window bug was unrepresentable. */ |
| 14 | +spec TierRoutingCorrect observes eGroundTruth, eResolution { |
| 15 | + var truthKnown: bool; |
| 16 | + var nonEmpty: bool; |
| 17 | + var remoteFirst: int; |
| 18 | + var remoteNext: int; |
| 19 | +
|
7 | 20 | start state Watching { |
8 | | - on eResolution do (r: (tier: Tier, remoteCovers: bool, localCovers: bool)) { |
9 | | - if (r.remoteCovers && !r.localCovers) { |
10 | | - assert r.tier == REMOTE, |
| 21 | + on eGroundTruth do (g: (nonEmpty: bool, remoteFirst: int, remoteNext: int)) { |
| 22 | + truthKnown = true; |
| 23 | + nonEmpty = g.nonEmpty; |
| 24 | + remoteFirst = g.remoteFirst; |
| 25 | + remoteNext = g.remoteNext; |
| 26 | + } |
| 27 | + on eResolution do (r: (outcome: Outcome, offset: int, firstChunkId: int)) { |
| 28 | + var remoteCovers: bool; |
| 29 | + var localCovers: bool; |
| 30 | + assert truthKnown, "eResolution observed before eGroundTruth: driver must announce the true extent first"; |
| 31 | + remoteCovers = nonEmpty && r.offset >= remoteFirst && r.offset < remoteNext; |
| 32 | + localCovers = (r.firstChunkId != -1) && (r.offset >= r.firstChunkId); |
| 33 | + if (remoteCovers && !localCovers) { |
| 34 | + assert r.outcome != LOCAL, |
11 | 35 | "INV#4 violated: an offset held only by the remote tier routed to the local tier (silent remote skip)"; |
12 | 36 | } |
13 | 37 | } |
|
0 commit comments