diff --git a/specs/README.md b/specs/README.md deleted file mode 100644 index cce373e97..000000000 --- a/specs/README.md +++ /dev/null @@ -1,833 +0,0 @@ -# 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 deleted file mode 100644 index 0dcbef0ae..000000000 --- a/specs/cbmc/payload_ring_span.cpp +++ /dev/null @@ -1,70 +0,0 @@ -// 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 deleted file mode 100755 index 751b508cc..000000000 --- a/specs/check.sh +++ /dev/null @@ -1,304 +0,0 @@ -#!/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 deleted file mode 100644 index 8e612debe..000000000 --- a/specs/tla/LeaseLifecycle.tla +++ /dev/null @@ -1,688 +0,0 @@ ---------------------------- 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 deleted file mode 100644 index adec2c4b2..000000000 --- a/specs/tla/LeaseLifecycle_O1_absorb.cfg +++ /dev/null @@ -1,29 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index debcbcfcc..000000000 --- a/specs/tla/LeaseLifecycle_O1_clean.cfg +++ /dev/null @@ -1,30 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index cd3b65838..000000000 --- a/specs/tla/LeaseLifecycle_O1_cut.cfg +++ /dev/null @@ -1,29 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 50972dbc9..000000000 --- a/specs/tla/LeaseLifecycle_O1_late.cfg +++ /dev/null @@ -1,28 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 4353ffd01..000000000 --- a/specs/tla/LeaseLifecycle_O1_skip.cfg +++ /dev/null @@ -1,31 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 1c9fde3a5..000000000 --- a/specs/tla/LeaseLifecycle_O1_slowreq.cfg +++ /dev/null @@ -1,35 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 6ab200188..000000000 --- a/specs/tla/LeaseLifecycle_O1_slowreq3.cfg +++ /dev/null @@ -1,32 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 04c856ebe..000000000 --- a/specs/tla/LeaseLifecycle_O1_tries.cfg +++ /dev/null @@ -1,31 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 634321bf9..000000000 --- a/specs/tla/LeaseLifecycle_O1_tries12.cfg +++ /dev/null @@ -1,31 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 4adab6db8..000000000 --- a/specs/tla/LeaseLifecycle_O1_tries5.cfg +++ /dev/null @@ -1,31 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 99ba625e4..000000000 --- a/specs/tla/LeaseLifecycle_O1_tries60.cfg +++ /dev/null @@ -1,31 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index ee25cca2f..000000000 --- a/specs/tla/LeaseLifecycle_O2_quar.cfg +++ /dev/null @@ -1,31 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 4db681e37..000000000 --- a/specs/tla/LeaseLifecycle_O2_reuse.cfg +++ /dev/null @@ -1,32 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 09ad3c972..000000000 --- a/specs/tla/LeaseLifecycle_O2_selfref.cfg +++ /dev/null @@ -1,30 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 547cbe544..000000000 --- a/specs/tla/LeaseLifecycle_O2_skew.cfg +++ /dev/null @@ -1,30 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index f569d108f..000000000 --- a/specs/tla/LeaseLifecycle_O3_false.cfg +++ /dev/null @@ -1,30 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index f1c7c3818..000000000 --- a/specs/tla/LeaseLifecycle_O3_falsenocut.cfg +++ /dev/null @@ -1,29 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 5bf66e22b..000000000 --- a/specs/tla/LeaseLifecycle_O3_rival.cfg +++ /dev/null @@ -1,30 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 0ace57dc1..000000000 --- a/specs/tla/LeaseLifecycle_O3_rivaljust.cfg +++ /dev/null @@ -1,30 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index c071edd58..000000000 --- a/specs/tla/LeaseLifecycle_O3_selflatch.cfg +++ /dev/null @@ -1,36 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 834ed9674..000000000 --- a/specs/tla/LeaseLifecycle_O3_selflatch_latch.cfg +++ /dev/null @@ -1,35 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index a36639c1a..000000000 --- a/specs/tla/LeaseLifecycle_O3_stops.cfg +++ /dev/null @@ -1,30 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 2b96ded99..000000000 --- a/specs/tla/LeaseLifecycle_O3_stops2.cfg +++ /dev/null @@ -1,33 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 9e4fc1a19..000000000 --- a/specs/tla/LeaseLifecycle_O4_bigger.cfg +++ /dev/null @@ -1,30 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index b5183ba6a..000000000 --- a/specs/tla/LeaseLifecycle_O4_compose.cfg +++ /dev/null @@ -1,31 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 564072259..000000000 --- a/specs/tla/LeaseLifecycle_O4_same.cfg +++ /dev/null @@ -1,31 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 6b72dd7cf..000000000 --- a/specs/tla/LeaseLifecycle_O4_skew.cfg +++ /dev/null @@ -1,29 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index e491eeba3..000000000 --- a/specs/tla/LeaseLifecycle_O5_cosweep.cfg +++ /dev/null @@ -1,32 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 8fe58ec3b..000000000 --- a/specs/tla/LeaseLifecycle_O5_refused.cfg +++ /dev/null @@ -1,29 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 60bc166e4..000000000 --- a/specs/tla/LeaseLifecycle_vac_cut.cfg +++ /dev/null @@ -1,27 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index e9e4b2011..000000000 --- a/specs/tla/LeaseLifecycle_vac_held.cfg +++ /dev/null @@ -1,28 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 98ff9d888..000000000 --- a/specs/tla/LeaseLifecycle_vac_latch.cfg +++ /dev/null @@ -1,27 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index cda6f63bd..000000000 --- a/specs/tla/LeaseLifecycle_vac_o4waited.cfg +++ /dev/null @@ -1,31 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index dbb059ebd..000000000 --- a/specs/tla/LeaseLifecycle_vac_quar.cfg +++ /dev/null @@ -1,27 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index c1dc2ab75..000000000 --- a/specs/tla/LeaseLifecycle_vac_recov.cfg +++ /dev/null @@ -1,27 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 2cd67e2dd..000000000 --- a/specs/tla/LeaseLifecycle_vac_refus.cfg +++ /dev/null @@ -1,27 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index f00b1b1ac..000000000 --- a/specs/tla/LeaseLifecycle_vac_refusedstart.cfg +++ /dev/null @@ -1,29 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index e15336cc1..000000000 --- a/specs/tla/LeaseLifecycle_vac_rival.cfg +++ /dev/null @@ -1,27 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 2b87641b3..000000000 --- a/specs/tla/LeaseLifecycle_vac_start.cfg +++ /dev/null @@ -1,27 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 7ff8dbc03..000000000 --- a/specs/tla/LeaseLifecycle_vac_stops2refusal.cfg +++ /dev/null @@ -1,33 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index b0ef9710b..000000000 --- a/specs/tla/LeaseLifecycle_vac_stops2rival.cfg +++ /dev/null @@ -1,33 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index 0147ba01b..000000000 --- a/specs/tla/LeaseLifecycle_vac_stopsrefusal.cfg +++ /dev/null @@ -1,30 +0,0 @@ -\*========================================================================= -\* 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 deleted file mode 100644 index f008a7db0..000000000 --- a/specs/tla/PublisherLease.cfg +++ /dev/null @@ -1,67 +0,0 @@ -\*=========================================================================== -\* 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 deleted file mode 100644 index bdd26fb32..000000000 --- a/specs/tla/PublisherLease.tla +++ /dev/null @@ -1,549 +0,0 @@ ----------------------------- 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 deleted file mode 100644 index c83c0ade8..000000000 --- a/specs/tla/PublisherLease_base5.cfg +++ /dev/null @@ -1,23 +0,0 @@ -\* 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 deleted file mode 100644 index c40a2225f..000000000 --- a/specs/tla/PublisherLease_base5_ovr.cfg +++ /dev/null @@ -1,24 +0,0 @@ -\* 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 deleted file mode 100644 index b158f71a4..000000000 --- a/specs/tla/PublisherLease_believers.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index ad29a3deb..000000000 --- a/specs/tla/PublisherLease_chunks2.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 77f96ebad..000000000 --- a/specs/tla/PublisherLease_chunks2_orphans.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 6a4a8efd6..000000000 --- a/specs/tla/PublisherLease_chunks2_prefix.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 3368391f4..000000000 --- a/specs/tla/PublisherLease_holders.cfg +++ /dev/null @@ -1,23 +0,0 @@ -\* 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 deleted file mode 100644 index 4c23dc49f..000000000 --- a/specs/tla/PublisherLease_holderssafe.cfg +++ /dev/null @@ -1,23 +0,0 @@ -\* 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 deleted file mode 100644 index ffa80b883..000000000 --- a/specs/tla/PublisherLease_nonlin_admit.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index a70cc8ec0..000000000 --- a/specs/tla/PublisherLease_nonlin_all.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 0ece10bd1..000000000 --- a/specs/tla/PublisherLease_nonlin_fence.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index b9c2203e6..000000000 --- a/specs/tla/PublisherLease_noovr0.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 0332c8b97..000000000 --- a/specs/tla/PublisherLease_noovr1.cfg +++ /dev/null @@ -1,24 +0,0 @@ -\* 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 deleted file mode 100644 index 2f1600cdf..000000000 --- a/specs/tla/PublisherLease_orphans.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 3eb1152ef..000000000 --- a/specs/tla/PublisherLease_overrun.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index a38da1d8a..000000000 --- a/specs/tla/PublisherLease_ovr0.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 7519c5d7f..000000000 --- a/specs/tla/PublisherLease_ovr1.cfg +++ /dev/null @@ -1,22 +0,0 @@ -\* 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 deleted file mode 100644 index cada91a4e..000000000 --- a/specs/tla/PublisherLease_selfrace.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 27bdd8bc1..000000000 --- a/specs/tla/PublisherLease_selfracelocked.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 42467b67c..000000000 --- a/specs/tla/PublisherLease_stalepid.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 3179c6883..000000000 --- a/specs/tla/PublisherLease_vac0.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index f51a0e555..000000000 --- a/specs/tla/PublisherLease_vac_admit.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index ece14eb22..000000000 --- a/specs/tla/PublisherLease_vac_bothadmit.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index b16a4c004..000000000 --- a/specs/tla/PublisherLease_vac_contested.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 8db6c1ea5..000000000 --- a/specs/tla/PublisherLease_vac_fence.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 46b681ce6..000000000 --- a/specs/tla/PublisherLease_vac_publish.cfg +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index 0b3afa49f..000000000 --- a/specs/tla/VersionAllocator.tla +++ /dev/null @@ -1,277 +0,0 @@ --------------------------- 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 deleted file mode 100644 index a7e496d21..000000000 --- a/specs/tla/ec_distinct.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index 31089dc8e..000000000 --- a/specs/tla/frontier_distinct.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index 719579f85..000000000 --- a/specs/tla/lin_budget.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index 20b2a5246..000000000 --- a/specs/tla/lin_ceiling.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index 6bd134260..000000000 --- a/specs/tla/lin_distinct.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index 525fe72ce..000000000 --- a/specs/tla/lin_floor.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index ba145a198..000000000 --- a/specs/tla/lin_publish.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index 032f662e8..000000000 --- a/specs/tla/lin_solerow.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index af93932d3..000000000 --- a/specs/tla/nocap3_ceiling.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index c0888c252..000000000 --- a/specs/tla/nocap3_distinct.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index f34bc4e70..000000000 --- a/specs/tla/nocap_ceiling.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index f929e0291..000000000 --- a/specs/tla/nocap_distinct.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index d3f8ddca8..000000000 --- a/specs/tla/nocap_ec.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index 273c149f9..000000000 --- a/specs/tla/nocapf_ceiling.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index 6a8dabb47..000000000 --- a/specs/tla/nocapf_distinct.cfg +++ /dev/null @@ -1,11 +0,0 @@ -\* 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 deleted file mode 100644 index f78ce86d4..000000000 --- a/specs/z3/clock_skew.py +++ /dev/null @@ -1,223 +0,0 @@ -#!/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())