Repository navigation
quest: plan Miri GenMC and OSS-Fuzz - #8473
Conversation
Adds ten quests from a /quest-plan on what could be proved about moq-net: an inductive routing invariant, a Tamarin model of the route key proof, whole-session fuzzing, Kani codec proofs, a JS replay of the fuzz corpus, mutation testing, Miri seeds with ThreadSanitizer, and trace validation for the resume, reconnect, and subscribe models. Moves route trace validation to m1 and adds a Coverage-table symbol check to the nightly models quest. Co-Authored-By: Claude <noreply@anthropic.com>
Follow-ups from the moq-net confidence plan: an m5 quest waiting on Miri's GenMC mode, and an m4 quest for continuous fuzzing on OSS-Fuzz behind the whole-session targets. Co-Authored-By: Claude <noreply@anthropic.com>
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 22 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
kixelated
left a comment
kixelated
left a comment
There was a problem hiding this comment.
Automated review by review (OpenAI)
Reviewed commit 4fa6aaf, separating the five-file follow-up delta from its #8472 parent. No new actionable findings in that delta.
Overall direction: the GenMC work explicitly waits on upstream support, bounds its test workloads, and records limitations; OSS-Fuzz waits on both whole-session targets and maintainer approval/contact selection. The build-profile and regression-replay requirements match the existing fuzz workflow. The inherited Kani proof-contract finding remains tracked in #8472: #8472 (review).
Verification limits: GitHub-only static review of the plans, stack comparison, current upstream Miri GenMC documentation, and existing fuzz documentation. No builds, tests, GenMC runs, OSS-Fuzz integration, or external application performed.
![pullfrog[bot]](https://avatars.githubusercontent.com/in/1768019?s=60&v=4){kind=small}
There was a problem hiding this comment.
ℹ️ Minor suggestions only — one caveat on the TSan plan; the three findings filed against the stacked #8472 still stand.
Reviewed changes
Reviewed the complete 18-file diff at 4fa6aaf end to end, including the 15 quest files inherited from the stacked #8472, and checked each plan's load-bearing claims against the tree (Nightly's fuzz matrix, sh/rs/miri.sh, .cargo/mutants.toml and mutants.yml, the verify-* Coverage tables, route/proof.rs plus js/net/src/lite/route_key.ts and the draft's Route Key Parameter, and every /quest/ link).
- m1 proofs and checks —
route-inductive(Apalache inductive invariant over the route rules),route-key-model(Tamarin proof of the Route Key Parameter),session-fuzz(whole-session fuzz on both protocols with a bystander oracle), plus the route trace validation promoted from m4. - m4 real-code checks —
codec-kani,fuzz-corpus-js,mutants,miri-seeds-tsan, and the resume/reconnect/subscribe trace validations reusing route's recorder. - Follow-ups —
oss-fuzz(waits on the maintainer's application and contact address, required behindsession-fuzz) andmiri-genmc(waits on upstreamcargo miri testsupport); the m1/m4/m5 indexes are updated. - Not repeated here — the three findings open on #8472 (per-form varint ranges, the mutation quest against
quest/m0/ci/trim.md, and the m1 cut gate) still apply to this branch; they are tracked with the parent PR that owns those files.
deepseek-v4.1-flash-1017 (free via Pullfrog for OSS) ｜ 𝕏
| - ThreadSanitizer: a `just rs tsan` recipe builds std with the sanitizer | ||
| (`-Zsanitizer=thread -Zbuild-std`) and runs the kio and moq-net library | ||
| tests at near-native speed, reaching the tests Miri ignores for foreign | ||
| calls or cost. A suppression needs a comment naming the false positive. |
There was a problem hiding this comment.
Rust's sanitizer docs state ThreadSanitizer does not support std::sync::atomic::fence, yet the goal and this bullet credit the TSan run with catching ordering bugs in kio's log, whose cross-thread ordering is exactly the fence(Acquire)/fence(Release) pair in log.rs. Scope TSan to the races it can model and leave fence ordering to the Miri passes (and m5's GenMC), otherwise this lane either suppresses the fence sites or claims coverage it cannot have.
Technical details
# TSan cannot model the fence ordering kio's log relies on
## Affected sites
- `quest/m4/miri-seeds-tsan.md:5-8` — goal: "an ordering bug in the locks, atomics, wakers, and kio's lock-free log fails Nightly"
- `quest/m4/miri-seeds-tsan.md:25-28` — the TSan bullet
- `quest/m4/miri-seeds-tsan.md:39` — Related row: "the ordering in kio's log these runs watch", which is the fence-ordered part
- `rs/kio/src/log.rs:199` — `fence(Ordering::Acquire)`
- `rs/kio/src/log.rs:582` — `fence(Ordering::Release)`
- `quest/m4/crossbeam-pin-fence.md` — calls that ordering "what only a weak-memory check can confirm"
## Required outcome
- The plan names which tool owns fence-ordered accesses, e.g. TSan for the atomics/locks/wakers and the Miri many-seeds or GenMC passes for the epoch fence, and the Related row stops implying TSan covers it.
## Suggested approach (optional)
- One sentence in the TSan bullet, e.g. "TSan does not model `atomic::fence`, so kio's epoch fence ordering stays with the Miri passes."
- Source: the Rust unstable book's `sanitizer` page, "ThreadSanitizer does not support atomic fences `std::sync::atomic::fence`, nor synchronization performed using inline assembly code."
|
quest land watch: the merge queue removed this pull request at 4fa6aaf because it conflicts with The land fixer works on it in the background, and the watcher re-enqueues it at the back of the queue once it is fixed or judged flaky, or hands it back here with what it needs. (written by quest land watch) |
|
quest land watch: armed auto-merge on this pull request at 388f850, so it joins the back of the merge queue once its required checks pass, with the land fixer's fix ( (written by quest land watch) |
Problem
moq-dev/moq#8472 suggested two follow-ups worth a quest: an exhaustive, shim-free replacement for loom once Miri supports it, and continuous fuzzing beyond Nightly's five minutes per target.
Approach
Stacked on #8472, which is queued: this branch starts from its head, so the diff shows only these two quests once it lands.
cargo miri testin GenMC mode.Decisions
Impact
Public API: none. Wire: none. Quest files only.
Alternatives
One PR per follow-up: both are small quest files from the same plan, so they share this one.
Follow-ups
None.
Models
Size: XS
Implementer: Claude Code, claude-fable-5-2, high effort
🤖 Generated with Claude Code
Review
mechanical fix by codex, gpt-6.1-sol, medium effort:
Merged base and re·solved the add/add quest conflict preserving both versions' intent; passed git diff --cached --check and nix develop --command just ci base.(head 388f850)Rewritten by
quest reviewafter each round.01a1c7ec-0589-7692-bd20-4c7ed2a6d58a, round 1The quest plans are coherent and their dependencies are explicit, with no actionable defects identified; builds and tests were not run as instructed.(Written by Claude Fable 5 with high effort)