[unbalancedparentheses]

Follow-ups to #247 (planted-bug sensitivity). Tests, fuzz oracles, the planted runner and docs only; no library code.

Fuzzer oracles (fuzz/src/oracles.rs, fuzz/src/driver.rs)

• V1/V2 restart decisions: every replacement in a flat root tree is required by the slot's own exit and restart mode, or by an upstream sibling's failure (any sibling for OneForAll, an earlier one for RestForOne).
• V1/V2/V5 required restarts: in a tree that was never closed and did not fail, once settled, every published Permanent instance (and Transient one that exited abnormally) has a successor, and so does every running non-Temporary cohort sibling. A missing restart is an exhausted budget that failed to fail the supervisor.
• V5 exhaustion: a "restart budget exhausted" failure only when grants in the window plus sibling reservations reach max_restarts.
• V6 backoff: OneForOne restart delays in virtual time match the bound for the failure streak (reset after stable_after), from zero through it with jitter.
• X3: a non-trapping actor linked only to a peer survives its Normal exit and otherwise publishes the peer's reason.
• X5 unlink: no Exit and no linked death after both sides unlinked.
• T1 cancel: a cancelled timer delivers no tick due after the cancel.
• One harness false positive found and fixed on the way (V5 measured too early for a collateral OneForAll child); kept as fuzz/tests/budget_reserved_after_round.rs.

Second independent checks

01, 02: Kani restart_window_admits_exactly_within_budget, now runner layer K (both are unobservable through the public API: reserve_retry re-checks the same window before admit_in_window runs). 06: fuzzer V6. 11: fuzzer X5. 21: fuzzer T1. Each shown failing with its bug planted.

Bounded waits

within!(..) (concurrency/tests/support/deadline.rs, 120 s, virtual on the simulator) wraps 177 completion awaits in integration tests. Under bug 08, T now fails 19 named tests in 212 s instead of hanging. Bug 20 still hangs tasks::actor::tests::backend_blocking_handles_send_and_request, a unit test inside concurrency/src/tasks/actor.rs (#240's file, left alone); the runner now names hung tests.

Flaky test

semantics_gaps::supervision_contract::concurrent_failures_coalesce_into_one_round read current() after the first crash's OneForAll round had begun stopping siblings (ChildUnavailable(Stopping)). It now takes every generation before crashing any. Pinned to one CPU on fede: before, 8 of 300 and 3 of 150 runs failed (all at that unwrap); after, 0 of 1000. A test assumption, not a library bug.

Matrix (docs/TESTING.md, "Planted-bug sensitivity")

Layer	Before (#247)	After
T (unit, integration, failpoints)	22, 2 hangs (08, 20)	23, 1 hang (20, unit test in tasks/actor.rs)
S (simulated suites)	15	17
C (fuzz harness tests)	6	11
F (cargo fuzz, 600 s)	9	19
V (TLA+ trace validation)	4	4
K (Kani, new)	-	2 (01, 02)

23 of 24 caught, every caught bug by at least two layers; 15 is still unobservable. Controls: unpatched baseline missed in every layer, F for 900 s twice (440k and 770k executions).

No library bugs found; no discrepancy between the new oracles and the TLA+ models (Supervision.tla Restarts/Retries match the restart table the oracles encode).

[github-actions]

🤖 Codex Code Review

No actionable issues found. The changes improve bounded waits and fuzzing coverage without modifying production actor behavior.

I couldn’t run tests: the pinned Rust toolchain requires initialization, which is blocked by the read-only Rustup directory.

---

Automated review by OpenAI Codex · gpt-6.1-sol · custom prompt

[github-actions]

🤖 Claude Code Review

Review: PR #265, planted-bug follow-ups

This PR only touches tests, the fuzz harness, docs and scripts. No runtime code in concurrency/src changes, so there is no production risk. The within! approach is a clear improvement over CI job timeouts. Most findings below are about how strict or lenient the new oracles are, plus one safety concern in run.sh.

concurrency/tests/support/deadline.rs

• Macro mechanics are correct.
  • file!() and line!() inside macro_rules! resolve to the invocation site.
  • $crate::deadline resolves because every test crate declares mod deadline at its root.
  • $future is evaluated exactly once.
• Simulator caveat. The PR excludes paused-Tokio tests because virtual time auto-advances while work runs outside Tokio. The simulator has the same property.
  • The OS-thread tests are already compiled out under spawned_sim, so this is fine today.
  • Consider stating the invariant explicitly in the module doc so a future #[cfg(not(spawned_sim))] removal doesn't silently create early timeouts.
• Optional consistency nit. Many files now mix within!(x) with the existing spawned_rt::tasks::timeout(LIMIT, x).await.unwrap_or_else(...) pattern. Unifying them later would help readability.

concurrency/tests/semantics_gaps.rs (~L1839)

• The fix is correct. Snapshotting every current() before the first Crash removes the 1-CPU race.
• let _ = actor.send(Crash) now also hides a send that fails for an unexpected reason. Suggestion: assert!(actor.send(Crash).is_ok() || !actor.child_handle().is_alive()).
• The explicit drop(actors) is fine but not needed.

fuzz/src/driver.rs

1. crash_child → self.may_stop(aref.id()) (~L1069). This increments causes for every crash variant.

   • If the non-panic branches below it already call may_stop, the count becomes 2 for those children.
   • Any oracle gated on causes == 1 (X8, and linked_reason) would then silently skip them.
   • Please check that X8's coverage of supervised children did not drop. If it did, call may_stop only in the Panic branch.

2. unlink_checks (~L1880): lock ordering. me.child_handle().exit_reason() and other.child_handle().exit_reason() run while holding self.world.lock().

   • Actors may still be live during eventual(), and Worker::drop takes the world lock.
   • If exit_reason() ever takes an actor-internal lock that the runtime holds while dropping state, this deadlocks.
   • linked_reason already reads exit_reason() before locking. Do the same here for consistency and safety.

3. run_body stores ChildHandles in State (world.rs started()). They are taken before leaks(), which is good.

   • During the run, though, they keep each actor's shared state alive.
   • Please confirm that no in-run oracle in eventual() checks weak or strong counts of that state. If one does, add a comment noting the dependency.

fuzz/src/oracles.rs

1. abnormal(None) == true cuts in opposite directions.

   • In restart_justified it makes the check lenient (unknown is treated as justified).
   • In required_restarts it makes the check strict: a Transient instance with no published reason is treated as requiring a restart. That is a potential false-positive V5 if publication lags dropped.
   • Suggest skipping when x.reason.is_none() in required_restarts.

2. budget_exhaustion parses "restart budget exhausted by " out of the failure string (~L250).

   • If the message wording changes, the oracle silently returns and never fires.
   • Prefer a structured failure kind. Failing that, add a debug_assert! or a violation when failure.contains("budget exhausted") but parsing fails.

3. timers: the violation label "T: ..." does not match the docs' T1 (cancel).

   • The docs say shrinking matches on the oracle name.
   • Use "T1: ..." to match the other oracle labels (V5, X3, …).

4. slack() is 10 ms + 25% of the bound. This is generous and could hide an off-by-one-exponent bug at small bounds.

   • Fine if deliberate, given the patch-06 catch.
   • Worth a comment explaining why a quarter of the bound is needed rather than a fixed creep allowance.

5. Option::is_none_or is used here and in driver.rs. It requires Rust 1.82. Check that this matches the fuzz crate's MSRV and toolchain pin.

fuzz/src/world.rs

• factory_call parses index from the slot path with unwrap_or(0) (~L565).
  • A path format change would silently attribute every call to slot 0, which corrupts V1/V2 and V6.
  • Prefer passing the index explicitly from worker_spec, or expect(...) on the parse for flat slots.

verification/planted/run.sh

• The guard narrowed from concurrency to concurrency/src. Verify that the revert step after each patch is scoped to concurrency/src as well (git checkout -- concurrency/src or git apply -R).
  • If it still resets concurrency/, uncommitted edits under concurrency/tests would now be wiped without warning.
• layer_K builds a bash -c string with '$KANI_ENV'. A path containing ' breaks it.
  • Pass the path as a positional argument instead: bash -c '... . "$1" ...' _ "$KANI_ENV".
• layer_T hang detail. If libtest printed no "has been running" line, the detail ends with a dangling ": ".
  • Fall back to e.g. unknown when $slow is empty.

Docs and CHANGELOG

• Accurate and thorough.
• Minor: the matrix uses "T1" while the code uses "T", as noted above.

Verdict

LGTM after addressing:

• the run.sh revert scope,
• the causes double-count question,
• the lock held across exit_reason().

The rest are hardening suggestions.

---

Automated review by Claude · claude-opus-5-5 · custom prompt

[github-actions]

🤖 Grok Code Review

I'll inspect the new deadline helper and the fuzzer oracles more closely, since those are the behavioral changes most likely to hide bugs.

---

Automated review by Grok (xAI) · grok-4.7 · custom prompt

[github-actions]

🤖 Gemini Code Review

The bounded-wait helper (within!), the concurrent_failures_coalesce_into_one_round flake fix, the Kani runner layer, and the new scenario-fuzzer oracles are well-structured and well-documented.

I found a couple of edge cases in the new fuzzer oracle state tracking that can cause false positives or missed checks under certain generated scenarios/schedules:

1. backoff_delays stability window does not account for stopped_sleep or unpublished startups (fuzz/src/oracles.rs:321-332)

            match instance(s, prev).map(|(_, x)| (x.started_end_at, x.stopped_begin_at)) {
                Some((Some(ready), Some(stop))) => {
                    let up = stop.saturating_sub(ready);
                    if up >= b.stable_after + margin {
                        (lo, hi) = (0, 0);
                    } else if up + margin > b.stable_after {
                        lo = 0;
                    }
                }
                Some((Some(_), None)) => lo = 0,
                _ => {}
            }

Two issues can cause lo..=hi to diverge from the supervisor's actual streak:

1. stopped_sleep shifts when the supervisor observes the exit: x.stopped_begin_at is recorded at the start of Worker::stopped() (fuzz/src/world.rs:352), before rt::sleep(self.hooks.stopped_sleep()) (0..=255ms). When a OneForOne child panics or stops itself, the supervisor only observes the exit after stopped() completes and Worker drops (end = ended_at(s, prev)). If stop - ready < b.stable_after but end - ready >= b.stable_after (because of stopped_sleep), the supervisor resets the streak to 0 (delay = bound(0)), while backoff_delays keeps lo > 0 and fires a false-positive V6 violation when b.jitter == false.
2. Unpublished startup_timeout instances can still set started_end_at: When startup_timeout fires while Worker::started() is sleeping in started_sleep, the actor task's started() future is not cancelled immediately; if it finishes its sleep before teardown/cleanup finishes, it sets x.started_end_at and then runs stopped(). If stop - ready >= b.stable_after + margin (e.g., from queued work or stopped_sleep), backoff_delays resets hi = 0 even though the supervisor never marked the generation ready and kept the non-zero streak.

Using stop.saturating_sub(ready) (gated on x.published) as the lower bound on uptime (to reset hi = 0) and end.saturating_sub(ready) as the upper bound on uptime (to reset lo = 0) avoids both false positives:

            if let Some((_, x)) = instance(s, prev) {
                if let Some(ready) = x.started_end_at {
                    let min_up = x
                        .stopped_begin_at
                        .map_or(Duration::ZERO, |stop| stop.saturating_sub(ready));
                    let max_up = end.saturating_sub(ready);
                    if x.published && min_up >= b.stable_after + margin {
                        (lo, hi) = (0, 0);
                    } else if max_up + margin > b.stable_after {
                        lo = 0;
                    }
                }
            }

2. Inst::published is only marked when targets() or crash_child() samples a child (fuzz/src/driver.rs:449-459, 902-915, 1515-1535)

mark_published is currently called only from Driver::targets() and Driver::crash_child() (on the single crashed child).

• spawn_supervisor does not mark the initial generations after builder.start().await succeeds.
• settled() / quiesce() does not mark the live generations after restarts settle.

As a result, in a scenario (or shrunk regression) that runs Supervisor followed by CrashChild { child: 0 } without an intervening op that calls targets(), sibling c1 (and any rebuilt generation) has published == false. In fuzz/src/oracles.rs, published == false causes required_restarts (lines 187, 219) to skip those instances/siblings and causes could_stop_itself (line 71) to treat them as unpublished startups.

Calling mark_published on live current() refs at the end of spawn_supervisor and in settled() (or at the end of quiesce()) ensures every generation observed alive in its slot is marked published = true.

3. Minor: restart_justified collateral check when a sibling drops just before prev.seq (fuzz/src/oracles.rs:150-156)

            let collateral = slots.iter().enumerate().any(|(k, other)| {
                upstream(sup.strategy, j, k)
                    && other.iter().any(|c| {
                        c.seq < next.seq
                            && ended(s, c).is_some_and(|e| e > prev.seq && e < next.seq)
                    })
            });

ended(s, c) for an Outcome::Instance is s.insts[i].dropped, which is recorded in Drop for Worker on the actor's task before the supervisor controller task is polled to receive the exit. If upstream sibling k drops at tick e while the supervisor is starting slot j (prev.seq > e, e.g. in a RestForOne round for j alone), and the supervisor then processes k's exit and supersedes the round, e will be < prev.seq even though k's exit is what stopped prev. Checking whether c's successor in other started after prev.seq (in addition to e < next.seq) would guard against that interleaving.

---

Automated review by Gemini · gemini-4-argon · custom prompt

[github-actions]

🤖 DeepSeek Code Review

Review notes

Mostly test-harness changes; the bounded within! waits are a clear improvement.

Issues

1. fuzz/src/oracles.rs, budget_exhaustion
let siblings = sup.children.saturating_sub(1); counts every declared sibling. required_restarts explicitly excludes RestartMode::Temporary siblings from cohort restarts, but this calculation does not. If Temporary siblings do not reserve restart budget, the oracle will overcount reservations and miss an exhaustion bug. Filter to restartable/reserving siblings (likely exclude RestartMode::Temporary).

2. fuzz/src/oracles.rs, restart_justified
   The collateral check only requires an upstream sibling attempt to have ended between prev.seq and next.seq; it does not require that the sibling actually triggered a restart round (e.g., its own mode/reason required a restart). A Temporary sibling that exits normally, or a Transient one that exits Normal, could falsely justify a restart of j. Add the same restart-required predicate used for the child itself to the candidate sibling before accepting it as collateral.

3. fuzz/src/driver.rs, nested_configure
factory_call(&world, parent_inst, &path, mode); ignores the returned call index and never pairs it with factory_outcome, leaving Call.outcome as Pending for nested supervisors. Currently oracles only handle sup.flat, so it is harmless, but it breaks the Call invariant and will cause wrong skips when oracles expand to nested trees. Record an explicit outcome or add an Outcome::NestedSupervisor variant.

4. fuzz/src/driver.rs, quiesce
while !self.timers.is_empty() { self.cancel_timer(0); } removes the first element repeatedly, O(n²) for many timers. Prefer for (timer, id) in self.timers.drain(..) { ... } and mark cancelled in one pass.

5. Lock/time ordering in fuzz/src/driver.rs and fuzz/src/world.rs
cancel_timer, closing, Worker::Drop, and the started/stopped hooks call now() while holding the World mutex (self.world.lock()). Today now() likely reads simulator time without locking, but if that ever changes it becomes a lock-inversion/deadlock. Capture let now = now(); before acquiring the lock in those places, as factory_call already does.

---

Automated review by DeepSeek · deepseek-v4-pro · custom prompt

[github-actions]

🤖 Kimi Code Review

No blocking correctness or concurrency issues found. The bounded waits are a useful improvement, and the new fuzz bookkeeping avoids holding the world lock across awaits.

Minor test-harness concerns:

• fuzz/src/oracles.rs, budget_exhaustion (around lines 225–244): the oracle silently returns when the human-readable failure string does not contain "restart budget exhausted by " or the parsed slot cannot be found. An unrelated error-message refactor could therefore disable V5 coverage without anyone noticing. Prefer structured failure information where possible, or at least expose an “oracle skipped/unparsed” diagnostic so this coverage regression is visible.

• concurrency/tests/semantics_gaps.rs (around lines 1847–1851): let _ = actor.send(Crash); suppresses every send error, although only errors caused by siblings already entering the restart round are expected. This can mask unrelated premature mailbox closure. Consider accepting the error only when the actor is observed stopping/dead and failing otherwise; retaining the collected handles and generation assertions otherwise looks correct.

Otherwise, the timer cancellation accounting, restart-oracle bounds, and within! macro usage look reasonable.

---

Automated review by Kimi (Moonshot AI) · kimi-k3.1-pro · custom prompt