Repository navigation
Conversation
Owner
|
Rebase, we broke master briefly by not enforcing rebase before merge :) |
The table's positional file is now a trait with TableFile as the one production impl and the default type parameter, so callers are unchanged. `open` becomes `load(file, inram_max_bytes)` with the env cap passed in. Its sync primitives, and StrongTxTable's dirty-tracking atomics, come through `rbitcoin_store::sync`, which re-exports std, or loom / shuttle under `--cfg loom` / `--cfg shuttle`; those crates still spell `try_update` as `fetch_update`, so the module adapts it. Pure move; the array_table suite pins it.
`tests/model` (`--test model`, empty under the default cfg) races one writer, up to two flushers, and readers calling `set` / `set_many` / `truncate` / `get` against `flush_dirty` over an in-memory ArrayFile with TableFile's logical end, persisted HWM, and reopen view, and with faults at `write_at` (whole or torn) and at both `set_logical_len` failure points. The writer's RAM states form one history and everything observed must come from it: each reader's `get` / `len` results fit the states in order; every successful flush, checked while it still holds the flush lock, leaves the file, its reopen, and `disk_len` at one state; a restart after the race reopens one state or the in-prefix rewrite residual the scenario names; one quiescent flush brings everything to the last state; a flush never writes below the lowest index the writer touched. loom (`--cfg loom`, preemption bound 3) explores interleavings and Acquire/Release; shuttle (`--cfg shuttle`, seeded PCT and random) covers shapes past loom's four-thread cap. `MODEL_LOOM_EXHAUSTIVE=1`, `MODEL_SHUTTLE_ITERS`, and `MODEL_SHUTTLE_DEPTH` raise the budget for a deep run; each scenario prints its execution count. Both crates are `cfg`-target dependencies of rbitcoin-store and never reach a product binary. corosensei (shuttle) pins windows-sys 0.59 beside the tree's 0.61; deny.toml skips that one duplicate.
After `truncate`, a flush that still shrank the file took the length-only branch and ignored `dirty_lo`, so every `set` below the old on-disk length that landed before it was dropped. No current caller reaches that branch: `disconnect_tip` and the open-time trim flush the shrink before the next set, so the sets that follow are appends. The contract is fixed for the next caller that does not. The shrink-only branch now requires nothing dirty below the new length; otherwise the general path rewrites from the lowest dirty index, then shrinks. `truncate` marks `new_len` instead of 0, so a plain shrink still writes no bytes. The model's lowest-touched pin fails on the old mark, since a plain shrink then rewrote `[0, n)` on disk. The default suite pins the lost write on the real TableFile.
On the fd-only path `get` loads `len`, then preads the slot. A truncate
landing in between shrinks the file, so the pread fails
`Corrupt("pread past logical end")`; and once a later set has regrown the
file, the pread returns the new value while `len()` still reports the
shorter table, a state no single writer step has. The in-RAM path
re-checks under the read lock and returns 0. The fd-only path now does
the same: a `Corrupt` pread, or a value that `len` does not cover after
the read, is the absent value. `pread_at` is the only `Corrupt` source
there.
`mark_dirty_index` bumps the generation, then reads `dirty_lo` with a Relaxed load. The clean step resets `dirty_lo` and CASes the generation to 0 with Release, but the bump's read side was Relaxed, so a set landing right after a clean could read the stale pre-reset `dirty_lo`, skip its CAS, and leave the next flush with nothing below `disk_len` to write: an in-prefix set lost on disk. x86 read-modify-writes are full fences, so only aarch64 can show it; loom's memory model finds it and shuttle cannot. The bump now acquires. `StrongTxTable` shares the helper.
The general path skipped `set_logical_len` when `n == disk`. After a rewrite that grew the file failed its HWM persist, the file's end was already ahead of `disk_len`; a truncate back to exactly `disk_len` then flushed without shrinking it, leaving a stale tail on disk that a reopen showed. The append path's `debug_assert` on the file end tripped on the same sequence. The length is now published on every rewrite. The module doc names the residuals a kill inside an in-prefix rewrite leaves: a torn range, or a new prefix over an old tail when the table also shrank.
`./scripts/model-check.sh loom|shuttle [cargo test args]` sets the engine cfg and a per-engine target silo (`target/model-<engine>`; the cfg invalidates every artifact, so it must not share `target/dev`), then runs `cargo test -p rbitcoin-store --test model`. `model.yml` runs both engines on every pull request and master push, not as a required check, and a nightly schedule at the deep budget (loom bound 5, a million shuttle schedules at depth 5) seeded by the run id, so coverage accumulates.
TESTING.md owns how to run the suite, the per-engine silo, what the pins are, which checker owns what (loom the lock-free kernels and their orderings, shuttle the shapes past four threads), and the CI versus nightly budgets. crash-recovery.md names the in-prefix rewrite residuals the suite reproduces. concurrency.md and the store AGENTS.md point at it. The changelog fragment records the fixes.
phlip9-github-agent
Bot
force-pushed
the
phlip9/store-array-table-model
branch
from
October 25, 2026 21:49
90f65bb to
1d137d7
Compare
![rearden-grok[bot]](https://avatars.githubusercontent.com/u/730881?s=60&v=4){kind=small}
Owner
|
Thanks for your work on this! I'm gonna do an alternative PR that instead reduces the concurrency guards in ArrayTable (because it's written only by 1 thread, and has a specific shape that doesn't need the level of guards it currently has). Might be that shape looks better than making these fixes on the existing shape. TIL about loom and shuttle. |
rearden-grok Bot
pushed a commit
that referenced
this pull request
Oct 26, 2026
The loom and shuttle harness follows phlip9's #1214: cfg-gated model tests, a separate target directory, and the same pull-request, push, dispatch, and nightly jobs. This pull request is an alternative to that ArrayTable model. Those scenarios stay on #1214. The models here are the script-pool claim order, the idle turn, the UTXO view stamp, the Class C sequence counter, and Class C flush exclusion. A script-pool claim release-publishes next after in_wave.
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.
I was skimming through
rbitcoin-storeyesterday and got a bit freaked out after seeing Relaxed atomics all over the place. IMO this sort of code is impossible to write correctly without a concurrency model checker 😅So anyway, I got a bit nerd-sniped and threw Fable and some Opus subagents at
ArrayTableovernight...For these sorts of low-level concurrent data structures, I typically use
tokio-rs/loom.loom's quite nice here, because it actually modelsRelaxed+Acquire/Release/AcqRelatomic ops. It also does exhaustive checking, so it runs every possible interleaving within a depth limit. Withloomwe managed to find a few (minor) concurrency and crash safety bugs! Beyond that, this should give us more confidence to optimize these data structures even further.Without too much extra effort, I've also added
awslabs/shuttle, which is similar but does probabilistic, randomized checking without a depth limit. It only models atomics asSeqCst(so basically x86-64). In this particular PR, it's not really adding much overloom. Rather,shuttlestarts to shine as we expand concurrency model checking up the stack. By comparison,loomstruggles to explore larger state spaces.Both
loomandshuttleare gated behindcfg(loom)andcfg(shuttle)flags respectively. They should never touch production code.(AI dump)
ArrayTablewrite-behind is model-checked underloomandshuttle, and the four defects the suite found are fixed, one commit each.Seam and shim.
ArrayTable<F: ArrayFile = TableFile>: the positional file is a six-method trait withTableFileas the one production impl, so callers are unchanged.rbitcoin_store::syncre-exportsstd, orloom/shuttleunder--cfg loom/--cfg shuttle. Both are cfg-target dependencies and never reach a product binary. They still spelltry_updateasfetch_update, so the module carries a one-trait adapter until tokio-rs/loom#429 and awslabs/shuttle#405 land.Suite.
cargo test -p rbitcoin-store --test model, empty under the default cfg. One writer, up to two flushers, and readers raceset/set_many/truncate/getagainstflush_dirtyover an in-memory file withTableFile's logical end, persisted HWM, reopen view, torn writes, and faults at bothset_logical_lenfailure points. The writer's RAM states form one history and everything observed must come from it: each reader'sget/lenresults fit the states in order; every successful flush, checked while it still holds the flush lock, leaves the file, its reopen, anddisk_lenat one state; a restart after the race reopens one state or the in-prefix rewrite residual the scenario names; a flush never writes below the lowest index the writer touched. loom runs 35 scenarios at preemption bound 3 in about 9 s and models Acquire/Release; shuttle runs 38 (three past loom's four-thread cap) with seeded PCT and random schedules in about 30 s../scripts/model-check.sh loom|shuttleruns either;model.ymlruns both per PR, not as a required check, and nightly at the deep budget seeded by the run id.Fixes, each shown Red by the scenarios its commit adds:
truncate, a flush that still shrank the file took the length-only branch and ignoreddirty_lo, so everysetbelow the old on-disk length that landed before it was dropped. No current caller reaches that branch:disconnect_tipflushes the shrink alone. Also pinned in the default suite on the realTableFile.getracing atruncatereturnedCorrupt("pread past logical end"), or a regrown slot's value whilelen()still reported the shorter table. It now reads as absent, as the in-RAM path already did.dirty_lothrough the bump's Relaxed read side and lose an in-prefix write. Only aarch64 can show it; loom finds it and shuttle cannot.set_logical_lenwhen the length matcheddisk_len; after a failed HWM persist that left a stale tail on disk that a reopen showed.Checked, not changed. A torn in-prefix rewrite, and a shrinking rewrite whose length publish fails or dies between its two writes, leave reopen images that are no state of the writer.
crash-recovery.mdnames both; the tip window's hash chain and trailing-null trim coverconfirmed. Hand-reverting 2e9726c, a37a099, and 0bea970 each fails a scenario. A deep run (loom bounds 4 and 5, exhaustive where it finished inside 15 min, four runs of 76M shuttle schedules at depths 3, 5, and 8) found nothing beyond the fixes above.StrongTxTableshares the fixed bump helper but has no flush lock and the same length-skip shape; it is the next model target.