Repository navigation
Model the drain gate and close the gaps it found (I1–I15) - #148
Merged
Merged
Conversation
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018Q1CeRNhSyhRPPUxMxaK2G
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018Q1CeRNhSyhRPPUxMxaK2G
A PlusCal model of the drain gate (G7): backend starts and retries, the stop signal's drain, DrainAndWait, the supervisor's restarts, and tailscaled and control as the environment. drain.cfg checks what holds (S2, S4, S7, L1, L2), each with a mutation that breaks it; the confirmed violations I1, I2, I4, I5, I6 and I7 are expected failures with their traces. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018Q1CeRNhSyhRPPUxMxaK2G
The stop signal and Leave reach the supervisor only once the first daemon was published; a Leave during the first start aborts it without a drain. S1 now covers external drains, and S8 checks that Leave does not stop a tailscaled that still advertises: I8 and I9 are its violations. Labels Change_fnReturned and Fetch_counted mark one Go point each, and the runner reads ACTION_CONSTRAINT anywhere in a cfg. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018Q1CeRNhSyhRPPUxMxaK2G
The endpoint gets its supervisor only if the first start's daemon is still alive, as startSupervisor's WaitForIP requires; I1 and I8 get traces Go can take. The counted-fetch and advertised steps fold into their neighbours, which brings the state space back to 3.8M states. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018Q1CeRNhSyhRPPUxMxaK2G
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Avx4VgFJZfWvG4uW5h6AU5
The drain gate judged its edits by what their LocalAPI calls returned and counted fetches from before the edit. The drain gate model found twelve interleavings (I1-I12) where a node left with control pointed at it, or a drained Service advertised again. tailscaled logs each prefs edit it applies before it sets the prefs, and a Service list fetch before it reads them, so the log orders the two: - the gate keeps one record of the last edit of tslink's removing a Service (drain, prune, readvertise, the lease holder), made before the edit is sent; Leave waits for a fetch logged after that edit took effect, whatever its call returned (I2, I3, I5, I7, I10, I11, I12) - an edit advertising a Service once drained, as a cancelled call carried out late, is undone (I4) - a daemon started drained removes what its state advertises, and DrainAndWait waits across a restart until one deadline (I1, I6, I8) The advertised flag is gone: a record exists only if tslink removed something, which is what there is to wait for. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Avx4VgFJZfWvG4uW5h6AU5
Leave cancelled the first start, which stopped tailscaled with no drain, though it ran and could advertise Services from the node's state (I9 of the drain gate model). Leave now hands the supervisor being started Leaving(): a start whose tailscaled runs goes on drained, StartContext drains and waits for control before it returns, and Leave waits for that run. A start that has not started tailscaled is still aborted at once. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Avx4VgFJZfWvG4uW5h6AU5
Checking the fixes against the drain gate model found more ways for a node to leave advertising, or before control fetched its drain: - a removal logged before the one recorded, read after the record was made, passed for it: the record keeps the Services its edit leaves, and only a removal leaving no more counts - a cancelled advertisement carried out during the floor's sleep: after the floor, the record and its fetch are checked again - Leave just after tailscaled crashed, before the supervisor replaced it: a published daemon that exited counts as a restart in progress - a tailscaled restarted before the drain and published after it: Leave drains it - a drain that cancelled a call and found nothing advertised: Leave looks again once the call would have been carried out Each has a test that fails without its fix. CLAUDE.md and the architecture page describe the drain as it is now. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Avx4VgFJZfWvG4uW5h6AU5
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01M3C8xuHSNGpeJcnZqiryTX
Checking the pass configurations against the rewritten model found three more ways for a node to leave advertising, or before control fetched its drain: - I13: Leave during the first start marked the gate drained before pruneServices ran, which then removed nothing and counted as done: a prune the drain stopped now makes the node need a drain - I14: a removal the lease holder made took effect, and tailscaled exited before control fetched it; the next tailscaled had nothing to drain, and Leave did not wait: unadvertiseAll records a removal pending on an earlier daemon for the drain as well as for drainAtStart - I15: readvertise's removal was fetched and the Service advertised again, then tailscaled crashed and the drain failed; Leave took the fetch of the removal for the drain's and stopped the next tailscaled before it drained its state: a removal counts as fetched only while tailscaled lists no more than it left Each has a test that fails without its fix and a mutation of the model that its property catches. drain.cfg passes; the drain-pass-* cfgs do not finish at their bounds yet (the models README says so), which a follow-up takes on. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01M3C8xuHSNGpeJcnZqiryTX
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01M3C8xuHSNGpeJcnZqiryTX
Merged
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.
When a container with Tailscale Services stops, tslink drains them and waits for control to fetch the drained Service list before it stops tailscaled (G7). This PR adds a TLA+ model of that drain gate (
test/models/drain.tla), a runner for it (make check-models), and fixes for the 15 interleavings the model found to break G7.Fixes
Each has a test in
pkg/tailscale/drain_test.gothat replays the model's counterexample and fails without the fix. The CHANGELOG has the user-facing summary. Among them:The model
drain.cfg(core actors, two Services, one restart) passes: 5 M distinct states, about 25 min.Not checked yet
drain-pass-*cfgs (confirmer, lease, prune paths) do not finish at their bounds.drain-pass-confirmer-restartexceeds 60 M distinct states and fills the disk;drain-pass-confirmerruns out of memory in the liveness check.test/models/README.mdsays so. Cutting their bounds is the follow-up.drained-pruned,no-start-record,no-listed-check) have not had a full run yet, because Docker went down when the disk filled. The 14 earlier ones were all caught by the previous run.Tests
go test ./...andgolangci-lint runpass locally. CI does not run the models.🤖 Generated with Claude Code
https://claude.ai/code/session_01M3C8xuHSNGpeJcnZqiryTX