Say what the lease comments actually guarantee - #154
Merged
Merged
Conversation
claude
Bot
force-pushed
the
claude/lease-comment-corrections
branch
2 times, most recently
from
September 24, 2026 18:49
ed3e8eb to
cdd22db
Compare
zaoxing
self-requested a review
September 24, 2026 22:51
zaoxing
marked this pull request as ready for review
September 24, 2026 22:51
zaoxing
force-pushed
the
fix/lease-recovery
branch
from
September 24, 2026 22:59
352d84f to
b03be36
Compare
zaoxing
force-pushed
the
claude/lease-comment-corrections
branch
from
September 24, 2026 23:02
cdd22db to
8af859c
Compare
Four comments promised more, or less precisely, than the code does: - renew_lease_if_due() said renewing at ttl/3 leaves two more tries. Four lease-thread wakes do fit before the row expires, but they only cover a renewal that runs late. A failed renewal costs the lease at once: a refusal drops it in the coordinator, and a transport error or timeout quarantines the writer on the first failure. - The sweep_spool_on_start comment in storage_service.h still read as the strong sweep-after-lease guarantee that 2b74d14 weakened in the .cpp. It now says the same: a quarantined holder lets its row lapse, a second process can take the lease and sweep, and the spool is not locked. - start_lease_wait_s said a predecessor with a longer TTL can outlast the default wait. The exact condition is a predecessor TTL above lease_ttl_s + publish_timeout_s (clock_skew_s cancels), 20 s on the defaults, so the native 30 s default falls 10 s short. - The claim read-back takes the expiry from rows[0] of an unordered read, while the rule is the minimum expires_at_ns under (term, lease_id). The comment says why that is safe here, so the next reader need not re-derive it. No code changes.
- renew_lease_if_due(): "four wakes fall between the renewal coming due and the row expiring" was nominal at best. last_renew_ns_ is stamped after the round trip, the tick counts from the end of the previous pass, and an index() call can hold lease_mutex_. It now says the renewal fires about a tick after it falls due, leaving roughly half the TTL for it to land. A server error quarantines as well as a transport error or timeout, and "on the first one" now allows for the client's read retries: a write that may have reached the server is never retried. - sweep_spool_on_start: any holder that stops renewing for a TTL, not only a quarantined one, lets a second process take the lease and sweep; one on another (database, table_prefix) never meets the lease; and the second process's Recover() lists the first's sealed packs, so both upload one spool. - start_lease_wait_s: the default wait is guaranteed to outlast a crashed predecessor only when its TTL is at most lease_ttl_s + publish_timeout_s, and clock_skew_s cancels only if it bounds the offset between the replica that stamped the row and the one serving the read. - claim_with_rival(): the client never re-sends an INSERT, and it is CatalogWriter that quarantines after one of unknown outcome. Comments only.
Rebased onto main, three of the rewritten comments said more than the code now does: - The ClickHouse client retries a write when its connection was never made, since nothing reached the server. The claim read-back no longer says the client never re-sends an INSERT, and the renewal comment no longer calls the retries reads-only. A write that may have reached the server is still never repeated, so the claim still wrote one row. - A quarantined cycle uploads nothing, so the spool-sweep caveat no longer says both processes then upload the one spool. A stalled holder that still holds its lease locally does, until a renewal or publish is refused, and so do two processes on different (database, table_prefix) pairs. Comments only.
…slack The sweep_spool_on_start comment said a quarantined holder uploads nothing without the lease. run_cycle() checks the lease once, before its upload batch, and UploadPending does not stop when the lease is lost, so a holder quarantined or refused while a batch is in flight finishes that batch (which can outlast the TTL) while a second process may already have taken the lease and swept; only its later cycles upload nothing. The renew_lease_if_due() comment counted the half-TTL slack from the row's last renewal, but the check reads last_renew_ns_, which index_bounded() stamps when index() returns: after the publish's own last renewal, and even when every pack was already committed so nothing was published or renewed. With index() holding lease_mutex_ meanwhile, the slack can be far less than half the TTL, or none. Say so.
zaoxing
force-pushed
the
claude/lease-comment-corrections
branch
from
September 28, 2026 01:04
592a90e to
68e6aee
Compare
zaoxing
added a commit
that referenced
this pull request
Sep 28, 2026
…ithmetic (#157) * Add TLA+, Z3 and CBMC specs for the lease, allocator and ring protocols * Say in the specs README that a failed renewal is never retried * Expect O1_tries5 to be refuted, and say which O1 caveats are model results * Say what the specs leave out, and check every verdict with specs/check.sh * Point the specs' line references at main after #150's squash * Correct the specs' retry wording and three stale citations * Point the specs' line references past #154's comments * Check the four-wake claim at TTL 6, and fix four stale spec citations
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: Four comments on the publisher lease said more than the code does, or said it loosely. One implied that renewal failures get retries. One still read as the strong spool-sweep guarantee that
2b74d14had already weakened. One gave the start-wait caveat only roughly. One left the reader to work out why the claim read-back can takerows[0].After: Each of the four comments now says what the code does and matches what the formal models checked. No code changes.
How.
storage_service.cpp,renew_lease_if_due(): four lease-thread wakes do fit between the renewal falling due and the row expiring. They cover a renewal that runs late, though, not one that fails. Every failed renewal costs the lease at once. A refusal drops it in the coordinator (reject_live, or the failed read-back). A transport error or timeout goes throughrenew_for_publish()'scatch, which quarantines the writer on the first failure.storage_service.h,sweep_spool_on_start: now matches the.cpp. A start refused the lease never touches the spool. A quarantined holder, though, lets its row lapse, so a second process can take the lease and sweep while the first is still writing. The spool is not locked.native_capture.py,start_lease_wait_s: the default wait outlasts a crashed predecessor exactly when that predecessor's TTL is at mostlease_ttl_s + publish_timeout_s, andclock_skew_scancels out. On the shipped defaults that limit is 20 s, so a predecessor on the native 30 s default outlasts the default wait by 10 s.lease_coordinator.cpp, the claim read-back: a comment explaining whyrows[0][2]is safe even though the rule is the minimumexpires_at_ns. The only other row that could share(term, lease_id)is a release's tombstone. Releases write at the holder's own term and claims always go tohead + 1, so a claim's term never already holds its own tombstone.To avoid conflicting with the fix PRs, this leaves
docs/catalog-descriptor-key.mdand the lines atstorage_service.cpp:435-437and:723-739,storage_service.h:216-218andcatalog_writer.cpp:273alone.python -m py_compilepasses on the Python file. The C++ was not built (no nvcc in this environment), but every changed line in the diff is a comment line.After independent review (592a90e)
The reviewer checked every original change against the code. The new comments were more accurate than the old ones, and six were tightened further. It is still comments only.
CatalogWriter, and the client never re-sends an INSERT.Rebased onto main after #150 merged (ad129a1, 68e6aee)
#150 was squash-merged, so this PR's two original commits were replayed onto main (71be2af) without conflicts, and the PR now targets main. It is still comments only: a script checks that every added or removed line is a comment.
Each comment was re-checked against main's current code, and these were corrected:
execute()repeats any statement whose connection was never made. The coordinator comment and the "first error that survives the client's retries" wording now say that a write is repeated only when it never connected.run_cycle()checks the lease once, at the start of the cycle. An upload batch already running continues after the lease is lost, so the sweep caveat now describes that window instead of claiming a quarantined holder uploads nothing.index()is in the way.index()holdslease_mutex_, andindex_bounded()restampslast_renew_ns_when it returns.Found, not fixed here (this PR is comments only):
index_bounded()setslast_renew_ns_ = steady_ns()wheneverindex()returns with skipped packs, even when every pack was already committed and nothing was published or renewed. That restarts the renewal clock without renewing the lease row. It needs a separate code fix: stamp only when the index published, or take the writer's last successful renewal time.