a73x/eitri

Watch

Fork 0

reconcile: the concurrency invariants are argued in prose and observed by nothing #97

New issue

Closed

opened 2026-08-23 09:36:17 +00:00 by a73x · 3 comments

a73x commented

2026-08-23 09:36:17 +00:00

(Migrated from git.a73x.sh)

[claude 2026-08-23] From the same mutation audit (branch comment-audit). internal/agent/reconcile has the repo's highest comment ratio and the most-argued concurrency invariants — and none of them are observable. Every mutation below stayed green under -race, most at -count=3 or higher.

The auditing agent's verdict: "this suite pins behaviour, not concurrency." The comments survived the audit not because they are irreducible rationale but because nothing can tell whether they still hold.

1. "Only IDLE workers are reaped" — `worker.go:76`

Mutation: deleted the idle check, so a busy worker is dropped from the map. -race -count=3 green.

The comment names its own consequence: two goroutines reconciling one VM — a concurrent Destroy/DeleteVM against a Boot/SaveVM, orphaning a hypervisor process.

Test shape: deliver → wedge the worker → reap → deliver again → assert one worker.

2. The GENERATION RULE — `worker.go:242-255`

20 lines, the package's most-argued comment. Two mutations, both green under -race: if !w.busy || gen != w.gen → if !w.busy, and deleting w.gen++.

Only the !w.busy half is pinned — TestNarrationCannotOutliveThePassThatSaidIt kills a straggler after the pass ended, never one from pass N landing while pass N+1 runs.

3. `collect` clones the rows

"The rows are CLONED … two reports marshalled concurrently would race on one message." Mutation: own := res.clone() → own := res. -race -count=5 green.

Test shape: two concurrent aggregates, both proto.Marshaled.

4. "One goroutine per VM — the worker IS the lock"

Mutation: go w.run() twice per worker. -race -count=3 green.

5. `netTracker.writeThrough` atomicity — `syncsvc/tracker.go:100`

Unlocking across the write is green at -race -count=3. The sibling statusTracker has TestStatusTrackerWriteThroughAtomic; netTracker has no equivalent.

TestStatusTrackerWriteThroughAtomic caught its mutation at -count=5 but passed a single -race run. As a one-shot CI alarm it may not fire on a real regression. Worth pinning the iteration count or restructuring the test.

Also found while mutating

quotaCheckLocked's early if e.MaxVCPUs == 0 && … return is dead code — every case below already guards on Max* > 0.
SeedLedger has no callers anywhere in the package.

Migrated from git-collab issue 457540744aac164aa3465e04dad6564deb02ef9b.

Original author: a73x dev@a73x.sh.

Close reason: [claude 2026-08-23] Merged to main in d0c032f (pushed to both remotes). Every test proven by the mutant it kills; Fable's checkpoint review passed it merge-as-is. make ci green, boot gate PASS (full smoke incl. UDP, cold_start=20s).

[claude 2026-08-23] From the same mutation audit (branch `comment-audit`). `internal/agent/reconcile` has the repo's highest comment ratio and the most-argued concurrency invariants — and **none of them are observable**. Every mutation below stayed green under `-race`, most at `-count=3` or higher. The auditing agent's verdict: *"this suite pins behaviour, not concurrency."* The comments survived the audit not because they are irreducible rationale but because nothing can tell whether they still hold. ### 1. "Only IDLE workers are reaped" — `worker.go:76` Mutation: deleted the idle check, so a busy worker is dropped from the map. `-race -count=3` green. The comment names its own consequence: two goroutines reconciling one VM — a concurrent Destroy/DeleteVM against a Boot/SaveVM, orphaning a hypervisor process. Test shape: deliver → wedge the worker → reap → deliver again → assert one worker. ### 2. The GENERATION RULE — `worker.go:242-255` 20 lines, the package's most-argued comment. Two mutations, both green under `-race`: `if !w.busy || gen != w.gen` → `if !w.busy`, and deleting `w.gen++`. Only the `!w.busy` half is pinned — `TestNarrationCannotOutliveThePassThatSaidIt` kills a straggler *after* the pass ended, never one from pass N landing while pass N+1 runs. ### 3. `collect` clones the rows "The rows are CLONED … two reports marshalled concurrently would race on one message." Mutation: `own := res.clone()` → `own := res`. `-race -count=5` green. Test shape: two concurrent `aggregate`s, both `proto.Marshal`ed. ### 4. "One goroutine per VM — the worker IS the lock" Mutation: `go w.run()` twice per worker. `-race -count=3` green. ### 5. `netTracker.writeThrough` atomicity — `syncsvc/tracker.go:100` Unlocking across the write is green at `-race -count=3`. The sibling `statusTracker` has `TestStatusTrackerWriteThroughAtomic`; `netTracker` has no equivalent. ### Related: one existing alarm is unreliable `TestStatusTrackerWriteThroughAtomic` caught its mutation at `-count=5` but **passed a single `-race` run**. As a one-shot CI alarm it may not fire on a real regression. Worth pinning the iteration count or restructuring the test. ### Also found while mutating - `quotaCheckLocked`'s early `if e.MaxVCPUs == 0 && …` return is **dead code** — every `case` below already guards on `Max* > 0`. - `SeedLedger` has **no callers** anywhere in the package. --- Migrated from git-collab issue `457540744aac164aa3465e04dad6564deb02ef9b`. Original author: a73x <dev@a73x.sh>. Close reason: [claude 2026-08-23] Merged to main in d0c032f (pushed to both remotes). Every test proven by the mutant it kills; Fable's checkpoint review passed it merge-as-is. make ci green, boot gate PASS (full smoke incl. UDP, cold_start=20s).

a73x commented

2026-08-23 09:47:54 +00:00

(Migrated from git.a73x.sh)

[claude 2026-08-23] Design for observing the reconcile concurrency invariants. Verified the headline claims by re-running two of the mutations myself (tree restored, git diff --quiet clean). One invariant's stated mechanism is obsolete and one incidental finding is wrong — both below.

1. Diagnosis: why this suite pins behaviour and not concurrency

Two structural reasons, and neither is "no way to wedge a worker" — the harness already has one (wedge() in worker_test.go, plus stepNoWait).

(a) Every assertion reads quiesced end-state. The canonical driver f.step is Step → waitIdle → aggregateNow. Quiesced end-state is interleaving-independent by construction, so no assertion in the suite can distinguish correct locking from broken locking. The wedge-based tests in worker_test.go are the exception, but they aim the wedge at liveness properties (report promptness, cross-VM concurrency, coalescing, the create cap) — none pairs a wedged worker with the structural stimulus that matters: a reap, a redeliver, a stale-generation publish, a concurrent collect.

(b) These are exclusion/ownership invariants, and -race is categorically blind to them here. Every shared structure in the package is individually mutex-guarded (manager.mu, worker.mu, Engine.mu, the fake provisioner's own lock). So the violating executions are race-clean: two goroutines reconciling one VM perform zero unsynchronized memory accesses in the test environment — each pass writes its own vmResult, and everything they share is locked. -race detects unsynchronized access, not violated ownership. Its silence is by design, not by luck, which is why -count=3 and higher bought nothing.

Corollary: the fix is not five unrelated tests. Invariants 1, 2 and 4 are the same invariant — at most one pass in flight per VM — violated by three different mutations, and it needs one missing observable plus a handful of forced interleavings. Invariant 3's hazard needs restating first (see below). Invariant 5 and the unreliable alarm share one deterministic pattern.

2. Strategy: deterministic wedge + an occupancy observable, extending the existing harness

Chosen: (a) one small addition to the reconcile test harness — an occupancy-tracking Images wrapper (per-vmID entry/exit gauge with a mutex-guarded high-water mark), composed with the existing wedge(); (b) for the trackers, a "park a writer inside write()" pattern that asserts mutual exclusion directly. All tests are channel-sequenced: the dangerous window is held open by a parked goroutine, the stimulus is applied, the observable is read. No repetition, no -count, deterministic under the make test flags CI actually uses (go test -race -shuffle=on ./... — count=1, checked).

Against -race + repetition: blind per (b) above, and empirically a coin flip even where it isn't blind — see §4.

Against making it structural: attractive for invariant 1 (a worker that deletes its own map entry on exit, with reap only signalling, turns "only idle workers are reaped" from a rule into ownership) and worth a follow-up issue if you want it. But types can't express "at most one goroutine executes passes for id" in Go — the go w.run() twice mutation defeats any map discipline from inside the structure — and nothing structural covers 2, 3 or 5. Any such refactor also needs these tests in place first to gate it. So: tests now; the structural rework for invariant 1 is optional and separately gated.

One negative-window caveat, stated once: two of the tests below assert "a second goroutine did NOT enter" via a 250ms select. That is the suite's established pattern (TestCreateConcurrencyIsCapped uses exactly this) and its reliability is scheduler liveness, not an interleaving lottery: under the mutation the second goroutine is runnable and blocked on nothing, so it reaches the probe within the window essentially always. False-pass requires the scheduler to starve a runnable goroutine for 250ms.

3. Per-invariant designs

Inv 1 — "Only IDLE workers are reaped" (worker.go:76)

Verified: I neutralized the idle check; suite green under -race -count=2.

Lives: worker_test.go, TestBusyWorkerIsNotReaped.
Harness: existing wedge().
Interleaving: deliver vm1 → wait arrived (pass parked in the fetch) → call m.reapAbsent(map[string]assignment{}) directly, modelling the transiently-unreadable-record tick the comment names (LoadVMs skips a live VM, dropping it out of live). Driving this through Step is not cleanly reachable (the record exists while the pass runs, so the union puts vm1 back in live); the manager layer is already a first-class test surface here (count, waitIdle).
Assert: m.count() == 1 immediately after reapAbsent — fully synchronous, zero timing. Then close(release), waitIdle, reapAbsent(empty) again → count() == 0 (the idle half, making the pair readable).
Failure message: "a busy worker was reaped: the next deliver spawns a second goroutine for this VM (concurrent Destroy vs Boot, orphaned hypervisor)".

Inv 2 — the GENERATION RULE (worker.go:242)

Lives: narrate_test.go, TestAStragglerFromAnEarlierPassCannotLandOnALaterOne — the missing sibling of TestNarrationCannotOutliveThePassThatSaidIt, which only pins the !w.busy half.
Harness: an Images fake with two behaviours: pass 1 captures its progress callback (as the existing straggler test does) then returns an error; pass 2 publishes a distinguishable narration line, then parks on release.
Interleaving: stepNoWait(snap(1, vm1)) → pass 1 fails, straggler captured, waitIdle. stepNoWait(snap(2, vm1)) → pass 2 parked mid-fetch (busy=true, gen advanced), wait for its narration. Invoke the captured pass-1 callback. aggregateNow.
Assert: the row's StatusDetail is pass 2's line, never pass 1's. Deterministic — the worker is parked, nothing races.
Kills both mutations: if !w.busy || gen != w.gen → if !w.busy: busy is true, straggler admitted, pass-1 detail lands. Delete w.gen++: both passes carry gen 0, equality holds, same landing.
Failure message: "a publish from pass N landed while pass N+1 was in flight: the generation half of the publish guard is gone — the report shows a phantom state from a finished pass".

Inv 3 — "collect clones the rows" (worker.go ~127) — the argued hazard is obsolete; the invariant survives on different grounds

Be skeptical here as invited: the comment's mechanism — "proto.Marshal writes a size cache … two reports marshalled concurrently would race on one message" — is no longer true. protobuf v1.36.11 (this repo's version) reads and writes the size cache with atomic.LoadInt32/StoreInt32 (verified in the module cache, internal/impl/encode.go:56,67,128). Concurrent Marshal of one message is race-clean, which is why the clone-removal mutation stayed green at -race -count=5 — there is no race to catch, and the issue's proposed test shape (two concurrent aggregates, both Marshalled) would be a permanently-green alarm. Do not build it.
The clone still earns its place, for a reason one line below the comment: vmResult.merge writes into the row — r.vm.SshHostPubkey = r.hostPubKey (reconcile.go:1090). Without the clone, every collect writes into the worker's live proto, and every report shares row pointers with every other report and with the worker (two Steps from concurrent sessions — the reconnect case syncsvc already documents — makes those writes genuinely concurrent).

Lives: worker_test.go, TestEveryReportOwnsItsRows.
Harness: none new.
Interleaving: none needed. Create vm1, waitIdle, then aggregateNow twice sequentially.
Assert: pointer non-identity — findVM(rep1,"vm1") != findVM(rep2,"vm1") (and both rows carry the pubkey). Single-threaded, deterministic, kills own := res outright.
Failure message: "two reports share one row proto: collect stopped cloning, and merge writes into a row other reports and the worker still hold".
Rider for the implementer: reword the CLONED comment — the size-cache claim is stale; the true argument is merge's write plus self-containment.

Inv 4 — "one goroutine per VM — the worker IS the lock"

Lives: worker_test.go, TestABusyVMNeverRunsTwoPassesAtOnce.
Harness: the occupancy wrapper: wrap Images to increment/decrement a per-vmID gauge (mutex-guarded, recording the high-water mark) around the wedge.
Interleaving: wedge vm1's create (arrived). While parked, stepNoWait a second snapshot containing vm1 — this sets pending, the coalescing path. Select on a second arrived for 250ms: a second arrival is an immediate fail. Then close(release), waitIdle, and assert highWater("vm1") == 1.
Why it kills the mutation: run's wait condition is pending == nil && !stopped — it deliberately does not check busy, because one loop can't be in two places. A second go w.run() loop is in a second place: it consumes the new pending while loop 1 is parked and enters the fetch. It is runnable and unblocked — scheduler liveness, not luck (the caveat in §2).
Failure message: "two reconcile passes entered the provisioner for one VM at once: the worker is no longer the lock". This test also backstops inv 1's consequence (a reaped-while-busy worker plus a redeliver produces occupancy 2).

Inv 5 — `netTracker.writeThrough` atomicity (server/syncsvc/tracker.go:103)

Lives: internal/server/syncsvc/tracker_test.go, TestNetTrackerWriteThroughHoldsTheLockAcrossTheWrite.
Harness: park-inside-write: writer A's write signals entered, then parks on a channel.
Interleaving: goroutine A: writeThrough("h1", "10.0.0.0/24", parkingWrite). Wait for A inside. Goroutine B: writeThrough("h1", "192.168.0.0/24", write that signals bEntered). Select bEntered vs 250ms: entered → fail; window passes → release A, drain both.
Assert: B never entered while A held the write-through; final cache equals the last value actually written (deterministic under correct code: B runs strictly after A).
Failure message: "a second write for the same host entered while the first was mid-write: decide→write→commit is no longer atomic per host — the cache can disagree with the row and suppress every later report".

4. The unreliable alarm: `TestStatusTrackerWriteThroughAtomic`

Verified the mechanism, and it is worse than "needs -count=5": I applied the unlock-across-the-write mutation and single -race runs flip ok/FAIL roughly coin-flip; -count=5 fails. Crucially the failure comes from the assertion, never a race report — the mutated code is still race-clean (the test's own mu covers lastWritten), so -race contributes nothing and the 300-pair lottery is the entire detector. It is also self-healing: a cache/row divergence is corrected by the next write of the other status, so only a divergence among the final few operations survives to the single end-state check. CI (make test) runs count=1: as a regression alarm this is a coin flip.
Fix: restructure, not pin the count. Rebuild it on the same park-inside-write pattern as inv 5 (parked "ready" writer, concurrent "failed" writer, exclusion + final-state assertions). Pinning -count (or looping internally) only raises the odds and keeps the self-healing blind spot. Keeping the stochastic loop as a cheap extra is fine, but the deterministic test is the alarm of record.
Same weakness elsewhere? No — checked both packages: the 300-pair loop is the only stochastic concurrency test; every other concurrent test is channel-sequenced (stepNoWait, wedge, syncsvc's own goroutine tests).

5. Incidental findings

quotaCheckLocked early return — confirmed, delete as a rider here. Every case below guards Max* > 0, so removing the early return changes no behaviour. "Dead" is slightly off: it executes (a fast path skipping the ledger sum when no caps are configured), but the saved work is a loop over tens of entries once per create attempt — noise. It is a guaranteed mutation blind spot and duplicates a rule the switch already codifies. One-line deletion; no separate issue.
SeedLedger — retire this finding, it is wrong. The auditor searched only the package. It has a production caller: internal/agent/run/cli.go:352, seeding the admission ledger from persisted records at agent startup — exactly what the Engine comment ("Rebuilt from persisted records via SeedLedger") points at. Not dead, no action, no issue.

Retired / corrected from the issue

Inv 3's stated mechanism (Marshal size-cache race) is obsolete under protobuf ≥1.36 — invariant kept, test redesigned to pointer ownership, comment needs rewording.
"SeedLedger has no callers" — false outside the package.
The implicit premise that wedging is impossible — the wedge exists; the gap is quiesce-before-assert plus no observable for exclusion, which is what the occupancy wrapper adds.

[claude 2026-08-23] Design for observing the reconcile concurrency invariants. Verified the headline claims by re-running two of the mutations myself (tree restored, `git diff --quiet` clean). One invariant's stated mechanism is obsolete and one incidental finding is wrong — both below. ## 1. Diagnosis: why this suite pins behaviour and not concurrency Two structural reasons, and neither is "no way to wedge a worker" — the harness already has one (`wedge()` in worker_test.go, plus `stepNoWait`). **(a) Every assertion reads quiesced end-state.** The canonical driver `f.step` is Step → `waitIdle` → `aggregateNow`. Quiesced end-state is interleaving-independent by construction, so no assertion in the suite *can* distinguish correct locking from broken locking. The wedge-based tests in worker_test.go are the exception, but they aim the wedge at liveness properties (report promptness, cross-VM concurrency, coalescing, the create cap) — none pairs a wedged worker with the structural stimulus that matters: a reap, a redeliver, a stale-generation publish, a concurrent collect. **(b) These are exclusion/ownership invariants, and `-race` is categorically blind to them here.** Every shared structure in the package is individually mutex-guarded (`manager.mu`, `worker.mu`, `Engine.mu`, the fake provisioner's own lock). So the violating executions are *race-clean*: two goroutines reconciling one VM perform zero unsynchronized memory accesses in the test environment — each pass writes its own `vmResult`, and everything they share is locked. `-race` detects unsynchronized access, not violated ownership. Its silence is by design, not by luck, which is why `-count=3` and higher bought nothing. Corollary: the fix is not five unrelated tests. Invariants 1, 2 and 4 are the *same* invariant — at most one pass in flight per VM — violated by three different mutations, and it needs one missing observable plus a handful of forced interleavings. Invariant 3's hazard needs restating first (see below). Invariant 5 and the unreliable alarm share one deterministic pattern. ## 2. Strategy: deterministic wedge + an occupancy observable, extending the existing harness **Chosen:** (a) one small addition to the reconcile test harness — an occupancy-tracking `Images` wrapper (per-vmID entry/exit gauge with a mutex-guarded high-water mark), composed with the existing `wedge()`; (b) for the trackers, a "park a writer inside `write()`" pattern that asserts mutual exclusion directly. All tests are channel-sequenced: the dangerous window is held open by a parked goroutine, the stimulus is applied, the observable is read. No repetition, no `-count`, deterministic under the `make test` flags CI actually uses (`go test -race -shuffle=on ./...` — count=1, checked). **Against `-race` + repetition:** blind per (b) above, and empirically a coin flip even where it isn't blind — see §4. **Against making it structural:** attractive for invariant 1 (a worker that deletes its own map entry on exit, with reap only signalling, turns "only idle workers are reaped" from a rule into ownership) and worth a follow-up issue if you want it. But types can't express "at most one goroutine executes passes for id" in Go — the `go w.run()` twice mutation defeats any map discipline from *inside* the structure — and nothing structural covers 2, 3 or 5. Any such refactor also needs these tests in place first to gate it. So: tests now; the structural rework for invariant 1 is optional and separately gated. One negative-window caveat, stated once: two of the tests below assert "a second goroutine did NOT enter" via a 250ms select. That is the suite's established pattern (`TestCreateConcurrencyIsCapped` uses exactly this) and its reliability is *scheduler liveness*, not an interleaving lottery: under the mutation the second goroutine is runnable and blocked on nothing, so it reaches the probe within the window essentially always. False-pass requires the scheduler to starve a runnable goroutine for 250ms. ## 3. Per-invariant designs ### Inv 1 — "Only IDLE workers are reaped" (worker.go:76) *Verified: I neutralized the idle check; suite green under `-race -count=2`.* - **Lives:** worker_test.go, `TestBusyWorkerIsNotReaped`. - **Harness:** existing `wedge()`. - **Interleaving:** deliver vm1 → wait `arrived` (pass parked in the fetch) → call `m.reapAbsent(map[string]assignment{})` directly, modelling the transiently-unreadable-record tick the comment names (LoadVMs skips a live VM, dropping it out of `live`). Driving this through Step is not cleanly reachable (the record exists while the pass runs, so the union puts vm1 back in `live`); the manager layer is already a first-class test surface here (`count`, `waitIdle`). - **Assert:** `m.count() == 1` immediately after `reapAbsent` — fully synchronous, zero timing. Then `close(release)`, `waitIdle`, `reapAbsent(empty)` again → `count() == 0` (the idle half, making the pair readable). - **Failure message:** "a busy worker was reaped: the next deliver spawns a second goroutine for this VM (concurrent Destroy vs Boot, orphaned hypervisor)". ### Inv 2 — the GENERATION RULE (worker.go:242) - **Lives:** narrate_test.go, `TestAStragglerFromAnEarlierPassCannotLandOnALaterOne` — the missing sibling of `TestNarrationCannotOutliveThePassThatSaidIt`, which only pins the `!w.busy` half. - **Harness:** an `Images` fake with two behaviours: pass 1 captures its progress callback (as the existing straggler test does) then returns an error; pass 2 publishes a distinguishable narration line, then parks on `release`. - **Interleaving:** `stepNoWait(snap(1, vm1))` → pass 1 fails, straggler captured, `waitIdle`. `stepNoWait(snap(2, vm1))` → pass 2 parked mid-fetch (`busy=true`, gen advanced), wait for its narration. Invoke the captured pass-1 callback. `aggregateNow`. - **Assert:** the row's `StatusDetail` is pass 2's line, never pass 1's. Deterministic — the worker is parked, nothing races. - **Kills both mutations:** `if !w.busy || gen != w.gen` → `if !w.busy`: busy is true, straggler admitted, pass-1 detail lands. Delete `w.gen++`: both passes carry gen 0, equality holds, same landing. - **Failure message:** "a publish from pass N landed while pass N+1 was in flight: the generation half of the publish guard is gone — the report shows a phantom state from a finished pass". ### Inv 3 — "collect clones the rows" (worker.go ~127) — **the argued hazard is obsolete; the invariant survives on different grounds** Be skeptical here as invited: the comment's mechanism — "proto.Marshal writes a size cache … two reports marshalled concurrently would race on one message" — is no longer true. protobuf v1.36.11 (this repo's version) reads and writes the size cache with `atomic.LoadInt32`/`StoreInt32` (verified in the module cache, `internal/impl/encode.go:56,67,128`). Concurrent Marshal of one message is race-clean, which is *why* the clone-removal mutation stayed green at `-race -count=5` — there is no race to catch, and the issue's proposed test shape (two concurrent aggregates, both Marshalled) would be a permanently-green alarm. Do not build it. The clone still earns its place, for a reason one line below the comment: **`vmResult.merge` writes into the row** — `r.vm.SshHostPubkey = r.hostPubKey` (reconcile.go:1090). Without the clone, every collect writes into the worker's live proto, and every report shares row pointers with every other report and with the worker (two Steps from concurrent sessions — the reconnect case syncsvc already documents — makes those writes genuinely concurrent). - **Lives:** worker_test.go, `TestEveryReportOwnsItsRows`. - **Harness:** none new. - **Interleaving:** none needed. Create vm1, `waitIdle`, then `aggregateNow` twice *sequentially*. - **Assert:** pointer non-identity — `findVM(rep1,"vm1") != findVM(rep2,"vm1")` (and both rows carry the pubkey). Single-threaded, deterministic, kills `own := res` outright. - **Failure message:** "two reports share one row proto: collect stopped cloning, and merge writes into a row other reports and the worker still hold". - **Rider for the implementer:** reword the CLONED comment — the size-cache claim is stale; the true argument is merge's write plus self-containment. ### Inv 4 — "one goroutine per VM — the worker IS the lock" - **Lives:** worker_test.go, `TestABusyVMNeverRunsTwoPassesAtOnce`. - **Harness:** the occupancy wrapper: wrap `Images` to increment/decrement a per-vmID gauge (mutex-guarded, recording the high-water mark) around the wedge. - **Interleaving:** wedge vm1's create (`arrived`). While parked, `stepNoWait` a second snapshot containing vm1 — this sets `pending`, the coalescing path. Select on a second `arrived` for 250ms: a second arrival is an immediate fail. Then `close(release)`, `waitIdle`, and assert `highWater("vm1") == 1`. - **Why it kills the mutation:** `run`'s wait condition is `pending == nil && !stopped` — it deliberately does not check `busy`, because one loop can't be in two places. A second `go w.run()` loop *is* in a second place: it consumes the new pending while loop 1 is parked and enters the fetch. It is runnable and unblocked — scheduler liveness, not luck (the caveat in §2). - **Failure message:** "two reconcile passes entered the provisioner for one VM at once: the worker is no longer the lock". This test also backstops inv 1's consequence (a reaped-while-busy worker plus a redeliver produces occupancy 2). ### Inv 5 — `netTracker.writeThrough` atomicity (server/syncsvc/tracker.go:103) - **Lives:** internal/server/syncsvc/tracker_test.go, `TestNetTrackerWriteThroughHoldsTheLockAcrossTheWrite`. - **Harness:** park-inside-write: writer A's `write` signals entered, then parks on a channel. - **Interleaving:** goroutine A: `writeThrough("h1", "10.0.0.0/24", parkingWrite)`. Wait for A inside. Goroutine B: `writeThrough("h1", "192.168.0.0/24", write that signals bEntered)`. Select `bEntered` vs 250ms: entered → fail; window passes → release A, drain both. - **Assert:** B never entered while A held the write-through; final cache equals the last value actually written (deterministic under correct code: B runs strictly after A). - **Failure message:** "a second write for the same host entered while the first was mid-write: decide→write→commit is no longer atomic per host — the cache can disagree with the row and suppress every later report". ## 4. The unreliable alarm: `TestStatusTrackerWriteThroughAtomic` Verified the mechanism, and it is worse than "needs -count=5": I applied the unlock-across-the-write mutation and single `-race` runs flip ok/FAIL roughly coin-flip; `-count=5` fails. Crucially the failure comes from the *assertion*, never a race report — the mutated code is still race-clean (the test's own `mu` covers `lastWritten`), so `-race` contributes nothing and the 300-pair lottery is the entire detector. It is also self-healing: a cache/row divergence is corrected by the next write of the other status, so only a divergence among the final few operations survives to the single end-state check. CI (`make test`) runs count=1: as a regression alarm this is a coin flip. **Fix: restructure, not pin the count.** Rebuild it on the same park-inside-write pattern as inv 5 (parked "ready" writer, concurrent "failed" writer, exclusion + final-state assertions). Pinning `-count` (or looping internally) only raises the odds and keeps the self-healing blind spot. Keeping the stochastic loop as a cheap extra is fine, but the deterministic test is the alarm of record. **Same weakness elsewhere?** No — checked both packages: the 300-pair loop is the only stochastic concurrency test; every other concurrent test is channel-sequenced (`stepNoWait`, `wedge`, syncsvc's own goroutine tests). ## 5. Incidental findings - **`quotaCheckLocked` early return — confirmed, delete as a rider here.** Every `case` below guards `Max* > 0`, so removing the early return changes no behaviour. "Dead" is slightly off: it executes (a fast path skipping the ledger sum when no caps are configured), but the saved work is a loop over tens of entries once per create attempt — noise. It is a guaranteed mutation blind spot and duplicates a rule the switch already codifies. One-line deletion; no separate issue. - **`SeedLedger` — retire this finding, it is wrong.** The auditor searched only the package. It has a production caller: `internal/agent/run/cli.go:352`, seeding the admission ledger from persisted records at agent startup — exactly what the Engine comment ("Rebuilt from persisted records via SeedLedger") points at. Not dead, no action, no issue. ## Retired / corrected from the issue - Inv 3's stated mechanism (Marshal size-cache race) is obsolete under protobuf ≥1.36 — invariant kept, test redesigned to pointer ownership, comment needs rewording. - "SeedLedger has no callers" — false outside the package. - The implicit premise that wedging is impossible — the wedge exists; the gap is quiesce-before-assert plus no observable for exclusion, which is what the occupancy wrapper adds.

a73x commented

2026-08-23 10:29:51 +00:00

(Migrated from git.a73x.sh)

[claude 2026-08-23] Claiming. Implementing Fable's design as posted: occupancy-wrapper + deterministic wedge for inv 1/2/4, pointer-ownership for inv 3, park-inside-write for inv 5 and the restructured statusTracker alarm. Riders: quotaCheckLocked early-return deletion and the CLONED comment reword. Every invariant will be mutation-proven before it lands.

a73x commented

2026-08-23 10:52:23 +00:00

(Migrated from git.a73x.sh)

[claude 2026-08-23] Done on branch reconcile-concurrency-observers (3 commits, off main 290ffad, make ci green). Fable's design followed as written; every invariant proven by its mutant at -race -count=5 -shuffle=on, 5/5 kills each, tree restored and git diff clean after every one.

inv 1 idle-only reap — mutant: delete the idle check. "a busy worker was reaped: the next deliver for this VM spawns a second goroutine for it, and a concurrent Destroy against a Boot orphans a hypervisor process"
inv 2 generation rule — two mutants (!w.busy || gen != w.gen -> !w.busy; delete w.gen++), both land pass 1's line on pass 2's row. Straggler invoked while pass 2 is parked mid-fetch; fully deterministic.
inv 3 collect clones — mutant: own := res. Asserted as pointer non-identity between two reports; single-threaded. Fable was right that the issue's proposed shape (two concurrent Marshals) would have been permanently green: protobuf v1.36.11 reads/writes sizeCache with atomics (verified in internal/impl/encode.go:56,67).
inv 4 one goroutine per VM — mutant: go w.run() twice. New occupancy gauge over the Images seam + a second assignment delivered while the first pass is parked. "two passes entered the provisioner for one VM at once: the worker is no longer the lock"
inv 5 netTracker atomicity — mutant: unlock across the write. Park-inside-write.

The unreliable alarm, measured rather than assumed: the old 300-pair TestStatusTrackerWriteThroughAtomic detected the unlock-across-write mutant on 3 of 12 single -race runs (make test runs count=1). Rebuilt on the parked-writer pattern: 5/5 at count=1. No stochastic loop kept — it added a second of runtime for a 25% alarm.

Riders:

quotaCheckLocked early return REMOVED. Not unreachable — it executes — but behaviourally dead: every switch arm below requires its own cap > 0, so no input (including negative caps) distinguishes the two spellings. TestQuotaZeroMeansUnlimited already covers it.
SeedLedger finding retired as Fable said: live caller at internal/agent/run/cli.go:352. Confirmed by grep across the whole tree, not the package.
Prose deleted where the new tests now hold it: reapAbsent's idle argument, the GENERATION RULE, collect's CLONED paragraph, netTracker.writeThrough's atomicity comment. The clone's stated mechanism was false as well as untested, so it was deleted rather than reworded.

2bc2ae23 (self-removing workers) evaluated and declined with reasoning posted there — the restructure trades an observed two-line check for a lock-order inversion, a stopped-but-mapped window in deliver, and eventual instead of synchronous Stop/reap.

[claude 2026-08-23] Done on branch `reconcile-concurrency-observers` (3 commits, off main 290ffad, make ci green). Fable's design followed as written; every invariant proven by its mutant at -race -count=5 -shuffle=on, 5/5 kills each, tree restored and git diff clean after every one. - inv 1 idle-only reap — mutant: delete the idle check. "a busy worker was reaped: the next deliver for this VM spawns a second goroutine for it, and a concurrent Destroy against a Boot orphans a hypervisor process" - inv 2 generation rule — two mutants (`!w.busy || gen != w.gen` -> `!w.busy`; delete `w.gen++`), both land pass 1's line on pass 2's row. Straggler invoked while pass 2 is parked mid-fetch; fully deterministic. - inv 3 collect clones — mutant: `own := res`. Asserted as pointer non-identity between two reports; single-threaded. Fable was right that the issue's proposed shape (two concurrent Marshals) would have been permanently green: protobuf v1.36.11 reads/writes sizeCache with atomics (verified in internal/impl/encode.go:56,67). - inv 4 one goroutine per VM — mutant: `go w.run()` twice. New occupancy gauge over the Images seam + a second assignment delivered while the first pass is parked. "two passes entered the provisioner for one VM at once: the worker is no longer the lock" - inv 5 netTracker atomicity — mutant: unlock across the write. Park-inside-write. The unreliable alarm, measured rather than assumed: the old 300-pair TestStatusTrackerWriteThroughAtomic detected the unlock-across-write mutant on 3 of 12 single -race runs (make test runs count=1). Rebuilt on the parked-writer pattern: 5/5 at count=1. No stochastic loop kept — it added a second of runtime for a 25% alarm. Riders: - quotaCheckLocked early return REMOVED. Not unreachable — it executes — but behaviourally dead: every switch arm below requires its own cap > 0, so no input (including negative caps) distinguishes the two spellings. TestQuotaZeroMeansUnlimited already covers it. - SeedLedger finding retired as Fable said: live caller at internal/agent/run/cli.go:352. Confirmed by grep across the whole tree, not the package. - Prose deleted where the new tests now hold it: reapAbsent's idle argument, the GENERATION RULE, collect's CLONED paragraph, netTracker.writeThrough's atomicity comment. The clone's stated mechanism was false as well as untested, so it was deleted rather than reworded. 2bc2ae23 (self-removing workers) evaluated and declined with reasoning posted there — the restructure trades an observed two-line check for a lock-order inversion, a stopped-but-mapped window in deliver, and eventual instead of synchronous Stop/reap.

No labels

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

a73x/eitri#97

No description provided.

Rows
Columns

reconcile: the concurrency invariants are argued in prose and observed by nothing #97

1. "Only IDLE workers are reaped" — worker.go:76

2. The GENERATION RULE — worker.go:242-255

3. collect clones the rows

4. "One goroutine per VM — the worker IS the lock"

5. netTracker.writeThrough atomicity — syncsvc/tracker.go:100

Related: one existing alarm is unreliable

Also found while mutating

1. Diagnosis: why this suite pins behaviour and not concurrency

2. Strategy: deterministic wedge + an occupancy observable, extending the existing harness

3. Per-invariant designs

Inv 1 — "Only IDLE workers are reaped" (worker.go:76)

Inv 2 — the GENERATION RULE (worker.go:242)

Inv 3 — "collect clones the rows" (worker.go ~127) — the argued hazard is obsolete; the invariant survives on different grounds

Inv 4 — "one goroutine per VM — the worker IS the lock"

Inv 5 — netTracker.writeThrough atomicity (server/syncsvc/tracker.go:103)

4. The unreliable alarm: TestStatusTrackerWriteThroughAtomic

5. Incidental findings

Retired / corrected from the issue

1. "Only IDLE workers are reaped" — `worker.go:76`

2. The GENERATION RULE — `worker.go:242-255`

3. `collect` clones the rows

5. `netTracker.writeThrough` atomicity — `syncsvc/tracker.go:100`

Inv 5 — `netTracker.writeThrough` atomicity (server/syncsvc/tracker.go:103)

4. The unreliable alarm: `TestStatusTrackerWriteThroughAtomic`