Skip to content

mempipe: make the crate testable under Miri - #23

Merged
gamozolabs merged 2 commits into
mainfrom
mempipe-miri-harness
Sep 24, 2026
Merged

gamozolabs merged 2 commits into
mainfrom
mempipe-miri-harness

Conversation

@gamozolabs

Copy link
Copy Markdown
Collaborator

Follow-up to #22: the Miri harness used to verify that fix, plus the reproducer example mentioned there.

Miri support (4e0237c)

Miri cannot execute shm_open or mmap, so this adds a heap-backed pipe that exists on every target: SendPipe::create_local() and the unsafe RecvPipe::open_raw(). The sushi_roll paths become thin wrappers over them and pipe init is shared by both constructors. No cfg(miri) in library code; the only Miri-specific lines are #[cfg_attr(miri, ignore)] on the three shm-based tests and the size constants in the new test.

It also fixes a latent provenance bug: both chunk pointers were derived from chunks[ii].0[0], which under Stacked Borrows only has provenance for that one byte, so every access past it was UB. Tree Borrows accepts it, which is why it went unnoticed. Now taken from the whole array with .cast::<UnsafeCell<u8>>().

A new multi_reader test runs on a local pipe everywhere and shrinks itself under Miri so it can be swept over seeds:

MIRIFLAGS="-Zmiri-preemption-rate=0.5 -Zmiri-seed=$seed" \
    cargo +nightly-2024-03-01 miri test -p mempipe -- multi_reader

Run with and without -Zmiri-tree-borrows; neither aliasing model contains the other. On the code before #22 this fails about a third of seeds with a data race between the sender's chunk write and a reader's chunk read. On current main it is clean for 30 seeds under each model, and also under -Zmiri-strict-provenance and -Zmiri-symbolic-alignment-check.

Reproducer example

examples/hang.rs is a native reproducer for the pre-#22 bug. Random preemption never hit the race on a 16-core box because it needs two stalls at once, so this injects them: signal handlers that busy-wait a few microseconds, fired at the sender and reader threads at a bounded duty cycle. The library runs unmodified. Settings that hang the old code within seconds are in its doc comment, as are settings that hit the ticket-0 hole (sequence checked first with client_seq still initialised to 0). Miri is the better regression test; this is for watching it happen natively.

🤖 Generated with Claude Code

gamozolabs and others added 2 commits September 23, 2026 17:18
Miri cannot execute shm_open or mmap, so add a heap-backed pipe that works
on every target: SendPipe::create_local() plus the unsafe
RecvPipe::open_raw(). The sushi_roll paths become thin wrappers over it,
and pipe init is shared by both constructors. Both handles remember which
backing store they hold so drop frees the right thing.

Take chunk pointers from the whole chunk array instead of its first
element. A pointer derived from chunks[i].0[0] only has provenance for
that one byte under Stacked Borrows, so every access past it was
undefined behaviour. Tree Borrows accepts it, which is why it went
unnoticed. Miri refuses to run the crate under Stacked Borrows until this
is fixed.

The three shm-based tests are ignored under Miri. A new multi_reader test
runs on a local pipe everywhere and shrinks itself under Miri so it can be
swept over seeds:

    MIRIFLAGS="-Zmiri-preemption-rate=0.5 -Zmiri-seed=N" \
        cargo +nightly-2024-03-01 miri test -p mempipe -- multi_reader

Run it with and without -Zmiri-tree-borrows; neither aliasing model
contains the other. On the code before the stranded-buffer fix (#22)
this sweep fails about a third of seeds with a data race between the
sender's chunk write and a reader's chunk read. On current main it is
clean under both models.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Random preemption never reproduced the pre-#22 stranding bug on a 16-core
machine because it needs two stalls at once: a reader between its loads
and the sender between its stores. examples/hang.rs injects them with
signal handlers that busy-wait a few microseconds, fired at the sender
and reader threads at a bounded duty cycle so a stopped thread is stuck
in the library, not in the handler. The library runs unmodified.

On a hang it prints the outstanding tickets; a duplicate or wrong payload
exits with its own message instead of masquerading as a hang. The doc
comment records settings that hang the old code within seconds and
settings that hit the ticket-0 hole of a sequence-first check with
client_seq still initialised to 0.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
@gamozolabs
gamozolabs merged commit cbb9c62 into main Sep 24, 2026
0 of 2 checks passed
@gamozolabs
gamozolabs deleted the mempipe-miri-harness branch September 24, 2026 00:23
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