Add seeded concurrency race harness for lease/reservation stores#148
Draft
bpapillon wants to merge 2 commits into
Draft
Add seeded concurrency race harness for lease/reservation stores#148bpapillon wants to merge 2 commits into
bpapillon wants to merge 2 commits into
Conversation
…alance The idempotent server hands a racing acquire the same active lease back. If that stale response lands after the local row's expiry (e.g. a concurrent extend pushed the server-side expiry forward), replace() saw an "expired" slot and rewrote it — resetting localRemainingCredits to the full grant and erasing debits whose reservations are still open, minting local credits. Found by the seeded race harness (seed 1061, both backends): replace with the SAME leaseId over an expired row now reconciles like an extend (granted-to-total, expiry only forward, balance untouched) and reports "kept", so the manager's redundant-release logic is unaffected.
…on stores The conformance suite pins sequential semantics; the truly concurrent interleavings (single-flight, extend-vs-expiry, release-vs-sweeper, replace-vs-reserve) were prose invariants only. Per seed, N workers run randomized op sequences over shared slots with seeded micro-yields varying the event-loop interleaving, against both the in-memory and (fake) Redis stores plus the lease manager over a scripted wire server; at quiescence the prose invariants are asserted (conservation, bounded leak, expiry monotonicity, pinned refunds/extends, exactly-once claims, no expired-balance serves via a clock-fenced probe). Deterministic per seed: RACE_SEED replays a failing schedule exactly; RACE_ITERATIONS scales the batch (default 40 per scenario/backend).
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.
The conformance suite (#147) pins sequential semantics with deterministic vectors and leaves the truly concurrent interleavings as prose invariants. This adds a seeded randomized race harness (
tests/races/) that exercises exactly those gaps, against both store backends (in-memory and Redis-via-fake, like the existing unit suites) and theCreditLeaseManagerover a scripted wire server with simulated latency.Races covered (one scenario each, plus mixed chaos):
replace) on one slot — keep-first, at most one writtenconsume) racing the sweeper — exactly-once claims; exact conservation (granted == remaining + open holds + consumed + crash-leaked) catches double and lost refundsreplaceracingtry_reserve— plus a clock-fenced probe proving no debit ever lands on an expired leaseEach run is deterministic per seed (seeded PRNG drives ops, amounts, virtual-clock advances, and the microtask/
setImmediateyields that vary interleaving; ids are counters). A failure prints the seed;RACE_SEED=<n>replays the exact schedule;RACE_ITERATIONS=<n>scales the batch (default 40 per scenario/backend, ~1s total in CI).Found defect (fixed here, first commit): at seed 1061 (both backends) the harness caught a real race — the idempotent server hands a racing acquire the same active lease back, and if that stale response lands after the local row's expiry (e.g. a concurrent extend pushed the server-side expiry forward),
replacerewrote the "expired" slot:localRemainingCreditsreset to the full grant, erasing debits whose reservations were still open (seed-1061 trace: installlse_srv_2→ reserve 40 + 7.75 → expiry passes → stalereplace(lse_srv_2)resets 452.25 → 500, minting 40 held credits). Fix: a same-id replace over an expired row reconciles like an extend (granted-to-total, expiry only forward, balance untouched) and reports "kept"; the manager's redundant-release logic is unaffected. Sequential regression tests added for both stores and the real-Redis integration suite (Lua verified against redis:7). Note for #147: SPEC.md'sreplaceprose ("only if the slot is empty or the existing lease is expired") should gain the same-id carve-out; no existing vector pins the old behavior.Local seed batches: 10,000 seeds per scenario/backend (120k runs, ~140s) clean after the fix; the harness was also validated by mutation testing (8 hand-injected store/manager bugs — dropped expiry guards, dropped refund/extend pins, clobbering replace, non-exactly-once consume, non-converging extend, releasing the installed lease — all caught with the failing seed reported).
Verification limits: the Redis store runs against the shared
fake-redis(synchronous Lua emulation), so real-Redis-only interleavings (e.g. gaps insideadd()'s index writes) are out of scope here, as is server-clock skew — both remain covered only by the opt-in integration suite.