M9: !Sync compile-fail (trybuild) + Send assertion (§6.2/§14.6)#29
Merged
Conversation
Proves single-writer enforcement at compile time. Adds a `trybuild` dev-dep and
`tests/ui.rs` + `tests/ui/wal_not_sync.rs` (+ pinned .stderr): asserting
`Wal<NullObserver>: Sync` must NOT compile -- the PhantomData<Cell<()>> marker
(§6.2) makes the handle !Sync, so concurrent writers are a compile error
("`Cell<()>` cannot be shared between threads safely"). The Send half (handle is
movable across threads) is asserted positively by a new `wal::tests::
handle_is_send`.
The runtime directory-lock requirement (§14.6) is ALREADY covered by the existing
`wal::tests::second_open_is_locked` (a second in-process Wal::open of the same dir
returns WalError::Locked via the exclusive flock on dir/LOCK) -- not duplicated.
trybuild .stderr fragility handled honestly: it is toolchain-sensitive, so it
runs ONLY in the per-PR `test` job (stable) -- the MSRV job is `cargo check`,
which builds the runner but does not execute it, so .stderr is compared against
exactly one toolchain. Regenerate with `TRYBUILD=overwrite cargo test --test ui`
on a rustc bump (documented in Cargo.toml, tests/ui.rs, §14.6). Generated +
verified on rustc 1.94.1; the diagnostic wording is stable rustc phrasing.
Docs: §14.6 (the !Sync + dir-lock bullets) + a new §14.13 single-writer DoD row +
CLAUDE.md. cargo test (22 ok-lines incl. ui/handle_is_send/second_open_is_locked),
clippy --all-targets -D warnings, cargo fmt --check, MSRV 1.85 (trybuild v1.0.117
builds, Cargo.lock updated) all green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Rpbwt9JT56hQvVXiqTS131
guyo13
pushed a commit
that referenced
this pull request
Jun 29, 2026
…Sync Per the review on PR #30 (closed unmerged): the loom publish-barrier harness was green independently of the crate (it imported only loom::sync::* and re-built the integrator's cursor inside the test), so it validated a textbook Release/Acquire fact, not this code. It can't be wired to the library either: the writer is `!Sync` by construction (PhantomData<Cell<()>>, §6.2, proven statically by the #29 trybuild test), so there is no intra-WAL shared-memory concurrency for loom to model -- and a static !Sync proof is stronger than an empirical model check. The only Release/Acquire barrier is the integrator's publish cursor (out of scope, §1/§15.7); the WAL's observer-ordering obligation is covered by the §15.8 DurabilityObserver contract tests. Docs-only correction (no code/dep/CI -- the loom dep/test/workflow lived only on the closed PR #30 and never reached main): - §14.6: replace the loom-harness bullet with a normative not-applicable note, conditioned on the writer staying !Sync (a future Sync redesign re-opens it). - §14.6 concurrency cross-ref + the tooling/deps list: de-loom'd. - v6 changelog: entry recording the removal + rationale. - CLAUDE.md: drop loom from the dev-tools list + a status entry. Same discipline as the §14.4d negative result: the characterized "why not" is the deliverable, not a silent deletion. cargo fmt --check clean (docs-only). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Rpbwt9JT56hQvVXiqTS131
guyo13
pushed a commit
that referenced
this pull request
Jun 29, 2026
…Sync Per the review on PR #30 (closed unmerged): the loom publish-barrier harness was green independently of the crate (it imported only loom::sync::* and re-built the integrator's cursor inside the test), so it validated a textbook Release/Acquire fact, not this code. It can't be wired to the library either: the writer is `!Sync` by construction (PhantomData<Cell<()>>, §6.2, proven statically by the #29 trybuild test), so there is no intra-WAL shared-memory concurrency for loom to model -- and a static !Sync proof is stronger than an empirical model check. The only Release/Acquire barrier is the integrator's publish cursor (out of scope, §1/§15.7); the WAL's observer-ordering obligation is covered by the §15.8 DurabilityObserver contract tests. Docs-only correction (no code/dep/CI -- the loom dep/test/workflow lived only on the closed PR #30 and never reached main): - §14.6: replace the loom-harness bullet with a normative not-applicable note, conditioned on the writer staying !Sync (a future Sync redesign re-opens it). - §14.6 concurrency cross-ref + the tooling/deps list: de-loom'd. - v6 changelog: entry recording the removal + rationale. - CLAUDE.md: drop loom from the dev-tools list + a status entry. Same discipline as the §14.4d negative result: the characterized "why not" is the deliverable, not a silent deletion. cargo fmt --check clean (docs-only). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Rpbwt9JT56hQvVXiqTS131
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
2 participants
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.
M9 §14.6 — single-writer enforced at compile time
Proves the single-writer contract (§6.2) at the type level, complementing the runtime directory lock.
What's here
!Synccompile-fail proof —trybuilddev-dep +tests/ui.rsrunner +tests/ui/wal_not_sync.rs(+ pinned.stderr): asserts thatWal<NullObserver>: Syncdoes not compile. The handle'sPhantomData<Cell<()>>marker makes it!Sync, so sharing a handle across threads — i.e. a concurrent second writer — is a compile error (Cell<()>cannot be shared between threads safely).Sendpositive assertion — newwal::tests::handle_is_sendasserts the handle isSend(movable to another thread). Together: "Send but !Sync".wal::tests::second_open_is_locked(a second in-processWal::openof the same dir returnsWalError::Lockedvia the exclusiveflockondir/LOCK). Not duplicated.trybuild
.stderrfragility — handled honestlyThe pinned diagnostic is toolchain-sensitive. To avoid cross-toolchain flakiness:
uitest runs only in the per-PRtestjob (stable). The MSRV job iscargo check, which builds the runner but does not execute it, so.stderris compared against exactly one toolchain.TRYBUILD=overwrite cargo test --test uiafter a rustc bump that changes the wording — documented inCargo.toml,tests/ui.rs, and §14.6.cannot be shared between threads safely) is stable rustc phrasing, and trybuild normalizes the$RUSTpath.If you'd prefer zero stderr maintenance, the alternative is a
compile_faildoctest (asserts non-compilation without pinning the message) — happy to switch; I went with trybuild as §14.6 specifies.Verification
cargo test(22 ok-lines incl.ui/handle_is_send/second_open_is_locked),cargo clippy --all-targets -D warnings,cargo fmt --check, MSRV 1.85 (trybuildv1.0.117 builds;Cargo.lockupdated) all green.Docs
§14.6 (the
!Sync+ dir-lock bullets marked implemented) + a new §14.13 single-writer DoD row + CLAUDE.md.M9 status
Fuzz F1–F4 ✅, Miri ✅,
!Sync/dir-lock ✅ here. Remaining: loom publish-barrier → soak → CI-matrix tidy-up; plus the F1–F4 N-CPU-hour release-gate observation (OPEN on a dedicated runner).🤖 Generated with Claude Code
Generated by Claude Code