Skip to content

Cover aliasing, panic safety, and cross-thread use under miri - #135

Open
cf-rhett wants to merge 1 commit into
jamesmunns:mainfrom
cf-rhett:soundness-tests
Open

Cover aliasing, panic safety, and cross-thread use under miri#135
cf-rhett wants to merge 1 commit into
jamesmunns:mainfrom
cf-rhett:soundness-tests

Conversation

@cf-rhett

Copy link
Copy Markdown

Summary

Three gaps in the current suite, all of them things that pass a normal cargo test and only bite under miri:

  • no test holds a read grant and a write grant into the same allocation at the same time, which is the aliasing case the whole design rests on
  • nothing unwinds out of commit or release, so a grant that panics partway through its teardown is untested
  • nothing puts the producer and consumer on separate threads, despite that being the crate's central claim

Six tests covering those, gated on std for std::thread and catch_unwind. The no-std and embedded builds are unaffected — cargo test with no features still passes, as does the full matrix below.

The unwind cases use a Notifier whose wakes panic. That is a convenient lever: it makes commit and release fail after the coordinator has been updated but before the grant has finished releasing its queue handle, which is exactly where a double release or a leaked Arc would hide. The tests assert the strong count returns to its baseline and that a Weak cannot be upgraded afterwards, and that the frame is still published and the write slot reopened.

Testing

Passes under both borrow models, 16 tests either way:

  • ./miri.sh
  • MIRIFLAGS="-Zmiri-disable-isolation -Zmiri-ignore-leaks -Zmiri-tree-borrows" cargo +nightly miri test --target x86_64-unknown-linux-gnu --features=std
  • cargo test --features=std
  • cargo test (no features)
  • cargo build --no-default-features
  • cargo build --features=std
  • cargo build --no-default-features --target=thumbv6m-none-eabi
  • cargo build --target=thumbv6m-none-eabi --features=portable-atomic-unsafe-assume-single-core

Note

Independent of my other open PRs, and touches a file none of them do. Worth mentioning that these leak under -Zmiri-disable-isolation alone on current main — that is the same leak #131 fixes, not anything new here, and they are clean once #131 lands.

The suite has no test that holds a read grant and a write grant into the same
allocation at once, none that unwinds out of a commit or release, and none that
puts the two halves on different threads. Each of those is a place where a stale
pointer, a double release, or a torn coordinator update would pass a normal run
and only show up under miri.

Six tests, gated on `std` for threads and `catch_unwind`, so the no-std builds
are unaffected. A panicking `Notifier` is the lever for the unwind cases: it
makes `commit` and `release` fail partway through, after the coordinator has
been updated but before the grant has finished tidying up.
@cf-rhett
cf-rhett marked this pull request as ready for review July 31, 2026 19:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant