Add TLA+, Z3 and CBMC specs for the lease, allocator and ring span arithmetic - #153
Closed
claude[bot] wants to merge 6 commits into
Closed
claude[bot] wants to merge 6 commits into
claude[bot] wants to merge 6 commits into
Conversation
claude
Bot
force-pushed
the
claude/formal-specs
branch
2 times, most recently
from
September 24, 2026 18:49
d3fad41 to
fe1f2e5
Compare
zaoxing
marked this pull request as ready for review
September 24, 2026 22:52
zaoxing
force-pushed
the
fix/lease-recovery
branch
from
September 24, 2026 22:59
352d84f to
b03be36
Compare
zaoxing
force-pushed
the
claude/formal-specs
branch
from
September 24, 2026 23:02
fe1f2e5 to
9f60e8e
Compare
zaoxing
changed the title
The safety arguments for the publisher lease, the version allocator and the start wait lived only in prose in docs/catalog-descriptor-key.md, and that prose has already been wrong once (the correction at :304-314). specs/ now machine-checks them against the code as of 2b74d14: - tla/VersionAllocator.tla: the sole-claimant allocation loop. - tla/PublisherLease.tla: claim/renew/release and the fenced publish. - tla/LeaseLifecycle.tla: the lease thread, quarantine, the 2 x TTL latch, the start wait and the spool sweep in CaptureStorageService. - z3/clock_skew.py: the fence margin and the default start wait. - cbmc/payload_ring_span.cpp: payload_compute_spans and its precondition. LeaseLifecycle.tla refutes three things the code currently relies on: the latch can fire with no rival when clock skew outlasts the quarantine window, two processes can sweep one spool at once, and a publish that only skips already-committed packs is counted as a renewal. The README gives the exact command for every config and the verdict each one should reach. Nothing in specs/ is built or run by DMI or CI.
The O1 caveat said the renewal retry budget applies only to refusals. It applies to no failure: a refusal drops the lease in the coordinator (reject_live, or the failed claim read-back), and a transport error, timeout or parse error is a ClickHouseError that quarantines the writer on the first one. The four lease-thread wakes are room for a renewal that runs late, not for one that fails. The same paragraph now calls the arithmetic, rather than the comment, correct and conservative.
…sults The O1_tries5 header was copied from O1_tries and said EXPECT: HOLDS, but FiveTriesFit is refuted at the constant level, as the README table and the results table in LeaseLifecycle.tla already say; TLC confirms it. The README introduced the two O1 caveats as neither a model result, though O1_absorb confirms the first and O1_skip is the second.
…k.sh An independent review found the specs README claiming more than the models show. This corrects the claims, adds the configs that back or bound them, and adds a script that re-runs the checks and compares every verdict. - Ring: only payload_compute_spans's span arithmetic is checked, not a ring protocol. The CBMC harness gains P5, that no span byte lands in the unconsumed region [tail, head); it holds with the precondition and fails without it. P5 takes head's offset from off1 rather than recomputing head % cap, which does not finish. - LeaseLifecycle settles every ClickHouse call in zero time, while keep_lease() holds lease_mutex_ across up to three requests bounded only by request_s (60 s against a 15 s TTL). O1_slowreq3 (MaxLate 3, no cycle) holds and O1_slowreq (MaxLate 4) is refuted, so the O1 HOLDS verdicts are qualified: they need each lease request to finish in about half the TTL. A follow-up PR will bound lease request time. - LIMITS 5 cited catalog_writer.cpp:519's publish-timeout cap to dismiss a late-landing unknown outcome, but that cap covers only publish_snapshot; the lease INSERT has no max_execution_time. The model lands such a row at once, so O2_quar and O3_false hold only under that assumption, and of the two suggested self-latch fixes only resetting held_elsewhere_since_ns_ is robust. - NoSelfRefusal flagged ticks on which the service was quarantined and took no claim. It now counts only a claim actually taken and refused by the service's own row; O2_selfref (Skew 1) is still refuted, and it holds at Skew 0. The history variable changed, so the LeaseLifecycle state counts are re-recorded; no verdict changed. - PublisherLease.cfg's AllSafety holds vacuously for NoOverlappingAdmit at the base constants. base5_ovr (refuted) proves base5 non-vacuous, and noovr1 / ovr1 add the one-chunk pair beside noovr0 / ovr0. - Limitations now also say: Linearizable needs insert_quorum as well as select_sequential_consistency on a replicated catalog; skew runs one way; Stop is never enabled and its tombstone differs from the code's; each allocator allocates once, with no cross-call monotonicity check. - Line references move to #150's head, c0361d7 (storage_service.cpp +6 from run_cycle on, storage_service.h sweep comment at :104-108), and commit references from the orphaned 2b74d14 to 204a8d2, the same tree. - Nits: seven Z3 checks, not six; O5_cosweep's config allows one cut (the trace takes none, and MaxCuts 0 is refuted too); the .tla no longer points at an LLruns/ directory or a vac_cosweep config; apt's cbmc on Ubuntu 20.04 is too old. specs/check.sh runs the fast set (every config but PublisherLease.cfg, believers, holderssafe, overrun, nonlin_fence, stalepid and noovr1, which --all adds), z3/clock_skew.py and both CBMC builds, compares each result with a table of expected verdicts, and exits non-zero on a mismatch or on a .cfg the table does not list. Tools come from TLA2TOOLS_JAR, CBMC and PYTHON. TLC runs in a scratch copy, so nothing lands in the tree. It is not wired into CI.
#150 was squash-merged as 7419fd0, and main then took #151, #152 and #139. The specs cited #150's head c0361d7; they now cite main at 71be2af. - storage_service.cpp moved up two lines (#151 builds the ClickHouse client from one ClickHouseConnection), native_capture.py moved with #149/#151/#152, and deciding_read() is now clickhouse_client.cpp:374. - #151 also made execute() retry a read after a transient failure, up to max_attempts (3 by default), and never a write that may have reached the server. The README's O1 caveat, its Limitations entry and LIMITS 3 in LeaseLifecycle.tla now say a lease request's reads can take up to three request timeouts, and RenewIfDue says the quarantining exception is the first to outlast those retries. No modelled outcome changes. - Refs that missed the code they describe, in files main did not change: the O1a quote is storage_service.h:233-234, not storage_service.cpp; the renewal in publish_snapshot is catalog_writer.cpp:490 and :579; publish_snapshot ends at :669; the config check with the quorum rule is :148-169; the chunk loop is :531; the watermark read-back is :608-628 (:611-627 for its refusal); the version allocator's statement lines; reject_live's comparison is lease_coordinator.cpp:222; and the start wait's knob checks are native_capture.py:351-354. - The README says what 204a8d2 is now that #150's branch is squashed. Comment and prose changes only; every verdict is unchanged.
The RenewIfDue comment said the exception that quarantines a renewal is the first to outlast the client's read retries. The claim INSERT is a write: execute() repeats it only when the connection was never made and never after a timeout, so its first failure after connecting quarantines at once. Say that, as the README already does. The "DURABLY CLAIMED, not solely claimed" quote in VersionAllocator.tla is at tests/test_native_catalog_lease_live.py:653-662, not :598-607 (that is the test's def and docstring; cite the docstring's point at :605-609 separately). Close three ranges that stopped partway through the code they cite on main: the fence-margin precondition is catalog_writer.cpp:148-160, the watermark publish with its read-back is :583-628, and the visibility write statement is :583-606.
zaoxing
force-pushed
the
claude/formal-specs
branch
from
September 28, 2026 01:04
a7e2858 to
cdc9c47
Compare
Collaborator
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Requested by Alan Liu · Slack thread
Before: The reasons the publisher lease, the version allocator and the start wait are safe were written down only as prose in
docs/catalog-descriptor-key.md. Nothing checked that prose against the code, and it has already been wrong once (the correction at:304-314).After: Five parts of the design are now checked by a machine against the code at
2b74d14: the lease/fence protocol, the version allocator, the storage service's lease lifecycle, the clock-skew and start-wait arithmetic, and the payload ring's span arithmetic.specs/README.mdgives the exact command for every model and the result each one should reach.This PR adds files under
specs/and nothing else (85 files). DMI and CI do not build, import or run anything inspecs/.How.
tla/VersionAllocator.tla,tla/PublisherLease.tlaandtla/LeaseLifecycle.tlaare checked with TLC.z3/clock_skew.pycovers the fence margin and the default start wait.cbmc/payload_ring_span.cppcheckspayload_compute_spansagainst its stated precondition.LeaseLifecycle.tlarefutes three things the service currently relies on:O3_selflatch). With clock skew, a writer can be refused by its own dropped row at the moment its quarantine ends. The2 x TTLlatch then fires "held by another publisher" when no other publisher exists.O5_cosweep). A quarantined incumbent lets its row lapse, so a second process can take the lease and sweep the spool while the first is still writing.skipped_packscounted as a renewal (O1_skip). A cycle that only skips packs that were already committed advanceslast_renew_ns_without renewing anything, so the lease can lapse while the service still believes it holds it.A fix for the lease-request timing gap comes in a follow-up PR on top of #150 (
fix/bound-lease-requests). The spool sweep needs an owner lock on the spool, and this PR series does not fix it.Note:
alan/blissful-brown-hiq82yhas an earlier copy ofspecs/, plus aRingCapacity.tlathat is not in this PR. The two branches will conflict if both land.Checked locally with TLC 2.19 on Java 21.
nocap_distinctrun with-deadlockcompletes with no error (1,117 generated / 836 distinct, as the README says).LeaseLifecycle_O3_selflatchis refuted onNoFalsePositiveLatch, as expected.python3 specs/z3/clock_skew.pyprintsALL CHECKS AS EXPECTED.After independent review (a7e2858)
The reviewer ran all 85 configurations, Z3 and CBMC, and every verdict matched. Each of four deliberate protocol breaks produced a counterexample. The fixes address what the models claimed beyond that:
O1_slowreq3(holds) andO1_slowreq(refuted: a stall of about 2/3 of a TTL lets the lease lapse) show the boundary.NoSelfRefusalnow counts only a real self-refusal.NoOverlappingAdmit.insert_quorumas well asselect_sequential_consistency.Stopis never enabled, and there is no cross-call allocator monotonicity check.specs/check.shchecks every configuration against its expected verdict: 80 passed, 0 failed on the fast set, and the 7 manual configurations pass with--all. No CI job was added.Rebased onto main after #150 merged (73e6cad, cdc9c47)
#150 was squash-merged, so this PR's own commits were replayed onto main (71be2af) without conflicts, and the PR now targets main.
specs/now points at main's code, about 100 references checked by printing the code each one names. About 20 references that were already wrong before the rebase were corrected too.specs/check.shgives 80 passed and 0 failed on the fast set. The diff touches onlyspecs/, and only comments or prose in the model files.