diff --git a/specs/README.md b/specs/README.md new file mode 100644 index 000000000..cce373e97 --- /dev/null +++ b/specs/README.md @@ -0,0 +1,833 @@ +# Formal specifications + +Machine-checked models of five pieces of DMI whose correctness arguments are +currently carried by prose: the catalog version allocator, the publisher lease +and fenced publish protocol, the lease *lifecycle* inside +`CaptureStorageService`, the clock-skew bounds in the fence margin and the +default start wait, and the payload ring's span arithmetic. Of the ring, only +the arithmetic that splits a reservation into two spans is checked; its +publish/consume protocol (the ready words, the head and tail updates and their +memory ordering) is not modelled. + +Nothing here is built, imported or executed by DMI. The specs are checked by +hand, with `specs/check.sh` or the commands below; none of them runs in CI. + +```text +specs/ +├── tla/ TLA+ models, checked with TLC +├── z3/ SMT encoding, checked with Z3 +└── cbmc/ C++ harness, checked with CBMC +``` + +Line references point at `main` @ `99ee4ae`. The models were written against +`204a8d2` (first published as `2b74d14`, the same tree), a commit on #150's +branch `fix/lease-recovery`; #150 was squash-merged into main as `7419fd0`, +and its later commits change only `run_cycle()`'s upload gate and comments, +which no model covers. Of what main took after `204a8d2`, only #151 +(`ef2a12f`) changes cited behaviour: `ClickHouseClient` now takes a +`ClickHouseConnection` (credentials, TLS, retry attempts), and `execute()` +retries a read after a transient failure but never a write that may have +reached the server. A repeated read, or a repeated write that never reached +the server, is one later request to these models, so no modelled outcome +changes; the retries only lengthen a lease request's worst case (see `O1`). +#154 (`99ee4ae`) changes comments only, and the quotes below follow its +rewrites of the renewal, spool-sweep and start-wait comments. + +## What each spec models + +| Spec | Models | Source of truth | +|---|---|---| +| `tla/VersionAllocator.tla` | the sole-claimant version allocation loop: floor read, jittered candidate, claim INSERT, singleton read-back, retry | `native/csrc/catalog/version_allocator.cpp:49-89`, header claim at `version_allocator.h:5-7`, watermark publish at `native/csrc/catalog/catalog_writer.cpp:583-628`, `clickhouse_client.cpp:374` | +| `tla/PublisherLease.tla` | the lease claim/renew/release protocol and the fenced publish: `claim_with_rival`, `head()`, `fence()`, `fence_eval()`, `reject_live()`, and `publish_snapshot`'s manifest chunks and watermark INSERT | `native/csrc/catalog/lease_coordinator.cpp:83-257`, `native/csrc/catalog/catalog_writer.cpp:148-169,478-669`, `clickhouse_client.cpp:374`, `docs/catalog-descriptor-key.md:280-420,456-545`, `src/dmi/storage/capture/clickhouse_lease.py:83-92,198-210` | +| `tla/LeaseLifecycle.tla` | the lease lifecycle *above* that protocol: the lease thread, the quarantine window, the `2 x TTL` latch, the start wait and the spool sweep | `native/csrc/catalog/storage_service.cpp:65-67,102-173,175-205,276-404,437-441,592-632,634-660,662-690,692-741,743-759,782-801`, `catalog_writer.cpp:243-253,268-274,285-293,296-310`, `lease_coordinator.cpp:45-55,57-68,70-81,230-257`, `indexer.cpp:258`, `src/dmi/storage/native_capture.py:270-280,374-378` | +| `z3/clock_skew.py` | two obligations: the two-host derivation behind the fence margin `publish_timeout_ns + clock_skew_ns`, and the default start wait `lease_ttl_s + publish_timeout_s + clock_skew_s` | the SQL at `docs/catalog-descriptor-key.md:352-362` (emitted by `catalog_writer.cpp:583`), the derivation at `:365-372`, the cap at `catalog_writer.cpp:519`; for the start wait, `native_capture.py:366-378`, `storage_service.cpp:662-690`, `lease_coordinator.cpp:148-163,232` | +| `cbmc/payload_ring_span.cpp` | `payload_compute_spans` and its stated precondition: the span arithmetic only, not the ring's publish/consume protocol | `native/csrc/ring/payload_ring.cuh:44-86` | + +All three TLA+ models are written against the **code**, not the prose. Where +the two disagree, the spec follows the code and a comment in the `.tla` says so. + +`LeaseLifecycle.tla` sits on top of `PublisherLease.tla` rather than beside it: +it abstracts `LeaseCoordinator` to its contract (*a claim presenting lease id L +is admitted iff the head row is dead or is L, refused with `kHeld` otherwise, +and may return an unknown outcome*) and models the service around it. That +contract is what `PublisherLease.tla` discharges. See **Limitations**. + +## Getting the tools + +```sh +# TLC -- a single jar, no install +curl -fsSLO https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar + +# Z3 (Python bindings include the solver) +pip install z3-solver + +# CBMC: a release package from github.com/diffblue/cbmc/releases. The .deb +# also unpacks without installing: dpkg -x ubuntu-*-cbmc-*.deb DIR puts the +# binaries in DIR/usr/bin. +``` + +Do not use apt's `cbmc` on Ubuntu 20.04: it is too old for this harness. Take +a release package instead. + +Recorded with TLC 2.19 on Java 21, Z3 4.13 (`z3-solver` 4.13.x) and CBMC 5.95, +and re-run with `specs/check.sh` on a TLC build from 2026-09, Z3 4.15 and CBMC +6.4.1. Any recent version of each should do; nothing here relies on a +version-specific feature. + +## Running the checks + +### All at once + +```sh +TLA2TOOLS_JAR=/path/to/tla2tools.jar CBMC=/path/to/cbmc PYTHON=/path/to/python \ + specs/check.sh +``` + +`check.sh` runs every TLC config not marked manual, `z3/clock_skew.py` and both +CBMC builds, compares each verdict with the one it expects, and exits non-zero +on any mismatch. The expected verdicts are a table at the top of the script +(`specs/check.sh --list`); a `.cfg` without a row, or a row without a `.cfg`, is +an error. `--all` adds the manual configs, which take minutes each: +`PublisherLease.cfg`, `believers`, `holderssafe`, `overrun`, `nonlin_fence`, +`stalepid` and `noovr1`. Arguments that are not options select checks by shell +glob, e.g. `specs/check.sh 'LeaseLifecycle_O3_*' 'cbmc_*'`. TLC runs in a +scratch copy of `specs/tla`, so no `states/` directory or trace file lands in +the tree. `TLC_WORKERS` (default 4) and `TLC_HEAP` (default `4g`) tune TLC, +and `GOTO_CC` overrides the `goto-cc` found next to `$CBMC`. + +The sections below give the commands for running one check by hand. + +### TLA+ + +Every `.cfg` in `specs/tla/` is one model: one set of constants, one invariant. +Run any of them from `specs/tla/`. + +**The allocator configs need `-deadlock` on the command line.** +`VersionAllocator.tla` has no stutter step: once every allocator reaches +`published` there is no next state, and TLC reports `Error: Deadlock reached.` +and stops — on `nocap_distinct` that happens after 97 of the 836 distinct +states, so without the flag the run *looks* clean for two seconds and has +checked almost nothing. `-deadlock` turns deadlock checking off (that is what +the flag does, despite the name), and the run completes. The +`PublisherLease_*` and `LeaseLifecycle_*` configs do not need it: they carry +`CHECK_DEADLOCK FALSE` in the `.cfg` itself. + +```sh +cd specs/tla + +# version allocator -- note -deadlock +java -XX:+UseParallelGC -Xmx3g -cp /path/to/tla2tools.jar tlc2.TLC \ + -workers 4 -deadlock -config lin_distinct.cfg VersionAllocator.tla + +# publisher lease +java -XX:+UseParallelGC -Xmx3g -cp /path/to/tla2tools.jar tlc2.TLC \ + -workers 4 -config PublisherLease_believers.cfg PublisherLease.tla + +# lease lifecycle +java -XX:+UseParallelGC -Xmx6g -cp /path/to/tla2tools.jar tlc2.TLC \ + -workers 4 -config LeaseLifecycle_O3_selflatch.cfg LeaseLifecycle.tla +``` + +`PublisherLease.cfg` is the base model — the protocol exactly as shipped, with +the combined `AllSafety` invariant. Each `PublisherLease_*.cfg` turns a single +knob away from it or swaps in a single invariant; its header comment says which. +`LeaseLifecycle_*.cfg` is grouped by obligation: `O1_*` renewal, `O2_*` +quarantine, `O3_*` the latch, `O4_*` the start wait, `O5_*` the spool sweep, and +`vac_*` the vacuity guards. + +The largest runs (`believers`, `holderssafe`, `overrun`, `nonlin_fence`, +`stalepid`, `noovr1` and `PublisherLease.cfg`) generate 15M-61M states and take +minutes each; `check.sh` runs them only with `--all`. Every `LeaseLifecycle` +run finishes in under two minutes. The rest finish in seconds. + +### Z3 + +```sh +python3 specs/z3/clock_skew.py +``` + +Prints one line per check and exits non-zero if any result differs from the +expected one. Seven checks, no arguments, a couple of seconds. + +### CBMC + +`cbmc` does not accept `-std=`, so the harness is compiled to a goto-binary +with `goto-cc` first and verified in a second step. The file is `.cpp` because +`payload_ring.cuh` uses a namespace; the two CUDA qualifiers are defined away +so the header compiles for the host. + +```sh +cd specs/cbmc +B=$(mktemp -d) # goto-binaries are build output; keep them out of the tree + +# the shipped contract: the documented precondition is assumed +goto-cc -std=c++11 payload_ring_span.cpp -o "$B/span.gb" +cbmc --unwind 80 --unwinding-assertions "$B/span.gb" + +# the same harness with the precondition dropped +goto-cc -std=c++11 -DDROP_PRECONDITION payload_ring_span.cpp -o "$B/span_nopre.gb" +cbmc --unwind 80 --unwinding-assertions --trace "$B/span_nopre.gb" +``` + +## Results + +State counts are TLC's own, as `generated / distinct`. Counterexample lengths, +in parentheses, are the number of states in the trace TLC printed, including +the initial state. + +**State counts for runs that completed are exact and reproducible.** Every +completed `VersionAllocator` and `PublisherLease` run in the tables below +reproduced its previously recorded distinct count to the state when re-run +with `check.sh`. The `LeaseLifecycle` counts were re-recorded after +`NoSelfRefusal` was tightened, which changed the history variable it reads and +so the number of distinct states in several configs; no verdict changed. + +**State counts and trace depths for refuted runs are not reproducible.** TLC +stops as soon as any worker hits the violation, so both the count and the +trace length depend on the worker count and on scheduling. The figures here +were recorded with 2, 4 or 8 workers; `NoOrphanManifestRows` has been seen at both +9 and 14 states on the same config. Only the verdict is stable for a refuted +run, not the number beside it. + +### Version allocator (`VersionAllocator.tla`) + +All configs use `Attempts = 3`, `MaxSpread = 1`. Run with `-deadlock`. + +| Config | Store | Allocators | Invariant | Verdict | States | +|---|---|---|---|---|---| +| `lin_distinct` | linearizable | 3 | `Distinct` | **holds** | 669,421 / 407,083 | +| `nocap3_distinct` | linearizable | 3 | `Distinct` | **holds** | 1,094,245 / 689,368 | +| `nocap3_ceiling` | linearizable | 3 | `CeilingNeverBinds` | **holds** | 1,094,245 / 689,368 | +| `nocap_distinct` | linearizable | 2 | `Distinct` | **holds** | 1,117 / 836 | +| `nocap_ceiling` | linearizable | 2 | `CeilingNeverBinds` | **holds** | 1,117 / 836 | +| `lin_ceiling` | linearizable | 3 | `CeilingNeverBinds` | violated (17) | 39,417 / 23,193 | +| `lin_solerow` | linearizable | 3 | `SoleRow` | violated (6) | 77 / 61 | +| `lin_floor` | linearizable | 3 | `FloorMonotonic` | violated (8) | 597 / 390 | +| `lin_publish` | linearizable | 3 | `NoPublishRefused` | violated (9) | 834 / 531 | +| `lin_budget` | linearizable | 3 | `NoBudgetExhaustion` | violated (17) | 39,376 / 23,154 | +| `nocapf_distinct` | shared stale frontier | 2 | `Distinct` | **holds** | 2,886,043 / 639,601 | +| `nocapf_ceiling` | shared stale frontier | 2 | `CeilingNeverBinds` | **holds** | 2,886,043 / 639,601 | +| `frontier_distinct` | shared stale frontier | 2 | `Distinct` | **holds** | 2,232,679 / 456,499 | +| `ec_distinct` | eventually consistent | 2 | `Distinct` | violated (9) | 1,464 / 724 | +| `nocap_ec` | eventually consistent | 2 | `Distinct` | violated (9) | 782 / 409 | + +`MaxVersion` is a state-space bound, not a quantity in the code, so +`CeilingNeverBinds` probes whether the bound hid behaviour. It binds at +`MaxVersion = 6` (`lin_ceiling`), which is why `nocap3_*` exists: at +`MaxVersion = 18` the ceiling is never reached and `Distinct` holds over a +state space the bound did not truncate. + +`SoleRow`, `FloorMonotonic`, `NoPublishRefused` and `NoBudgetExhaustion` are +refutation targets — claims the allocator is sometimes read as making but does +not make. Their counterexamples are the point, not a defect. + +### Publisher lease (`PublisherLease.tla`) + +Base model: two publishers, `Lids = {1,2,3}`, `MaxTerm = 3`, `MaxTime = 5`, +`MaxVersion = 2`, `MaxAttempts = 2`, `TTL = 2`, `PT = 1`, `SKEW = 0`, +`NumChunks = 1`, linearizable store, cap enforced, writer lock held, fresh +`publish_id`. Each config below differs from it only as its name says. + +| Config | Invariant | Verdict | States | +|---|---|---|---| +| `PublisherLease.cfg` (base) | `AllSafety` | **holds** (its `NoOverlappingAdmit` conjunct vacuously; see below) | 19,807,266 / 9,665,700 | +| `base5` (`MaxTerm 5`, `MaxTime 8`) | `AllSafety` | **holds** | 5,195,821 / 2,408,145 | +| `base5_ovr` (`base5`, `AllowOverrun`) | `NoOverlappingAdmit` | violated (29) | 1,432,673 / 678,409 | +| `believers` | `AtMostOneBeliever` | **holds** | 19,807,266 / 9,665,700 | +| `holderssafe` | `TwoHoldersIsSafe` | **holds** | 19,807,266 / 9,665,700 | +| `holders` | `AtMostOneHolder` | violated (12) | 10,865 / 6,280 | +| `noovr0` (empty refs, cap enforced) | `NoOverlappingAdmit` | **holds** | 1,761,711 / 799,611 | +| `ovr0` (empty refs, `AllowOverrun`) | `NoOverlappingAdmit` | violated (15) | 64,379 / 34,191 | +| `noovr1` (`noovr0` with 1 chunk) | `NoOverlappingAdmit` | **holds** | 15,555,231 / 7,204,077 | +| `ovr1` (`noovr1`, `AllowOverrun`) | `NoOverlappingAdmit` | violated (32) | 4,235,316 / 2,001,749 | +| `overrun` (`AllowOverrun`, 1 chunk) | `NoOverlappingAdmit` | **holds** (vacuously) | 20,855,772 / 9,873,900 | +| `selfrace` (shared writer, no lock) | `WatermarkMonotonic` | violated (29) | 11,890,931 / 6,074,002 | +| `selfracelocked` (shared writer, lock) | `AllSafety` | **holds** | 947,826 / 524,274 | +| `orphans` | `NoOrphanManifestRows` | violated (14) | 43,456 / 23,086 | +| `chunks2_orphans` (2 chunks) | `NoOrphanManifestRows` | violated (14) | 33,994 / 18,091 | +| `chunks2_prefix` (2 chunks) | `OrphansArePrefixes` | **holds** | 1,892,754 / 909,324 | +| `chunks2` (2 chunks) | `AllSafety` | **holds** | 1,892,754 / 909,324 | +| `stalepid` (reused `publish_id`) | `AllSafety` | **holds** | 15,073,338 / 7,368,006 | +| `nonlin_fence` (non-linearizable) | `AtMostOneFenceable` | **holds** | 61,324,208 / 12,215,084 | +| `nonlin_admit` (non-linearizable) | `NoOverlappingAdmit` | violated (27) | 5,093,065 / 1,273,001 | +| `nonlin_all` (non-linearizable) | `AllSafety` | violated (27) | 5,176,956 / 1,293,712 | + +`nonlin_fence` is the one thing that survives a non-linearizable store: at most +one publisher can *pass the fence* at a time even then. What it does not +survive is the admission window — `nonlin_admit` — so the fence being sole does +not make the publish sole. Read the three `nonlin_*` rows together. + +#### Vacuity guards + +Each of these is an invariant we *want* refuted: the counterexample is the proof +that the model reaches the state the safety invariants are quantified over. An +invariant that holds because its subject is unreachable proves nothing. + +| Config | Guard | Refuted at | States | +|---|---|---|---| +| `vac_publish` | `NeverPublishes` | yes (16) | 74,958 / 38,597 | +| `vac_fence` | `NeverFences` | yes (5) | 169 / 98 | +| `vac_admit` | `NeverAdmits` | yes (15) | 49,953 / 26,385 | +| `vac_contested` | `NeverContested` | yes (7) | 745 / 417 | +| `vac_bothadmit` | `NoBelieverDuringAdmit` | yes (20) | 335,283 / 167,905 | +| `vac0` | `NeverAdmits` at the `ovr0` / `noovr0` constants | yes (7) | 763 / 434 | + +`vac0` is the one that matters for reading the table above. At the base +constants, `overrun` reports `NoOverlappingAdmit` as holding — but it holds +**vacuously**: the term budget at `MaxTerm = 3` with a manifest chunk is too +small to reach a takeover at all, so no two watermark statements are ever in +flight to compare. The same goes for the base run itself: `AllSafety` includes +`NoOverlappingAdmit`, so `PublisherLease.cfg` holding says nothing about +overlapping admissions. That does not make its other four conjuncts vacuous, +but it does not show them reached either; the guards above do that for the +publish, fence and admission states. `base5`, `noovr0`, `ovr0`, `noovr1`, `ovr1` and `vac0` exist for that +reason, and each holding run has a partner that differs only in allowing the +statement cap to overrun and is refuted, which proves the takeover is reached +at its constants: + +| Holds (cap enforced) | Refuted (`AllowOverrun`) | Publish | +|---|---|---| +| `base5` (`AllSafety`) | `base5_ovr` | one manifest chunk, `MaxTerm 5` | +| `noovr0` | `ovr0` | empty refs, `MaxTerm 4` | +| `noovr1` | `ovr1` | one manifest chunk, `MaxTerm 4` | + +`vac0` also refutes `NeverAdmits` at the `ovr0`/`noovr0` constants, which proves +admissions are reached there. Those pairs, not the `overrun` row or the base +run, are the evidence about the takeover instant. + +### Lease lifecycle (`LeaseLifecycle.tla`) + +Time is in **ticks** of `TTL/6`, the lease thread's own period +(`storage_service.cpp:65-67`), so `ttl/6`, `ttl/3` and `2*ttl` are all exact +integers. Most configs run one service with `TTL = 6`. + +#### O1 — renewal keeps the lease alive + +| Config | Invariant | Verdict | States | +|---|---|---|---| +| `O1_tries` | `ThreeTriesFit` + `FourTriesFit` | **holds** | 11 / 9 | +| `O1_tries12` (`TTL 12`) | `ThreeTriesFit` + `FourTriesFit` | **holds** | 6 / 6 | +| `O1_tries60` (`TTL 60`) | `ThreeTriesFit` + `FourTriesFit` | **holds** | 6 / 6 | +| `O1_tries5` | `FiveTriesFit` | violated (constant-level) | — | +| `O1_clean` | `NoPhantomLease` | **holds**, if requests are fast (see below) | 206 / 126 | +| `O1_cut` (ClickHouse cut) | `NoPhantomLease` | **holds**, if requests are fast | 7,419 / 3,660 | +| `O1_late` (`MaxLate 1`) | `NoPhantomLease` | **holds**, if requests are fast | 21,085 / 9,276 | +| `O1_slowreq3` (`MaxLate 3`, no cycle) | `NoPhantomLease` | **holds** | 382 / 230 | +| `O1_slowreq` (`MaxLate 4`, no cycle) | `NoPhantomLease` | violated (10) | 450 / 281 | +| `O1_absorb` | `OneFailureAbsorbed` | violated (9) | 314 / 175 | +| `O1_skip` (`AllowSkipPublish`) | `NoPhantomLease` | violated (19) | 479 / 265 | + +**The `O1` HOLDS verdicts assume every lease request completes in about half +the TTL.** The model settles each ClickHouse call in the step that issues it: +`RenewIfDue`, `EnsureLease` and `StartClaim` take zero time. The code does not. +`keep_lease()` holds `lease_mutex_` across `renew_lease()`, which is three +requests (head read, claim `INSERT`, read-back). Each attempt is bounded only +by the client's `request_s` — 60 s by default, against a 15 s default TTL — +and a read that fails transiently is repeated, up to the client's +`max_attempts` (3 by default) attempts in all, so one read can take three +request timeouts plus a short backoff (`clickhouse_client.cpp:484-520`). A +slow request delays every later wake exactly as a late wake does, so +`MaxLate` stands in for it. With no publishes to renew the row +(`CycleOn = FALSE`, the idle service), `NoPhantomLease` holds at +`MaxLate = 3`, half the TTL (`O1_slowreq3`), and falls at `MaxLate = 4` +(`O1_slowreq`): the row expires under a service that still believes it holds +it. So `O1_clean`, `O1_cut` and `O1_late` show the renewal schedule is sound +while requests are fast, not that the lease survives a slow ClickHouse. +Nothing in the code bounds a lease request below half the TTL yet; a +follow-up PR will bound lease request time. + +`O1_tries`, `O1_tries12` and `O1_tries60` (`FourTriesFit` holds at `TTL` 6, 12 +and 60) and `O1_tries5` (`FiveTriesFit` refuted at `TTL` 60) together pin the +tick arithmetic in the comment at `storage_service.cpp:635-638`: with no +`index()` in the way, *"the renewal fires within about a tick of falling due, +leaving at least roughly half the TTL for it to land before the row +expires"*. Exactly **four** lease-thread wakes fall between the instant the +renewal falls due (`last_renew + ttl/3`) and the instant the row dies +(`last_renew + ttl`), at every phase offset: three fit, four fit, five do +not. So the first falls within a tick of due, with more than half the TTL +still to run. (Before #154 the comment said *"which leaves two more tries"*, +three wakes; `ThreeTriesFit` is that claim.) +The arithmetic is correct on the tick grid, and nominal: it assumes every wake +is on time and every renewal completes at once, which `O1_slowreq` shows is +load-bearing, and `last_renew_ns_` is stamped after the round trip returns, +not when the row is written. `FiveTriesFit` is refuted at the constant level — +the arithmetic is decided before any state is explored, so TLC reports no +state count. + +The rest of that comment (`:638-652`) states two caveats. The first is read +from the code and confirmed by `O1_absorb`; the second is a model result: + +* *"Whatever slack is left covers a renewal that runs late, not one that + fails."* A failed renewal costs the lease at once, whatever the cause. A + refusal drops it in the coordinator (`reject_live`, + `lease_coordinator.cpp:236`, or the failed read-back at `:138`). A transport + error, timeout, server error or parse error is a `ClickHouseError` and takes + the `std::exception` path at `catalog_writer.cpp:285-292`, which quarantines + on the *first* error that survives the client's retries (*"a write is + repeated only when its connection was never made; one that may have reached + the server never is"*). No renewal failure is retried under the same lease. + `O1_absorb` is that, refuted as expected. +* The stamp `index_bounded()` puts in `last_renew_ns_` after an `index()` + *"is taken even when every pack was already committed, so index() published + nothing and renewed nothing"*. `O1_skip` shows that is a real defect, not a + modelling artefact. See below. + +**`O1_skip` — a lease can lapse under a service that still believes it holds +it.** `storage_service.cpp:439-441` bumps `last_renew_ns_` when +`indexed_packs > 0 || skipped_packs > 0`, with the comment *"a publish renews +the lease"*. But `indexer.cpp:258` gates the whole publish on +`!all_rows.empty() || !indexed.empty()`: an index pass whose packs were all +already committed returns `skipped_packs > 0` and never calls +`renew_for_publish()`. The bump pushes the next renewal out by `ttl/3` without +anything having touched the row. TLC's shortest trace (19 states), at +`TTL = 6` so `ttl/3 = 2` ticks: + +1. Tick 0. `s1` starts, claims lease 1. Its row expires at tick 6, and + `last_renew_ns_ = 0`, so the renewal falls due at tick 2. +2. Tick 1. The lease thread wakes, finds `1 - 0 < ttl/3`, and returns without + renewing. +3. Tick 2. Before the lease thread wakes, a cycle indexes a batch whose packs + were all already committed. `skipped_packs > 0`, nothing is published, + `last_renew_ns_ := 2`. The lease thread then finds `2 - 2 < ttl/3` and + stands down. The renewal is now not due until tick 4. +4. Tick 3. The lease thread stands down again: `3 - 2 < ttl/3`. +5. Tick 4. Same as tick 2: a second skip-bump lands first, + `last_renew_ns_ := 4`, and the lease thread stands down. The due date moves + to 6. +6. Tick 5. The lease thread stands down: `5 - 4 < ttl/3`. +7. Tick 6. The row, untouched since tick 0, expires. `held_lease() != nullptr` + is still true and `phase = run`, so `NoPhantomLease` falls. + +Because each bump lands at exactly the renewal interval, ahead of the lease +thread's wake in the tick the renewal falls due, the lease thread is starved +indefinitely — it never once reaches its own due test as true. +**Reachability caveat:** this needs skip-only passes landing close enough +together to keep resetting the clock, and no single concrete deployment +scenario chaining them was demonstrated. The state machine reaches it; a +production trace has not been shown. The guard should test `indexed_packs > 0` +alone, or the indexer should report whether it actually published. + +#### O2 — the quarantine window + +| Config | Invariant | Verdict | States | +|---|---|---|---| +| `O2_quar` | `QuarantineOutlastsItsRow` | **holds**, if an unknown outcome lands at once (see below) | 7,419 / 3,660 | +| `O2_skew` (`Skew 1`) | `QuarantineOutlastsItsRow` | violated (27) | 1,948 / 1,049 | +| `O2_reuse` (`ReuseLid`) | `QuarantineOutlastsItsRow` | violated (27) | 1,635 / 851 | +| `O2_selfref` (`Skew 1`) | `NoSelfRefusal` | violated (26) | 2,494 / 1,324 | + +`QuarantineTakesNothing` holds everywhere it is checked: a quarantined writer +takes no claim at all, not even with a fresh `lease_id` +(`storage_service.cpp:698-704`). + +With `Skew = 0` the window at `catalog_writer.cpp:273` does outlast the row it +dropped. With one tick of skew it does not — the window is +`now_monotonic_ns() + lease_ttl_ns` on the **local** steady clock, while the +row's expiry is read from whichever replica answers, which may report it live a +skew later. `O2_reuse` is a counterfactual: presenting the *dropped* lease id +after the window would be worse still, which is why the fresh-id rule at +`lease_coordinator.cpp:45-55` is right. `O2_selfref` is the price of that rule: +`reject_live`'s `claimants == 1` exemption cannot recognise a fresh id, so a +writer can be refused by its own dropped row. + +`NoSelfRefusal` is refuted only by a claim the service actually takes and that +comes back `kHeld` from a head row the service itself wrote (`SelfRefused` in +the `.tla`). A tick on which the service is quarantined, backing off or +holding a lease takes no claim and is never counted. `O2_selfref` runs at +`Skew = 1`; with `Skew = 0` and every other constant the same, the invariant +holds (7,419 / 3,660 states), so in this model a self-refusal needs replica +skew, or a late-landing row the model does not have (see Limitations). + +**`O2_quar` holds only if an outcome-unknown statement lands at once.** When a +request fails with its outcome unknown, the model either drops it or lands its +row at that same instant, expiring a TTL later. Nothing in the code bounds a +later landing: `catalog_writer.cpp:519-520`'s `max_execution_time` covers only +`publish_snapshot`'s statements, and the lease `INSERT` +(`lease_coordinator.cpp:214-227`) carries only the `insert_quorum` settings. A +lease `INSERT` the client gave up on can still land later, and its row then +outlives the quarantine window by as much as it landed late. + +#### O3 — the `2 x TTL` latch + +| Config | Invariant | Verdict | States | +|---|---|---|---| +| `O3_rival` (persistent rival) | `NeverLatches` | violated (70) | 102,421 / 49,985 | +| `O3_rivaljust` | `NoFalsePositiveLatch` | **holds** | 154,642 / 72,699 | +| `O3_stops2` (rival stops < 2 TTL) | `NeverLatches` | **holds** | 290,254 / 137,745 | +| `O3_false` (`Skew 0`) | `NoFalsePositiveLatch` | **holds**, if an unknown outcome lands at once | 290,254 / 137,745 | +| `O3_falsenocut` (`Skew 0`, no cut) | `NoFalsePositiveLatch` | **holds** | 1,743 / 1,166 | +| `O3_selflatch` (`Skew 1`, no rival) | `NoFalsePositiveLatch` | violated (65) | 13,076 / 8,958 | +| `O3_selflatch_latch` (`Skew 1`, no rival) | `NeverLatches` | violated (65) | 17,339 / 11,859 | +| `O3_stops` | `NeverLatches` | **holds** — but see below | 821 / 563 | + +The latch is justified when it is meant to be: a rival that keeps renewing does +latch (`O3_rival`), and it latches *legitimately* — `O3_rivaljust` shows the +rival really did hold a live row at every instant of the window. A rival that +stops inside two TTLs does **not** latch (`O3_stops2`, 137,745 states). With no +skew, no false positive is reachable at all (`O3_false`) — as long as an +outcome-unknown statement lands at the instant it fails, which is the +assumption `O2_quar` rests on too. + +**`O3_selflatch` — the latch fires with no rival in existence.** `Foreign = +FALSE`, `MaxCuts = 0`: no other publisher, no ClickHouse outage, only bounded +request timeouts and `Skew = 1`. The service latches +`"publisher lease held by another publisher for over 2 x TTL"` against itself, +at depth 65 to 70 depending on scheduling. Two independent causes, both +needed: + +1. The quarantine window at `catalog_writer.cpp:273` is measured on the local + steady clock with **no skew allowance**, while the row it dropped is read + from a replica that may still report it live. `204a8d2` gave the start wait + a `+ clock_skew_s` term; the quarantine window did not get one. The writer + therefore comes out of quarantine and is refused by its own corpse. +2. `storage_service.cpp:751` tests `now - held_elsewhere_since_ns_ >= 2 * ttl`, + and `held_elsewhere_since_ns_` is set on the **first** refusal (`:746`) and + cleared only by a **successful** claim (`:728`). The justification written + directly above it at `:748-750` — *"a refusal that has lasted 2 x TTL is a + publisher that means to stay"* — requires an unbroken **run** of refusals. + The code measures elapsed time since the first one instead, and nothing in + between resets it. + +The trace, at `TTL = 6` and `Skew = 1`: + +1. Tick 0. `s1` starts, claims lease 1, sweeps, runs. Its row expires at 7. +2. Tick 2. A renewal returns an unknown outcome. `renew_for_publish` takes the + `std::exception` path and quarantines: lease 1 is dropped locally with no + tombstone, the window is set to `now + ttl` = tick 8. The statement had in + fact landed, so the server row now lives to tick 9. +3. Tick 8. The window ends and `ensure_publisher_lease` claims with a fresh + lease id. The row from step 2 is dead on the true clock at 8 but reads live + on a replica one tick behind, so the claim comes back `kHeld`. + `held_elsewhere_since_ns_ := 8`. **This is the only refusal in the trace.** +4. Tick 9. The row really does expire. The refusal run is broken here + (`runBroken := TRUE`), which is exactly what `NoFalsePositiveLatch` watches. +5. Ticks 9 and 15. Two further acquire attempts return unknown outcomes and + take the `catalog_writer.cpp:296-310` path, quarantining again each time. + Neither is a refusal, and neither is a success — so `:728` never runs and + `held_elsewhere_since_ns_` stays at 8. (The second of these does leave a + live row on the server, expiring at 22.) +6. Tick 21. The last window ends, the claim is refused by that row, and + `21 - 8 = 13 >= 2 * ttl = 12`. `latch_failure` fires with + *"publisher lease held by another publisher for over 2 x TTL"*. + +`Foreign = FALSE` throughout: no other publisher exists in the model. The only +thing that ever held the row was the service itself, and the single refusal it +is latching on happened thirteen ticks earlier and lasted one tick. + +Suggested fixes, one for each: add `clock_skew_ns` to the quarantine window at +`catalog_writer.cpp:273`, matching what the start wait now does; and reset +`held_elsewhere_since_ns_ = 0` whenever a claim is *not* refused with `kHeld` +— on a quarantine, on a transport error, on anything that breaks the run — +rather than only on success. Either one alone kills this trace, and both are +independently wrong, but only the second is robust. The model lands an +outcome-unknown statement at the instant the client gives up on it, and the code +does not bound a later landing: the lease `INSERT` carries no +`max_execution_time` (see `O2`). A row that lands late outlives a skew-padded +window as easily as an unpadded one, so the first fix alone does not close the +self-latch. Resetting `held_elsewhere_since_ns_` does, whatever the row's +lifetime, because the refusal clock then measures an unbroken run. + +#### O4 — the start wait + +| Config | Invariant | Verdict | States | +|---|---|---|---| +| `O4_same` (`PredTTL == TTL`) | `StartAlwaysSucceeds` | **holds** | 98 / 66 | +| `O4_skew` (`Skew 1`) | `StartAlwaysSucceeds` | **holds** | 85 / 59 | +| `O4_bigger` (`PredTTL > TTL + PT`) | `StartAlwaysSucceeds` | violated (16) | 16 / 16 | +| `O4_compose` | `NoConcurrentHolder` | **holds** | 11,635 / 5,769 | + +The start wait composes correctly: `O4_compose` finds no instant at which two +parties both believe they hold the lease. The `O4_same` / `O4_bigger` pair +reproduces, inside the state machine, the threshold the Z3 script proves in the +reals — a predecessor whose TTL exceeds the successor's `ttl + publish_timeout` +outlasts the wait. + +#### O5 — the spool sweep + +| Config | Invariant | Verdict | States | +|---|---|---|---| +| `O5_refused` | `RefusedStartNeverSweeps` | **holds** | 15 / 14 | +| `O5_cosweep` | `SweepOnlyWhenAlone` | violated (22) | 5,747 / 3,418 | + +A start that is refused the catalog never touches the spool — `O5_refused` +holds, which is `test_a_start_refused_the_lease_leaves_the_spool_unswept` +generalised over the model. + +**`O5_cosweep` — two processes sweep one spool at once.** No ClickHouse cut is +needed, and no skew: the config allows one cut (`MaxCuts = 1`), but the trace +below takes none, and the run is refuted just the same with `MaxCuts = 0`; +`Skew = 0`. The trace, at `TTL = 6`: + +1. Tick 0. `s1` starts, claims lease 1 (row expires at tick 6), sweeps the + spool, and enters `run`. It is now the live sink, writing `.open` packs. +2. Tick 0. `s2` starts on the same spool and is refused the lease, so it begins + polling inside `acquire_lease_at_start`. +3. Tick 2. `s1`'s lease thread takes an unknown-outcome error and quarantines. + `quarantine()` discards the lease **without** the release tombstone, so the + server row stays live to its TTL. `s1` does not stop — it is still in + `run`, still holding the spool open. +4. Tick 6. The row expires by itself. `s2`'s next poll succeeds and it takes + lease 2. +5. Tick 6. `s2` proceeds past the lease to `sweep_spool_on_start` and calls + `Recover()`, which deletes every `.open` file it does not own — including + `s1`'s in-progress packs — and records the count in + `state_.swept_on_start` as a success. Both services are now in `run` and + `coSweep` is set: `SweepOnlyWhenAlone` falls at depth 22. + +Nothing reports an error. `s1` keeps writing into files that have been +unlinked, and `s2`'s `swept_on_start` counts a live sink's work as recovered +debris. + +This is not a new discovery so much as the **witness for the comment `204a8d2` +already weakened**. `storage_service.cpp:113-118` now says *"usually"* and +names exactly this gap: *"a holder that is quarantined has let its row lapse, +and a second process can take the lease in that gap"*. That comment is correct. +Since #154 the header says the same. `storage_service.h:104-122` still says +*"It runs after the lease is taken, so a start refused the catalog never +touches the spool"*, which is true of a *refused* start, and now adds that +this *"keeps a second process off a live spool only usually: a holder that +stops renewing for a TTL (quarantined, or stalled) lets its row lapse, and a +second process can take the lease and sweep while the first is still +writing"*. `O5_cosweep` is the quarantined case. The real fix is the spool +owner lock the `.cpp` comment defers. + +#### Vacuity guards + +Every one of these must be refuted, or the run above it proves nothing. + +| Config | Guard | Refuted at | States | +|---|---|---|---| +| `vac_held` | `VacHeld` | yes (2) | 2 / 2 | +| `vac_quar` | `VacQuarantine` | yes (8) | 211 / 126 | +| `vac_recov` | `VacRecovered` | yes (26) | 1,915 / 1,020 | +| `vac_refus` | `VacRefusal` | yes (27) | 2,541 / 1,350 | +| `vac_rival` | `VacRivalHeld` | yes (2) | 182 / 109 | +| `vac_cut` | `VacCut` | yes (2) | 6 / 6 | +| `vac_latch` | `VacLatch` | yes (68) | 104,456 / 50,506 | +| `vac_start` | `VacStartWaited` | yes (2) | 2 / 2 | +| `vac_o4waited` | `VacStartWaited` at the `O4` constants | yes (2) | 2 / 2 | +| `vac_refusedstart` | `StartAlwaysSucceeds` at the `O5_refused` constants | yes (2) | 2 / 2 | +| `vac_stops2refusal` | `VacRefusal` at the `O3_stops2` constants | yes (27) | 5,770 / 3,131 | +| `vac_stops2rival` | `VacRivalHeld` at the `O3_stops2` constants | yes (2) | 186 / 109 | +| `vac_stopsrefusal` | `VacRefusal` at the `O3_stops` constants | **NO — holds** | 821 / 563 | + +`SweepOnlyWhenAlone` is its own vacuity guard: it is refuted, so the co-sweep +state is reachable by construction. No separate guard config is shipped for it. + +**One guard held, and it condemns its own run.** `LeaseLifecycle_O3_stops.cfg` +was the first attempt at *"a rival that stops inside two TTLs does not latch"*, +and it reported `NeverLatches` as holding over 563 states. `vac_stopsrefusal` +shows why: at those constants, with `MaxCuts = 0`, the rival can **never claim +the catalog at all**, so the service is never refused, so of course it never +latches. That run is vacuous and carries no weight. `O3_stops2.cfg` replaces +it — the same claim at constants where the rival does claim, does hold, and +does stop — and is proved non-vacuous by `vac_stops2refusal` and +`vac_stops2rival`. Both configs are kept here so the disclosure is checkable. + +### Z3 — clock skew, two obligations + +| Check | Result | +|---|---| +| real skew `d <= clock_skew_ns` overlaps a holder's admitted statement | `unsat` | +| real skew `d > clock_skew_ns` overlaps | `sat` | +| margin with the `+ clock_skew_ns` term dropped, any `d > 0` | `sat` | +| start wait, predecessor TTL `==` successor TTL | `unsat` | +| start wait, predecessor 30 s vs successor 15 s / 5 s / 0 s | `sat` | +| start wait, `Tp <= Ts + p` (the threshold) | `unsat` | +| start wait, `Tp > Ts + p` (above it) | `sat` | + +`unsat` here is a proof over all timings — for any publish timeout, any +declared bound, any expiry and any schedule — not a sample of one. All +quantities are reals: no discretisation and no bound on the magnitudes. + +The second obligation discharges the change `204a8d2` made at +`native_capture.py:374-378`, which added `+ clock_skew_s` to the default start +wait. The result: **the wait outlasts a crashed predecessor iff +`predecessor_ttl <= successor_ttl + publish_timeout`**, and `clock_skew_s` +cancels out of that condition entirely. It pays for real replica skew exactly +and buys **zero** headroom against a TTL mismatch. + +The config comment at `native_capture.py:270-280` states that threshold: the +default wait *"is guaranteed to outlast a crashed predecessor only when its +TTL is at most lease_ttl_s + publish_timeout_s"*, *"20 s on these defaults"*. +On the shipped Python defaults — `lease_ttl_s = 15`, `publish_timeout_s = 5` — +any predecessor TTL up to **20 s** is outlasted. The native default TTL is +30 s (`catalog_writer.h:34`), which processes predating these knobs used, so a +restart after one of those gives up 10 s early. The script's second start-wait +check pins exactly that case (successor 15 s / 5 s / 0 s, so a 20 s wait +against a 30 s row, 10 s short). Every start-wait check also carries the +successor's own fence margin, +`lease_ttl_s - publish_timeout_s - clock_skew_s >= 0.1 s` +(`native_capture.py:366-372`, `catalog_writer.cpp:148-160`): a successor +outside it is refused at construction and never waits at all. + +The comment also names the skew that matters *at start*: it *"assumes +clock_skew_s bounds the offset between the replica that stamped the +predecessor's row and the one serving the read"*, so between ClickHouse +**replicas**, not between DMI hosts. `reject_live` compares +`head.live_until_ns > head.now_ns` with both sides stamped server-side inside +one query (`lease_coordinator.cpp:148-163,232`), so the successor's own clock +never enters it. + +### CBMC — payload ring spans + +Five assertions over `payload_compute_spans`, for every capacity in `1..64`, +every `head` up to `2^40` and every `nbytes`: + +| Assertion | With the precondition | Without it | +|---|---|---| +| P1 `len1 + len2 == n` | SUCCESS | SUCCESS | +| P2 `off1 + len1 <= cap` | SUCCESS | SUCCESS | +| P3 `off2 + len2 <= cap` | SUCCESS | **FAILURE** | +| P4 spans disjoint | SUCCESS | **FAILURE** | +| P5 no span byte lies in the unconsumed region `[tail, head)` | SUCCESS | **FAILURE** | + +Witness for the P3/P4 failures: `cap = 22`, `head = 15`, `tail = 0` — so seven +bytes are free — and `n = 1152921504606846983`. The second span runs past the +end of the buffer. + +P5 is the property the precondition exists for: a reservation never overwrites +bytes the consumer has not released. It picks any byte of the reservation and +any unconsumed position and asserts that the spans put them at different buffer +offsets. It takes head's offset from `off1`, which both branches of +`payload_compute_spans` set to `head % capacity` on their first line, rather +than recomputing `head % cap`: asking the solver to prove two 64-bit dividers +equal does not finish. P5 therefore checks the span lengths and the wrap point +and trusts that one assignment. With it the proof takes a few seconds. + +## Limitations + +Read this section before quoting any result above. + +**The two-host clock skew is assumed inside the TLA+ models, not verified by +them.** `PublisherLease.tla` runs with `SKEW = 0` and a single server clock +(`now`), and `LeaseLifecycle.tla`'s `Skew` is a whole tick of `TTL/6`, not a +derivation. Both therefore take the skew bound as *given* and check the rest of +the protocol on top of it. The bound itself, and the start-wait obligation, are +closed separately by `z3/clock_skew.py`. The results are independent: the TLA+ +runs do not corroborate the Z3 ones, or the reverse. + +**The catalog tables are always read linearizably in `PublisherLease`, except +where a config says otherwise.** Every deciding read in `PublisherLease.tla` +sees every accepted row whenever `Linearizable = TRUE`, which is every config +except the three `nonlin_*`. That is the single load-bearing assumption of the +safety argument. On a replicated deployment it takes two settings, not one: +`select_sequential_consistency=1` on every deciding read +(`clickhouse_client.cpp:374`) is only the read half, and means something only +if every deciding write waited for the same quorum, which is `insert_quorum` +(`LeaseCoordinator::quorum_write`, `lease_coordinator.cpp:37-43`, and its twin +in `version_allocator.cpp`). `insert_quorum` is optional and unset by default, +so a replicated catalog must set it. The model assumes both are in force; it +does not check either. + +**The non-linearizable store model is a generous over-approximation.** With +`Linearizable = FALSE` a deciding read may observe any subset of the in-flight +inserts on top of what has replicated. Real ClickHouse replicas are not that +adversarial. The `nonlin_*` counterexamples are therefore "this is what you are +exposed to if the setting is not in force", not "this exact interleaving will +occur". Their value is the shape of the failure and which obligations fall, not +a probability. + +**`LeaseLifecycle` settles every ClickHouse call in zero time, so its `O1` +HOLDS verdicts assume each lease request completes in about half the TTL.** +`RenewIfDue`, `EnsureLease` and `StartClaim` issue and settle a request in one +step. In the code `keep_lease()` holds `lease_mutex_` across `renew_lease()`, +three requests, each attempt bounded only by `request_s` (60 s by default, +against a 15 s TTL), and a read that fails transiently is repeated, up to +`max_attempts` (3 by default) attempts in all. `O1_slowreq3` / `O1_slowreq` +put the threshold at half the TTL for the idle service: `NoPhantomLease` holds +at `MaxLate = 3` and falls at 4. Nothing in the code bounds lease requests +that tightly yet; a follow-up PR will bound lease request time. See the `O1` +section. + +**An outcome-unknown statement lands at once or never.** The model's "landed" +branch stamps the row at the instant the client sees the failure. The code +bounds nothing later: `catalog_writer.cpp:519-520`'s `max_execution_time` is +set only on `publish_snapshot`'s statements, and the lease `INSERT` +(`lease_coordinator.cpp:214-227`) carries only the `insert_quorum` settings. A +lease row that lands late outlives the quarantine window by as much. `O2_quar` +and `O3_false` hold only under this assumption, and of the two fixes suggested +under `O3`, adding `clock_skew_ns` to the quarantine window is insufficient on +its own; resetting `held_elsewhere_since_ns_` whenever a run of refusals breaks +is the robust one. + +**`LeaseLifecycle`'s skew runs one way.** Every live row is seen `Skew` ticks +longer than its true expiry (`hExp` adds `Skew`), as if every read went to a +replica lagging by the full bound. A replica that reports a row dead early, or +successive reads that disagree in opposite directions, are not modelled. + +**`Stop` is never enabled in `LeaseLifecycle`.** Every shipped config sets +`AllowStop = FALSE`, so no verdict depends on it. Its tombstone also differs +from the code's: the model overwrites the head's expiry with `now`, instantly +and as seen by every replica, and only while ClickHouse is up; the code inserts +a separate tombstone row (`lease_coordinator.cpp:70-90`) that can fail, be read +through a lagging replica, or land with an unknown outcome. + +**Each allocator in `VersionAllocator` allocates once.** An allocator runs one +`allocate_version()` call to `done`, `published`, `refused` or `failed` and +stops, so the model says nothing about successive calls from one process, and +it has no cross-call monotonicity invariant (that a process's second version +exceeds its first). `FloorMonotonic` compares a returned version with the +watermark at that moment, not with the same process's earlier versions. + +**The ring check is span arithmetic only.** `payload_ring_span.cpp` checks +`payload_compute_spans` against its precondition; the ring's publish/consume +protocol (ready words, the head and tail atomics, their memory ordering, the +CUDA side) is not modelled. P5 takes head's buffer offset from `off1` rather +than recomputing `head % cap` (see the CBMC section). + +**`LeaseLifecycle` abstracts `LeaseCoordinator` to its contract, so every +HOLDS verdict in its tables is conditional on `PublisherLease.tla` discharging +that contract.** A contested head — two rows at one term, +`lease_coordinator.cpp:237-246` — is not modelled. It can only *add* `kHeld` +refusals, so the refutations (`O1_skip`, `O2_*`, `O3_selflatch*`, `O5_cosweep`) +survive under it; the HOLDS verdicts do not stand on their own. Read them as +"holds, given the coordinator behaves as `PublisherLease.tla` says it does". + +**`LeaseLifecycle`'s `ttl/6` time grain cannot see a sub-tick race.** One tick +is the lease thread's own period, which makes `ttl/6`, `ttl/3` and `2*ttl` +exact, but anything finer than a sixth of the TTL is invisible to it. The real +start poll is `ttl/10` clamped to 50-500 ms — *finer* than one tick — so a +start the model reports as refused purely at an expiry boundary would be +retried sooner in reality. In the other direction, `MaxLate = 0` means the +lease thread wakes exactly on its tick; real OS scheduling and slow requests +can only make it later, which strictly reduces the number of renewal attempts +in the window. `O1_late` runs `MaxLate = 1`, and `O1_slowreq3` / `O1_slowreq` +find where lateness breaks `O1` (see the zero-time limitation above). + +**Counts and trace depths for REFUTED runs are scheduling-dependent; counts +for completed runs are exact.** Stated again here because it is the most +commonly misread number in the tables. A refuted run's count tells you nothing +reproducible. A completed run's count does, and every completed run above +reproduced its recorded figure exactly when re-run with `check.sh` (the +`LeaseLifecycle` ones since `NoSelfRefusal` was tightened). + +**`overrun` holding at the base constants proves nothing.** See the vacuity +note in the `PublisherLease` section: at `MaxTerm = 3` the takeover race is out +of budget, so the obligation holds because its subject is unreachable, and +the same goes for the base run's `AllSafety`. The `base5` / `base5_ovr`, +`noovr0` / `ovr0` and `noovr1` / `ovr1` pairs carry that claim. The same trap +caught `LeaseLifecycle_O3_stops`, disclosed above. + +**Every result is bounded.** TLC explores the state space cut off by the +constants in each `.cfg` — at most three lease ids, five or eight time steps, +two manifest chunks, two or three concurrent actors, twenty-four ticks of lease +lifetime. An invariant reported as holding holds *within that bound*. +`CeilingNeverBinds` and the vacuity guards probe whether a specific bound hid +behaviour; they do not turn a bounded check into a proof. CBMC's result is +likewise bounded at capacity 64 and `head < 2^40`. Only the Z3 results are +unbounded. + +**Two or three actors, not N.** The TLA+ models run with one to three +concurrent processes. A protocol bug that needs four simultaneous claimants +would not be found. + +**Liveness is not modelled.** Every invariant here is a safety property. The +specs say nothing about a publisher making progress, and the contested-head +quarantine — a deliberate liveness cost — is not measured. `NeverLatches` is a +safety invariant about a latch being *reachable*, not a claim about recovery. + +**The specs model the code as of the revision they were written against.** +They are not regenerated from the source and nothing checks that they still +match it. Re-read the `.tla` header comments against the cited lines before +trusting a result after the catalog code changes. diff --git a/specs/cbmc/payload_ring_span.cpp b/specs/cbmc/payload_ring_span.cpp new file mode 100644 index 000000000..0dcbef0ae --- /dev/null +++ b/specs/cbmc/payload_ring_span.cpp @@ -0,0 +1,70 @@ +// Bounded proof of the payload ring's two-span arithmetic. +// +// Source of truth: native/csrc/ring/payload_ring.cuh:44-86 +// payload_free_bytes(head, tail, capacity) :49-53 +// payload_compute_spans(head, capacity, nbytes) :66-86 +// +// The header states one precondition at :59-60: +// payload_free_bytes(head, tail, capacity) >= nbytes +// and one producer-side invariant at :46-47: +// head - tail <= capacity +// +// Build it twice -- with the precondition and with -DDROP_PRECONDITION -- to +// see whether the precondition is load-bearing or merely defensive. See +// specs/README.md for the exact goto-cc / cbmc invocations. +// +// The file is C++ (.cpp) because payload_ring.cuh uses a namespace; the two +// CUDA qualifiers are defined away so the same header compiles for the host. + +#define __host__ +#define __device__ +#include "../../native/csrc/ring/payload_ring.cuh" +#include + +int main() { + uint64_t cap, head, tail, n; + + // Capacity is bounded only to keep the proof bounded; every capacity in + // 1..64 is covered, wrap and non-wrap alike. + __CPROVER_assume(cap >= 1 && cap <= 64); + + // The producer-side ring invariant (payload_ring.cuh:46-47). + __CPROVER_assume(head >= tail); + __CPROVER_assume(head - tail <= cap); + + // head is otherwise unconstrained up to 2^40, so `head % capacity` takes + // every residue at an arbitrary number of wraps, not just the first lap. + __CPROVER_assume(head <= (uint64_t)1 << 40); + +#ifndef DROP_PRECONDITION + // The documented precondition (payload_ring.cuh:59-60). + __CPROVER_assume(n <= ring::payload_free_bytes(head, tail, cap)); +#endif + + ring::TwoSpan s = ring::payload_compute_spans(head, cap, n); + + assert(s.len1 + s.len2 == n); // P1 spans cover the request + assert(s.off1 + s.len1 <= cap); // P2 span 1 stays in the buffer + assert(s.off2 + s.len2 <= cap); // P3 span 2 stays in the buffer + assert(s.len2 == 0 || s.off2 + s.len2 <= s.off1); // P4 the two spans are disjoint + + // P5 no byte the spans cover lies in the unconsumed region [tail, head). + // Pick any byte i of the reservation and any unconsumed position j; the + // buffer offset the spans give byte i is not the one j occupies. j's + // offset is found by stepping back head - j (1..cap, by the ring + // invariant) from head's own offset, taken as s.off1: both branches of + // payload_compute_spans set off1 = head % capacity on their first line. + // Recomputing head % cap here instead would ask the solver to prove two + // 64-bit dividers equal, which does not finish; P5 therefore checks the + // lengths and the wrap point, and trusts that one assignment. + uint64_t i, j; + __CPROVER_assume(i < n); + __CPROVER_assume(tail <= j && j < head); + const uint64_t back = head - j; // 1..cap + const uint64_t j_off = back <= s.off1 ? s.off1 - back + : s.off1 + cap - back; + const uint64_t written = i < s.len1 ? s.off1 + i : s.off2 + (i - s.len1); + assert(written != j_off); // P5 spans avoid unconsumed bytes + + return 0; +} diff --git a/specs/check.sh b/specs/check.sh new file mode 100755 index 000000000..751b508cc --- /dev/null +++ b/specs/check.sh @@ -0,0 +1,304 @@ +#!/usr/bin/env bash +# Run the spec checks and compare every verdict with the expected one. +# +# specs/check.sh the fast set: every config not marked manual, +# plus z3/clock_skew.py and the CBMC harness +# specs/check.sh --all the manual (multi-minute) configs as well +# specs/check.sh PATTERN... only the checks whose name matches a +# shell glob, e.g. 'LeaseLifecycle_O3_*' cbmc +# specs/check.sh --list print the expected-verdict table and exit +# +# Exits 0 when every verdict matches, 1 on any mismatch, 2 when a tool is +# missing or the table and specs/tla/ disagree. +# +# Tools, located through the environment: +# TLA2TOOLS_JAR path to tla2tools.jar (required for the TLA+ checks) +# JAVA java binary (default: java) +# CBMC cbmc binary (default: cbmc) +# GOTO_CC goto-cc binary (default: goto-cc next to +# $CBMC, else on PATH) +# PYTHON a Python with z3-solver (default: python3) +# TLC_WORKERS TLC worker threads (default: 4) +# TLC_HEAP JVM heap for TLC (default: 4g) +# +# TLC runs in a scratch copy of specs/tla, so no states/ directory or trace +# file lands in the tree. The scratch directory is removed on success and +# kept, with every log, when something does not match. +set -uo pipefail + +SPECS=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) + +# name expected set +# expected: holds | violated +# set: fast | manual (manual: minutes each; run with --all) +EXPECTED=$(cat <<'EOF' +lin_distinct holds fast +nocap3_distinct holds fast +nocap3_ceiling holds fast +nocap_distinct holds fast +nocap_ceiling holds fast +lin_ceiling violated fast +lin_solerow violated fast +lin_floor violated fast +lin_publish violated fast +lin_budget violated fast +nocapf_distinct holds fast +nocapf_ceiling holds fast +frontier_distinct holds fast +ec_distinct violated fast +nocap_ec violated fast +PublisherLease holds manual +PublisherLease_base5 holds fast +PublisherLease_base5_ovr violated fast +PublisherLease_believers holds manual +PublisherLease_holderssafe holds manual +PublisherLease_holders violated fast +PublisherLease_noovr0 holds fast +PublisherLease_ovr0 violated fast +PublisherLease_noovr1 holds manual +PublisherLease_ovr1 violated fast +PublisherLease_overrun holds manual +PublisherLease_selfrace violated fast +PublisherLease_selfracelocked holds fast +PublisherLease_orphans violated fast +PublisherLease_chunks2_orphans violated fast +PublisherLease_chunks2_prefix holds fast +PublisherLease_chunks2 holds fast +PublisherLease_stalepid holds manual +PublisherLease_nonlin_fence holds manual +PublisherLease_nonlin_admit violated fast +PublisherLease_nonlin_all violated fast +PublisherLease_vac_publish violated fast +PublisherLease_vac_fence violated fast +PublisherLease_vac_admit violated fast +PublisherLease_vac_contested violated fast +PublisherLease_vac_bothadmit violated fast +PublisherLease_vac0 violated fast +LeaseLifecycle_O1_tries holds fast +LeaseLifecycle_O1_tries12 holds fast +LeaseLifecycle_O1_tries60 holds fast +LeaseLifecycle_O1_tries5 violated fast +LeaseLifecycle_O1_clean holds fast +LeaseLifecycle_O1_cut holds fast +LeaseLifecycle_O1_late holds fast +LeaseLifecycle_O1_slowreq3 holds fast +LeaseLifecycle_O1_slowreq violated fast +LeaseLifecycle_O1_absorb violated fast +LeaseLifecycle_O1_skip violated fast +LeaseLifecycle_O2_quar holds fast +LeaseLifecycle_O2_skew violated fast +LeaseLifecycle_O2_reuse violated fast +LeaseLifecycle_O2_selfref violated fast +LeaseLifecycle_O3_rival violated fast +LeaseLifecycle_O3_rivaljust holds fast +LeaseLifecycle_O3_stops2 holds fast +LeaseLifecycle_O3_false holds fast +LeaseLifecycle_O3_falsenocut holds fast +LeaseLifecycle_O3_selflatch violated fast +LeaseLifecycle_O3_selflatch_latch violated fast +LeaseLifecycle_O3_stops holds fast +LeaseLifecycle_O4_same holds fast +LeaseLifecycle_O4_skew holds fast +LeaseLifecycle_O4_bigger violated fast +LeaseLifecycle_O4_compose holds fast +LeaseLifecycle_O5_refused holds fast +LeaseLifecycle_O5_cosweep violated fast +LeaseLifecycle_vac_held violated fast +LeaseLifecycle_vac_quar violated fast +LeaseLifecycle_vac_recov violated fast +LeaseLifecycle_vac_refus violated fast +LeaseLifecycle_vac_rival violated fast +LeaseLifecycle_vac_cut violated fast +LeaseLifecycle_vac_latch violated fast +LeaseLifecycle_vac_start violated fast +LeaseLifecycle_vac_o4waited violated fast +LeaseLifecycle_vac_refusedstart violated fast +LeaseLifecycle_vac_stops2refusal violated fast +LeaseLifecycle_vac_stops2rival violated fast +LeaseLifecycle_vac_stopsrefusal holds fast +z3_clock_skew as-expected fast +cbmc_span SSSSS fast +cbmc_span_noprecondition SSFFF fast +EOF +) +# The two cbmc rows give the expected result of assertions P1..P5 in order, +# S for SUCCESS and F for FAILURE. + +die() { echo "check.sh: $*" >&2; exit 2; } + +ALL=0 +LIST=0 +PATTERNS=() +for arg in "$@"; do + case "$arg" in + --all) ALL=1 ;; + --list) LIST=1 ;; + -h|--help) sed -n '2,/^set -uo/p' "$0" | sed '$d; s/^# \{0,1\}//'; exit 0 ;; + -*) die "unknown option: $arg" ;; + *) PATTERNS+=("$arg") ;; + esac +done + +if [[ $LIST -eq 1 ]]; then + echo "$EXPECTED" + exit 0 +fi + +# Every .cfg must have a row, and every TLA+ row a .cfg, or the table has +# drifted from the directory. +table_names=$(awk '{print $1}' <<<"$EXPECTED") +drift=0 +for cfg in "$SPECS"/tla/*.cfg; do + name=$(basename "$cfg" .cfg) + grep -qx "$name" <<<"$table_names" || { echo "no expected verdict for tla/$name.cfg" >&2; drift=1; } +done +while read -r name _; do + case "$name" in z3_*|cbmc_*) continue ;; esac + [[ -f "$SPECS/tla/$name.cfg" ]] || { echo "table row $name has no tla/$name.cfg" >&2; drift=1; } +done <<<"$EXPECTED" +[[ $drift -eq 0 ]] || die "the expected-verdict table and specs/tla/ disagree" + +selected() { # name set + local name=$1 set=$2 + if [[ ${#PATTERNS[@]} -gt 0 ]]; then + local p + for p in "${PATTERNS[@]}"; do + # shellcheck disable=SC2053 + [[ $name == $p ]] && return 0 + done + return 1 + fi + [[ $set == fast || $ALL -eq 1 ]] +} + +# Work out which tools the selected checks need, and fail early and clearly. +need_tlc=0 need_z3=0 need_cbmc=0 +while read -r name _ set; do + selected "$name" "$set" || continue + case "$name" in + z3_*) need_z3=1 ;; + cbmc_*) need_cbmc=1 ;; + *) need_tlc=1 ;; + esac +done <<<"$EXPECTED" +[[ $need_tlc$need_z3$need_cbmc != 000 ]] || die "no check matches: ${PATTERNS[*]}" + +JAVA=${JAVA:-java} +PYTHON=${PYTHON:-python3} +CBMC=${CBMC:-cbmc} +WORKERS=${TLC_WORKERS:-4} +HEAP=${TLC_HEAP:-4g} + +if [[ $need_tlc -eq 1 ]]; then + [[ -n ${TLA2TOOLS_JAR:-} ]] || die "set TLA2TOOLS_JAR to the path of tla2tools.jar (see specs/README.md, Getting the tools)" + [[ -f $TLA2TOOLS_JAR ]] || die "TLA2TOOLS_JAR=$TLA2TOOLS_JAR does not exist" + command -v "$JAVA" >/dev/null || die "java not found (set JAVA to a Java 11+ binary)" +fi +if [[ $need_z3 -eq 1 ]]; then + command -v "$PYTHON" >/dev/null || die "PYTHON=$PYTHON not found" + "$PYTHON" -c 'import z3' 2>/dev/null || die "PYTHON=$PYTHON cannot import z3 (pip install z3-solver, or point PYTHON at a Python that has it)" +fi +if [[ $need_cbmc -eq 1 ]]; then + command -v "$CBMC" >/dev/null || die "cbmc not found (set CBMC to the cbmc binary; apt's cbmc on Ubuntu 20.04 is too old, see specs/README.md)" + CBMC=$(command -v "$CBMC") + if [[ -z ${GOTO_CC:-} ]]; then + if [[ -x $(dirname "$CBMC")/goto-cc ]]; then GOTO_CC=$(dirname "$CBMC")/goto-cc; else GOTO_CC=goto-cc; fi + fi + command -v "$GOTO_CC" >/dev/null || die "goto-cc not found (set GOTO_CC; it ships with cbmc)" +fi + +WORK=$(mktemp -d "${TMPDIR:-/tmp}/dmi-specs-check.XXXXXX") +mkdir -p "$WORK/tla" "$WORK/logs" "$WORK/states" "$WORK/cbmc" +cp "$SPECS"/tla/*.tla "$SPECS"/tla/*.cfg "$WORK/tla/" + +pass=0 fail=0 +FAILED=() + +report() { # status name expected got detail + printf '%-4s %-36s expected %-11s got %-11s %s\n' "$1" "$2" "$3" "$4" "$5" + if [[ $1 == PASS ]]; then pass=$((pass + 1)); else fail=$((fail + 1)); FAILED+=("$2"); fi +} + +run_tlc() { # name expected + local name=$1 expected=$2 module extra=() log got detail start secs + case "$name" in + LeaseLifecycle_*) module=LeaseLifecycle.tla ;; + PublisherLease*) module=PublisherLease.tla ;; + *) module=VersionAllocator.tla; extra=(-deadlock) ;; # no stutter step + esac + log="$WORK/logs/$name.log" + start=$(date +%s) + (cd "$WORK/tla" && "$JAVA" -XX:+UseParallelGC "-Xmx$HEAP" -cp "$TLA2TOOLS_JAR" tlc2.TLC \ + -workers "$WORKERS" "${extra[@]}" -metadir "$WORK/states/$name" \ + -config "$name.cfg" "$module") "$log" 2>&1 + secs=$(( $(date +%s) - start )) + if grep -q '^Model checking completed. No error has been found.' "$log"; then + got=holds + elif grep -qE '^Error: Invariant .* is violated|^Error: The invariant of .* is equal to FALSE' "$log"; then + got=violated + else + got=error + fi + detail=$(grep -oE '^[0-9]+ states generated, [0-9]+ distinct states found' "$log" | tail -1 \ + | sed -E 's/ states generated, / \/ /; s/ distinct states found//') + detail="${detail:-no state count}, ${secs}s" + if [[ $got == violated ]]; then + # Which invariant fell, and the trace length TLC printed (states, + # including the initial one). Both vary with scheduling; see README. + local inv depth + inv=$(grep -oE '^Error: (Invariant [^ ]+ is violated|The invariant of [^ ]+ is equal to FALSE)' "$log" \ + | head -1 | sed -E 's/^Error: (Invariant |The invariant of )//; s/ is .*//') + depth=$(grep -oE '^State [0-9]+:' "$log" | tail -1 | grep -oE '[0-9]+') + detail="$inv${depth:+ at depth $depth}; $detail" + fi + if [[ $got == "$expected" ]]; then report PASS "$name" "$expected" "$got" "($detail)" + else report FAIL "$name" "$expected" "$got" "($detail; log: $log)"; fi +} + +run_z3() { # name expected + local log="$WORK/logs/$1.log" got + if "$PYTHON" "$SPECS/z3/clock_skew.py" "$log" 2>&1; then got=as-expected; else got=mismatch; fi + local n + n=$(grep -cE ' OK$' "$log") + if [[ $got == "$2" ]]; then report PASS "$1" "$2" "$got" "($n checks)" + else report FAIL "$1" "$2" "$got" "(log: $log)"; fi +} + +run_cbmc() { # name expected + local name=$1 expected=$2 defs=() gb log got + [[ $name == *_noprecondition ]] && defs=(-DDROP_PRECONDITION) + gb="$WORK/cbmc/$name.gb" + log="$WORK/logs/$name.log" + if ! "$GOTO_CC" -std=c++11 "${defs[@]}" "$SPECS/cbmc/payload_ring_span.cpp" -o "$gb" "$log" 2>&1; then + report FAIL "$name" "$expected" "build-error" "(log: $log)"; return + fi + "$CBMC" --unwind 80 --unwinding-assertions "$gb" >"$log" 2>&1 + # [main.assertion.N] ... : SUCCESS|FAILURE, in assertion order. + got=$(grep -E '^\[main\.assertion\.[0-9]+\]' "$log" \ + | sed -E 's/^\[main\.assertion\.([0-9]+)\].*: (SUCCESS|FAILURE)$/\1 \2/' \ + | sort -n | awk '{printf "%s", substr($2, 1, 1)}') + if [[ $got == "$expected" ]]; then report PASS "$name" "$expected" "$got" "(P1..P5)" + else report FAIL "$name" "$expected" "${got:-error}" "(log: $log)"; fi +} + +while read -r name expected set; do + selected "$name" "$set" || continue + case "$name" in + z3_*) run_z3 "$name" "$expected" ;; + cbmc_*) run_cbmc "$name" "$expected" ;; + *) run_tlc "$name" "$expected" ;; + esac +done <<<"$EXPECTED" + +echo +echo "$pass passed, $fail failed" +if [[ $fail -gt 0 ]]; then + echo "mismatched: ${FAILED[*]}" + echo "logs kept in $WORK/logs" + exit 1 +fi +rm -rf "$WORK" +if [[ ${#PATTERNS[@]} -eq 0 && $ALL -eq 0 ]]; then + echo "manual configs not run (use --all):" $(awk '$3 == "manual" {print $1}' <<<"$EXPECTED") +fi +exit 0 diff --git a/specs/tla/LeaseLifecycle.tla b/specs/tla/LeaseLifecycle.tla new file mode 100644 index 000000000..8e612debe --- /dev/null +++ b/specs/tla/LeaseLifecycle.tla @@ -0,0 +1,688 @@ +--------------------------- MODULE LeaseLifecycle --------------------------- +(***************************************************************************) +(* The LEASE LIFECYCLE LAYER of *) +(* native/csrc/catalog/storage_service.cpp *) +(* on projectdmx/dmi main @ 99ee4ae (803 lines). *) +(* *) +(* SCOPE. This models the SERVICE's lease lifecycle -- the lease thread, *) +(* the quarantine window, the 2 x TTL latch, the start wait and the spool *) +(* sweep -- NOT the claim/read-back protocol underneath it. The *) +(* LeaseCoordinator is abstracted to its CONTRACT: *) +(* *) +(* a claim presenting lease id L is ADMITTED iff the head row is dead *) +(* or the head row IS L (lease_coordinator.cpp:230-257 reject_live), *) +(* REFUSED with kHeld otherwise, and may return an UNKNOWN outcome *) +(* when the request cannot be completed. *) +(* *) +(* That contract -- three round trips, contested heads, the fence, the *) +(* tombstone, replica staleness -- is discharged by PublisherLease.tla in *) +(* this directory. Anything this module says about the coordinator is *) +(* only as strong as that discharge; see LIMITS at the foot of the file. *) +(* *) +(* SOURCE LINES (99ee4ae). Every action names the code it stands for. *) +(* storage_service.cpp *) +(* :65-67 lease_tick_ns = max(ttl/6, 10ms) -> Tick *) +(* :102-173 start() schema, lease, sweep, reconcile *) +(* :119-133 the spool sweep, AFTER the lease *) +(* :175-205 stop() release only if a lease is held *) +(* :276-404 run_cycle() ensure_publisher_lease at :284 *) +(* :437-441 "a publish renews the lease" *) +(* :592-632 keep_lease() the lease thread *) +(* :634-660 renew_lease_if_due() *) +(* :662-690 acquire_lease_at_start() *) +(* :692-741 ensure_publisher_lease() *) +(* :743-759 lease_held_elsewhere() the 2 x TTL latch *) +(* :782-801 latch_failure() permanent *) +(* catalog_writer.cpp *) +(* :243-253 quarantine_in_force() now < quarantine_until *) +(* :268-274 quarantine() drop the lease, window = now + lease_ttl *) +(* :285-293 renew_for_publish() std::exception -> quarantine() *) +(* :296-310 acquire_lease() std::exception -> quarantine() *) +(* lease_coordinator.cpp *) +(* :45-55 acquire() reuses the HELD lease_id, else mints a fresh one *) +(* :57-68 renew() always presents the held lease_id *) +(* :70-81 release() the tombstone: expiry := now *) +(* :230-257 reject_live() *) +(* indexer.cpp:258 "if (!all_rows.empty() || !indexed.empty())" -- the *) +(* publish is SKIPPED when every pack was already *) +(* committed, yet storage_service.cpp:439 still treats *) +(* skipped_packs > 0 as "a publish renews the lease". *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS + Services, \* the CaptureStorageService instances + TTL, \* writer.lease_ttl_ns, in TICKS. 6 keeps ttl/6 and + \* ttl/3 exact integers, which is what the code divides by + PT, \* publish_timeout_ns: the statement cap + Skew, \* clock_skew: ticks of extra life a row is seen to have + \* on a LAGGING replica (lease_coordinator.cpp:232) + PredTTL, \* the TTL a crashed PREDECESSOR ran with. The config + \* comment (native_capture.py:271-280) says one above + \* lease_ttl + publish_timeout outlasts the default wait + StartWait, \* start_lease_wait_ns (storage_service.cpp:667) + MaxTime, + MaxLate, \* ticks of OS lateness allowed on a lease-thread wake + Foreign, \* TRUE: a rival publisher may claim the catalog + ForeignStops, \* TRUE: the rival may stop, releasing with a tombstone + ForeignBudget, \* how many times the rival may take the catalog + ForeignStopBy, \* the rival renews only while now < this (so a + \* "rival that stops within two TTLs" can be pinned) + MaxCuts, \* how many ClickHouse cut/restore pairs are allowed + AllowUnknown, \* TRUE: a write to a LIVE ClickHouse may time out with + \* its outcome unknown (the client's bounded timeouts) + AllowSkipPublish, \* TRUE: model indexer.cpp:258 -- an index pass whose + \* packs were all already committed returns + \* skipped_packs > 0 WITHOUT publishing, while + \* storage_service.cpp:439-441 bumps last_renew_ns_ anyway + ReuseLid, \* COUNTERFACTUAL for obligation 2: TRUE makes a + \* post-quarantine acquire present the DROPPED lease_id + \* instead of a fresh one + CycleOn, \* TRUE: model run_cycle()'s ensure_publisher_lease (:284) + PredHolds, \* TRUE: a crashed predecessor's row is live at Init + AllowStop, \* TRUE: a service may call stop() + MaxReacq \* cap on the re-acquisition counter (a state bound only) + +VARIABLES + now, chUp, cuts, + hOwner, hLid, hExp, lidGen, \* the lease table HEAD (abstracted) + held, myLid, qUntil, lastRenew, \* per service: the writer's lease state + heSince, nextClaim, \* held_elsewhere_since_ns_, next_claim_ns_ + wake, cwake, phase, swept, reacq, dropped, + runBroken, startWaited, selfRef, coSweep, \* history variables + fWake, fLid, fBudget, fHeld \* the rival publisher + +envVars == <> +headVars == <> +locVars == <> +resVars == <> +rivVars == <> +vars == <> + +----------------------------------------------------------------------------- +(* Derived constants, exactly as the code computes them. *) + +\* storage_service.cpp:65-67 lease_tick_ns(ttl) = max(ttl/6, 10ms). The +\* 10 ms floor only bites for a TTL under 60 ms, which the writer's own +\* config precondition (catalog_writer.cpp:148-160) already forbids. +Tick == IF TTL \div 6 > 0 THEN TTL \div 6 ELSE 1 +DueAfter == TTL \div 3 \* storage_service.cpp:654 +LatchWin == 2 * TTL \* storage_service.cpp:751 +\* storage_service.cpp:668-669 clamp(ttl/10, 50ms, 500ms). One tick is the +\* finest grain this model has and is COARSER than the real poll, so the +\* model can only under-report how promptly a start wait notices an expiry. +StartPoll == 1 + +Owners == Services \cup {"none", "F", "P"} +Never == MaxTime + 99 \* a wake time that never arrives + +----------------------------------------------------------------------------- +(* The abstracted LeaseCoordinator. *) +(* hExp already carries Skew: a row written at t is SEEN as live until *) +(* t + TTL + Skew by a replica lagging by Skew. A tombstone *) +(* (lease_coordinator.cpp:83-89) reads its own expiry and now_ns from the *) +(* same replica, so it is dead at once and carries no Skew. *) +HeadLive == now < hExp + +\* lease_coordinator.cpp:230-257. claimants is always 1 here: a contested +\* head (two rows at one term) is PublisherLease.tla's obligation, and it +\* can only ADD refusals, never remove them. +Admits(lid) == (~HeadLive) \/ (hLid = lid) +ForeignLive == (hOwner = "F") /\ HeadLive +Quarantined(s) == now < qUntil[s] \* catalog_writer.cpp:245 + +CanOk(lid) == chUp /\ Admits(lid) +CanRefused(lid) == chUp /\ ~Admits(lid) +CanUnknown == (~chUp) \/ AllowUnknown +CanLand(lid) == chUp /\ AllowUnknown /\ Admits(lid) + +\* storage_service.cpp:743-759, in the code's own evaluation order: :746 +\* sets held_elsewhere_since_ns_ to now when it was 0, and only THEN does +\* :751 compare, so the FIRST refusal in a run never latches. +NewSince(s) == IF heSince[s] = 0 THEN now ELSE heSince[s] +LatchNow(s) == now - NewSince(s) >= LatchWin + +----------------------------------------------------------------------------- +Init == + /\ now = 0 /\ chUp = TRUE /\ cuts = 0 /\ lidGen = 1 + \* A crashed predecessor that ran with PredTTL and was renewed at t = 0: + \* its row stays live with no tombstone (storage_service.cpp:186-188 -- a + \* killed or quarantined holder writes none). + /\ hOwner = IF PredHolds THEN "P" ELSE "none" + /\ hLid = 0 + /\ hExp = IF PredHolds THEN PredTTL + Skew ELSE 0 + /\ held = [s \in Services |-> FALSE] + /\ myLid = [s \in Services |-> 0] + /\ qUntil = [s \in Services |-> 0] + /\ lastRenew = [s \in Services |-> 0] + /\ heSince = [s \in Services |-> 0] + /\ nextClaim = [s \in Services |-> 0] + /\ wake = [s \in Services |-> Never] + /\ cwake = [s \in Services |-> Never] + /\ phase = [s \in Services |-> "start"] + /\ swept = [s \in Services |-> FALSE] + /\ reacq = [s \in Services |-> 0] + /\ dropped = [s \in Services |-> 0] \* the lease id a quarantine dropped + /\ runBroken = [s \in Services |-> FALSE] + /\ startWaited = [s \in Services |-> FALSE] + /\ selfRef = FALSE + /\ coSweep = FALSE + /\ fWake = Never /\ fLid = 0 + /\ fBudget = IF Foreign THEN ForeignBudget ELSE 0 + /\ fHeld = FALSE + +----------------------------------------------------------------------------- +(* storage_service.cpp:692-741 ensure_publisher_lease(). *) +(* Called from the lease thread (:612) and from every cycle (:284). *) +(* Constrains headVars and locVars only. *) + +EnsureLease(s) == + \/ \* :693 already holds one; :696 already failed; :698-704 quarantined, + \* which takes NO claim at all, not even a fresh lease_id; :706 the + \* post-refusal backoff. All four are no-ops on the lease state. + /\ \/ held[s] + \/ phase[s] = "failed" + \/ Quarantined(s) + \/ now < nextClaim[s] + /\ UNCHANGED <> + \/ \* :710 writer_.acquire_lease(holder) + /\ ~held[s] /\ phase[s] # "failed" + /\ ~Quarantined(s) /\ now >= nextClaim[s] + /\ LET lid == IF ReuseLid /\ myLid[s] # 0 + THEN myLid[s] \* the COUNTERFACTUAL + ELSE lidGen \* :708-709 a fresh lease_id + IN \/ \* admitted :727-733 + /\ CanOk(lid) + /\ hOwner' = s /\ hLid' = lid /\ hExp' = now + TTL + Skew + /\ lidGen' = IF lid = lidGen THEN lidGen + 1 ELSE lidGen + /\ held' = [held EXCEPT ![s] = TRUE] + /\ myLid' = [myLid EXCEPT ![s] = lid] + /\ lastRenew' = [lastRenew EXCEPT ![s] = now] \* :727 + /\ heSince' = [heSince EXCEPT ![s] = 0] \* :728 + /\ nextClaim' = [nextClaim EXCEPT ![s] = 0] \* :729 + /\ reacq' = [reacq EXCEPT ![s] = + IF @ < MaxReacq THEN @ + 1 ELSE @] + /\ UNCHANGED <> + \/ \* :712-713 refused as held -> lease_held_elsewhere() + /\ CanRefused(lid) + /\ heSince' = [heSince EXCEPT ![s] = NewSince(s)] + /\ nextClaim' = [nextClaim EXCEPT ![s] = now + Tick] + /\ phase' = [phase EXCEPT ![s] = + IF LatchNow(s) THEN "failed" ELSE "run"] + /\ UNCHANGED <> + \/ \* :720-726 unknown outcome -> catalog_writer.cpp:307 quarantine() + /\ CanUnknown + /\ \E landed \in {TRUE, FALSE} : + /\ landed => CanLand(lid) + /\ IF landed + THEN /\ hOwner' = s /\ hLid' = lid + /\ hExp' = now + TTL + Skew + /\ lidGen' = IF lid = lidGen THEN lidGen+1 + ELSE lidGen + ELSE /\ lidGen' = IF lid = lidGen THEN lidGen+1 + ELSE lidGen + /\ UNCHANGED <> + /\ qUntil' = [qUntil EXCEPT ![s] = now + TTL] \* writer:273 + /\ dropped' = [dropped EXCEPT ![s] = lid] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* storage_service.cpp:634-660 renew_lease_if_due(). *) + +RenewIfDue(s) == + \/ \* :654 not due yet + /\ now - lastRenew[s] < DueAfter + /\ UNCHANGED <> + \/ /\ now - lastRenew[s] >= DueAfter + /\ \/ \* :655-659 renewed. lease_coordinator.cpp:67 presents the HELD id + /\ CanOk(myLid[s]) + /\ hOwner' = s /\ hLid' = myLid[s] /\ hExp' = now + TTL + Skew + /\ lastRenew' = [lastRenew EXCEPT ![s] = now] \* :656 + /\ heSince' = [heSince EXCEPT ![s] = 0] \* :657 + /\ UNCHANGED <> + \/ \* :617-621 kHeld from reject_live. lease_coordinator.cpp:236 + \* resets lease_ BEFORE throwing, so the local lease is gone too. + /\ CanRefused(myLid[s]) + /\ held' = [held EXCEPT ![s] = FALSE] + /\ heSince' = [heSince EXCEPT ![s] = NewSince(s)] + /\ nextClaim' = [nextClaim EXCEPT ![s] = now + Tick] + /\ phase' = [phase EXCEPT ![s] = + IF LatchNow(s) THEN "failed" ELSE "run"] + /\ UNCHANGED <> + \/ \* :625-628 unknown outcome. catalog_writer.cpp:285-292 + \* renew_for_publish(): ONE std::exception -- the first the client + \* does not retry away (it repeats a read after a transient + \* failure, and a write only if it never connected; never a + \* timeout) -- quarantines the writer and discards the lease. + \* The claim INSERT is a write, so its first failure after + \* connecting quarantines at once. There is no second try. + /\ CanUnknown + /\ \E landed \in {TRUE, FALSE} : + /\ landed => CanLand(myLid[s]) + /\ IF landed + THEN /\ hOwner' = s /\ hLid' = myLid[s] + /\ hExp' = now + TTL + Skew /\ UNCHANGED lidGen + ELSE UNCHANGED headVars + /\ held' = [held EXCEPT ![s] = FALSE] \* discard_local_lease + /\ qUntil' = [qUntil EXCEPT ![s] = now + TTL] \* writer:273 + /\ dropped' = [dropped EXCEPT ![s] = myLid[s]] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* storage_service.cpp:600-631 the lease thread's body. *) + +\* The step just taken was ensure_publisher_lease()'s claim, refused kHeld +\* by a head row this service wrote itself. Only the refused branch of +\* EnsureLease sets next_claim_ns_ to now + Tick while no lease is held +\* (admitted resets it to 0; unknown leaves it at a value <= now; the no-op +\* branch can only carry over a refusal from earlier in the same instant, +\* already counted then), and a refusal leaves the head unchanged, so hOwner +\* is the refusing row's owner. A quarantined or backing-off service takes +\* no claim and is not counted. +SelfRefused(s) == + /\ ~held[s] + /\ nextClaim'[s] = now + Tick + /\ hOwner = s + +LeaseThreadTick(s) == + /\ phase[s] = "run" + /\ now = wake[s] + /\ \E late \in 0..MaxLate : + wake' = [wake EXCEPT ![s] = now + Tick + late] + /\ IF ~held[s] THEN EnsureLease(s) ELSE RenewIfDue(s) \* :611-616 + /\ selfRef' = (selfRef \/ SelfRefused(s)) + /\ UNCHANGED <> + +\* :607-608 the thread returns for good once the service has latched. +LeaseThreadExit(s) == + /\ phase[s] = "failed" /\ wake[s] # Never + /\ wake' = [wake EXCEPT ![s] = Never] + /\ cwake' = [cwake EXCEPT ![s] = Never] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* storage_service.cpp:276-404 the cycle loop, reduced to its two *) +(* lease-relevant acts: ensure_publisher_lease() at :284, and the *) +(* last_renew_ns_ bump at :437-441. *) + +CycleTick(s) == + /\ CycleOn + /\ phase[s] = "run" + /\ now = cwake[s] + /\ cwake' = [cwake EXCEPT ![s] = now + 1] + /\ \/ EnsureLease(s) \* :284 + \/ \* :437-441 a publish that DID reach the catalog: the fenced + \* statement renewed the row (catalog_writer.cpp:490) and :440 + \* records that. + /\ held[s] /\ CanOk(myLid[s]) + /\ hOwner' = s /\ hLid' = myLid[s] /\ hExp' = now + TTL + Skew + /\ lastRenew' = [lastRenew EXCEPT ![s] = now] + /\ UNCHANGED <> + \/ \* :439 + indexer.cpp:258 -- every pack in the batch was already + \* committed, so `all_rows` and `indexed` are both empty, the + \* publish block is SKIPPED and renew_for_publish() is never + \* called. index() still returns skipped_packs > 0, and + \* :439-441 bumps last_renew_ns_ as if the row had been renewed. + /\ AllowSkipPublish /\ held[s] /\ chUp + /\ lastRenew' = [lastRenew EXCEPT ![s] = now] + /\ UNCHANGED <> + /\ selfRef' = (selfRef \/ SelfRefused(s)) + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* storage_service.cpp:102-173 start(). *) + +StartClaim(s) == + /\ phase[s] = "start" + /\ (wake[s] = Never \/ now = wake[s]) + /\ LET lid == lidGen IN + \/ \* :672-674 acquired + /\ CanOk(lid) + /\ hOwner' = s /\ hLid' = lid /\ hExp' = now + TTL + Skew + /\ lidGen' = lidGen + 1 + /\ held' = [held EXCEPT ![s] = TRUE] + /\ myLid' = [myLid EXCEPT ![s] = lid] + /\ lastRenew' = [lastRenew EXCEPT ![s] = now] \* :673 + /\ phase' = [phase EXCEPT ![s] = "sweep"] + /\ wake' = [wake EXCEPT ![s] = now + Tick] + /\ cwake' = [cwake EXCEPT ![s] = now + 1] + /\ UNCHANGED <> + \/ \* :675-687 refused; retry every poll until the deadline, then throw + /\ CanRefused(lid) + /\ IF now >= StartWait \* :678 + THEN /\ phase' = [phase EXCEPT ![s] = "refused"] \* :679-684 + /\ UNCHANGED <> + ELSE /\ UNCHANGED phase + /\ wake' = [wake EXCEPT ![s] = now + StartPoll] \* :686 + /\ startWaited' = [startWaited EXCEPT ![s] = TRUE] + /\ UNCHANGED <> + \/ \* a ClickHouse error at start is NOT a lease refusal (:676), so it + \* propagates and start() fails outright. + /\ CanUnknown + /\ phase' = [phase EXCEPT ![s] = "refused"] + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* storage_service.cpp:119-133 the sweep, AFTER the lease and never before. +Sweep(s) == + /\ phase[s] = "sweep" + /\ swept' = [swept EXCEPT ![s] = TRUE] + /\ phase' = [phase EXCEPT ![s] = "run"] + \* Obligation 5: was ANOTHER service live (its sink writing into a spool) + \* when this sweep ran? storage_service.cpp:113-118 admits this is only + \* "usually" prevented. + /\ coSweep' = (coSweep \/ \E t \in Services \ {s} : phase[t] = "run") + /\ UNCHANGED <> + +\* storage_service.cpp:175-205 stop(). A quarantined writer holds no lease, +\* so it writes NO tombstone (:186-188) and its row stays live to its TTL. +Stop(s) == + /\ AllowStop /\ phase[s] \in {"run", "failed"} + /\ phase' = [phase EXCEPT ![s] = "stopped"] + /\ wake' = [wake EXCEPT ![s] = Never] + /\ cwake' = [cwake EXCEPT ![s] = Never] + /\ IF held[s] /\ chUp + THEN /\ hExp' = now /\ UNCHANGED <> \* :193 + ELSE UNCHANGED headVars + /\ held' = [held EXCEPT ![s] = FALSE] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* The rival publisher: another CaptureStorageService on the same catalog. *) +(* It obeys the same contract, and renews on the same ttl/3 schedule. *) + +RivalClaim == + /\ Foreign /\ ~fHeld /\ fBudget > 0 /\ chUp /\ ~HeadLive + /\ hOwner' = "F" /\ hLid' = lidGen /\ hExp' = now + TTL + Skew + /\ lidGen' = lidGen + 1 + /\ fLid' = lidGen /\ fHeld' = TRUE /\ fBudget' = fBudget - 1 + /\ fWake' = now + DueAfter + /\ UNCHANGED <> + +RivalRenew == + /\ fHeld /\ chUp /\ now = fWake /\ Admits(fLid) /\ now < ForeignStopBy + /\ hOwner' = "F" /\ hLid' = fLid /\ hExp' = now + TTL + Skew + /\ UNCHANGED lidGen + /\ fWake' = now + DueAfter + /\ UNCHANGED <> + +\* Renewal refused: the rival lost the head and gives up (it has its own +\* lifecycle, which this model does not need). +RivalLost == + /\ fHeld /\ chUp /\ now = fWake /\ (~Admits(fLid) \/ now >= ForeignStopBy) + /\ fHeld' = FALSE /\ fWake' = Never + /\ UNCHANGED <> + +\* stop() with a tombstone (lease_coordinator.cpp:83-89): expiry := now. +RivalStop == + /\ ForeignStops /\ fHeld /\ chUp + /\ hExp' = now /\ UNCHANGED <> + /\ fHeld' = FALSE /\ fWake' = Never + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Cut == /\ chUp /\ cuts < MaxCuts + /\ chUp' = FALSE /\ cuts' = cuts + 1 + /\ UNCHANGED <> +Restore == /\ ~chUp /\ chUp' = TRUE + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Time. A discrete-event clock: it only advances when nothing is due at *) +(* the current instant, so every scheduled wake is served. *) + +Due(s) == + \/ (phase[s] = "run" /\ now = wake[s]) + \/ (phase[s] = "run" /\ CycleOn /\ now = cwake[s]) + \/ (phase[s] = "start" /\ (wake[s] = Never \/ now = wake[s])) + \/ (phase[s] = "sweep") + \/ (phase[s] = "failed" /\ wake[s] # Never) + +TimeTick == + /\ now < MaxTime + /\ \A s \in Services : ~Due(s) + /\ ~(fHeld /\ now = fWake) + /\ now' = now + 1 + \* History for obligation 3: since the latch clock started, was there an + \* instant at which NO foreign publisher held a live row? If so, the + \* "refusal that has lasted 2 x TTL" (storage_service.cpp:748-750) did + \* not in fact last. + /\ runBroken' = [s \in Services |-> + runBroken[s] \/ (heSince[s] # 0 /\ ~ForeignLive)] + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Next == + \/ \E s \in Services : LeaseThreadTick(s) + \/ \E s \in Services : LeaseThreadExit(s) + \/ \E s \in Services : CycleTick(s) + \/ \E s \in Services : StartClaim(s) + \/ \E s \in Services : Sweep(s) + \/ \E s \in Services : Stop(s) + \/ RivalClaim \/ RivalRenew \/ RivalLost \/ RivalStop + \/ Cut \/ Restore + \/ TimeTick + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* THE OBLIGATIONS *) +----------------------------------------------------------------------------- + +TypeOK == + /\ now \in 0..MaxTime + /\ hOwner \in Owners + /\ \A s \in Services : phase[s] \in + {"start","sweep","run","failed","refused","stopped"} + +\* --- O1 renewal keeps the lease alive ----------------------------------- +\* O1a. The service never BELIEVES it holds a lease whose row is not the +\* live head. storage_service.h:247-248, on the thread that runs +\* keep_lease() (storage_service.cpp:592-632): "so neither the cycle +\* backoff nor a slow upload can let the lease lapse while the service +\* still runs." +NoPhantomLease == + \A s \in Services : + (held[s] /\ phase[s] \in {"run","sweep"}) => (hLid = myLid[s] /\ HeadLive) + +\* O1b. storage_service.cpp:635-638: "The lease thread wakes every ttl/6, +\* so with no index() in the way the renewal fires within about a tick of +\* falling due, leaving at least roughly half the TTL for it to land before +\* the row expires." How many lease-thread wakes fall between the instant +\* the renewal falls due (last_renew + ttl/3) and the instant the row dies +\* (last_renew + ttl)? Four at every offset puts the first within a tick of +\* due, with more than half the TTL left. THREE -- the due one and two +\* more -- is what the comment claimed before #154 ("which leaves two more +\* tries"). Pure arithmetic over the tick grid, quantified over every phase +\* offset. +TriesInWindow(off) == + Cardinality({k \in 0..(3 * TTL) : /\ k * Tick + off >= DueAfter + /\ k * Tick + off < TTL}) +ThreeTriesFit == \A off \in 1..Tick : TriesInWindow(off) >= 3 +FourTriesFit == \A off \in 1..Tick : TriesInWindow(off) >= 4 +FiveTriesFit == \A off \in 1..Tick : TriesInWindow(off) >= 5 + +\* O1c. Is a renewal failure ABSORBED -- does the service still hold its +\* lease after one? (catalog_writer.cpp:285-292 quarantines on the first +\* std::exception, so this is expected to be REFUTED.) +OneFailureAbsorbed == + \A s \in Services : (phase[s] = "run" /\ Quarantined(s)) => held[s] + +\* --- O2 quarantine ------------------------------------------------------ +\* storage_service.cpp:698-704 -- a quarantined writer takes no claim at all. +QuarantineTakesNothing == + \A s \in Services : Quarantined(s) => ~held[s] + +\* Nobody but the head owner believes it holds a lease. +NoConcurrentHolder == + /\ \A s \in Services : held[s] => (hOwner = s /\ hLid = myLid[s] /\ HeadLive) + /\ fHeld => (hOwner = "F" \/ ~HeadLive) + +\* storage_service.cpp:699-701: "no claim ... until the window (one TTL) has +\* passed AND THAT LEASE'S ROW HAS EXPIRED WITH IT". Checked directly: at +\* every instant at or after the window's end, the row the quarantine +\* dropped is dead. +QuarantineOutlastsItsRow == + \A s \in Services : + (qUntil[s] > 0 /\ now >= qUntil[s] /\ dropped[s] # 0) + => ~(hLid = dropped[s] /\ HeadLive) + +\* Does a writer ever take a claim and get refused kHeld by a row it wrote +\* ITSELF? (The price of the fresh-lease_id rule: reject_live's +\* claimants==1 exemption at lease_coordinator.cpp:233 cannot recognise a +\* fresh id.) Only a claim actually taken counts -- see SelfRefused: a +\* tick on which the service is quarantined, backing off or holding a +\* lease makes no claim and is never flagged. +NoSelfRefusal == ~selfRef + +\* --- O3 the 2 x TTL latch ---------------------------------------------- +\* storage_service.cpp:748-750: "our own dropped row is dead within one TTL +\* of the loss, and a handover ends sooner still. A refusal that has lasted +\* 2 x TTL is a publisher that means to stay." The latch is justified only +\* if the refusals really did LAST -- a foreign publisher held a live row at +\* every instant of the window. +NoFalsePositiveLatch == + \A s \in Services : (phase[s] = "failed") => ~runBroken[s] + +NeverLatches == \A s \in Services : phase[s] # "failed" + +\* --- O4 the start wait -------------------------------------------------- +StartAlwaysSucceeds == \A s \in Services : phase[s] # "refused" + +\* --- O5 spool ordering -------------------------------------------------- +\* test_a_start_refused_the_lease_leaves_the_spool_unswept +RefusedStartNeverSweeps == + \A s \in Services : (phase[s] = "refused") => ~swept[s] + +\* storage_service.cpp:113-118, weakened by #150's 204a8d2 from a guarantee to +\* "only usually", as #154 weakened the header (storage_service.h:104-122) +\* too. The STRONG form, which neither comment now claims: +SweepOnlyWhenAlone == ~coSweep + +\* --- vacuity guards. EVERY ONE OF THESE MUST BE REFUTED. --------------- +VacQuarantine == \A s \in Services : ~Quarantined(s) +VacLatch == \A s \in Services : phase[s] # "failed" +VacRecovered == \A s \in Services : ~(reacq[s] > 0 /\ held[s]) +VacRefusal == \A s \in Services : heSince[s] = 0 +VacStartWaited == \A s \in Services : ~startWaited[s] +VacRivalHeld == ~fHeld +VacCut == chUp +VacHeld == \A s \in Services : ~held[s] +VacCoSweep == ~coSweep + +----------------------------------------------------------------------------- +(* VERDICTS (re-recorded with specs/check.sh) *) +(* specs/check.sh re-runs every config and compares each verdict with *) +(* the one below; specs/README.md has the full tables. *) +(* *) +(* config invariant verdict distinct *) +(* ------------------ ------------------------ ---------- --------- *) +(* O1_tries Three+FourTriesFit HOLDS 9 *) +(* O1_tries12/60 Three+FourTriesFit HOLDS 6 *) +(* O1_tries5 FiveTriesFit REFUTED - *) +(* -> exactly FOUR wakes fall in the window *) +(* O1_clean NoPhantomLease HOLDS 126 *) +(* O1_cut NoPhantomLease HOLDS 3,660 *) +(* O1_late (MaxLate 1) NoPhantomLease HOLDS 9,276 *) +(* O1_slowreq3 NoPhantomLease HOLDS 230 *) +(* O1_slowreq NoPhantomLease REFUTED 281 *) +(* -> O1 holds only while each lease request *) +(* finishes within about half the TTL; LIMITS 3 *) +(* O1_absorb OneFailureAbsorbed REFUTED 175 *) +(* O1_skip NoPhantomLease REFUTED 265 *) +(* O2_quar QuarantineOutlastsItsRow HOLDS 3,660 *) +(* O2_skew (Skew 1) QuarantineOutlastsItsRow REFUTED 1,049 *) +(* O2_selfref (Skew 1) NoSelfRefusal REFUTED 1,324 *) +(* O2_reuse QuarantineOutlastsItsRow REFUTED 851 *) +(* O3_rival NeverLatches REFUTED 49,985 *) +(* O3_rivaljust NoFalsePositiveLatch HOLDS 72,699 *) +(* -> a persistent rival latches, and legitimately *) +(* O3_stops2 NeverLatches HOLDS 137,745 *) +(* O3_false (Skew 0) NoFalsePositiveLatch HOLDS 137,745 *) +(* O3_selflatch NoFalsePositiveLatch REFUTED 8,958 *) +(* O3_selflatch_latch NeverLatches REFUTED 11,859 *) +(* -> a latch with NO rival in existence *) +(* O4_same StartAlwaysSucceeds HOLDS 66 *) +(* O4_skew StartAlwaysSucceeds HOLDS 59 *) +(* O4_bigger StartAlwaysSucceeds REFUTED 16 *) +(* O4_compose NoConcurrentHolder HOLDS 5,769 *) +(* O5_refused RefusedStartNeverSweeps HOLDS 14 *) +(* O5_cosweep SweepOnlyWhenAlone REFUTED 3,418 *) +(* *) +(* VACUITY GUARDS -- every one REFUTED, as it must be: *) +(* vac_held, vac_quar, vac_recov, vac_refus, vac_rival, vac_cut, *) +(* vac_latch, vac_start, vac_o4waited, vac_refusedstart, *) +(* vac_stops2refusal, vac_stops2rival. SweepOnlyWhenAlone needs no *) +(* guard of its own: O5_cosweep refutes it, so co-sweep is reachable. *) +(* ONE GUARD HELD, AND CONDEMNS ITS RUN: vac_stopsrefusal (VacRefusal) *) +(* HOLDS on LeaseLifecycle_O3_stops.cfg, so THAT run is vacuous -- with *) +(* no ClickHouse cut the rival can never claim. O3_stops2.cfg replaces *) +(* it and is proved non-vacuous by vac_stops2refusal/vac_stops2rival. *) +----------------------------------------------------------------------------- +(* LIMITS *) +(* *) +(* 1. The LeaseCoordinator is a contract, not a protocol. A contested head *) +(* (two rows at one term, lease_coordinator.cpp:237-246) is omitted; it *) +(* can only ADD kHeld refusals, so every "this latches / this lapses" *) +(* refutation below is preserved under it, and every "this HOLDS" *) +(* verdict is conditional on PublisherLease.tla's discharge. *) +(* 2. Time is TTL/6 per tick, so ttl/6, ttl/3 and 2*ttl are exact but *) +(* anything finer than a sixth of the TTL is invisible. The real start *) +(* poll is ttl/10 clamped to 50-500 ms, FINER than one tick, so a start *) +(* the model reports as refused purely at an expiry boundary would be *) +(* retried sooner in reality. *) +(* 3. EVERY CLICKHOUSE CALL TAKES ZERO TIME. RenewIfDue, EnsureLease and *) +(* StartClaim settle a request in the step that issues it. In the code *) +(* keep_lease() holds lease_mutex_ across renew_lease(), which is up to *) +(* three requests, each attempt bounded only by the client's request_s *) +(* (60 s by default, against a 15 s TTL), and a read that fails *) +(* transiently is repeated, up to max_attempts (3 by default) attempts *) +(* in all, so a slow request delays every later wake. MaxLate stands in *) +(* for that delay (and for OS lateness): with no publishes (CycleOn *) +(* FALSE) NoPhantomLease holds at MaxLate = 3, half the TTL *) +(* (O1_slowreq3), and is refuted at MaxLate = 4 (O1_slowreq). So *) +(* O1_clean, O1_cut and O1_late hold only if each lease request *) +(* completes within about half the TTL; nothing in the code bounds it *) +(* there yet. *) +(* 4. The cycle loop is reduced to ensure_publisher_lease() plus the *) +(* last_renew_ns_ bump. Uploads, backoff and pending_index_ never touch *) +(* the lease and are omitted. *) +(* 5. An outcome-unknown statement lands, if it lands at all, at the *) +(* instant the client sees the failure: the "landed" branch stamps its *) +(* row with now + TTL. Nothing in the code bounds a later landing. *) +(* catalog_writer.cpp:519-520's max_execution_time applies only to *) +(* publish_snapshot's statements; the lease INSERT *) +(* (lease_coordinator.cpp:214-227) carries only the insert_quorum *) +(* settings. A lease INSERT the client gave up on can land later and *) +(* stamp a row that outlives the quarantine window by as much. O2_quar *) +(* and O3_false HOLD only under the instant-landing assumption, and the *) +(* README's first suggested fix (clock_skew in the quarantine window) *) +(* does not survive a late landing on its own; the second (reset *) +(* held_elsewhere_since_ns_ whenever a run of refusals breaks) does. *) +(* 6. Skew runs one way. hExp adds Skew to every live row, so a replica *) +(* only ever reports a row live LONGER than it is; one that reports it *) +(* dead early, or two replicas disagreeing in opposite directions *) +(* across successive reads, is not modelled. *) +(* 7. Stop is never enabled: AllowStop is FALSE in every shipped config, *) +(* so no verdict depends on it. Its tombstone also differs from the *) +(* code's: it overwrites the head's expiry with now, instantly and on *) +(* every replica, and only when ClickHouse is up. The code inserts a *) +(* separate row (lease_coordinator.cpp:70-90) that can fail, be read *) +(* through a lagging replica, or land with an unknown outcome. *) +============================================================================= diff --git a/specs/tla/LeaseLifecycle_O1_absorb.cfg b/specs/tla/LeaseLifecycle_O1_absorb.cfg new file mode 100644 index 000000000..adec2c4b2 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O1_absorb.cfg @@ -0,0 +1,29 @@ +\*========================================================================= +\* O1c: how many consecutive renewal FAILURES are absorbed? +\* One ClickHouse cut. EXPECT: REFUTED (catalog_writer.cpp:285-292 +\* quarantines on the first std::exception, so zero are absorbed). +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 1 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT OneFailureAbsorbed diff --git a/specs/tla/LeaseLifecycle_O1_clean.cfg b/specs/tla/LeaseLifecycle_O1_clean.cfg new file mode 100644 index 000000000..debcbcfcc --- /dev/null +++ b/specs/tla/LeaseLifecycle_O1_clean.cfg @@ -0,0 +1,30 @@ +\*========================================================================= +\* O1 baseline: one service, ClickHouse up throughout, no rival. +\* Does the lease thread keep the row alive? EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoPhantomLease +INVARIANT QuarantineTakesNothing +INVARIANT NoConcurrentHolder diff --git a/specs/tla/LeaseLifecycle_O1_cut.cfg b/specs/tla/LeaseLifecycle_O1_cut.cfg new file mode 100644 index 000000000..cd3b65838 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O1_cut.cfg @@ -0,0 +1,29 @@ +\*========================================================================= +\* O1a under a ClickHouse cut: does the service ever BELIEVE it +\* holds a lease whose row has lapsed? EXPECT: HOLDS (the quarantine +\* drops the local lease at the same instant). +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoPhantomLease diff --git a/specs/tla/LeaseLifecycle_O1_late.cfg b/specs/tla/LeaseLifecycle_O1_late.cfg new file mode 100644 index 000000000..50972dbc9 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O1_late.cfg @@ -0,0 +1,28 @@ +\*========================================================================= +\* O1a with the lease thread allowed to wake one tick late. +\* EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 1 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoPhantomLease diff --git a/specs/tla/LeaseLifecycle_O1_skip.cfg b/specs/tla/LeaseLifecycle_O1_skip.cfg new file mode 100644 index 000000000..4353ffd01 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O1_skip.cfg @@ -0,0 +1,31 @@ +\*========================================================================= +\* O1a with indexer.cpp:258 modelled: an index pass whose packs +\* were ALL already committed publishes nothing, yet +\* storage_service.cpp:439-441 bumps last_renew_ns_ anyway. +\* EXPECT: REFUTED -- the row lapses under a service that still +\* believes it holds the lease. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 16 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = TRUE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoPhantomLease diff --git a/specs/tla/LeaseLifecycle_O1_slowreq.cfg b/specs/tla/LeaseLifecycle_O1_slowreq.cfg new file mode 100644 index 000000000..1c9fde3a5 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O1_slowreq.cfg @@ -0,0 +1,35 @@ +\*========================================================================= +\* O1a when a lease request is SLOW. The model settles every ClickHouse +\* call in zero time; in the code keep_lease() holds lease_mutex_ across +\* renew_lease(), so a request that takes k ticks delays the next wake by +\* k. MaxLate stands in for that delay. No cycle (CycleOn FALSE), so +\* only the lease thread renews: the idle service. MaxLate = 3 (half the +\* TTL) still holds; MaxLate = 4 lets the row expire under a service +\* that still believes it holds it. EXPECT: VIOLATED. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 4 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = FALSE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoPhantomLease +INVARIANT QuarantineTakesNothing +INVARIANT NoConcurrentHolder diff --git a/specs/tla/LeaseLifecycle_O1_slowreq3.cfg b/specs/tla/LeaseLifecycle_O1_slowreq3.cfg new file mode 100644 index 000000000..6ab200188 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O1_slowreq3.cfg @@ -0,0 +1,32 @@ +\*========================================================================= +\* O1a when a lease request is slow, at the largest delay that still +\* holds: the partner of LeaseLifecycle_O1_slowreq.cfg, with MaxLate = 3 +\* (half the TTL) instead of 4. No cycle (CycleOn FALSE), so only the +\* lease thread renews. EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 3 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = FALSE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoPhantomLease +INVARIANT QuarantineTakesNothing +INVARIANT NoConcurrentHolder diff --git a/specs/tla/LeaseLifecycle_O1_tries.cfg b/specs/tla/LeaseLifecycle_O1_tries.cfg new file mode 100644 index 000000000..04c856ebe --- /dev/null +++ b/specs/tla/LeaseLifecycle_O1_tries.cfg @@ -0,0 +1,31 @@ +\*========================================================================= +\* O1b: the tick arithmetic of storage_service.cpp:635-638, a renewal +\* that "fires within about a tick of falling due" (before #154: "leaves +\* two more tries"). A constant-expression invariant; the +\* smallest possible behaviour suffices. EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 1 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT ThreeTriesFit +INVARIANT FourTriesFit diff --git a/specs/tla/LeaseLifecycle_O1_tries12.cfg b/specs/tla/LeaseLifecycle_O1_tries12.cfg new file mode 100644 index 000000000..634321bf9 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O1_tries12.cfg @@ -0,0 +1,31 @@ +\*========================================================================= +\* O1b: the tick arithmetic of storage_service.cpp:635-638, a renewal +\* that "fires within about a tick of falling due" (before #154: "leaves +\* two more tries"). A constant-expression invariant; the +\* smallest possible behaviour suffices. EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 12 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 1 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT ThreeTriesFit +INVARIANT FourTriesFit diff --git a/specs/tla/LeaseLifecycle_O1_tries5.cfg b/specs/tla/LeaseLifecycle_O1_tries5.cfg new file mode 100644 index 000000000..4adab6db8 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O1_tries5.cfg @@ -0,0 +1,31 @@ +\*========================================================================= +\* O1b: the tick arithmetic of storage_service.cpp:635-638, a renewal +\* that "fires within about a tick of falling due" (before #154: "leaves +\* two more tries"). A constant-expression invariant; the +\* smallest possible behaviour suffices. EXPECT: REFUTED (four wakes +\* fit at every phase offset, five do not). +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 60 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 1 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT FiveTriesFit diff --git a/specs/tla/LeaseLifecycle_O1_tries60.cfg b/specs/tla/LeaseLifecycle_O1_tries60.cfg new file mode 100644 index 000000000..99ba625e4 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O1_tries60.cfg @@ -0,0 +1,31 @@ +\*========================================================================= +\* O1b: the tick arithmetic of storage_service.cpp:635-638, a renewal +\* that "fires within about a tick of falling due" (before #154: "leaves +\* two more tries"). A constant-expression invariant; the +\* smallest possible behaviour suffices. EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 60 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 1 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT ThreeTriesFit +INVARIANT FourTriesFit diff --git a/specs/tla/LeaseLifecycle_O2_quar.cfg b/specs/tla/LeaseLifecycle_O2_quar.cfg new file mode 100644 index 000000000..ee25cca2f --- /dev/null +++ b/specs/tla/LeaseLifecycle_O2_quar.cfg @@ -0,0 +1,31 @@ +\*========================================================================= +\* O2: quarantine. One cut, outcome-unknown writes allowed, no +\* skew. Does the one-TTL window really outlast the row it dropped, +\* and can a quarantined writer ever hold? EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT QuarantineTakesNothing +INVARIANT QuarantineOutlastsItsRow +INVARIANT NoConcurrentHolder diff --git a/specs/tla/LeaseLifecycle_O2_reuse.cfg b/specs/tla/LeaseLifecycle_O2_reuse.cfg new file mode 100644 index 000000000..4db681e37 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O2_reuse.cfg @@ -0,0 +1,32 @@ +\*========================================================================= +\* O2 COUNTERFACTUAL: ReuseLid = TRUE makes the post-quarantine +\* acquire present the DROPPED lease_id, which reject_live's +\* claimants==1 exemption (lease_coordinator.cpp:233) then admits. +\* Same invariants as O2_quar. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 1 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = TRUE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT QuarantineTakesNothing +INVARIANT QuarantineOutlastsItsRow +INVARIANT NoConcurrentHolder diff --git a/specs/tla/LeaseLifecycle_O2_selfref.cfg b/specs/tla/LeaseLifecycle_O2_selfref.cfg new file mode 100644 index 000000000..09ad3c972 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O2_selfref.cfg @@ -0,0 +1,30 @@ +\*========================================================================= +\* O2: is the fresh-lease_id rule's price real -- can a writer be +\* refused by its OWN dropped row? EXPECT: REFUTED (a self-refusal +\* is reachable), which matters because that refusal feeds the +\* 2 x TTL latch clock at storage_service.cpp:743-759. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 1 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoSelfRefusal diff --git a/specs/tla/LeaseLifecycle_O2_skew.cfg b/specs/tla/LeaseLifecycle_O2_skew.cfg new file mode 100644 index 000000000..547cbe544 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O2_skew.cfg @@ -0,0 +1,30 @@ +\*========================================================================= +\* O2: the same with clock_skew_s = one tick, which #150's own +\* start-wait change (204a8d2) says a lagging replica can have. +\* storage_service.cpp:699-701 claims the window ends only once "that +\* lease's row has expired with it". EXPECT: REFUTED. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 1 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT QuarantineOutlastsItsRow diff --git a/specs/tla/LeaseLifecycle_O3_false.cfg b/specs/tla/LeaseLifecycle_O3_false.cfg new file mode 100644 index 000000000..f569d108f --- /dev/null +++ b/specs/tla/LeaseLifecycle_O3_false.cfg @@ -0,0 +1,30 @@ +\*========================================================================= +\* O3: is 2 x TTL enough to TELL the two apart? A rival that +\* stops inside two TTLs, plus one ClickHouse cut. +\* NoFalsePositiveLatch says a latched service really did face an +\* unbroken run of foreign refusals. EXPECT: REFUTED. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 22 + MaxLate = 0 + Foreign = TRUE + ForeignStops = TRUE + ForeignBudget = 1 + ForeignStopBy = 6 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoFalsePositiveLatch diff --git a/specs/tla/LeaseLifecycle_O3_falsenocut.cfg b/specs/tla/LeaseLifecycle_O3_falsenocut.cfg new file mode 100644 index 000000000..f1c7c3818 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O3_falsenocut.cfg @@ -0,0 +1,29 @@ +\*========================================================================= +\* O3 control: the same rival, but ClickHouse never cut and no +\* outcome-unknown writes. EXPECT: HOLDS -- the false positive needs +\* the quarantine, not merely a rival that comes and goes. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 22 + MaxLate = 0 + Foreign = TRUE + ForeignStops = TRUE + ForeignBudget = 2 + ForeignStopBy = 6 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoFalsePositiveLatch diff --git a/specs/tla/LeaseLifecycle_O3_rival.cfg b/specs/tla/LeaseLifecycle_O3_rival.cfg new file mode 100644 index 000000000..5bf66e22b --- /dev/null +++ b/specs/tla/LeaseLifecycle_O3_rival.cfg @@ -0,0 +1,30 @@ +\*========================================================================= +\* O3, the positive direction: a rival that takes the catalog and +\* keeps renewing. test_a_rival_that_takes_over_during_a_cut_still_latches +\* says the service must latch. EXPECT: REFUTED (i.e. the latch IS +\* reached), and the trace shows it at >= 2 x TTL after the rival. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 22 + MaxLate = 0 + Foreign = TRUE + ForeignStops = FALSE + ForeignBudget = 1 + ForeignStopBy = 99 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NeverLatches diff --git a/specs/tla/LeaseLifecycle_O3_rivaljust.cfg b/specs/tla/LeaseLifecycle_O3_rivaljust.cfg new file mode 100644 index 000000000..0ace57dc1 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O3_rivaljust.cfg @@ -0,0 +1,30 @@ +\*========================================================================= +\* O3, the positive direction: a rival that takes the catalog and +\* keeps renewing. test_a_rival_that_takes_over_during_a_cut_still_latches +\* says the service must latch. EXPECT: REFUTED (i.e. the latch IS +\* reached), and the trace shows it at >= 2 x TTL after the rival. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 22 + MaxLate = 0 + Foreign = TRUE + ForeignStops = FALSE + ForeignBudget = 1 + ForeignStopBy = 99 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoFalsePositiveLatch diff --git a/specs/tla/LeaseLifecycle_O3_selflatch.cfg b/specs/tla/LeaseLifecycle_O3_selflatch.cfg new file mode 100644 index 000000000..c071edd58 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O3_selflatch.cfg @@ -0,0 +1,36 @@ +\*========================================================================= +\* O3, the sharp case: NO rival publisher exists at all. Skew = 1 tick, so +\* a lagging replica reports a row as live one tick past its TTL, while the +\* quarantine window (catalog_writer.cpp:273) is measured on the LOCAL +\* monotonic clock and carries no skew allowance. A writer can therefore be +\* refused by its OWN dropped row at the instant its quarantine ends. +\* Each such refusal feeds storage_service.cpp:743-759, whose clock is never +\* reset except by a SUCCESSFUL claim. EXPECT: REFUTED -- the service +\* latches "publisher lease held by another publisher" with no other +\* publisher in existence. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 1 + PredTTL = 6 + StartWait = 0 + MaxTime = 24 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoFalsePositiveLatch +INVARIANT NeverLatches diff --git a/specs/tla/LeaseLifecycle_O3_selflatch_latch.cfg b/specs/tla/LeaseLifecycle_O3_selflatch_latch.cfg new file mode 100644 index 000000000..834ed9674 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O3_selflatch_latch.cfg @@ -0,0 +1,35 @@ +\*========================================================================= +\* O3, the sharp case: NO rival publisher exists at all. Skew = 1 tick, so +\* a lagging replica reports a row as live one tick past its TTL, while the +\* quarantine window (catalog_writer.cpp:273) is measured on the LOCAL +\* monotonic clock and carries no skew allowance. A writer can therefore be +\* refused by its OWN dropped row at the instant its quarantine ends. +\* Each such refusal feeds storage_service.cpp:743-759, whose clock is never +\* reset except by a SUCCESSFUL claim. EXPECT: REFUTED -- the service +\* latches "publisher lease held by another publisher" with no other +\* publisher in existence. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 1 + PredTTL = 6 + StartWait = 0 + MaxTime = 24 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NeverLatches diff --git a/specs/tla/LeaseLifecycle_O3_stops.cfg b/specs/tla/LeaseLifecycle_O3_stops.cfg new file mode 100644 index 000000000..a36639c1a --- /dev/null +++ b/specs/tla/LeaseLifecycle_O3_stops.cfg @@ -0,0 +1,30 @@ +\*========================================================================= +\* SUPERSEDED -- THIS RUN IS VACUOUS. With no ClickHouse cut the incumbent +\* never stops renewing, so the rival can never claim and the service is +\* never refused at all: vac_stopsrefusal (VacRefusal) HOLDS here, which +\* proves the vacuity. Use LeaseLifecycle_O3_stops2.cfg instead. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 22 + MaxLate = 0 + Foreign = TRUE + ForeignStops = TRUE + ForeignBudget = 1 + ForeignStopBy = 6 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NeverLatches diff --git a/specs/tla/LeaseLifecycle_O3_stops2.cfg b/specs/tla/LeaseLifecycle_O3_stops2.cfg new file mode 100644 index 000000000..2b96ded99 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O3_stops2.cfg @@ -0,0 +1,33 @@ +\*========================================================================= +\* O3, the negative direction, done properly: the rival can only get in +\* while a ClickHouse cut stops the incumbent renewing -- which is exactly +\* how test_a_rival_that_stops_within_two_ttls_does_not_latch stages it. +\* One cut, and a rival pinned to stop by t = TTL (well inside 2 x TTL). +\* EXPECT: HOLDS -- the service takes the lease back and never latches. +\* (The earlier O3_stops run, with no cut, was VACUOUS: the rival could +\* never claim at all. vac_stops_refusal below proves this one is not.) +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 22 + MaxLate = 0 + Foreign = TRUE + ForeignStops = TRUE + ForeignBudget = 1 + ForeignStopBy = 6 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NeverLatches diff --git a/specs/tla/LeaseLifecycle_O4_bigger.cfg b/specs/tla/LeaseLifecycle_O4_bigger.cfg new file mode 100644 index 000000000..9e4fc1a19 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O4_bigger.cfg @@ -0,0 +1,30 @@ +\*========================================================================= +\* O4: a predecessor that ran with a LARGER TTL -- the native 30 s +\* default the config comment (native_capture.py:271-280) warns +\* about. PredTTL 12 against a service configured for 6, so the +\* default wait is still 7. EXPECT: REFUTED, confirming the comment. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 12 + StartWait = 7 + MaxTime = 16 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = TRUE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT StartAlwaysSucceeds diff --git a/specs/tla/LeaseLifecycle_O4_compose.cfg b/specs/tla/LeaseLifecycle_O4_compose.cfg new file mode 100644 index 000000000..b5183ba6a --- /dev/null +++ b/specs/tla/LeaseLifecycle_O4_compose.cfg @@ -0,0 +1,31 @@ +\*========================================================================= +\* O4 composed with quarantine and the latch: the successor takes +\* the predecessor's lease after the wait, then meets a ClickHouse +\* cut and a rival. Does the wait compose? EXPECT: HOLDS for +\* NoConcurrentHolder; the latch invariant is checked separately. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 7 + MaxTime = 18 + MaxLate = 0 + Foreign = TRUE + ForeignStops = FALSE + ForeignBudget = 1 + ForeignStopBy = 99 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = TRUE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT NoConcurrentHolder +INVARIANT QuarantineTakesNothing diff --git a/specs/tla/LeaseLifecycle_O4_same.cfg b/specs/tla/LeaseLifecycle_O4_same.cfg new file mode 100644 index 000000000..564072259 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O4_same.cfg @@ -0,0 +1,31 @@ +\*========================================================================= +\* O4: a crashed predecessor that ran with the SAME knobs. The +\* default start wait is lease_ttl + publish_timeout + clock_skew +\* (native_capture.py:374-378) = 6 + 1 + 0. +\* test_a_restart_within_the_ttl_of_a_killed_predecessor_succeeds. +\* EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 7 + MaxTime = 12 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = TRUE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT StartAlwaysSucceeds diff --git a/specs/tla/LeaseLifecycle_O4_skew.cfg b/specs/tla/LeaseLifecycle_O4_skew.cfg new file mode 100644 index 000000000..6b72dd7cf --- /dev/null +++ b/specs/tla/LeaseLifecycle_O4_skew.cfg @@ -0,0 +1,29 @@ +\*========================================================================= +\* O4: the same, with a replica lagging by one tick. This is +\* exactly what #150's 204a8d2 added clock_skew_s to the default for. +\* EXPECT: HOLDS (start wait 6 + 1 + 1 = 8). +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 1 + PredTTL = 6 + StartWait = 8 + MaxTime = 12 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = TRUE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT StartAlwaysSucceeds diff --git a/specs/tla/LeaseLifecycle_O5_cosweep.cfg b/specs/tla/LeaseLifecycle_O5_cosweep.cfg new file mode 100644 index 000000000..e491eeba3 --- /dev/null +++ b/specs/tla/LeaseLifecycle_O5_cosweep.cfg @@ -0,0 +1,32 @@ +\*========================================================================= +\* O5: two services on one spool. storage_service.cpp:113-118 +\* (as #150's 204a8d2 rewrote it) admits a quarantined holder lets its row +\* lapse and "a second process can take the lease in that gap". +\* SweepOnlyWhenAlone is the STRONG form, which neither that comment nor +\* the header (storage_service.h:104-122, since #154) claims. +\* EXPECT: REFUTED. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1, s2} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 14 + MaxTime = 16 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = FALSE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT SweepOnlyWhenAlone diff --git a/specs/tla/LeaseLifecycle_O5_refused.cfg b/specs/tla/LeaseLifecycle_O5_refused.cfg new file mode 100644 index 000000000..8fe58ec3b --- /dev/null +++ b/specs/tla/LeaseLifecycle_O5_refused.cfg @@ -0,0 +1,29 @@ +\*========================================================================= +\* O5: a start refused the lease must leave the spool unswept. +\* test_a_start_refused_the_lease_leaves_the_spool_unswept, with +\* start_lease_wait_s = 0. EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1, s2} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 10 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = FALSE + PredHolds = TRUE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT RefusedStartNeverSweeps diff --git a/specs/tla/LeaseLifecycle_vac_cut.cfg b/specs/tla/LeaseLifecycle_vac_cut.cfg new file mode 100644 index 000000000..60bc166e4 --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_cut.cfg @@ -0,0 +1,27 @@ +\*========================================================================= +\* VACUITY GUARD -- MUST BE REFUTED. VacCut +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 1 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacCut diff --git a/specs/tla/LeaseLifecycle_vac_held.cfg b/specs/tla/LeaseLifecycle_vac_held.cfg new file mode 100644 index 000000000..e9e4b2011 --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_held.cfg @@ -0,0 +1,28 @@ +\*========================================================================= +\* O1 baseline: one service, ClickHouse up throughout, no rival. +\* Does the lease thread keep the row alive? EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacHeld diff --git a/specs/tla/LeaseLifecycle_vac_latch.cfg b/specs/tla/LeaseLifecycle_vac_latch.cfg new file mode 100644 index 000000000..98ff9d888 --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_latch.cfg @@ -0,0 +1,27 @@ +\*========================================================================= +\* VACUITY GUARD -- MUST BE REFUTED. VacLatch +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 22 + MaxLate = 0 + Foreign = TRUE + ForeignStops = FALSE + ForeignBudget = 1 + ForeignStopBy = 99 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacLatch diff --git a/specs/tla/LeaseLifecycle_vac_o4waited.cfg b/specs/tla/LeaseLifecycle_vac_o4waited.cfg new file mode 100644 index 000000000..cda6f63bd --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_o4waited.cfg @@ -0,0 +1,31 @@ +\*========================================================================= +\* O4: a crashed predecessor that ran with the SAME knobs. The +\* default start wait is lease_ttl + publish_timeout + clock_skew +\* (native_capture.py:374-378) = 6 + 1 + 0. +\* test_a_restart_within_the_ttl_of_a_killed_predecessor_succeeds. +\* EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 7 + MaxTime = 12 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = TRUE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacStartWaited diff --git a/specs/tla/LeaseLifecycle_vac_quar.cfg b/specs/tla/LeaseLifecycle_vac_quar.cfg new file mode 100644 index 000000000..dbb059ebd --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_quar.cfg @@ -0,0 +1,27 @@ +\*========================================================================= +\* VACUITY GUARD -- MUST BE REFUTED. VacQuarantine +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacQuarantine diff --git a/specs/tla/LeaseLifecycle_vac_recov.cfg b/specs/tla/LeaseLifecycle_vac_recov.cfg new file mode 100644 index 000000000..c1dc2ab75 --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_recov.cfg @@ -0,0 +1,27 @@ +\*========================================================================= +\* VACUITY GUARD -- MUST BE REFUTED. VacRecovered +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 14 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacRecovered diff --git a/specs/tla/LeaseLifecycle_vac_refus.cfg b/specs/tla/LeaseLifecycle_vac_refus.cfg new file mode 100644 index 000000000..2cd67e2dd --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_refus.cfg @@ -0,0 +1,27 @@ +\*========================================================================= +\* VACUITY GUARD -- MUST BE REFUTED. VacRefusal +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 18 + MaxLate = 0 + Foreign = TRUE + ForeignStops = FALSE + ForeignBudget = 1 + ForeignStopBy = 99 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacRefusal diff --git a/specs/tla/LeaseLifecycle_vac_refusedstart.cfg b/specs/tla/LeaseLifecycle_vac_refusedstart.cfg new file mode 100644 index 000000000..f00b1b1ac --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_refusedstart.cfg @@ -0,0 +1,29 @@ +\*========================================================================= +\* O5: a start refused the lease must leave the spool unswept. +\* test_a_start_refused_the_lease_leaves_the_spool_unswept, with +\* start_lease_wait_s = 0. EXPECT: HOLDS. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1, s2} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 10 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = FALSE + PredHolds = TRUE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT StartAlwaysSucceeds diff --git a/specs/tla/LeaseLifecycle_vac_rival.cfg b/specs/tla/LeaseLifecycle_vac_rival.cfg new file mode 100644 index 000000000..e15336cc1 --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_rival.cfg @@ -0,0 +1,27 @@ +\*========================================================================= +\* VACUITY GUARD -- MUST BE REFUTED. VacRivalHeld +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 18 + MaxLate = 0 + Foreign = TRUE + ForeignStops = FALSE + ForeignBudget = 1 + ForeignStopBy = 99 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacRivalHeld diff --git a/specs/tla/LeaseLifecycle_vac_start.cfg b/specs/tla/LeaseLifecycle_vac_start.cfg new file mode 100644 index 000000000..2b87641b3 --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_start.cfg @@ -0,0 +1,27 @@ +\*========================================================================= +\* VACUITY GUARD -- MUST BE REFUTED. VacStartWaited +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 7 + MaxTime = 12 + MaxLate = 0 + Foreign = FALSE + ForeignStops = FALSE + ForeignBudget = 0 + ForeignStopBy = 0 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = TRUE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacStartWaited diff --git a/specs/tla/LeaseLifecycle_vac_stops2refusal.cfg b/specs/tla/LeaseLifecycle_vac_stops2refusal.cfg new file mode 100644 index 000000000..7ff8dbc03 --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_stops2refusal.cfg @@ -0,0 +1,33 @@ +\*========================================================================= +\* O3, the negative direction, done properly: the rival can only get in +\* while a ClickHouse cut stops the incumbent renewing -- which is exactly +\* how test_a_rival_that_stops_within_two_ttls_does_not_latch stages it. +\* One cut, and a rival pinned to stop by t = TTL (well inside 2 x TTL). +\* EXPECT: HOLDS -- the service takes the lease back and never latches. +\* (The earlier O3_stops run, with no cut, was VACUOUS: the rival could +\* never claim at all. vac_stops_refusal below proves this one is not.) +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 22 + MaxLate = 0 + Foreign = TRUE + ForeignStops = TRUE + ForeignBudget = 1 + ForeignStopBy = 6 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacRefusal diff --git a/specs/tla/LeaseLifecycle_vac_stops2rival.cfg b/specs/tla/LeaseLifecycle_vac_stops2rival.cfg new file mode 100644 index 000000000..b0ef9710b --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_stops2rival.cfg @@ -0,0 +1,33 @@ +\*========================================================================= +\* O3, the negative direction, done properly: the rival can only get in +\* while a ClickHouse cut stops the incumbent renewing -- which is exactly +\* how test_a_rival_that_stops_within_two_ttls_does_not_latch stages it. +\* One cut, and a rival pinned to stop by t = TTL (well inside 2 x TTL). +\* EXPECT: HOLDS -- the service takes the lease back and never latches. +\* (The earlier O3_stops run, with no cut, was VACUOUS: the rival could +\* never claim at all. vac_stops_refusal below proves this one is not.) +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 22 + MaxLate = 0 + Foreign = TRUE + ForeignStops = TRUE + ForeignBudget = 1 + ForeignStopBy = 6 + MaxCuts = 1 + AllowUnknown = TRUE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacRivalHeld diff --git a/specs/tla/LeaseLifecycle_vac_stopsrefusal.cfg b/specs/tla/LeaseLifecycle_vac_stopsrefusal.cfg new file mode 100644 index 000000000..0147ba01b --- /dev/null +++ b/specs/tla/LeaseLifecycle_vac_stopsrefusal.cfg @@ -0,0 +1,30 @@ +\*========================================================================= +\* O3, the negative direction: a rival that stops well inside two +\* TTLs (ForeignStopBy = TTL), ClickHouse never cut. +\* test_a_rival_that_stops_within_two_ttls_does_not_latch. +\* EXPECT: HOLDS -- no latch. +\*========================================================================= +SPECIFICATION Spec +CHECK_DEADLOCK FALSE +CONSTANTS + Services = {s1} + TTL = 6 + PT = 1 + Skew = 0 + PredTTL = 6 + StartWait = 0 + MaxTime = 22 + MaxLate = 0 + Foreign = TRUE + ForeignStops = TRUE + ForeignBudget = 1 + ForeignStopBy = 6 + MaxCuts = 0 + AllowUnknown = FALSE + AllowSkipPublish = FALSE + ReuseLid = FALSE + CycleOn = TRUE + PredHolds = FALSE + AllowStop = FALSE + MaxReacq = 2 +INVARIANT VacRefusal diff --git a/specs/tla/PublisherLease.cfg b/specs/tla/PublisherLease.cfg new file mode 100644 index 000000000..f008a7db0 --- /dev/null +++ b/specs/tla/PublisherLease.cfg @@ -0,0 +1,67 @@ +\*=========================================================================== +\* PublisherLease.cfg -- THE BASE MODEL: the protocol exactly as shipped. +\* +\* Linearizable TRUE = deciding_read() really is sequentially +\* consistent (clickhouse_client.cpp:374) +\* AllowOverrun FALSE = max_execution_time is honoured +\* (catalog_writer.cpp:519-520) +\* WriterLock TRUE = the re-entrant writer lock (doc :539-543) +\* FreshPublishId TRUE = publish_id minted per call +\* (catalog_writer.cpp:529) +\* SelfRace FALSE = each Publisher is its own writer +\* +\* Sibling configs in this directory, each a single knob turned, with the +\* verdict TLC returned. Full results table and run commands: specs/README.md. +\* Counterexample lengths below are the traces TLC printed on the recorded +\* run; parallel BFS does not guarantee a minimal trace, so a re-run may +\* report a different length for the same violation. +\* +\* At THESE constants the takeover race is out of the term budget, so +\* AllSafety's NoOverlappingAdmit conjunct holds vacuously here. The +\* configs that carry it come in pairs, cap enforced vs cap overrun: +\* +\* PublisherLease_base5.cfg base with MaxTerm 5 / MaxTime 8 -- the +\* term budget the takeover race needs +\* PublisherLease_base5_ovr.cfg same, cap may be OVERRUN +\* -> NoOverlappingAdmit VIOLATED +\* PublisherLease_noovr0.cfg empty-refs publish, cap ENFORCED +\* -> NoOverlappingAdmit HOLDS (799,611) +\* PublisherLease_ovr0.cfg same, cap may be OVERRUN (doc :503) +\* -> NoOverlappingAdmit VIOLATED (17) +\* PublisherLease_noovr1.cfg noovr0 with one manifest chunk +\* -> NoOverlappingAdmit HOLDS +\* PublisherLease_ovr1.cfg same, cap may be OVERRUN +\* -> NoOverlappingAdmit VIOLATED +\* PublisherLease_holders.cfg -> AtMostOneHolder VIOLATED (11) +\* PublisherLease_holderssafe.cfg -> TwoHoldersIsSafe HOLDS (9,665,700) +\* PublisherLease_believers.cfg -> AtMostOneBeliever HOLDS (9,665,700) +\* PublisherLease_orphans.cfg -> NoOrphanManifestRows VIOLATED (9) +\* PublisherLease_selfrace.cfg -> WatermarkMonotonic VIOLATED (29) +\* PublisherLease_selfracelocked.cfg -> AllSafety HOLDS (524,274) +\* PublisherLease_chunks2*.cfg two manifest chunks +\* PublisherLease_nonlin_*.cfg Linearizable = FALSE +\* PublisherLease_vac*.cfg vacuity guards -- every one of these is +\* EXPECTED to be refuted; the trace proves +\* the model reaches the state the safety +\* invariants are quantified over +\*=========================================================================== +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT AllSafety +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease.tla b/specs/tla/PublisherLease.tla new file mode 100644 index 000000000..bdd26fb32 --- /dev/null +++ b/specs/tla/PublisherLease.tla @@ -0,0 +1,549 @@ +---------------------------- MODULE PublisherLease ---------------------------- +(***************************************************************************) +(* A TLA+ model of the DMI publisher lease + fenced publish protocol. *) +(* *) +(* SOURCE OF TRUTH (everything below is modelled from the CODE; where the *) +(* code and the prose disagree the comment says so): *) +(* *) +(* native/csrc/catalog/lease_coordinator.cpp *) +(* :102-142 claim_with_rival -- head read, reject_live, insert, *) +(* singleton read-back. THREE round trips, so a rival row *) +(* can land in either gap. Modelled as three actions: *) +(* ClaimHead / ClaimInsert / ClaimRead. *) +(* :83 release_statement -- the TOMBSTONE: an already-expired *) +(* row at the holder's OWN term. Modelled in Release. *) +(* :144-165 head() -- one deciding read, GROUP BY *) +(* (term,lid) at max(term), min(expires_at_ns) per lease, *) +(* ORDER BY lease_id DESC, live_until = max over claimants. *) +(* :167-180 fence() -- resolves ONE lease at the head term *) +(* (LIMIT 1 after lease_id DESC) and asks: is it mine, and *) +(* does it have more than publish_timeout + clock_skew left. *) +(* :182-195 fence_eval -- a DECIDING read (comment says why). *) +(* :230-257 reject_live -- admits iff the head is wholly dead *) +(* OR (claimants == 1 AND the single head lease is mine). *) +(* The claimants>1 branch is the contested-head quarantine. *) +(* *) +(* native/csrc/catalog/catalog_writer.cpp *) +(* :478-669 publish_snapshot -- renew, then per manifest chunk *) +(* (fenced INSERT, read-back, renew), then the fenced *) +(* watermark INSERT, then the owners read-back. *) +(* :583 "The barrier, the fence and the visibility write are ONE *) +(* server-side statement." Modelled as WmAdmit (predicate *) +(* evaluated at admission) + WmLand (row becomes durable *) +(* LATER) -- these are deliberately NOT atomic, because the *) +(* doc's "takeover instant" residual lives in that gap. *) +(* :148-169 config precondition lease_ttl > publish_timeout + *) +(* clock_skew + margin, and clock_skew != 0 with quorum. *) +(* :519 max_execution_time = publish_timeout -- modelled as the *) +(* statement deadline `dl` and the ManAbort/WmAbort actions. *) +(* *) +(* native/csrc/catalog/clickhouse_client.cpp:374 *) +(* deciding_read() == {select_sequential_consistency = 1}. *) +(* Modelled by the constant Linearizable (see Views below). *) +(* *) +(* docs/catalog-descriptor-key.md :290-360, :304-314, :461-560, :655+ *) +(* src/dmi/storage/capture/clickhouse_lease.py :83-92, :198-210 *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS + Publishers, \* publish OPERATIONS (one pc each) + SelfRace, \* TRUE maps every Publisher onto ONE Writer, i.e. two + \* concurrent publish_snapshot() calls on one + \* ClickHouseCatalogWriter sharing one lease_id -- + \* the doc's "One writer racing itself" (:526). + Lids, \* the lease_id pool. `<` on these models ClickHouse's + \* UUID collation (doc :304-314 is explicit that it is + \* NOT text order); the protocol must be correct for ANY + \* total order, so claims pick their id nondeterministically + \* from the pool rather than in increasing order. + MaxTerm, MaxTime, MaxVersion, MaxAttempts, + TTL, \* lease_ttl_ns + PT, \* publish_timeout_ns == max_execution_time + SKEW, \* clock_skew_ns + NumChunks, \* manifest chunks per publish (catalog_writer.cpp:531) + Linearizable, \* TRUE = select_sequential_consistency=1 honoured + \* FALSE = a deciding read may MISS an accepted insert + AllowOverrun, \* TRUE models doc :503 "max_execution_time is checked + \* between processing blocks ... a statement blocked in a + \* lock can overrun it" + WriterLock, \* TRUE models the re-entrant writer lock (doc :539-543) + FreshPublishId \* TRUE = publish_id minted per call (catalog_writer.cpp:529) + +VARIABLES + rows, \* the append-only {prefix}_publisher_lease table. + \* NO UPDATE ANYWHERE: every action only ever adds. + settled, \* rows guaranteed visible to every replica + now, \* the SERVER clock (doc :317-320: expiries and the fence are + \* both stamped server-side) + lease, \* [Writers -> PublisherLease or NoLease] + pc, ret, ctm, clid, chunk, ver, att, + manifest, \* {prefix}_snapshot_manifest rows + wm, \* {prefix}_index_watermark rows + inflight, \* statements admitted (predicate evaluated) but not landed + used, \* lease_ids ever minted. new_uuid_v4() never repeats, and + \* two DISTINCT writers can never mint the same id -- only + \* a fork (SelfRace) shares one. + maxLanded, wmOutOfOrder + +vars == <> + +---------------------------------------------------------------------------- +(* helpers *) +SetMax(S) == IF S = {} THEN 0 ELSE CHOOSE x \in S : \A y \in S : y <= x +SetMin(S) == CHOOSE x \in S : \A y \in S : x <= y + +NoLease == [term |-> 0, lid |-> 0, exp |-> 0] + +(* Client writer objects. The PublisherLease object lives on the writer, + the program counter on the operation. *) +Writers == IF SelfRace THEN {"shared"} ELSE Publishers +WriterOf(p) == IF SelfRace THEN "shared" ELSE p + +(***************************************************************************) +(* THE STORE MODEL. *) +(* *) +(* Views is the set of table images a single deciding read may observe. *) +(* With select_sequential_consistency=1 (clickhouse_client.cpp:374) a read *) +(* sees every accepted row. Without it, the replica it lands on may be *) +(* behind: it sees everything already replicated (`settled`) and any *) +(* subset of what is accepted but still in flight. This is the single *) +(* load-bearing assumption of the whole safety argument -- doc :304 *) +(* "Where that safety comes from is the read-back" -- so it is a knob. *) +(***************************************************************************) +Views == IF Linearizable THEN {rows} + ELSE {V \in SUBSET rows : settled \subseteq V} + +(* head() -- lease_coordinator.cpp:144-165 *) +HTerm(V) == SetMax({r.term : r \in V}) +HeadSet(V) == {r \in V : r.term = HTerm(V)} +HLids(V) == {r.lid : r \in HeadSet(V)} +(* "A lease's expiry at a term is the MINIMUM expires_at_ns written under + its (term, lease_id)" -- doc :327-328, clickhouse_lease.py:83-92. This is + exactly what makes the release tombstone end the lease. *) +MinExpOf(V, l) == SetMin({r.exp : r \in {q \in HeadSet(V) : q.lid = l}}) +(* ORDER BY lease_id DESC -> the greatest id under the collation *) +TopLid(V) == SetMax(HLids(V)) +LiveUntil(V) == SetMax({MinExpOf(V, l) : l \in HLids(V)}) +NClaim(V) == Cardinality(HLids(V)) + +(* reject_live -- lease_coordinator.cpp:230-257. Returns (admits) iff the + whole head term is dead, or there is exactly ONE claimant at the head and + it is me. claimants > 1 quarantines the term until every claim at it + expires (doc :508 "Lease acquisition is not the window it looks like"). *) +RejectLivePasses(V, l) == + \/ LiveUntil(V) <= now + \/ (NClaim(V) = 1 /\ TopLid(V) = l) + +(* fence() -- lease_coordinator.cpp:167-180, doc :352-362. + ONE subquery reading ONE row (doc :378 explains why the two-subquery form + is unsound). The margin is publish cap PLUS host clock skew bound + (clickhouse_lease.py:198-210, the S - (b - a) >= 0 derivation). *) +FenceOk(V, l) == + /\ V # {} + /\ TopLid(V) = l + /\ MinExpOf(V, TopLid(V)) > now + PT + SKEW + +PubId(p) == IF FreshPublishId THEN <> ELSE <> + +Busy(w) == \E q \in Publishers : + WriterOf(q) = w /\ pc[q] \notin {"idle", "done", "failed"} + +MyStmt(p) == {s \in inflight : s.who = p} + +---------------------------------------------------------------------------- +Init == + /\ rows = {} /\ settled = {} /\ now = 0 + /\ lease = [w \in Writers |-> NoLease] + /\ pc = [p \in Publishers |-> "idle"] + /\ ret = [p \in Publishers |-> "idle"] + /\ ctm = [p \in Publishers |-> 0] + /\ clid = [p \in Publishers |-> 0] + /\ chunk = [p \in Publishers |-> 0] + /\ ver = [p \in Publishers |-> 0] + /\ att = [p \in Publishers |-> 0] + /\ manifest = {} /\ wm = {} /\ inflight = {} /\ used = {} + /\ maxLanded = 0 /\ wmOutOfOrder = FALSE + +(* The server clock. Bounded so the model closes. *) +Tick == + /\ now < MaxTime + /\ now' = now + 1 + /\ UNCHANGED <> + +(* Replication catching up. Only meaningful when ~Linearizable. *) +Settle == + /\ ~Linearizable + /\ \E r \in rows \ settled : settled' = settled \cup {r} + /\ UNCHANGED <> + +(* acquire_publisher_lease() then publish_snapshot(). + lease_coordinator.cpp:53-54: acquire() reuses the HELD lease_id and + otherwise mints a fresh UUID -- minted BEFORE the head read. *) +StartPublish(p) == + /\ pc[p] = "idle" + /\ att[p] < MaxAttempts + /\ WriterLock => ~Busy(WriterOf(p)) + /\ \/ /\ lease[WriterOf(p)].term > 0 + /\ clid' = [clid EXCEPT ![p] = lease[WriterOf(p)].lid] + /\ UNCHANGED used + \/ /\ lease[WriterOf(p)].term = 0 + /\ \E l \in Lids \ used : + /\ clid' = [clid EXCEPT ![p] = l] + /\ used' = used \cup {l} + /\ att' = [att EXCEPT ![p] = att[p] + 1] + /\ pc' = [pc EXCEPT ![p] = "claim_head"] + /\ ret' = [ret EXCEPT ![p] = "pub_alloc"] + /\ chunk' = [chunk EXCEPT ![p] = 0] + /\ UNCHANGED <> + +(* ---- claim: lease_coordinator.cpp:102-142, three round trips ---- *) + +(* Round trip 1: head() + reject_live. These are one query plus pure local + computation on its result, so nothing can interleave INSIDE them. + acquire() reuses the held lease_id, otherwise a fresh one (:53-54). *) +ClaimHead(p) == + LET w == WriterOf(p) IN + LET l == IF lease[w].term > 0 THEN lease[w].lid ELSE clid[p] IN + /\ pc[p] = "claim_head" + /\ \E V \in Views : + \/ /\ RejectLivePasses(V, l) + /\ HTerm(V) + 1 <= MaxTerm \* MODEL BOUND, not protocol + /\ ctm' = [ctm EXCEPT ![p] = HTerm(V) + 1] + /\ clid' = [clid EXCEPT ![p] = l] + /\ pc' = [pc EXCEPT ![p] = "claim_insert"] + /\ UNCHANGED lease + \/ /\ ~RejectLivePasses(V, l) \* throws kHeld; resets lease_ + /\ lease' = [lease EXCEPT ![w] = NoLease] + /\ pc' = [pc EXCEPT ![p] = "failed"] + /\ UNCHANGED <> + /\ UNCHANGED <> + +(* Round trip 2: the claim INSERT (:214-228). Append only. *) +ClaimInsert(p) == + /\ pc[p] = "claim_insert" + /\ LET r == [term |-> ctm[p], lid |-> clid[p], exp |-> now + TTL] IN + /\ rows' = rows \cup {r} + /\ settled' = IF Linearizable THEN settled \cup {r} ELSE settled + /\ pc' = [pc EXCEPT ![p] = "claim_read"] + /\ UNCHANGED <> + +(* Round trip 3: the singleton read-back (:115-137). THIS is where the + safety comes from, per doc :304-314 -- not from the fence. *) +ClaimRead(p) == + LET w == WriterOf(p) IN + /\ pc[p] = "claim_read" + /\ \E V \in Views : + LET mine == {q \in V : q.term = ctm[p]} IN + LET owners == {q.lid : q \in mine} IN + \/ /\ owners = {clid[p]} + /\ lease' = [lease EXCEPT ![w] = + [term |-> ctm[p], lid |-> clid[p], + exp |-> SetMin({q.exp : q \in mine})]] + /\ pc' = [pc EXCEPT ![p] = ret[p]] + \/ /\ owners # {clid[p]} \* :138-141, claim refused + /\ lease' = [lease EXCEPT ![w] = NoLease] + /\ pc' = [pc EXCEPT ![p] = "failed"] + /\ UNCHANGED <> + +(* release() -- lease_coordinator.cpp:70-90. A TOMBSTONE, not an UPDATE and + not a fenced head write: an already-expired row at the holder's OWN term, + so min(expires_at_ns) for that (term,lease_id) collapses to now. *) +Release(w) == + /\ lease[w].term > 0 + /\ ~Busy(w) + /\ LET r == [term |-> lease[w].term, lid |-> lease[w].lid, exp |-> now] IN + /\ rows' = rows \cup {r} + /\ settled' = IF Linearizable THEN settled \cup {r} ELSE settled + /\ lease' = [lease EXCEPT ![w] = NoLease] + /\ UNCHANGED <> + +(* ---- publish: catalog_writer.cpp:478-669 ---- *) + +PubAlloc(p) == + /\ pc[p] = "pub_alloc" + /\ SetMax({r.ver : r \in wm}) + 1 <= MaxVersion + /\ ver' = [ver EXCEPT ![p] = SetMax({r.ver : r \in wm}) + 1] + /\ pc' = [pc EXCEPT ![p] = IF NumChunks = 0 THEN "wm_admit" ELSE "man_next"] + /\ UNCHANGED <> + +ManNext(p) == + /\ pc[p] = "man_next" + /\ chunk' = [chunk EXCEPT ![p] = chunk[p] + 1] + /\ pc' = [pc EXCEPT ![p] = "man_admit"] + /\ UNCHANGED <> + +(* The fenced manifest INSERT (catalog_writer.cpp:533-547). A fence refusal + writes ZERO rows WITHOUT raising (doc :417) -- hence the else branch goes + straight to the read-back, which is what catches it. *) +ManAdmit(p) == + LET w == WriterOf(p) IN + /\ pc[p] = "man_admit" + /\ \E V \in Views : + \/ /\ lease[w].term > 0 /\ FenceOk(V, lease[w].lid) + /\ inflight' = inflight \cup + {[who |-> p, kind |-> "manifest", ver |-> ver[p], + pid |-> PubId(p), pack |-> chunk[p], dl |-> now + PT]} + /\ pc' = [pc EXCEPT ![p] = "man_land"] + \/ /\ ~(lease[w].term > 0 /\ FenceOk(V, lease[w].lid)) + /\ pc' = [pc EXCEPT ![p] = "man_read"] + /\ UNCHANGED inflight + /\ UNCHANGED <> + +ManLand(p) == + /\ pc[p] = "man_land" + /\ \E s \in MyStmt(p) : + /\ (now <= s.dl \/ AllowOverrun) + /\ manifest' = manifest \cup + {[ver |-> s.ver, pid |-> s.pid, pack |-> s.pack]} + /\ inflight' = inflight \ {s} + /\ pc' = [pc EXCEPT ![p] = "man_read"] + /\ UNCHANGED <> + +(* max_execution_time / timeout_overflow_mode=throw (catalog_writer.cpp:519) *) +ManAbort(p) == + /\ pc[p] = "man_land" + /\ ~AllowOverrun + /\ \E s \in MyStmt(p) : now > s.dl /\ inflight' = inflight \ {s} + /\ pc' = [pc EXCEPT ![p] = "failed"] + /\ UNCHANGED <> + +(* "Every conditional manifest INSERT is read back before the next renewal" + -- doc :416, catalog_writer.cpp:556-567. Then the renewal (:579). *) +ManRead(p) == + /\ pc[p] = "man_read" + /\ \/ /\ \E m \in manifest : + m.ver = ver[p] /\ m.pid = PubId(p) /\ m.pack = chunk[p] + /\ pc' = [pc EXCEPT ![p] = "claim_head"] + /\ ret' = [ret EXCEPT ![p] = + IF chunk[p] < NumChunks THEN "man_next" ELSE "wm_admit"] + \/ /\ ~\E m \in manifest : + m.ver = ver[p] /\ m.pid = PubId(p) /\ m.pack = chunk[p] + /\ pc' = [pc EXCEPT ![p] = "failed"] + /\ UNCHANGED ret + /\ UNCHANGED <> + +(* THE visibility write -- catalog_writer.cpp:583-606. Barrier AND fence AND + the INSERT are ONE server-side statement, so both predicates are evaluated + HERE, at admission. The row lands in WmLand, possibly later: doc :496 + "A's watermark statement must evaluate the fence before B's lease row + commits, and still be in flight when B publishes." *) +WmAdmit(p) == + LET w == WriterOf(p) IN + /\ pc[p] = "wm_admit" + /\ \E V \in Views : + \/ /\ SetMax({r.ver : r \in wm}) < ver[p] \* the version barrier + /\ lease[w].term > 0 /\ FenceOk(V, lease[w].lid) + /\ inflight' = inflight \cup + {[who |-> p, kind |-> "watermark", ver |-> ver[p], + pid |-> PubId(p), pack |-> 0, dl |-> now + PT]} + /\ pc' = [pc EXCEPT ![p] = "wm_land"] + \/ /\ ~( SetMax({r.ver : r \in wm}) < ver[p] + /\ lease[w].term > 0 /\ FenceOk(V, lease[w].lid) ) + /\ pc' = [pc EXCEPT ![p] = "wm_read"] + /\ UNCHANGED inflight + /\ UNCHANGED <> + +WmLand(p) == + /\ pc[p] = "wm_land" + /\ \E s \in MyStmt(p) : + /\ (now <= s.dl \/ AllowOverrun) + /\ wm' = wm \cup {[ver |-> s.ver, pid |-> s.pid]} + /\ inflight' = inflight \ {s} + /\ wmOutOfOrder' = (wmOutOfOrder \/ (s.ver <= maxLanded)) + /\ maxLanded' = SetMax({maxLanded, s.ver}) + /\ pc' = [pc EXCEPT ![p] = "wm_read"] + /\ UNCHANGED <> + +WmAbort(p) == + /\ pc[p] = "wm_land" + /\ ~AllowOverrun + /\ \E s \in MyStmt(p) : now > s.dl /\ inflight' = inflight \ {s} + /\ pc' = [pc EXCEPT ![p] = "failed"] + /\ UNCHANGED <> + +(* "Ownership, not occupancy" -- catalog_writer.cpp:608-628 *) +WmRead(p) == + /\ pc[p] = "wm_read" + /\ \/ /\ \E r \in wm : r.ver = ver[p] /\ r.pid = PubId(p) + /\ pc' = [pc EXCEPT ![p] = "done"] + \/ /\ ~\E r \in wm : r.ver = ver[p] /\ r.pid = PubId(p) + /\ pc' = [pc EXCEPT ![p] = "failed"] + /\ UNCHANGED <> + +Reset(p) == + /\ pc[p] \in {"done", "failed"} + /\ pc' = [pc EXCEPT ![p] = "idle"] + /\ UNCHANGED <> + +Next == + \/ Tick \/ Settle + \/ \E w \in Writers : Release(w) + \/ \E p \in Publishers : + \/ StartPublish(p) \/ ClaimHead(p) \/ ClaimInsert(p) \/ ClaimRead(p) + \/ PubAlloc(p) \/ ManNext(p) \/ ManAdmit(p) \/ ManLand(p) + \/ ManAbort(p) \/ ManRead(p) + \/ WmAdmit(p) \/ WmLand(p) \/ WmAbort(p) \/ WmRead(p) + \/ Reset(p) + +Spec == Init /\ [][Next]_vars + +---------------------------------------------------------------------------- +(***************************************************************************) +(* OBLIGATIONS *) +(***************************************************************************) + +WatermarkStmts == {s \in inflight : s.kind = "watermark"} + +(* A statement whose max_execution_time has passed is guaranteed to be + aborted by the server (timeout_overflow_mode = throw, + catalog_writer.cpp:519-520), so it can no longer make anything visible. + Counting it would be a MODELLING ARTIFACT: in this spec a statement sits + in `inflight` until its Abort action is scheduled, which the real server + does not allow. AllowOverrun removes the guarantee (doc :503: the cap is + "checked between processing blocks rather than pre-empted"). *) +CanStillLand(s) == AllowOverrun \/ now <= s.dl +LandableWmStmts == {s \in WatermarkStmts : CanStillLand(s)} + +(*-------------------------------------------------------------------------*) +(* 1. NoOverlappingAdmit -- THE safety property. *) +(* catalog_writer.cpp:525-528 ("a publisher whose lease was taken over *) +(* makes NO snapshot visible") and doc :335-350. *) +(* No two watermark-admitting statements are in flight at once. *) +(* EXPECTED: HOLDS with Linearizable /\ ~AllowOverrun. *) +(*-------------------------------------------------------------------------*) +NoOverlappingAdmit == Cardinality(LandableWmStmts) <= 1 + +(* The same property stated over distinct WRITERS, so that the "one writer + racing itself" configuration can be separated from the lease property. *) +NoOverlappingWriters == + \A s1, s2 \in WatermarkStmts : + WriterOf(s1.who) = WriterOf(s2.who) \/ s1 = s2 + +(*-------------------------------------------------------------------------*) +(* 2. WatermarkMonotonic -- index_watermark.index_version strictly *) +(* increases. doc :280-286 (the 1% residual) and :526 (one writer *) +(* racing itself: "an already-pinned watermark grew"). *) +(* EXPECTED: HOLDS with WriterLock; FAILS without it. *) +(*-------------------------------------------------------------------------*) +WatermarkMonotonic == ~wmOutOfOrder + +(*-------------------------------------------------------------------------*) +(* 3. CompleteManifest -- every visible watermark row has a complete *) +(* manifest behind it. catalog_writer.cpp:556-567, doc :416-419. *) +(* EXPECTED: HOLDS. *) +(*-------------------------------------------------------------------------*) +CompleteManifest == + \A r \in wm : \A c \in 1..NumChunks : + \E m \in manifest : m.ver = r.ver /\ m.pid = r.pid /\ m.pack = c + +(* and the other direction: the snapshot a reader assembles for a watermark + row is EXACTLY the packs that publish intended -- no orphan is ever + attributed to it. This is the non-vacuous half of obligation 5. *) +SnapshotExact == + \A r \in wm : \A m \in manifest : + (m.pid = r.pid) => (m.ver = r.ver /\ m.pack \in 1..NumChunks) + +(*-------------------------------------------------------------------------*) +(* 4. TwoBelieversIsSafe -- doc :516. *) +(* Believers: writers that hold a PublisherLease object they consider *) +(* live. The doc CLAIMS two can exist at once and that this is safe. *) +(*-------------------------------------------------------------------------*) +Believers == {w \in Writers : lease[w].term > 0 /\ lease[w].exp > now} + +(* Refutation target, STRONG reading of doc :516: two writers hold leases + that are BOTH unexpired on the server clock at the same instant. *) +AtMostOneBeliever == Cardinality(Believers) <= 1 + +(* Refutation target, WEAK reading of doc :516 -- and the one the doc's own + last sentence uses: '"only one publisher holds the lease" is not + literally true of the CLIENT OBJECTS, only of the row the fence + resolves.' A holder here is any writer still carrying a PublisherLease + object it has not been told it lost. *) +Holders == {w \in Writers : lease[w].term > 0} +AtMostOneHolder == Cardinality(Holders) <= 1 + +(* and the safety question asked of the weak reading *) +TwoHoldersIsSafe == + (Cardinality(Holders) > 1) => + /\ Cardinality({w \in Holders : FenceOk(rows, lease[w].lid)}) <= 1 + /\ Cardinality(LandableWmStmts) <= 1 + +(* The safety half: at most one believer can ever pass the fence, because + the fence resolves ONE lease at the head term (lease_coordinator.cpp:174 + ORDER BY lease_id DESC LIMIT 1). EXPECTED: HOLDS. *) +AtMostOneFenceable == + Cardinality({w \in Writers : + lease[w].term > 0 /\ FenceOk(rows, lease[w].lid)}) <= 1 + +TwoBelieversIsSafe == AtMostOneFenceable /\ NoOverlappingAdmit + +(*-------------------------------------------------------------------------*) +(* 5. OrphanManifestInert -- doc :465-487. *) +(* Orphans: manifest rows whose publish never wrote a watermark row. *) +(* Refutation target NoOrphanManifestRows is EXPECTED TO FAIL (the *) +(* weakening is real); SnapshotExact above is the inertness claim. *) +(*-------------------------------------------------------------------------*) +(* A manifest row with no watermark row is not yet an orphan if its publish + is still running -- that is just a publish in flight. A REAL orphan is + one whose publish has ENDED (refused at the watermark, or refused at the + renewal between the two statements) with no watermark row behind it. *) +LivePid(pid) == \E p \in Publishers : + PubId(p) = pid /\ pc[p] \notin {"idle", "done", "failed"} +Orphans == {m \in manifest : + ~LivePid(m.pid) /\ ~\E r \in wm : r.pid = m.pid} +NoOrphanManifestRows == Orphans = {} + +(* "no worse than documented": an orphan is always a PREFIX of a publish's + chunks -- the takeover cuts the loop, it does not scatter rows. *) +OrphansArePrefixes == + \A m \in Orphans : \A c \in 1..m.pack : + \E m2 \in manifest : m2.pid = m.pid /\ m2.pack = c + +(* Combined invariant used for the "everything at once" runs. *) +AllSafety == + /\ NoOverlappingAdmit + /\ WatermarkMonotonic + /\ CompleteManifest + /\ SnapshotExact + /\ AtMostOneFenceable + +(*-------------------------------------------------------------------------*) +(* VACUITY GUARDS. Each of these is an invariant we WANT TLC to refute: *) +(* the violation trace is the proof that the model actually reaches the *) +(* state the safety invariants are quantified over. An invariant that *) +(* holds only because its subject is unreachable proves nothing. *) +(*-------------------------------------------------------------------------*) +NeverPublishes == wm = {} \* refuted => snapshots do land +NeverFences == ~\E w \in Writers : + lease[w].term > 0 /\ FenceOk(rows, lease[w].lid) +NeverAdmits == LandableWmStmts = {} \* refuted => the fence admits +NeverContested == \A V \in {rows} : NClaim(V) <= 1 \* contested head +NeverTwoBelievers == Cardinality(Believers) <= 1 +(* two believers WHILE one of them is mid-flight in a visibility write *) +NoBelieverDuringAdmit == + ~(Cardinality(Holders) > 1 /\ LandableWmStmts # {}) + +(* model bound, used as a TLC state constraint *) +Bound == /\ now <= MaxTime + /\ HTerm(rows) <= MaxTerm +============================================================================= diff --git a/specs/tla/PublisherLease_base5.cfg b/specs/tla/PublisherLease_base5.cfg new file mode 100644 index 000000000..c83c0ade8 --- /dev/null +++ b/specs/tla/PublisherLease_base5.cfg @@ -0,0 +1,23 @@ +\* BASE MODEL: the protocol exactly as shipped. +\* Linearizable store (select_sequential_consistency=1, clickhouse_client.cpp:374), +\* max_execution_time enforced, writer lock held, fresh publish_id per call. +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2} + MaxTerm = 5 + MaxTime = 8 + MaxVersion = 2 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT AllSafety +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_base5_ovr.cfg b/specs/tla/PublisherLease_base5_ovr.cfg new file mode 100644 index 000000000..c40a2225f --- /dev/null +++ b/specs/tla/PublisherLease_base5_ovr.cfg @@ -0,0 +1,24 @@ +\* Non-vacuity guard for base5: the base5 constants with the statement cap +\* allowed to overrun (AllowOverrun TRUE). base5's AllSafety HOLDS means +\* something only if the takeover race is reachable at these constants; +\* this run reaches it. EXPECT: NoOverlappingAdmit VIOLATED. +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2} + MaxTerm = 5 + MaxTime = 8 + MaxVersion = 2 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = TRUE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NoOverlappingAdmit +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_believers.cfg b/specs/tla/PublisherLease_believers.cfg new file mode 100644 index 000000000..b158f71a4 --- /dev/null +++ b/specs/tla/PublisherLease_believers.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT AtMostOneBeliever +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_chunks2.cfg b/specs/tla/PublisherLease_chunks2.cfg new file mode 100644 index 000000000..ad29a3deb --- /dev/null +++ b/specs/tla/PublisherLease_chunks2.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 1 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 2 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT AllSafety +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_chunks2_orphans.cfg b/specs/tla/PublisherLease_chunks2_orphans.cfg new file mode 100644 index 000000000..77f96ebad --- /dev/null +++ b/specs/tla/PublisherLease_chunks2_orphans.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 1 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 2 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NoOrphanManifestRows +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_chunks2_prefix.cfg b/specs/tla/PublisherLease_chunks2_prefix.cfg new file mode 100644 index 000000000..6a4a8efd6 --- /dev/null +++ b/specs/tla/PublisherLease_chunks2_prefix.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 1 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 2 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT OrphansArePrefixes +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_holders.cfg b/specs/tla/PublisherLease_holders.cfg new file mode 100644 index 000000000..3368391f4 --- /dev/null +++ b/specs/tla/PublisherLease_holders.cfg @@ -0,0 +1,23 @@ +\* BASE MODEL: the protocol exactly as shipped. +\* Linearizable store (select_sequential_consistency=1, clickhouse_client.cpp:374), +\* max_execution_time enforced, writer lock held, fresh publish_id per call. +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT AtMostOneHolder +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_holderssafe.cfg b/specs/tla/PublisherLease_holderssafe.cfg new file mode 100644 index 000000000..4c23dc49f --- /dev/null +++ b/specs/tla/PublisherLease_holderssafe.cfg @@ -0,0 +1,23 @@ +\* BASE MODEL: the protocol exactly as shipped. +\* Linearizable store (select_sequential_consistency=1, clickhouse_client.cpp:374), +\* max_execution_time enforced, writer lock held, fresh publish_id per call. +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT TwoHoldersIsSafe +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_nonlin_admit.cfg b/specs/tla/PublisherLease_nonlin_admit.cfg new file mode 100644 index 000000000..ffa80b883 --- /dev/null +++ b/specs/tla/PublisherLease_nonlin_admit.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2} + MaxTerm = 2 + MaxTime = 3 + MaxVersion = 1 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = FALSE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NoOverlappingAdmit +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_nonlin_all.cfg b/specs/tla/PublisherLease_nonlin_all.cfg new file mode 100644 index 000000000..a70cc8ec0 --- /dev/null +++ b/specs/tla/PublisherLease_nonlin_all.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2} + MaxTerm = 2 + MaxTime = 3 + MaxVersion = 1 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = FALSE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT AllSafety +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_nonlin_fence.cfg b/specs/tla/PublisherLease_nonlin_fence.cfg new file mode 100644 index 000000000..0ece10bd1 --- /dev/null +++ b/specs/tla/PublisherLease_nonlin_fence.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2} + MaxTerm = 2 + MaxTime = 3 + MaxVersion = 1 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = FALSE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT AtMostOneFenceable +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_noovr0.cfg b/specs/tla/PublisherLease_noovr0.cfg new file mode 100644 index 000000000..b9c2203e6 --- /dev/null +++ b/specs/tla/PublisherLease_noovr0.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 4 + MaxTime = 8 + MaxVersion = 2 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 0 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NoOverlappingAdmit +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_noovr1.cfg b/specs/tla/PublisherLease_noovr1.cfg new file mode 100644 index 000000000..0332c8b97 --- /dev/null +++ b/specs/tla/PublisherLease_noovr1.cfg @@ -0,0 +1,24 @@ +\* noovr0's constants with ONE manifest chunk instead of an empty-refs +\* publish, cap enforced. EXPECT: NoOverlappingAdmit HOLDS. Its partner +\* PublisherLease_ovr1.cfg (the same with AllowOverrun) is refuted, so this +\* HOLDS is not vacuous. About 15M states: a manual run, not in check.sh. +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 4 + MaxTime = 8 + MaxVersion = 2 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NoOverlappingAdmit +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_orphans.cfg b/specs/tla/PublisherLease_orphans.cfg new file mode 100644 index 000000000..2f1600cdf --- /dev/null +++ b/specs/tla/PublisherLease_orphans.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NoOrphanManifestRows +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_overrun.cfg b/specs/tla/PublisherLease_overrun.cfg new file mode 100644 index 000000000..3eb1152ef --- /dev/null +++ b/specs/tla/PublisherLease_overrun.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = TRUE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NoOverlappingAdmit +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_ovr0.cfg b/specs/tla/PublisherLease_ovr0.cfg new file mode 100644 index 000000000..a38da1d8a --- /dev/null +++ b/specs/tla/PublisherLease_ovr0.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 4 + MaxTime = 8 + MaxVersion = 2 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 0 + Linearizable = TRUE + AllowOverrun = TRUE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NoOverlappingAdmit +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_ovr1.cfg b/specs/tla/PublisherLease_ovr1.cfg new file mode 100644 index 000000000..7519c5d7f --- /dev/null +++ b/specs/tla/PublisherLease_ovr1.cfg @@ -0,0 +1,22 @@ +\* noovr1 with the statement cap allowed to overrun (AllowOverrun TRUE): +\* the non-vacuity guard for noovr1. EXPECT: NoOverlappingAdmit VIOLATED. +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 4 + MaxTime = 8 + MaxVersion = 2 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = TRUE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NoOverlappingAdmit +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_selfrace.cfg b/specs/tla/PublisherLease_selfrace.cfg new file mode 100644 index 000000000..cada91a4e --- /dev/null +++ b/specs/tla/PublisherLease_selfrace.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = TRUE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = FALSE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT WatermarkMonotonic +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_selfracelocked.cfg b/specs/tla/PublisherLease_selfracelocked.cfg new file mode 100644 index 000000000..27bdd8bc1 --- /dev/null +++ b/specs/tla/PublisherLease_selfracelocked.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = TRUE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT AllSafety +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_stalepid.cfg b/specs/tla/PublisherLease_stalepid.cfg new file mode 100644 index 000000000..42467b67c --- /dev/null +++ b/specs/tla/PublisherLease_stalepid.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 2 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = FALSE +CONSTRAINT Bound +INVARIANT AllSafety +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_vac0.cfg b/specs/tla/PublisherLease_vac0.cfg new file mode 100644 index 000000000..3179c6883 --- /dev/null +++ b/specs/tla/PublisherLease_vac0.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 4 + MaxTime = 8 + MaxVersion = 2 + MaxAttempts = 1 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 0 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NeverAdmits +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_vac_admit.cfg b/specs/tla/PublisherLease_vac_admit.cfg new file mode 100644 index 000000000..f51a0e555 --- /dev/null +++ b/specs/tla/PublisherLease_vac_admit.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NeverAdmits +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_vac_bothadmit.cfg b/specs/tla/PublisherLease_vac_bothadmit.cfg new file mode 100644 index 000000000..ece14eb22 --- /dev/null +++ b/specs/tla/PublisherLease_vac_bothadmit.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NoBelieverDuringAdmit +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_vac_contested.cfg b/specs/tla/PublisherLease_vac_contested.cfg new file mode 100644 index 000000000..b16a4c004 --- /dev/null +++ b/specs/tla/PublisherLease_vac_contested.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NeverContested +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_vac_fence.cfg b/specs/tla/PublisherLease_vac_fence.cfg new file mode 100644 index 000000000..8db6c1ea5 --- /dev/null +++ b/specs/tla/PublisherLease_vac_fence.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NeverFences +CHECK_DEADLOCK FALSE diff --git a/specs/tla/PublisherLease_vac_publish.cfg b/specs/tla/PublisherLease_vac_publish.cfg new file mode 100644 index 000000000..46b681ce6 --- /dev/null +++ b/specs/tla/PublisherLease_vac_publish.cfg @@ -0,0 +1,20 @@ +SPECIFICATION Spec +CONSTANTS + Publishers = {p1, p2} + SelfRace = FALSE + Lids = {1, 2, 3} + MaxTerm = 3 + MaxTime = 5 + MaxVersion = 2 + MaxAttempts = 2 + TTL = 2 + PT = 1 + SKEW = 0 + NumChunks = 1 + Linearizable = TRUE + AllowOverrun = FALSE + WriterLock = TRUE + FreshPublishId = TRUE +CONSTRAINT Bound +INVARIANT NeverPublishes +CHECK_DEADLOCK FALSE diff --git a/specs/tla/VersionAllocator.tla b/specs/tla/VersionAllocator.tla new file mode 100644 index 000000000..0b3afa49f --- /dev/null +++ b/specs/tla/VersionAllocator.tla @@ -0,0 +1,277 @@ +-------------------------- MODULE VersionAllocator -------------------------- +(***************************************************************************) +(* A TLA+ model of the DMI "sole-claimant" catalog version allocator. *) +(* *) +(* SOURCE OF TRUTH *) +(* native/csrc/catalog/version_allocator.cpp:49-89 (allocate_version) *) +(* native/csrc/catalog/version_allocator.h:5-7 (the claim we check) *) +(* native/csrc/catalog/clickhouse_client.cpp:374 (deciding_read) *) +(* native/csrc/catalog/catalog_writer.cpp:583-628 (watermark publish) *) +(* *) +(* The C++ loop, verbatim in structure: *) +(* *) +(* for (attempt = 0; attempt < allocation_attempts; ++attempt) { *) +(* claimed = max_version("capture_version_claims","version"); //:52*) +(* floor = max(claimed, max_version("index_watermark",...)); //:53*) +(* spread = attempt == 0 ? 0 : rng() % (8*attempt + 1); //:57*) +(* candidate = floor + 1 + spread; //:61*) +(* INSERT (candidate, claim_id) with insert_quorum; //:63*) +(* owners = SELECT claim_id WHERE version = candidate; //:72*) +(* if (owners == {claim_id}) return candidate; //:79*) +(* } *) +(* throw CatalogError(kAllocation, ...); //:85*) +(* *) +(* Both reads carry deciding_read() = select_sequential_consistency=1. *) +(* The whole point of this spec is to ask what that setting buys and what *) +(* it does NOT buy. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets, TLC + +CONSTANTS + Allocators, \* the concurrent allocator processes (one per driver process) + MaxVersion, \* version ceiling -- a STATE-SPACE BOUND, not in the code + Attempts, \* AllocatorConfig::allocation_attempts (16 in production) + MaxSpread, \* bound on the jitter; the code's bound is 8*attempt + Mode \* store consistency model, one of: + \* "Linearizable" -- a read sees every insert that + \* completed before it. What + \* select_sequential_consistency=1 + \* is claimed to buy. + \* "EventuallyConsistent"-- each reader has its OWN stale + \* view: two allocators can be + \* reading different replicas at + \* different points. + \* "SharedStaleFrontier" -- a weaker-than-linearizable but + \* SINGLE global lag: all readers + \* share one prefix. Kept because + \* it is a strictly stronger store + \* than #2 and the results differ. + +(***************************************************************************) +(* One claim_id per (process, attempt): the code mints a fresh uuid_v4 on *) +(* every attempt (version_allocator.cpp:62), so ids never repeat. *) +(***************************************************************************) +ClaimIds == Allocators \X (0 .. Attempts - 1) + +VARIABLES + at, \* ClaimIds -> 0..MaxVersion. The append-only claims table. + \* at[c] = 0 means "this row was never inserted". + seen, \* Allocators -> SUBSET ClaimIds. PER-READER visibility: the + \* rows THIS allocator's deciding reads can observe. + \* Linearizable: an insert enters every allocator's view in the + \* same step, so seen[a] = Inserted for all a, always. + \* EventuallyConsistent: a row is accepted (lands in `at`) but + \* enters one allocator's view at a time, via Reveal. Each + \* reader therefore observes its own arbitrary subset of the + \* accepted inserts. + \* SharedStaleFrontier: Reveal adds the row to EVERY view at + \* once -- one global lag instead of per-replica lag. + pc, \* Allocators -> control point inside allocate_version + attempt, \* Allocators -> the loop counter, 0-based like the C++ + cand, \* Allocators -> the candidate currently being tried + ret, \* Allocators -> value returned by allocate_version (0 = none) + retPubMax, \* Allocators -> max(index_version) published at the INSTANT + \* this allocator returned. Snapshotted so FloorMonotonic can + \* be phrased as a state invariant. + published \* SUBSET (1..MaxVersion). Rows in {prefix}_index_watermark. + +vars == <> + +Max2(x, y) == IF x > y THEN x ELSE y +MaxOf(S) == CHOOSE x \in S : \A y \in S : y <= x + +Inserted == { c \in ClaimIds : at[c] # 0 } \* durably accepted rows +Visible(a) == { c \in Inserted : c \in seen[a] } \* what a's reads return + +\* max_version("capture_version_claims","version") -- version_allocator.cpp:52 +MaxClaimVersion(a) == + IF Visible(a) = {} THEN 0 ELSE MaxOf({ at[c] : c \in Visible(a) }) +\* max_version("index_watermark","index_version") -- version_allocator.cpp:54 +MaxPublished == IF published = {} THEN 0 ELSE MaxOf(published) + +\* spread -- version_allocator.cpp:57-60. 0 on the first attempt, otherwise +\* uniform in [0, 8*attempt]. We bound it by MaxSpread to close the model. +Spreads(k) == IF k = 0 THEN {0} ELSE 0 .. MaxSpread + +TypeOK == + /\ at \in [ClaimIds -> 0 .. MaxVersion] + /\ seen \in [Allocators -> SUBSET ClaimIds] + /\ pc \in [Allocators -> {"idle","picked","inserted","done","failed", + "published","refused"}] + /\ attempt \in [Allocators -> 0 .. Attempts - 1] + /\ cand \in [Allocators -> 0 .. MaxVersion] + /\ ret \in [Allocators -> 0 .. MaxVersion] + /\ retPubMax \in [Allocators -> 0 .. MaxVersion] + /\ published \subseteq (1 .. MaxVersion) + +Init == + /\ at = [c \in ClaimIds |-> 0] + /\ seen = [a \in Allocators |-> {}] + /\ pc = [a \in Allocators |-> "idle"] + /\ attempt = [a \in Allocators |-> 0] + /\ cand = [a \in Allocators |-> 0] + /\ ret = [a \in Allocators |-> 0] + /\ retPubMax = [a \in Allocators |-> 0] + /\ published = {} + +(***************************************************************************) +(* Pick: the two deciding reads that compute `floor`, plus the choice of *) +(* jitter. version_allocator.cpp:52-61. *) +(* *) +(* MODELLING NOTE: the code does TWO separate reads (claims, then the *) +(* watermark); we take them in one atomic step. Both quantities are *) +(* monotonically non-decreasing, so splitting them could only yield a *) +(* floor <= the atomic one -- i.e. a staler floor. Since every property *) +(* that can be broken by a stale floor is already broken in this model *) +(* (see FloorMonotonic), the merge hides nothing we go on to claim. *) +(***************************************************************************) +Pick(a) == + /\ pc[a] = "idle" + /\ LET fl == Max2(MaxClaimVersion(a), MaxPublished) IN + \E s \in Spreads(attempt[a]) : + /\ fl + 1 + s <= MaxVersion \* STATE-SPACE BOUND, see report + /\ cand' = [cand EXCEPT ![a] = fl + 1 + s] + /\ pc' = [pc EXCEPT ![a] = "picked"] + /\ UNCHANGED <> + +(***************************************************************************) +(* Insert: the quorum INSERT of (candidate, claim_id). *) +(* version_allocator.cpp:63-71 + quorum_write() at :32-38. *) +(***************************************************************************) +Insert(a) == + /\ pc[a] = "picked" + /\ LET c == <> IN + /\ at' = [at EXCEPT ![c] = cand[a]] + /\ seen' = IF Mode = "Linearizable" + THEN [b \in Allocators |-> seen[b] \cup {c}] + ELSE seen + /\ pc' = [pc EXCEPT ![a] = "inserted"] + /\ UNCHANGED <> + +(***************************************************************************) +(* Reveal: an accepted-but-not-yet-visible row becomes readable. Disabled *) +(* under Linearizable. This is precisely what *) +(* select_sequential_consistency=1 (clickhouse_client.cpp:374) is supposed *) +(* to rule out: a replica answering a read from behind the quorum. *) +(* *) +(* EventuallyConsistent reveals the row to ONE allocator -- two allocators *) +(* can be talking to replicas at different points. SharedStaleFrontier *) +(* reveals it to ALL at once -- the store lags, but every reader lags by *) +(* the same amount. The difference decides obligation 3; see the report. *) +(***************************************************************************) +Reveal == + /\ Mode # "Linearizable" + /\ \E c \in Inserted : + IF Mode = "SharedStaleFrontier" + THEN /\ \E b \in Allocators : c \notin seen[b] + /\ seen' = [b \in Allocators |-> seen[b] \cup {c}] + ELSE \E b \in Allocators : + /\ c \notin seen[b] + /\ seen' = [seen EXCEPT ![b] = seen[b] \cup {c}] + /\ UNCHANGED <> + +(***************************************************************************) +(* ReadBack: the deciding read of every claim_id at `candidate`, and the *) +(* ownership test. version_allocator.cpp:72-84, and the budget throw at *) +(* :85-88. *) +(***************************************************************************) +ReadBack(a) == + /\ pc[a] = "inserted" + /\ LET me == <> + owners == { c \in Visible(a) : at[c] = cand[a] } + IN IF owners = {me} + THEN /\ pc' = [pc EXCEPT ![a] = "done"] + /\ ret' = [ret EXCEPT ![a] = cand[a]] + /\ retPubMax' = [retPubMax EXCEPT ![a] = MaxPublished] + /\ UNCHANGED attempt + ELSE /\ UNCHANGED <> + /\ IF attempt[a] = Attempts - 1 + THEN /\ pc' = [pc EXCEPT ![a] = "failed"] \* throws + /\ UNCHANGED attempt + ELSE /\ pc' = [pc EXCEPT ![a] = "idle"] + /\ attempt' = [attempt EXCEPT ![a] = attempt[a] + 1] + /\ UNCHANGED <> + +(***************************************************************************) +(* Publish: the conditional watermark INSERT the caller runs with the *) +(* allocated version. catalog_writer.cpp:587-596 guards it with *) +(* coalesce((SELECT max(index_version) FROM index_watermark),0) < V *) +(* and the read-back at :611-627 turns a refusal into kPublishRace. *) +(* This action is NOT part of the allocator; it is here so obligation 4 *) +(* (FloorMonotonic) has something to be about. *) +(***************************************************************************) +Publish(a) == + /\ pc[a] = "done" + /\ IF ret[a] > MaxPublished + THEN /\ published' = published \cup {ret[a]} + /\ pc' = [pc EXCEPT ![a] = "published"] + ELSE /\ UNCHANGED published + /\ pc' = [pc EXCEPT ![a] = "refused"] \* kPublishRace + /\ UNCHANGED <> + +Next == \/ \E a \in Allocators : Pick(a) \/ Insert(a) \/ ReadBack(a) \/ Publish(a) + \/ Reveal + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* OBLIGATIONS *) +----------------------------------------------------------------------------- + +(***************************************************************************) +(* O1 Distinct -- the protocol's ACTUAL guarantee. *) +(* version_allocator.h:5-7: "proceed only as the sole claimant". *) +(* EXPECTED: TRUE under Linearizable, FALSE under EventuallyConsistent *) +(* (see the report for the SharedStaleFrontier surprise). *) +(***************************************************************************) +Distinct == + \A a, b \in Allocators : + (a # b /\ ret[a] # 0 /\ ret[b] # 0) => ret[a] # ret[b] + +(***************************************************************************) +(* O2 SoleRow -- the claim people MISREAD the header as making: *) +(* "exactly one claim row stands at a returned version". *) +(* EXPECTED: FALSE, even under Linearizable. A loser's INSERT can *) +(* land after the winner's read-back. This is the invariant *) +(* tests/test_native_catalog_lease_live.py:653-662 says is false *) +(* ("DURABLY CLAIMED, not solely claimed"; the test's docstring at *) +(* :605-609 makes the same point). *) +(***************************************************************************) +SoleRow == + \A a \in Allocators : + ret[a] # 0 => Cardinality({ c \in Inserted : at[c] = ret[a] }) = 1 + +(***************************************************************************) +(* O3 FloorMonotonic -- no returned version is <= a published *) +(* index_version at the moment it is returned. *) +(* EXPECTED: FALSE. floor is read, not held; the watermark can *) +(* overtake it before the read-back. catalog_writer.cpp:595 is the *) +(* guard that actually enforces monotonicity, not the allocator. *) +(***************************************************************************) +FloorMonotonic == + \A a \in Allocators : ret[a] # 0 => ret[a] > retPubMax[a] + +(***************************************************************************) +(* O4 NoPublishRefused -- a returned version is always publishable. *) +(* EXPECTED: FALSE, and it is the same race as O3 seen downstream: *) +(* the conditional INSERT at catalog_writer.cpp:595 refuses, and *) +(* :611-627 raises kPublishRace. *) +(***************************************************************************) +NoPublishRefused == \A a \in Allocators : pc[a] # "refused" + +(***************************************************************************) +(* O5 NoBudgetExhaustion -- nobody burns the whole attempt budget. *) +(* EXPECTED: FALSE. version_allocator.cpp:85 throws kAllocation. *) +(***************************************************************************) +NoBudgetExhaustion == \A a \in Allocators : pc[a] # "failed" + +(***************************************************************************) +(* VACUITY PROBE -- is the artificial MaxVersion ceiling ever reached? *) +(* If TLC reports NO violation of this, the ceiling never blocked a Pick *) +(* and the bound cannot have hidden behaviour. *) +(***************************************************************************) +CeilingNeverBinds == + \A a \in Allocators : + pc[a] = "idle" => Max2(MaxClaimVersion(a), MaxPublished) + 1 <= MaxVersion + +============================================================================= diff --git a/specs/tla/ec_distinct.cfg b/specs/tla/ec_distinct.cfg new file mode 100644 index 000000000..a7e496d21 --- /dev/null +++ b/specs/tla/ec_distinct.cfg @@ -0,0 +1,11 @@ +\* ec_distinct -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2} + MaxVersion = 5 + Attempts = 3 + MaxSpread = 1 + Mode = "EventuallyConsistent" +INVARIANTS + TypeOK + Distinct diff --git a/specs/tla/frontier_distinct.cfg b/specs/tla/frontier_distinct.cfg new file mode 100644 index 000000000..31089dc8e --- /dev/null +++ b/specs/tla/frontier_distinct.cfg @@ -0,0 +1,11 @@ +\* frontier_distinct -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2} + MaxVersion = 5 + Attempts = 3 + MaxSpread = 1 + Mode = "SharedStaleFrontier" +INVARIANTS + TypeOK + Distinct diff --git a/specs/tla/lin_budget.cfg b/specs/tla/lin_budget.cfg new file mode 100644 index 000000000..719579f85 --- /dev/null +++ b/specs/tla/lin_budget.cfg @@ -0,0 +1,11 @@ +\* lin_budget -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2, a3} + MaxVersion = 6 + Attempts = 3 + MaxSpread = 1 + Mode = "Linearizable" +INVARIANTS + TypeOK + NoBudgetExhaustion diff --git a/specs/tla/lin_ceiling.cfg b/specs/tla/lin_ceiling.cfg new file mode 100644 index 000000000..20b2a5246 --- /dev/null +++ b/specs/tla/lin_ceiling.cfg @@ -0,0 +1,11 @@ +\* lin_ceiling -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2, a3} + MaxVersion = 6 + Attempts = 3 + MaxSpread = 1 + Mode = "Linearizable" +INVARIANTS + TypeOK + CeilingNeverBinds diff --git a/specs/tla/lin_distinct.cfg b/specs/tla/lin_distinct.cfg new file mode 100644 index 000000000..6bd134260 --- /dev/null +++ b/specs/tla/lin_distinct.cfg @@ -0,0 +1,11 @@ +\* lin_distinct -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2, a3} + MaxVersion = 6 + Attempts = 3 + MaxSpread = 1 + Mode = "Linearizable" +INVARIANTS + TypeOK + Distinct diff --git a/specs/tla/lin_floor.cfg b/specs/tla/lin_floor.cfg new file mode 100644 index 000000000..525fe72ce --- /dev/null +++ b/specs/tla/lin_floor.cfg @@ -0,0 +1,11 @@ +\* lin_floor -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2, a3} + MaxVersion = 6 + Attempts = 3 + MaxSpread = 1 + Mode = "Linearizable" +INVARIANTS + TypeOK + FloorMonotonic diff --git a/specs/tla/lin_publish.cfg b/specs/tla/lin_publish.cfg new file mode 100644 index 000000000..ba145a198 --- /dev/null +++ b/specs/tla/lin_publish.cfg @@ -0,0 +1,11 @@ +\* lin_publish -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2, a3} + MaxVersion = 6 + Attempts = 3 + MaxSpread = 1 + Mode = "Linearizable" +INVARIANTS + TypeOK + NoPublishRefused diff --git a/specs/tla/lin_solerow.cfg b/specs/tla/lin_solerow.cfg new file mode 100644 index 000000000..032f662e8 --- /dev/null +++ b/specs/tla/lin_solerow.cfg @@ -0,0 +1,11 @@ +\* lin_solerow -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2, a3} + MaxVersion = 6 + Attempts = 3 + MaxSpread = 1 + Mode = "Linearizable" +INVARIANTS + TypeOK + SoleRow diff --git a/specs/tla/nocap3_ceiling.cfg b/specs/tla/nocap3_ceiling.cfg new file mode 100644 index 000000000..af93932d3 --- /dev/null +++ b/specs/tla/nocap3_ceiling.cfg @@ -0,0 +1,11 @@ +\* nocap3_ceiling -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2, a3} + MaxVersion = 18 + Attempts = 3 + MaxSpread = 1 + Mode = "Linearizable" +INVARIANTS + TypeOK + CeilingNeverBinds diff --git a/specs/tla/nocap3_distinct.cfg b/specs/tla/nocap3_distinct.cfg new file mode 100644 index 000000000..c0888c252 --- /dev/null +++ b/specs/tla/nocap3_distinct.cfg @@ -0,0 +1,11 @@ +\* nocap3_distinct -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2, a3} + MaxVersion = 18 + Attempts = 3 + MaxSpread = 1 + Mode = "Linearizable" +INVARIANTS + TypeOK + Distinct diff --git a/specs/tla/nocap_ceiling.cfg b/specs/tla/nocap_ceiling.cfg new file mode 100644 index 000000000..f34bc4e70 --- /dev/null +++ b/specs/tla/nocap_ceiling.cfg @@ -0,0 +1,11 @@ +\* nocap_ceiling -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2} + MaxVersion = 12 + Attempts = 3 + MaxSpread = 1 + Mode = "Linearizable" +INVARIANTS + TypeOK + CeilingNeverBinds diff --git a/specs/tla/nocap_distinct.cfg b/specs/tla/nocap_distinct.cfg new file mode 100644 index 000000000..f929e0291 --- /dev/null +++ b/specs/tla/nocap_distinct.cfg @@ -0,0 +1,11 @@ +\* nocap_distinct -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2} + MaxVersion = 12 + Attempts = 3 + MaxSpread = 1 + Mode = "Linearizable" +INVARIANTS + TypeOK + Distinct diff --git a/specs/tla/nocap_ec.cfg b/specs/tla/nocap_ec.cfg new file mode 100644 index 000000000..d3f8ddca8 --- /dev/null +++ b/specs/tla/nocap_ec.cfg @@ -0,0 +1,11 @@ +\* nocap_ec -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2} + MaxVersion = 12 + Attempts = 3 + MaxSpread = 1 + Mode = "EventuallyConsistent" +INVARIANTS + TypeOK + Distinct diff --git a/specs/tla/nocapf_ceiling.cfg b/specs/tla/nocapf_ceiling.cfg new file mode 100644 index 000000000..273c149f9 --- /dev/null +++ b/specs/tla/nocapf_ceiling.cfg @@ -0,0 +1,11 @@ +\* nocapf_ceiling -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2} + MaxVersion = 12 + Attempts = 3 + MaxSpread = 1 + Mode = "SharedStaleFrontier" +INVARIANTS + TypeOK + CeilingNeverBinds diff --git a/specs/tla/nocapf_distinct.cfg b/specs/tla/nocapf_distinct.cfg new file mode 100644 index 000000000..6a8dabb47 --- /dev/null +++ b/specs/tla/nocapf_distinct.cfg @@ -0,0 +1,11 @@ +\* nocapf_distinct -- see the obligation comment in VersionAllocator.tla +SPECIFICATION Spec +CONSTANTS + Allocators = {a1, a2} + MaxVersion = 12 + Attempts = 3 + MaxSpread = 1 + Mode = "SharedStaleFrontier" +INVARIANTS + TypeOK + Distinct diff --git a/specs/z3/clock_skew.py b/specs/z3/clock_skew.py new file mode 100644 index 000000000..f78ce86d4 --- /dev/null +++ b/specs/z3/clock_skew.py @@ -0,0 +1,223 @@ +#!/usr/bin/env python3 +"""Two-host clock-skew bound for the fenced watermark INSERT. + +Discharges the derivation in docs/catalog-descriptor-key.md:365-372, which the +document files under "Verification this repository cannot run" (:680-711) +because reproducing it was believed to need two hosts with a stepped clock. + +The fence predicate (docs/catalog-descriptor-key.md:352-362, emitted by +native/csrc/catalog/catalog_writer.cpp:583) admits the holder's watermark +statement only while + + expires_at_ns > now64() + publish_timeout_ns + clock_skew_ns + +evaluated on the holder's host, and native/csrc/catalog/catalog_writer.cpp:519 +caps that statement at max_execution_time = publish_timeout_ns on the same +host. A successor may claim once ITS host's clock passes expires_at_ns. + +Model. One true time line. Host A (holder) reads true time + a, host B +(successor) reads true time + b; d = b - a is the step between them. Clock +RATES are equal -- the fence is stamped and evaluated server-side, so only the +offset matters. All quantities are reals: no discretisation, no bound on the +magnitudes. + + p publish_timeout_ns (= max_execution_time) + S clock_skew_ns, the DECLARED bound carried in the fence margin + e expires_at_ns, as stamped on host A's clock + t_adm true time at which A's statement is admitted + t_end true time at which A's statement stops running + t_claim true time at which B's claim becomes possible + +Overlap -- the unsafety the bound is supposed to exclude -- is B claiming +while A's admitted statement is still in flight. + +Expected: UNSAT for d <= S (no overlap exists, for any p, S, e and any +schedule), SAT for d > S (the documented race is reachable). UNSAT is a proof +over all timings, which is strictly more than a two-host experiment can show. + +Second obligation: the default START WAIT. #150's commit 204a8d2 ("Count +clock skew in the default start wait") changed the default in +src/dmi/storage/native_capture.py:374-378 from + + lease_ttl_s + publish_timeout_s +to + lease_ttl_s + publish_timeout_s + clock_skew_s + +and the config comment at :270-280 states when that wait suffices: + + "None waits lease_ttl_s + publish_timeout_s + clock_skew_s; 0 fails at + once. That is guaranteed to outlast a crashed predecessor only when its + TTL is at most lease_ttl_s + publish_timeout_s: clock_skew_s cancels, + since the wait adds it and a lagging replica sees the row live that + much longer" + +start_wait_constraints() below encodes that claim against the code that +decides it: the successor gives up at start + start_lease_wait_ns +(native/csrc/catalog/storage_service.cpp:662-690, a steady-clock deadline), +and a claim is refused while the predecessor's row still reads live under +LeaseCoordinator::reject_live -- head.live_until_ns > head.now_ns, with BOTH +sides of that comparison stamped by the ClickHouse replica serving the read +(native/csrc/catalog/lease_coordinator.cpp:148-163, :232). The skew that +matters here is therefore between REPLICAS, not between DMI hosts: the +predecessor's expires_at_ns was stamped on the replica that took its INSERT, +and the successor's now64() comes from whichever replica answers head(). +""" +from z3 import And, Reals, Solver, sat, unsat + + +def overlap_constraints(s, d_vs_S): + p, S, e, a, b, d, t_adm, t_end, t_claim = Reals( + "p S e a b d t_adm t_end t_claim") + + # Configuration is non-degenerate: catalog_writer.cpp:132-147 requires a + # positive publish timeout, and the declared skew bound is unsigned + # (clock_skew_ns, catalog_writer.h:36), so never negative. + s.add(p > 0, S >= 0) + + # B's host is stepped ahead of A's by d. + s.add(b == a + d, d >= 0) + + # The fence admits A's statement only while more than p + S of lease life + # remains ON A'S OWN CLOCK. A's clock reads (true time + a). + s.add(e - (t_adm + a) > p + S) + + # max_execution_time caps the admitted statement at p, measured on the same + # clock. Equal rates, so p of A-clock time is p of true time. + s.add(t_end <= t_adm + p) + + # B may claim only once B's clock has passed the recorded expiry. + s.add(t_claim + b >= e) + + # THE UNSAFE STATE: B claims while A's statement is still in flight. + s.add(t_claim < t_end) + + s.add(d_vs_S(d, S)) + return d, S + + +def start_wait_constraints(s, extra): + """Can a crashed predecessor outlast the successor's default start wait? + + One true time line. The replica that stamped the predecessor's lease row + reads true time + ra; the replica answering the successor's head() reads + true time + rb. d = ra - rb is the step between them; |d| <= S, the + DECLARED bound, is the hypothesis under test. Rates are equal -- both + stamps come from now64(9) server-side -- so only the offset matters. + + All in seconds, as ClickHouseCatalogConfig takes them: + + Tp the PREDECESSOR's lease TTL + Ts the SUCCESSOR's lease_ttl_s + p the successor's publish_timeout_s + S the successor's clock_skew_s + t_ins true time of the predecessor's LAST lease row, then it crashes + t_start true time the successor's start() begins waiting + + The row is stamped expires_at_ns = (t_ins + ra) + Tp. A poll at true time + t reads now_ns = t + rb and is refused while expires_at_ns > now_ns, i.e. + while t < t_ins + Tp + d. The successor polls until t_start + W, with + + W = Ts + p + S (native_capture.py:376-378) + + THE FAILURE STATE: the whole window is refused, so start() raises kHeld on + a predecessor that is already dead -- + + t_start + W < t_ins + Tp + d + """ + Tp, Ts, p, S, d, t_ins, t_start = Reals("Tp Ts p S d t_ins t_start") + + # Non-degenerate knobs (native_capture.py:355-358 rejects the rest). + s.add(Tp > 0, Ts > 0, p > 0, S >= 0) + + # The successor's own fence margin: native_capture.py:366-372 (and the + # native writer, catalog_writer.cpp:148-160) refuses a TTL that does not + # exceed publish_timeout_s + clock_skew_s by at least 0.1 s, so a + # successor outside it never starts at all. + s.add(Ts - p - S >= 0.1) + + # Real replica skew within the declared bound, either direction. + s.add(d <= S, d >= -S) + + # A restart: the successor starts no earlier than the predecessor's last + # lease row. t_start == t_ins is the worst case (renew, crash, restart). + s.add(t_start >= t_ins) + + # The default start wait. + W = Ts + p + S + + # THE FAILURE STATE: every poll in the window is refused. + s.add(t_start + W < t_ins + Tp + d) + + s.add(extra(Tp, Ts, p, S)) + return Tp, Ts, p, S + + +def check_start_wait(name, extra, expect): + s = Solver() + start_wait_constraints(s, extra) + got = s.check() + ok = got == expect + print(f"{name:<44} {str(got):<7} expected {str(expect):<7} " + f"{'OK' if ok else 'MISMATCH'}") + if got == sat: + print(f" witness: {s.model()}") + return ok + + +def check(name, d_vs_S, expect): + s = Solver() + overlap_constraints(s, d_vs_S) + got = s.check() + ok = got == expect + print(f"{name:<44} {str(got):<7} expected {str(expect):<7} " + f"{'OK' if ok else 'MISMATCH'}") + if got == sat: + print(f" witness: {s.model()}") + return ok + + +def main(): + results = [ + # 1. Real skew within the declared bound: no overlap, for any timing. + check("real skew <= clock_skew_ns", + lambda d, S: d <= S, unsat), + # 2. Real skew above the declared bound: the documented race appears. + check("real skew > clock_skew_ns", + lambda d, S: d > S, sat), + # 3. What the + clock_skew_ns term in the margin actually buys: drop it + # (keep the cap) and ANY positive step between the hosts overlaps. + check("margin without the skew term, any d > 0", + lambda d, S: And(S == 0, d > 0), sat), + + # --- the default start wait (204a8d2) --------------------------- + # (a) Same knobs on both sides: the wait outlasts the dead + # predecessor, for any TTL, any timeout, any declared bound and + # any real skew within it. + check_start_wait("start wait, predecessor TTL == successor TTL", + lambda Tp, Ts, p, S: Tp == Ts, unsat), + # (b) The config comment's 30 s case (native_capture.py:278-280): a + # predecessor on the native 30 s default against a successor on + # the shipped defaults, 15 s / 5 s / 0 s -- a 20 s wait. + check_start_wait("start wait, predecessor 30s vs 15s/5s/0s", + lambda Tp, Ts, p, S: And(Tp == 30, Ts == 15, + p == 5, S == 0), sat), + # (c) The exact threshold. The S in the wait pays for the real skew + # exactly, so the whole slack for a TTL mismatch is p: + # the wait outlasts the predecessor <=> Tp <= Ts + p + # Checked as a pair -- no failure at or below it, a failure + # everywhere above it. + check_start_wait("start wait, Tp <= Ts + p (the threshold)", + lambda Tp, Ts, p, S: Tp <= Ts + p, unsat), + check_start_wait("start wait, Tp > Ts + p (above it)", + lambda Tp, Ts, p, S: Tp > Ts + p, sat), + ] + print() + if all(results): + print("ALL CHECKS AS EXPECTED") + return 0 + print("UNEXPECTED RESULT") + return 1 + + +if __name__ == "__main__": + raise SystemExit(main())