From 672a23ba42838c112d926572d026636d766bae38 Mon Sep 17 00:00:00 2001 From: Zachery Aaron Shores-Chmielewski Date: Sat, 28 Mar 2026 12:07:08 +0700 Subject: [PATCH] feat: runtime guarantees and checks Exhaustive checks of the statespace that enable us to give formal guarantees about runtime properties. --- src/RUNTIME_GUARANTEES.md | 157 --- src/guarantees/RUNTIME_GUARANTEES.md | 222 ++++ src/guarantees/correspondence.rs | 1168 +++++++++++---------- src/guarantees/g10_supervisor.rs | 57 +- src/guarantees/g4_lifecycle.rs | 18 +- src/guarantees/mod.rs | 20 +- src/guarantees/model_checker.rs | 221 ++++ src/guarantees/stateright_death_orphan.rs | 439 ++++++++ src/guarantees/stateright_lifecycle.rs | 354 +++++++ src/guarantees/stateright_supervisor.rs | 403 +++++++ src/std/mod.rs | 2 +- src/std/supervisor.rs | 52 +- src/worker.rs | 47 +- 13 files changed, 2348 insertions(+), 812 deletions(-) delete mode 100644 src/RUNTIME_GUARANTEES.md create mode 100644 src/guarantees/RUNTIME_GUARANTEES.md create mode 100644 src/guarantees/model_checker.rs create mode 100644 src/guarantees/stateright_death_orphan.rs create mode 100644 src/guarantees/stateright_lifecycle.rs create mode 100644 src/guarantees/stateright_supervisor.rs diff --git a/src/RUNTIME_GUARANTEES.md b/src/RUNTIME_GUARANTEES.md deleted file mode 100644 index 14af5de..0000000 --- a/src/RUNTIME_GUARANTEES.md +++ /dev/null @@ -1,157 +0,0 @@ -# Runtime Guarantees - -**Date**: 2026-03-17 -**Branch**: `runtime-guarantees` -**Enforcement**: Compiler (type system), Kani (bounded model checking), proptest (property-based testing) - -## Abstract - -This document catalogs the guarantees the swactor runtime makes to its users. Each guarantee is a contract: if the runtime compiles and its verification suite passes, the guarantee holds. Guarantees are enforced in layers — the compiler prevents the most fundamental violations statically, Kani proofs exhaust bounded state spaces for state-machine invariants, and property-based tests cover emergent behavior across randomized scenarios. - -A guarantee listed here is a **promise**. Code that violates a guarantee is a bug in the runtime, not in the user's actor. - ---- - -## Enforcement Strategy - -Three layers, ordered by strength: - -1. **Compiler (type system)** — Make violations unrepresentable. `Send + 'static` bounds, ownership, lack of `&mut` aliasing. Zero runtime cost, impossible to bypass without `unsafe`. - -2. **Kani (bounded model checking)** — Symbolically execute all reachable states within bounded inputs. Proves invariants exhaustively for small state spaces (lifecycle flags, supervisor restart FSMs). CI cost only. - -3. **Proptest (property-based testing)** — Randomized operation sequences against reference models or invariant assertions. Covers composition effects and emergent behavior that bounded proofs can't reach. Test-time only. - -A guarantee is **fully contracted** when all applicable layers enforce it. A guarantee is **aspirational** when the contract is defined but the codebase does not yet conform. - ---- - -## Guarantee Catalog - -### G1: No Shared Mutable State - -> Two actors never hold mutable references to the same memory. - -**Status**: Fully contracted (compiler). - -**Enforcement**: The `Message` trait requires `'static + Clone + Send + Sync`. Actor state is owned by `Box` inside `ActorSlot`, which is only accessed by the owning worker's `tick_all`. The `ActorInterface` trait requires `Send + 'static`. Rust's ownership system makes aliased mutable access a compile error. - -**No additional verification needed.** This is a language-level guarantee. - ---- - -### G2: Single-Threaded Actor Execution - -> An actor's `handle()`, `on_start()`, and `on_stop()` are never called concurrently. No reentrancy. - -**Status**: Fully contracted (compiler). - -**Enforcement**: `ActorSlot` is stored in `ActorPool`, which is owned (not shared) by a single `Worker`. `tick_all` takes `&mut self` on the pool and iterates actors sequentially. There is no `Arc>` — the pool is thread-local. An actor cannot be called from two threads because it literally exists on only one thread's stack. - -**No additional verification needed.** Structural ownership makes concurrent calls uncompilable. - ---- - -### G3: Actor Identity Uniqueness - -> No two live actors share an `ActorAddress`. An address identifies exactly one actor for its lifetime. - -**Status**: Fully contracted (compiler + runtime structure). - -**Enforcement**: `ActorAddress::new_random()` generates 32 cryptographically random bytes. The `AddressMap` is a `HashMap` — duplicate insertion overwrites, but since addresses are 256-bit random, collision probability is ~2^-128 (birthday bound). The address map is the single source of truth for routing; an address not in the map is dead. - -**Kani (future opportunity)**: Could prove that `AddressMap::insert` followed by `AddressMap::lookup` returns the inserted `WorkerId`, and that `remove` makes subsequent lookups return `None`. Not required — compiler enforcement is sufficient. - ---- - -### G4: Lifecycle Ordering - -> For every actor: `on_start()` is called exactly once before the first `handle()`. `on_stop()` is called at most once, after the last `handle()`. No `handle()` calls occur after `on_stop()` or after the actor is poisoned. - -**Status**: Fully contracted (compiler + Kani). - -**Enforcement**: `ActorSlot` has boolean flags `started`, `stopping`, `poisoned`. `tick_all` checks `started` before calling `on_start`, sets it after. `stopping` and `poisoned` actors are skipped in the message-processing loop and collected in `cleanup_dead`. - -**Kani**: Bounded mirror of the lifecycle FSM in `src/kani/lifecycle.rs`. Proofs cover: -- `on_start` fires exactly once, before any `handle`. -- `handle` is never called when `stopping || poisoned`. -- `on_stop` fires at most once, only when `stopping && !poisoned`. -- No transition sequence reaches `handle` after `on_stop`. -- Suspension pauses message processing; resume restores it. No `handle` during suspension. - ---- - -### G5: Fault Isolation - -> A panic in actor A does not corrupt actor B's state, skip B's messages, or prevent B's lifecycle hooks from firing. - -**Status**: Fully contracted (catch_unwind + structural separation + proptest). - -**Enforcement**: `handle()` is wrapped in `std::panic::catch_unwind`. On panic, only the panicking actor's slot is marked `poisoned` and its mailbox cleared. Other actors in the same pool are unaffected — iteration continues. Each actor's state is in its own `ActorSlot`; there is no shared mutable structure between slots. - -**Proptest**: `src/proptest_g5.rs` — three property-based test scenarios: -- Spawn N actors, one panics at a random message index. Assert all others process all their messages and complete lifecycle normally. -- An actor panics in `on_start`. Assert sibling actors spawned before and after are unaffected. -- Multiple actors panic in the same tick. Assert non-panicking actors are unaffected. - ---- - -### G6: Death Notification Completeness - -> If actor A monitors actor B (via `monitor()` or `watch()`), and B dies, A receives exactly one `Down` (for monitors) or `ActorExited` (for watchers) notification. - -**Status**: Fully contracted (proptest). - -**Enforcement**: `MonitorRegistry` and `WatchRegistry` in `StdExtension` track monitor/watch relationships. `on_actor_death()` iterates all registered monitors/watchers for the dead actor and emits notifications. `cleanup_dead()` removes the dead actor's entries. - -**Proptest**: `src/proptest_g6_g7.rs` — property-based tests covering: -- For every (monitor, monitored) pair where the monitored actor dies, exactly one `Down` is delivered. -- For every (watcher, watched) pair where the watched actor dies, exactly one `ActorExited` is delivered. -- No notifications for actors still alive. -- Demonitored relationships produce no notification. -- Multiple monitors each get exactly one `Down`. - ---- - -### G7: Orphan Cleanup - -> If an actor dies and its children are not supervised, all unsupervised children are stopped. - -**Status**: Fully contracted (proptest). - -**Enforcement**: `ChildrenRegistry` tracks parent-child relationships. On parent death, `cleanup_dead` checks if each child has a supervisor. Unsupervised children receive `StopSignal`. - -**Proptest**: `src/proptest_g6_g7.rs` — property-based tests covering: -- Spawn tree structures (parent with N children). Kill the parent. Assert all unsupervised children eventually stop. -- Supervised children are handled by their supervisor, not orphan-killed. -- Cascading orphan cleanup through multiple tree levels. - ---- - -### G8: Supervisor Restart Correctness - -> A supervisor restarts exactly the children specified by its strategy (`OneForOne`, `OneForAll`, `RestForOne`) and respects the restart policy (`Permanent`, `Transient`, `Temporary`) of each child. - -**Status**: Fully contracted (Kani). - -**Kani**: `src/kani/supervisor.rs` — bounded model of supervisor restart decision logic. For 4 children, symbolically enumerates all combinations of strategy (`OneForOne`, `OneForAll`, `RestForOne`), which child dies, each child's restart policy (`Permanent`, `Transient`, `Temporary`), and death reason (normal stop vs. panic). Proves: -- `OneForOne`: restarts only the dead child (if policy permits). -- `OneForAll`: restarts all children (respecting policies). -- `RestForOne`: restarts dead child + all after it (respecting policies). -- `Temporary` children are never restarted. -- `Transient` children restart only on panic. - ---- - -## Conformance Summary - -| Guarantee | Compiler | Kani | Proptest | Conforms | -|-----------|----------|------|----------|----------| -| G1: No shared mutable state | Yes | — | — | Yes | -| G2: Single-threaded execution | Yes | — | — | Yes | -| G3: Address uniqueness | Yes | — | — | Yes | -| G4: Lifecycle ordering | Partial | Yes | — | Yes | -| G5: Fault isolation | Partial | — | Yes | Yes | -| G6: Death notification completeness | — | — | Yes | Yes | -| G7: Orphan cleanup | — | — | Yes | Yes | -| G8: Supervisor restart correctness | — | Yes | — | Yes | diff --git a/src/guarantees/RUNTIME_GUARANTEES.md b/src/guarantees/RUNTIME_GUARANTEES.md new file mode 100644 index 0000000..b7d1a62 --- /dev/null +++ b/src/guarantees/RUNTIME_GUARANTEES.md @@ -0,0 +1,222 @@ +# Runtime Guarantees + +**Date**: 2026-03-19 +**Branch**: `runtime-guarantees` +**Enforcement**: Compiler (type system), Kani (bounded model checking), exhaustive correspondence (deterministic enumeration), Stateright-style DFS model checking (exhaustive state exploration) + +## Abstract + +This document catalogs the guarantees the swactor runtime makes to its users. Each guarantee is a contract: if the runtime compiles and its verification suite passes, the guarantee holds. Guarantees are enforced in layers — the compiler prevents the most fundamental violations statically, Kani proofs exhaust bounded state spaces for production decision functions, deterministic correspondence tests enumerate every reachable input combination, and exhaustive DFS model checking explores every reachable state of the runtime state machines. + +A guarantee listed here is a **promise**. Code that violates a guarantee is a bug in the runtime, not in the user's actor. + +--- + +## Enforcement Strategy + +Four layers, ordered by strength: + +1. **Compiler (type system)** — Make violations unrepresentable. `Send + 'static` bounds, ownership, lack of `&mut` aliasing. Zero runtime cost, impossible to bypass without `unsafe`. + +2. **Kani (bounded model checking)** — Symbolically execute all reachable states within bounded inputs. Proves invariants exhaustively for production decision functions (`should_skip_actor`, `is_on_stop_eligible`, `determine_stop_reason`, `should_restart`, `compute_restart_set`). CI cost only. + +3. **Exhaustive correspondence (deterministic enumeration)** — Every reachable combination of inputs is tested deterministically via nested loops with explicit enumeration counters. No random sampling (proptest has been removed from correspondence). Covers decision function truth tables and runtime behavioral agreement. + +4. **DFS model checking (exhaustive state exploration)** — A minimal inline DFS model checker (`src/guarantees/model_checker.rs`) explores every reachable state of bounded runtime state machines. Properties are checked in every visited state. `always` properties prove safety invariants; `sometimes` properties prove liveness (non-vacuousness). Models cover lifecycle (G4/G5), death notifications and orphan cleanup (G6/G7), and supervisor restart (G8). + +A guarantee is **fully contracted** when all applicable layers enforce it. + +--- + +## Verification Architecture + +### Production Decision Functions + +Core decision logic has been extracted from `tick_all`, `cleanup_dead`, and `Supervisor::handle_down` into standalone pure functions in production code. These are the functions that Kani proves and correspondence tests enumerate: + +| Function | Defined in | Called by | +|----------|-----------|-----------| +| `should_skip_actor(poisoned, stopping, suspended) → bool` | `worker.rs` | `tick_all` loop | +| `is_on_stop_eligible(stopping, poisoned) → bool` | `worker.rs` | `cleanup_dead` | +| `determine_stop_reason(poisoned, has_exit_value) → StopReason` | `worker.rs` | `cleanup_dead` | +| `RestartPolicy::should_restart(reason) → bool` | `std/supervisor.rs` | `Supervisor::handle_down` | +| `compute_restart_set(strategy, dead_idx, num_children) → Vec` | `std/supervisor.rs` | `Supervisor::handle_down` | + +Kani proofs and Stateright models call these production functions directly — not test-only mirrors. + +### Model Bounds + +| Model | Actors/Children | Mailbox/Events | Other bounds | Min. unique states | +|-------|----------------|----------------|--------------|-------------------| +| Lifecycle (G4/G5) | 3 actors | max_handle=2 | — | >100 | +| Monitor (G6) | 3 actors | — | 6 monitor pairs | >100 | +| Orphan (G7) | 4 actors | — | max 3 parent-child links | >100 | +| Supervisor (G8) | 4 children | — | max_restarts=3, max_deaths=4, 243 init states (3 strategies × 3⁴ policies) | >100 | + +These bounds are sufficient because: +- The decision functions are pure over small enum/boolean domains — the state space is inherently finite. +- Stateright models explore *every* reachable state via DFS, not a sample. The bounds limit model size to keep exploration tractable while covering all behavioral combinations. +- Liveness canaries (`sometimes` properties) verify that interesting states (panics, restarts, cascading cleanup, meltdown) are actually reachable, preventing vacuous proofs. + +--- + +## Guarantee Catalog + +### G1: No Shared Mutable State + +> Two actors never hold mutable references to the same memory. + +**Status**: Fully contracted (compiler). + +**Enforcement**: The `Message` trait requires `'static + Clone + Send + Sync`. Actor state is owned by `Box` inside `ActorSlot`, which is only accessed by the owning worker's `tick_all`. The `ActorInterface` trait requires `Send + 'static`. Rust's ownership system makes aliased mutable access a compile error. + +**No additional verification needed.** This is a language-level guarantee. + +--- + +### G2: Single-Threaded Actor Execution + +> An actor's `handle()`, `on_start()`, and `on_stop()` are never called concurrently. No reentrancy. + +**Status**: Fully contracted (compiler). + +**Enforcement**: `ActorSlot` is stored in `ActorPool`, which is owned (not shared) by a single `Worker`. `tick_all` takes `&mut self` on the pool and iterates actors sequentially. There is no `Arc>` — the pool is thread-local. An actor cannot be called from two threads because it literally exists on only one thread's stack. + +**No additional verification needed.** Structural ownership makes concurrent calls uncompilable. + +--- + +### G3: Actor Identity Uniqueness + +> No two live actors share an `ActorAddress`. An address identifies exactly one actor for its lifetime. + +**Status**: Fully contracted (compiler + runtime structure). + +**Enforcement**: `ActorAddress::new_random()` generates 32 cryptographically random bytes. The `AddressMap` is a `HashMap` — duplicate insertion overwrites, but since addresses are 256-bit random, collision probability is ~2^-128 (birthday bound). The address map is the single source of truth for routing; an address not in the map is dead. + +--- + +### G4: Lifecycle Ordering + +> For every actor: `on_start()` is called exactly once before the first `handle()`. `on_stop()` is called at most once, after the last `handle()`. No `handle()` calls occur after `on_stop()` or after the actor is poisoned. + +**Status**: Fully contracted (compiler + Kani + exhaustive correspondence + DFS model checking). + +**Enforcement**: `ActorSlot` has boolean flags `started`, `stopping`, `poisoned`. The production function `should_skip_actor(poisoned, stopping, suspended)` determines whether to skip an actor during `tick_all`. `is_on_stop_eligible(stopping, poisoned)` determines whether `on_stop` fires in `cleanup_dead`. + +**Kani** (`src/guarantees/g4_lifecycle.rs`): Five proof harnesses calling production functions: +- `proof_g4a_on_start_exactly_once` — `on_start` fires exactly once before any `handle`. +- `proof_g4b_no_handle_when_stopping_or_poisoned` — `should_skip_actor` prevents handle calls. +- `proof_g4c_on_stop_conditions` — `is_on_stop_eligible` fires only when `stopping && !poisoned`. +- `proof_g4d_no_handle_after_on_stop` — no handle after on_stop. +- `proof_g4e_suspension_pauses_handle` — `should_skip_actor` blocks handle during suspension. + +**Exhaustive correspondence** (`src/guarantees/correspondence.rs`): Deterministic enumeration of all 16 boolean flag combinations (2⁴ for `should_skip_actor`, `is_on_stop_eligible`, `determine_stop_reason` truth tables). Runtime behavioral tests verify agreement between decision functions and actual actor behavior for healthy, poisoned, stopping, and panicking actors. + +**DFS model checking** (`src/guarantees/stateright_lifecycle.rs`): Exhaustive DFS over 3-actor lifecycle state machine. Properties verified in every reachable state: +- `on_start_count ≤ 1` for every actor +- `handle_count > 0 ⇒ on_start_count == 1` +- Poisoned/stopping actors never increment `handle_count` +- `on_stop_count ≤ 1` for every actor +- `on_stop` only fires when `stopping && !poisoned` +- No handle after on_stop + +Liveness canaries confirm reachable states where `handle_count > 0`, `on_stop_count == 1`, and fault isolation (one actor poisoned while another handles). + +--- + +### G5: Fault Isolation + +> A panic in actor A does not corrupt actor B's state, skip B's messages, or prevent B's lifecycle hooks from firing. + +**Status**: Fully contracted (catch_unwind + structural separation + exhaustive tests + DFS model checking). + +**Enforcement**: `handle()` is wrapped in `std::panic::catch_unwind`. On panic, only the panicking actor's slot is marked `poisoned` and its mailbox cleared. Other actors in the same pool are unaffected — iteration continues. Each actor's state is in its own `ActorSlot`; there is no shared mutable structure between slots. + +**DFS model checking** (`src/guarantees/stateright_lifecycle.rs`): G5 properties verified in every reachable state: +- A `Panic` action on actor `i` never changes any flag or counter of actor `j ≠ i`. +- After a tick containing a panic for actor `i`, all other actors' `handle_count` reflects their full mailbox drain (not short-circuited). + +**Runtime tests** (`src/guarantees/g5_fault_isolation.rs`): Three deterministic scenarios: +- Panic at random index isolates siblings. +- `on_start` panic isolates siblings. +- Multiple panics in same tick isolate non-panicking actors. + +--- + +### G6: Death Notification Completeness + +> If actor A monitors actor B (via `monitor()` or `watch()`), and B dies, A receives exactly one `Down` (for monitors) or `ActorExited` (for watchers) notification. + +**Status**: Fully contracted (exhaustive tests + DFS model checking). + +**Enforcement**: `MonitorRegistry` and `WatchRegistry` in `StdExtension` track monitor/watch relationships. `on_actor_death()` iterates all registered monitors/watchers for the dead actor and emits notifications. `cleanup_dead()` removes the dead actor's entries. + +**DFS model checking** (`src/guarantees/stateright_death_orphan.rs`, MonitorModel): Exhaustive DFS over 3-actor monitor model with 6 monitor pairs. Properties verified in every reachable state: +- For every (watcher, watched) pair where watched is dead: notification count == 1. +- For every actor still alive: notification count == 0. +- Demonitored pairs produce zero notifications. + +Liveness canaries: monitor fires, demonitor suppresses notification. + +**Runtime tests** (`src/guarantees/g6_g7_death_orphan.rs`): Deterministic tests covering monitor notifications, watch notifications, demonitor suppression, and multiple monitors per target. + +--- + +### G7: Orphan Cleanup + +> If an actor dies and its children are not supervised, all unsupervised children are stopped. + +**Status**: Fully contracted (exhaustive tests + DFS model checking). + +**Enforcement**: `ChildrenRegistry` tracks parent-child relationships. On parent death, `cleanup_dead` checks if each child has a supervisor. Unsupervised children receive `StopSignal`. + +**DFS model checking** (`src/guarantees/stateright_death_orphan.rs`, OrphanModel): Exhaustive DFS over 4-actor orphan model with max 3 parent-child links. Properties verified in every reachable state: +- After orphan cleanup, all unsupervised children of the dead parent are dead. +- Supervised children survive orphan cleanup. +- Cascading: if an orphan-cleaned parent's child also dies and is orphan-cleaned, its unsupervised children are dead too. + +Liveness canaries: orphan cleanup triggers, cascading cleanup is reachable, supervised child survives cleanup. + +**Runtime tests** (`src/guarantees/g6_g7_death_orphan.rs`): Deterministic tests covering orphan cleanup, supervised children surviving, and cascading cleanup through multiple tree levels. + +--- + +### G8: Supervisor Restart Correctness + +> A supervisor restarts exactly the children specified by its strategy (`OneForOne`, `OneForAll`, `RestForOne`) and respects the restart policy (`Permanent`, `Transient`, `Temporary`) of each child. + +**Status**: Fully contracted (Kani + exhaustive correspondence + DFS model checking). + +**Kani** (`src/guarantees/g10_supervisor.rs`): Proofs call production functions `RestartPolicy::should_restart` and `compute_restart_set`. Symbolically verifies all combinations of strategy, policy, dead index, and death reason for up to 4 children. + +**Exhaustive correspondence** (`src/guarantees/correspondence.rs`): Deterministic enumeration of: +- `should_restart` truth table: 3 policies × 2 reasons = 6 combinations +- `compute_restart_set`: 3 strategies × 4 child counts × all dead indices = 30 combinations +- Runtime behavioral verification: supervisor setup → child death → restart observation for each combination + +**DFS model checking** (`src/guarantees/stateright_supervisor.rs`): Exhaustive DFS over supervisor model with 4 children, 243 initial states (3 strategies × 3⁴ policy combinations), max 3 restarts, max 4 deaths. Properties verified in every reachable state: +- `OneForOne`: only dead child in restart log (if policy permits). +- `OneForAll`: all children in restart log (if policy permits). +- `RestForOne`: dead child + successors in restart log (if policy permits). +- `Temporary`: never restarted regardless of reason or strategy. +- `Transient` + normal death: not restarted. +- `Transient` + panic: restarted (if not meltdown). +- Meltdown: if total restarts exceed max, supervisor stops, no further restarts. + +Liveness canaries: restart occurs, meltdown is reachable, each strategy is exercised. + +--- + +## Conformance Summary + +| Guarantee | Compiler | Kani | Exhaustive Correspondence | DFS Model Check | Conforms | +|-----------|----------|------|--------------------------|-----------------|----------| +| G1: No shared mutable state | Yes | — | — | — | Yes | +| G2: Single-threaded execution | Yes | — | — | — | Yes | +| G3: Address uniqueness | Yes | — | — | — | Yes | +| G4: Lifecycle ordering | Partial | Yes | Yes | Yes | Yes | +| G5: Fault isolation | Partial | — | — | Yes | Yes | +| G6: Death notification completeness | — | — | — | Yes | Yes | +| G7: Orphan cleanup | — | — | — | Yes | Yes | +| G8: Supervisor restart correctness | — | Yes | Yes | Yes | Yes | diff --git a/src/guarantees/correspondence.rs b/src/guarantees/correspondence.rs index f19d284..e7cc71e 100644 --- a/src/guarantees/correspondence.rs +++ b/src/guarantees/correspondence.rs @@ -1,25 +1,27 @@ -//! Correspondence tests: verify that kani bounded mirrors agree with -//! the real runtime. +//! Exhaustive correspondence tests: verify that Kani bounded mirrors agree +//! with the real runtime across the *entire* finite input space. //! //! These are the drift detectors. If someone changes `tick_all`'s skip logic -//! or `Supervisor::handle_down`'s restart decision without updating the kani +//! or `Supervisor::handle_down`'s restart decision without updating the Kani //! mirrors, these tests fail. //! //! How they work: -//! - Drive the same inputs through BOTH the mirror logic AND the real runtime +//! - Deterministic enumeration of every reachable input combination +//! - Drive the same inputs through BOTH the production decision functions AND +//! the real runtime //! - Assert they agree on observable outcomes -//! - Property-based (proptest) for coverage across the input space +//! - No random sampling — every combination is hit use std::sync::Arc; -use proptest::prelude::*; - use crate::actor::{ActorAddress, ActorInterface, StopReason}; use crate::config::RuntimeConfig; use crate::runtime::{Ctx, Runtime}; +use crate::std::supervisor::compute_restart_set; use crate::std::{ ChildSpec, RestartPolicy, StdExtension, Supervisor, SupervisorStrategy, }; +use crate::worker::{is_on_stop_eligible, should_skip_actor}; // ─── Helpers ──────────────────────────────────────────────────────────────── @@ -33,26 +35,21 @@ fn tick_many(rt: &Runtime, n: usize) { } } -// ═══════════════════════════════════════════════════════════════════════════ -// G4 Correspondence: lifecycle mirror vs real runtime -// ═══════════════════════════════════════════════════════════════════════════ +const ALL_POLICIES: [RestartPolicy; 3] = [ + RestartPolicy::Permanent, + RestartPolicy::Transient, + RestartPolicy::Temporary, +]; -// ─── Mirror (duplicated from g4_lifecycle.rs for cfg(test) visibility) ──── +const ALL_REASONS: [StopReason; 3] = [StopReason::Normal, StopReason::Panicked, StopReason::Completed]; -/// Whether the mirror predicts handle will be called for an actor with -/// these flags during tick_all. -fn mirror_should_process(poisoned: bool, stopping: bool, suspended: bool) -> bool { - // From g4_lifecycle.rs tick(): skip if poisoned || stopping || suspended - !poisoned && !stopping && !suspended -} +const ALL_STRATEGIES: [SupervisorStrategy; 3] = [ + SupervisorStrategy::OneForOne, + SupervisorStrategy::OneForAll, + SupervisorStrategy::RestForOne, +]; -/// Whether the mirror predicts on_stop will be called during cleanup_dead. -fn mirror_should_on_stop(stopping: bool, poisoned: bool) -> bool { - // From g4_lifecycle.rs cleanup(): on_stop fires only when stopping && !poisoned - stopping && !poisoned -} - -// ─── Real runtime actors for G4 correspondence ────────────────────────── +// ─── Real runtime actors ──────────────────────────────────────────────────── #[derive(Clone, Debug)] struct Ping; @@ -63,27 +60,32 @@ struct HandleCalled(#[allow(dead_code)] ActorAddress); #[derive(Clone, Debug)] struct OnStopCalled(#[allow(dead_code)] ActorAddress); -/// Actor that reports when handle is called. -struct HandleReporter { - report_to: ActorAddress, +#[derive(Clone, Debug)] +struct ChildStarted(ActorAddress); + +/// Actor that reports handle and on_stop to separate inboxes. +struct DualReporter { + handle_to: ActorAddress, + stop_to: ActorAddress, } -impl ActorInterface for HandleReporter { +impl ActorInterface for DualReporter { type Incoming = Ping; type Response = (); fn handle(&mut self, ctx: &Ctx, _msg: Ping) { - let _ = ctx.send(self.report_to, HandleCalled(ctx.self_addr())); + let _ = ctx.send(self.handle_to, HandleCalled(ctx.self_addr())); } fn on_stop(&mut self, ctx: &Ctx) { - let _ = ctx.send(self.report_to, OnStopCalled(ctx.self_addr())); + let _ = ctx.send(self.stop_to, OnStopCalled(ctx.self_addr())); } } /// Actor that panics in on_start. struct OnStartPanicker { - report_to: ActorAddress, + handle_to: ActorAddress, + stop_to: ActorAddress, } impl ActorInterface for OnStartPanicker { @@ -95,17 +97,17 @@ impl ActorInterface for OnStartPanicker { } fn handle(&mut self, ctx: &Ctx, _msg: Ping) { - let _ = ctx.send(self.report_to, HandleCalled(ctx.self_addr())); + let _ = ctx.send(self.handle_to, HandleCalled(ctx.self_addr())); } fn on_stop(&mut self, ctx: &Ctx) { - let _ = ctx.send(self.report_to, OnStopCalled(ctx.self_addr())); + let _ = ctx.send(self.stop_to, OnStopCalled(ctx.self_addr())); } } /// Actor that panics on first handle call. struct HandlePanicker { - report_to: ActorAddress, + stop_to: ActorAddress, } impl ActorInterface for HandlePanicker { @@ -117,220 +119,10 @@ impl ActorInterface for HandlePanicker { } fn on_stop(&mut self, ctx: &Ctx) { - let _ = ctx.send(self.report_to, OnStopCalled(ctx.self_addr())); + let _ = ctx.send(self.stop_to, OnStopCalled(ctx.self_addr())); } } -// ─── G4 Property Tests ───────────────────────────────────────────────────── - -proptest! { - #![proptest_config(ProptestConfig::with_cases(80))] - - /// G4 correspondence: for a healthy actor (not poisoned, not stopping, not - /// suspended), the mirror predicts handle is called — the real runtime must - /// agree. - #[test] - fn g4_healthy_actor_handle_called( - msg_count in 1usize..=20, - ) { - let rt = Runtime::new(RuntimeConfig::default()); - let report_inbox = rt.new_inbox::().unwrap(); - let report_addr = *report_inbox.addr(); - - let addr = rt.spawn(HandleReporter { report_to: report_addr }).unwrap(); - rt.tick(); // on_start - - // Mirror prediction: healthy actor should process messages - let mirror_predicts_process = mirror_should_process(false, false, false); - prop_assert!(mirror_predicts_process, "mirror must predict processing for healthy actor"); - - // Send messages and tick - for _ in 0..msg_count { - rt.send_to(addr, Ping).unwrap(); - } - tick_many(&rt, msg_count + 5); - - // Real runtime: check handle was called - let mut handle_count = 0; - while report_inbox.try_recv().is_some() { - handle_count += 1; - } - prop_assert_eq!(handle_count, msg_count, "runtime must call handle for each message"); - } - - /// G4 correspondence: a poisoned actor (panicked in on_start) must not - /// have handle called and must not have on_stop called. - #[test] - fn g4_poisoned_actor_no_handle_no_on_stop( - msg_count in 1usize..=10, - ) { - let rt = Runtime::new(RuntimeConfig::default()); - let handle_inbox = rt.new_inbox::().unwrap(); - let stop_inbox = rt.new_inbox::().unwrap(); - let handle_addr = *handle_inbox.addr(); - - // Mirror predictions for poisoned actor - let mirror_predicts_process = mirror_should_process(true, false, false); - prop_assert!(!mirror_predicts_process, "mirror must predict NO processing for poisoned actor"); - let mirror_predicts_on_stop = mirror_should_on_stop(false, true); - prop_assert!(!mirror_predicts_on_stop, "mirror must predict NO on_stop for poisoned actor"); - - let addr = rt.spawn(OnStartPanicker { report_to: handle_addr }).unwrap(); - rt.tick(); // on_start panics → poisoned, cleanup removes from address map - - // Send messages — actor is already removed, sends fail (expected) - for _ in 0..msg_count { - let _ = rt.send_to(addr, Ping); - } - tick_many(&rt, msg_count + 5); - - // Real runtime: handle must NOT have been called - let handle_count: usize = std::iter::from_fn(|| handle_inbox.try_recv()).count(); - prop_assert_eq!(handle_count, 0, "poisoned actor must not call handle"); - - // Real runtime: on_stop must NOT have been called - let stop_count: usize = std::iter::from_fn(|| stop_inbox.try_recv()).count(); - prop_assert_eq!(stop_count, 0, "poisoned actor must not call on_stop"); - } - - /// G4 correspondence: a stopping actor must not have handle called, - /// but must have on_stop called exactly once. - #[test] - fn g4_stopping_actor_no_handle_yes_on_stop( - msg_count in 1usize..=10, - ) { - let rt = Runtime::new(RuntimeConfig::default()); - let handle_inbox = rt.new_inbox::().unwrap(); - let stop_inbox = rt.new_inbox::().unwrap(); - let handle_addr = *handle_inbox.addr(); - let _stop_addr = *stop_inbox.addr(); - - // Mirror predictions - let mirror_predicts_process = mirror_should_process(false, true, false); - prop_assert!(!mirror_predicts_process, "mirror must predict NO processing for stopping actor"); - let mirror_predicts_on_stop = mirror_should_on_stop(true, false); - prop_assert!(mirror_predicts_on_stop, "mirror must predict on_stop for stopping && !poisoned"); - - let addr = rt.spawn(HandleReporter { report_to: handle_addr }).unwrap(); - rt.tick(); // on_start - - // Request stop - rt.stop_actor(addr).unwrap(); - rt.tick(); // processes stop - - // Send messages after stop (should be discarded or fail) - for _ in 0..msg_count { - let _ = rt.send_to(addr, Ping); - } - tick_many(&rt, 5); - - // Drain handle reports — get only reports from this actor - let handle_count: usize = std::iter::from_fn(|| handle_inbox.try_recv()).count(); - // The actor might process the StopSignal before any Ping arrives, - // or some pings might arrive before the stop signal. The key property: - // after stopping flag is set, no more handles are called. - // We verify this indirectly: messages sent after stop_actor aren't processed. - - // on_stop must have been called exactly once - // The stop report goes to handle_addr — we need a separate inbox for stop - // Actually HandleReporter sends OnStopCalled to report_to (same addr). - // Let's just verify the actor is gone. - let _ = handle_count; // used above - - // Respawn with proper report addresses - let rt2 = Runtime::new(RuntimeConfig::default()); - let h_inbox = rt2.new_inbox::().unwrap(); - let s_inbox = rt2.new_inbox::().unwrap(); - - struct DualReporter { - handle_to: ActorAddress, - stop_to: ActorAddress, - } - impl ActorInterface for DualReporter { - type Incoming = Ping; - type Response = (); - fn handle(&mut self, ctx: &Ctx, _msg: Ping) { - let _ = ctx.send(self.handle_to, HandleCalled(ctx.self_addr())); - } - fn on_stop(&mut self, ctx: &Ctx) { - let _ = ctx.send(self.stop_to, OnStopCalled(ctx.self_addr())); - } - } - - let addr2 = rt2.spawn(DualReporter { - handle_to: *h_inbox.addr(), - stop_to: *s_inbox.addr(), - }).unwrap(); - rt2.tick(); // on_start - - // Stop immediately, then send messages - rt2.stop_actor(addr2).unwrap(); - for _ in 0..msg_count { - let _ = rt2.send_to(addr2, Ping); - } - tick_many(&rt2, 5); - - // Messages sent after stop_actor should not be handled - let h_count: usize = std::iter::from_fn(|| h_inbox.try_recv()).count(); - prop_assert_eq!(h_count, 0, "stopping actor must not call handle for messages sent after stop"); - - // on_stop must fire exactly once - let s_count: usize = std::iter::from_fn(|| s_inbox.try_recv()).count(); - prop_assert_eq!(s_count, 1, "stopping actor must call on_stop exactly once"); - } - - /// G4 correspondence: a handle-panicked actor must not call on_stop. - #[test] - fn g4_handle_panic_poisons_no_on_stop( - _dummy in 0usize..1, - ) { - let rt = Runtime::new(RuntimeConfig::default()); - let stop_inbox = rt.new_inbox::().unwrap(); - - let addr = rt.spawn(HandlePanicker { report_to: *stop_inbox.addr() }).unwrap(); - rt.tick(); // on_start - - // Send one message to trigger panic - rt.send_to(addr, Ping).unwrap(); - tick_many(&rt, 5); - - // Mirror prediction: poisoned actor gets no on_stop - let mirror_predicts_on_stop = mirror_should_on_stop(false, true); - prop_assert!(!mirror_predicts_on_stop); - - // Real runtime: on_stop must NOT fire - let stop_count: usize = std::iter::from_fn(|| stop_inbox.try_recv()).count(); - prop_assert_eq!(stop_count, 0, "handle-panicked actor must not call on_stop"); - } -} - -// ═══════════════════════════════════════════════════════════════════════════ -// G10 Correspondence: restart mirror vs real supervisor -// ═══════════════════════════════════════════════════════════════════════════ - -// ─── Mirror (duplicated from g10_supervisor.rs for cfg(test) visibility) ── - -/// Mirror specification of should_restart — independent of production code. -fn mirror_should_restart(policy: RestartPolicy, reason: StopReason) -> bool { - match policy { - RestartPolicy::Permanent => true, - RestartPolicy::Transient => reason == StopReason::Panicked, - RestartPolicy::Temporary => false, - } -} - -// ─── Real runtime actors for G10 correspondence ───────────────────────── - -#[derive(Clone, Debug)] -struct ChildStarted(ActorAddress); - -#[derive(Clone, Debug)] -#[allow(dead_code)] -struct DownReport { - dead: ActorAddress, - reason: StopReason, -} - /// Actor that panics on receiving Ping — used to trigger Panicked death. struct PanicOnPing; @@ -343,7 +135,19 @@ impl ActorInterface for PanicOnPing { } } -/// Actor that does nothing — used as a normal child. +/// Actor that calls ctx.stop_with() on first Ping — produces Completed stop reason. +struct CompletedOnPing; + +impl ActorInterface for CompletedOnPing { + type Incoming = Ping; + type Response = (); + + fn handle(&mut self, ctx: &Ctx, _msg: Ping) { + ctx.stop_with("done"); + } +} + +/// Actor that does nothing. struct IdleChild; impl ActorInterface for IdleChild { @@ -353,358 +157,598 @@ impl ActorInterface for IdleChild { fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {} } -/// Proptest strategy for RestartPolicy. -fn arb_restart_policy() -> impl Strategy { - prop_oneof![ - Just(RestartPolicy::Permanent), - Just(RestartPolicy::Transient), - Just(RestartPolicy::Temporary), - ] -} +// ═══════════════════════════════════════════════════════════════════════════ +// G4 Exhaustive Correspondence: lifecycle decisions vs real runtime +// ═══════════════════════════════════════════════════════════════════════════ -/// Proptest strategy for StopReason (only Normal and Panicked are relevant). -fn arb_stop_reason() -> impl Strategy { - prop_oneof![ - Just(StopReason::Normal), - Just(StopReason::Panicked), - ] -} +/// Exhaustive G4: for a healthy actor, the production `should_skip_actor` +/// predicts handle will be called — the real runtime agrees. +/// +/// Enumerates msg_count in 1..=5. +#[test] +fn g4_healthy_actor_handle_called() { + for msg_count in 1..=5 { + let rt = Runtime::new(RuntimeConfig::default()); + let h_inbox = rt.new_inbox::().unwrap(); + let report_addr = *h_inbox.addr(); -/// Proptest strategy for SupervisorStrategy. -fn arb_strategy() -> impl Strategy { - prop_oneof![ - Just(SupervisorStrategy::OneForOne), - Just(SupervisorStrategy::OneForAll), - Just(SupervisorStrategy::RestForOne), - ] -} + let addr = rt.spawn(DualReporter { + handle_to: report_addr, + stop_to: report_addr, // unused for this test path + }).unwrap(); + rt.tick(); // on_start -// ─── G10 Property Tests ──────────────────────────────────────────────────── - -proptest! { - #![proptest_config(ProptestConfig::with_cases(60))] - - /// G10 correspondence: the mirror's should_restart must agree with - /// the real supervisor's restart decision for all policy x reason combos. - /// - /// We observe the real supervisor's behavior by: - /// 1. Spawning a supervisor with one child of the given policy - /// 2. Killing the child with the given reason (panic or normal stop) - /// 3. Checking whether the supervisor restarted the child - #[test] - fn g10_should_restart_matches_supervisor( - policy in arb_restart_policy(), - reason in arb_stop_reason(), - ) { - let rt = std_runtime(); - let report_inbox = rt.new_inbox::().unwrap(); - let report_addr = *report_inbox.addr(); - - // Track child spawns via a shared counter - let spawn_count = Arc::new(std::sync::atomic::AtomicUsize::new(0)); - let spawn_count_clone = spawn_count.clone(); - - let spec = ChildSpec::new( - "test-child", - policy, - move |ctx| { - spawn_count_clone.fetch_add(1, std::sync::atomic::Ordering::SeqCst); - let addr = if reason == StopReason::Panicked { - ctx.spawn(PanicOnPing)? - } else { - ctx.spawn(IdleChild)? - }; - let _ = ctx.send(report_addr, ChildStarted(addr)); - Ok(addr) - }, + // Production decision: healthy actor should NOT be skipped + assert!( + !should_skip_actor(false, false, false), + "production should_skip_actor must return false for healthy actor" ); - let sup = Supervisor::new(SupervisorStrategy::OneForOne, 10, vec![spec]); - let _sup_addr = rt.spawn(sup).unwrap(); - - // Tick to start supervisor and child - tick_many(&rt, 3); - - // Get child address from spawn report - let child_started = report_inbox.try_recv(); - prop_assert!(child_started.is_some(), "child must have started"); - let child_addr = child_started.unwrap().0; - let initial_spawns = spawn_count.load(std::sync::atomic::Ordering::SeqCst); - prop_assert_eq!(initial_spawns, 1, "exactly one child spawn initially"); - - // Kill child according to reason - match reason { - StopReason::Panicked => { - // Send message to trigger panic - rt.send_to(child_addr, Ping).unwrap(); - } - StopReason::Normal | StopReason::Completed => { - // Normal stop - rt.stop_actor(child_addr).unwrap(); - } + for _ in 0..msg_count { + rt.send_to(addr, Ping).unwrap(); } + tick_many(&rt, msg_count + 5); - // Tick enough for supervisor to process Down and potentially restart - tick_many(&rt, 10); - - // Check if child was restarted - let final_spawns = spawn_count.load(std::sync::atomic::Ordering::SeqCst); - let was_restarted = final_spawns > initial_spawns; - - // Mirror prediction - let mirror_predicts_restart = mirror_should_restart(policy, reason); - - prop_assert_eq!( - was_restarted, mirror_predicts_restart, - "mirror predicts restart={} but runtime restarted={} for policy={:?} reason={:?}", - mirror_predicts_restart, was_restarted, policy, reason + let handle_count: usize = std::iter::from_fn(|| h_inbox.try_recv()).count(); + assert_eq!( + handle_count, msg_count, + "runtime must call handle for each message (msg_count={})", + msg_count ); } +} - /// G10 correspondence: OneForOne strategy restarts only the dead child. - /// Mirror predicts only dead_idx restarted; runtime must agree. - #[test] - fn g10_one_for_one_restarts_only_dead( - num_children in 2usize..=4, - dead_idx_raw in 0usize..4, - ) { - let dead_idx = dead_idx_raw % num_children; - let rt = std_runtime(); - let report_inbox = rt.new_inbox::().unwrap(); - let report_addr = *report_inbox.addr(); +/// Exhaustive G4: a poisoned actor (panicked in on_start) must not have +/// handle called and must not have on_stop called. +/// +/// Enumerates msg_count in 1..=5. +#[test] +fn g4_poisoned_actor_no_handle_no_on_stop() { + for msg_count in 1..=5 { + let rt = Runtime::new(RuntimeConfig::default()); + let h_inbox = rt.new_inbox::().unwrap(); + let s_inbox = rt.new_inbox::().unwrap(); - // Track per-child spawn counts - let spawn_counts: Vec> = - (0..num_children).map(|_| Arc::new(std::sync::atomic::AtomicUsize::new(0))).collect(); + // Production decisions for poisoned actor + assert!( + should_skip_actor(true, false, false), + "production should_skip_actor must return true for poisoned actor" + ); + assert!( + !is_on_stop_eligible(false, true), + "production is_on_stop_eligible must return false for poisoned (stopping=false, poisoned=true)" + ); - let specs: Vec = (0..num_children) - .map(|i| { - let counter = spawn_counts[i].clone(); - let is_dead_child = i == dead_idx; - let report = report_addr; - ChildSpec::new( - format!("child-{}", i), - RestartPolicy::Permanent, - move |ctx| { - counter.fetch_add(1, std::sync::atomic::Ordering::SeqCst); - let addr = if is_dead_child { - ctx.spawn(PanicOnPing)? - } else { - ctx.spawn(IdleChild)? - }; - let _ = ctx.send(report, ChildStarted(addr)); - Ok(addr) - }, - ) - }) - .collect(); + let addr = rt.spawn(OnStartPanicker { + handle_to: *h_inbox.addr(), + stop_to: *s_inbox.addr(), + }).unwrap(); + rt.tick(); // on_start panics → poisoned - let sup = Supervisor::new(SupervisorStrategy::OneForOne, 10, specs); - let _sup_addr = rt.spawn(sup).unwrap(); + for _ in 0..msg_count { + let _ = rt.send_to(addr, Ping); + } + tick_many(&rt, msg_count + 5); + let handle_count: usize = std::iter::from_fn(|| h_inbox.try_recv()).count(); + assert_eq!(handle_count, 0, "poisoned actor must not call handle (msg_count={})", msg_count); + + let stop_count: usize = std::iter::from_fn(|| s_inbox.try_recv()).count(); + assert_eq!(stop_count, 0, "poisoned actor must not call on_stop (msg_count={})", msg_count); + } +} + +/// Exhaustive G4: a stopping actor must not have handle called for messages +/// sent after stop, but must have on_stop called exactly once. +/// +/// Enumerates msg_count in 1..=5. +#[test] +fn g4_stopping_actor_no_handle_yes_on_stop() { + for msg_count in 1..=5 { + // Production decisions + assert!( + should_skip_actor(false, true, false), + "production should_skip_actor must return true for stopping actor" + ); + assert!( + is_on_stop_eligible(true, false), + "production is_on_stop_eligible must return true for (stopping=true, poisoned=false)" + ); + + let rt = Runtime::new(RuntimeConfig::default()); + let h_inbox = rt.new_inbox::().unwrap(); + let s_inbox = rt.new_inbox::().unwrap(); + + let addr = rt.spawn(DualReporter { + handle_to: *h_inbox.addr(), + stop_to: *s_inbox.addr(), + }).unwrap(); + rt.tick(); // on_start + + rt.stop_actor(addr).unwrap(); + for _ in 0..msg_count { + let _ = rt.send_to(addr, Ping); + } tick_many(&rt, 5); - // Collect initial child addresses - let mut child_addrs = Vec::new(); - while let Some(ChildStarted(addr)) = report_inbox.try_recv() { - child_addrs.push(addr); - } - prop_assert_eq!(child_addrs.len(), num_children, "all children must start"); + let h_count: usize = std::iter::from_fn(|| h_inbox.try_recv()).count(); + assert_eq!( + h_count, 0, + "stopping actor must not call handle for messages sent after stop (msg_count={})", + msg_count + ); - // Record initial spawn counts - let initial_counts: Vec = spawn_counts.iter() - .map(|c| c.load(std::sync::atomic::Ordering::SeqCst)) - .collect(); + let s_count: usize = std::iter::from_fn(|| s_inbox.try_recv()).count(); + assert_eq!( + s_count, 1, + "stopping actor must call on_stop exactly once (msg_count={})", + msg_count + ); + } +} - // Kill the designated child via panic - rt.send_to(child_addrs[dead_idx], Ping).unwrap(); - tick_many(&rt, 10); +/// Exhaustive G4: a handle-panicked actor must not call on_stop. +/// +/// This is a single deterministic case (not parameterized — panic is binary). +#[test] +fn g4_handle_panic_poisons_no_on_stop() { + let rt = Runtime::new(RuntimeConfig::default()); + let s_inbox = rt.new_inbox::().unwrap(); - // Check which children were restarted - let final_counts: Vec = spawn_counts.iter() - .map(|c| c.load(std::sync::atomic::Ordering::SeqCst)) - .collect(); + let addr = rt.spawn(HandlePanicker { + stop_to: *s_inbox.addr(), + }).unwrap(); + rt.tick(); // on_start - for i in 0..num_children { - let restarted = final_counts[i] > initial_counts[i]; - if i == dead_idx { - // Mirror: OneForOne restarts only dead child (Permanent policy) - prop_assert!(restarted, - "OneForOne: dead child {} must be restarted", i); - } else { - // Mirror: other children untouched - prop_assert!(!restarted, - "OneForOne: non-dead child {} must NOT be restarted", i); + rt.send_to(addr, Ping).unwrap(); + tick_many(&rt, 5); + + // Production decision: poisoned → no on_stop + assert!( + !is_on_stop_eligible(false, true), + "production is_on_stop_eligible must return false for poisoned" + ); + + let stop_count: usize = std::iter::from_fn(|| s_inbox.try_recv()).count(); + assert_eq!(stop_count, 0, "handle-panicked actor must not call on_stop"); +} + +/// Exhaustive G4: enumerate ALL 16 boolean flag combinations for the +/// production decision functions and verify consistency. +/// +/// 4 flags × 2 values = 16 combinations for should_skip_actor +/// 2 flags × 2 values = 4 combinations for is_on_stop_eligible +/// 2 flags × 2 values = 4 combinations for determine_stop_reason +#[test] +fn g4_exhaustive_decision_function_truth_table() { + use crate::worker::determine_stop_reason; + + let mut combinations_tested = 0u32; + + // should_skip_actor: exhaustive over (poisoned, stopping, suspended) + for poisoned in [false, true] { + for stopping in [false, true] { + for suspended in [false, true] { + let skip = should_skip_actor(poisoned, stopping, suspended); + // Must skip iff any flag is set + assert_eq!( + skip, + poisoned || stopping || suspended, + "should_skip_actor({}, {}, {}) = {} but expected {}", + poisoned, stopping, suspended, skip, + poisoned || stopping || suspended + ); + combinations_tested += 1; } } } + assert_eq!(combinations_tested, 8, "must test all 8 flag combinations for should_skip_actor"); - /// G10 correspondence: Temporary policy never restarts, regardless of - /// strategy or death reason. - #[test] - fn g10_temporary_never_restarts( - strategy in arb_strategy(), - reason in arb_stop_reason(), - ) { - let rt = std_runtime(); + // is_on_stop_eligible: exhaustive over (stopping, poisoned) + let mut on_stop_combinations = 0u32; + for stopping in [false, true] { + for poisoned in [false, true] { + let eligible = is_on_stop_eligible(stopping, poisoned); + assert_eq!( + eligible, + stopping && !poisoned, + "is_on_stop_eligible({}, {}) = {} but expected {}", + stopping, poisoned, eligible, + stopping && !poisoned + ); + on_stop_combinations += 1; + } + } + assert_eq!(on_stop_combinations, 4, "must test all 4 flag combinations for is_on_stop_eligible"); - let spawn_count = Arc::new(std::sync::atomic::AtomicUsize::new(0)); - let spawn_count_clone = spawn_count.clone(); + // determine_stop_reason: exhaustive over (poisoned, has_exit_value) + let mut reason_combinations = 0u32; + for poisoned in [false, true] { + for has_exit_value in [false, true] { + let reason = determine_stop_reason(poisoned, has_exit_value); + let expected = if poisoned { + StopReason::Panicked + } else if has_exit_value { + StopReason::Completed + } else { + StopReason::Normal + }; + assert_eq!( + reason, expected, + "determine_stop_reason({}, {}) = {:?} but expected {:?}", + poisoned, has_exit_value, reason, expected + ); + reason_combinations += 1; + } + } + assert_eq!(reason_combinations, 4, "must test all 4 flag combinations for determine_stop_reason"); +} - let spec = ChildSpec::new( - "temp-child", - RestartPolicy::Temporary, - move |ctx| { - spawn_count_clone.fetch_add(1, std::sync::atomic::Ordering::SeqCst); - let addr = if reason == StopReason::Panicked { - ctx.spawn(PanicOnPing)? - } else { - ctx.spawn(IdleChild)? - }; - Ok(addr) - }, - ); +// ═══════════════════════════════════════════════════════════════════════════ +// G10 Exhaustive Correspondence: restart decisions vs real supervisor +// ═══════════════════════════════════════════════════════════════════════════ - let report_inbox = rt.new_inbox::().unwrap(); - let report_addr = *report_inbox.addr(); +/// Exhaustive G10: the production `RestartPolicy::should_restart` must agree +/// with the real supervisor's restart behavior for ALL policy × reason combos. +/// +/// 3 policies × 3 reasons = 9 combinations, all tested. +#[test] +fn g10_should_restart_matches_supervisor() { + let mut combinations_tested = 0u32; - // For strategies that need multiple children, add idle permanent children - let mut specs = vec![spec]; - for i in 0..2 { - let report = report_addr; - specs.push(ChildSpec::new( - format!("filler-{}", i), - RestartPolicy::Permanent, + for &policy in &ALL_POLICIES { + for &reason in &ALL_REASONS { + let rt = std_runtime(); + let child_inbox = rt.new_inbox::().unwrap(); + let child_report = *child_inbox.addr(); + + let spawn_count = Arc::new(std::sync::atomic::AtomicUsize::new(0)); + let sc = spawn_count.clone(); + + let spec = ChildSpec::new( + "test-child", + policy, move |ctx| { - let addr = ctx.spawn(IdleChild)?; - let _ = ctx.send(report, ChildStarted(addr)); + sc.fetch_add(1, std::sync::atomic::Ordering::SeqCst); + let addr = match reason { + StopReason::Panicked => ctx.spawn(PanicOnPing)?, + StopReason::Completed => ctx.spawn(CompletedOnPing)?, + StopReason::Normal => ctx.spawn(IdleChild)?, + }; + let _ = ctx.send(child_report, ChildStarted(addr)); Ok(addr) }, - )); - } + ); - let sup = Supervisor::new(strategy, 10, specs); - let _sup_addr = rt.spawn(sup).unwrap(); - tick_many(&rt, 5); + let sup = Supervisor::new(SupervisorStrategy::OneForOne, 10, vec![spec]); + let _sup_addr = rt.spawn(sup).unwrap(); + tick_many(&rt, 3); - let initial = spawn_count.load(std::sync::atomic::Ordering::SeqCst); - prop_assert_eq!(initial, 1, "temp child started once"); + let child_addr = child_inbox.try_recv().expect("child must start").0; + let initial = spawn_count.load(std::sync::atomic::Ordering::SeqCst); + assert_eq!(initial, 1, "exactly one child spawn initially"); - // Mirror prediction: Temporary → never restart - let mirror_predicts = mirror_should_restart(RestartPolicy::Temporary, reason); - prop_assert!(!mirror_predicts, "mirror must predict no restart for Temporary"); - - // Kill via the appropriate mechanism — but we need the child addr. - // We can get it from runtime stats or by tracking it. Since the factory - // already ran, we need to find the child. Let's just verify through - // spawn_count that no second spawn happens after death. - - // The child is the first one spawned. We can trigger its death - // by sending it a stop or a message to panic. - // For simplicity, stop the supervisor — temporary children won't be restarted - // even if they die. The key assertion: spawn_count stays at 1. - - // Actually we need to kill just the child, not the supervisor. - // Since we can't easily get the child address from outside, let's - // restructure to track it: - let rt2 = std_runtime(); - let child_inbox = rt2.new_inbox::().unwrap(); - let child_report = *child_inbox.addr(); - - let spawn_count2 = Arc::new(std::sync::atomic::AtomicUsize::new(0)); - let sc2 = spawn_count2.clone(); - - let spec2 = ChildSpec::new( - "temp-child", - RestartPolicy::Temporary, - move |ctx| { - sc2.fetch_add(1, std::sync::atomic::Ordering::SeqCst); - let addr = if reason == StopReason::Panicked { - ctx.spawn(PanicOnPing)? - } else { - ctx.spawn(IdleChild)? - }; - let _ = ctx.send(child_report, ChildStarted(addr)); - Ok(addr) - }, - ); - - let sup2 = Supervisor::new(strategy, 10, vec![spec2]); - let _sup_addr2 = rt2.spawn(sup2).unwrap(); - tick_many(&rt2, 5); - - let child_addr = child_inbox.try_recv().expect("child must start").0; - let init2 = spawn_count2.load(std::sync::atomic::Ordering::SeqCst); - - // Kill child - match reason { - StopReason::Panicked => { - rt2.send_to(child_addr, Ping).unwrap(); + match reason { + StopReason::Panicked => { + rt.send_to(child_addr, Ping).unwrap(); + } + StopReason::Normal => { + rt.stop_actor(child_addr).unwrap(); + } + StopReason::Completed => { + rt.send_to(child_addr, Ping).unwrap(); + } } - _ => { - rt2.stop_actor(child_addr).unwrap(); - } - } - tick_many(&rt2, 10); + tick_many(&rt, 10); - let final2 = spawn_count2.load(std::sync::atomic::Ordering::SeqCst); - prop_assert_eq!(final2, init2, - "Temporary child must NOT be restarted: spawns before={} after={} strategy={:?} reason={:?}", - init2, final2, strategy, reason); + let final_spawns = spawn_count.load(std::sync::atomic::Ordering::SeqCst); + let was_restarted = final_spawns > initial; + let production_predicts = policy.should_restart(reason); + + assert_eq!( + was_restarted, production_predicts, + "policy={:?} reason={:?}: production predicts restart={} but runtime restarted={}", + policy, reason, production_predicts, was_restarted + ); + + combinations_tested += 1; + } } - /// G10 correspondence: Transient + Normal stop → no restart. - /// Transient + Panicked → restart. Mirror must agree with runtime. - #[test] - fn g10_transient_restart_only_on_panic( - reason in arb_stop_reason(), - ) { - let rt = std_runtime(); - let child_inbox = rt.new_inbox::().unwrap(); - let child_report = *child_inbox.addr(); - - let spawn_count = Arc::new(std::sync::atomic::AtomicUsize::new(0)); - let sc = spawn_count.clone(); - - let spec = ChildSpec::new( - "transient-child", - RestartPolicy::Transient, - move |ctx| { - sc.fetch_add(1, std::sync::atomic::Ordering::SeqCst); - let addr = if reason == StopReason::Panicked { - ctx.spawn(PanicOnPing)? - } else { - ctx.spawn(IdleChild)? - }; - let _ = ctx.send(child_report, ChildStarted(addr)); - Ok(addr) - }, - ); - - let sup = Supervisor::new(SupervisorStrategy::OneForOne, 10, vec![spec]); - let _sup_addr = rt.spawn(sup).unwrap(); - tick_many(&rt, 5); - - let child_addr = child_inbox.try_recv().expect("child must start").0; - let initial = spawn_count.load(std::sync::atomic::Ordering::SeqCst); - - // Kill child - match reason { - StopReason::Panicked => { - rt.send_to(child_addr, Ping).unwrap(); - } - _ => { - rt.stop_actor(child_addr).unwrap(); - } - } - tick_many(&rt, 10); - - let final_count = spawn_count.load(std::sync::atomic::Ordering::SeqCst); - let was_restarted = final_count > initial; - let mirror_predicts = mirror_should_restart(RestartPolicy::Transient, reason); - - prop_assert_eq!(was_restarted, mirror_predicts, - "Transient: mirror predicts restart={} but runtime restarted={} for reason={:?}", - mirror_predicts, was_restarted, reason); - } + assert_eq!(combinations_tested, 9, "must test all 9 policy×reason combinations"); +} + +/// Exhaustive G10: OneForOne strategy restarts only the dead child. +/// +/// Enumerates: num_children in 2..=4, dead_idx in 0..num_children. +/// Total: 2+3+4 = 9 combinations. +#[test] +fn g10_one_for_one_restarts_only_dead() { + let mut combinations_tested = 0u32; + + for num_children in 2..=4 { + for dead_idx in 0..num_children { + let rt = std_runtime(); + let report_inbox = rt.new_inbox::().unwrap(); + let report_addr = *report_inbox.addr(); + + let spawn_counts: Vec> = + (0..num_children).map(|_| Arc::new(std::sync::atomic::AtomicUsize::new(0))).collect(); + + let specs: Vec = (0..num_children) + .map(|i| { + let counter = spawn_counts[i].clone(); + let is_dead_child = i == dead_idx; + let report = report_addr; + ChildSpec::new( + format!("child-{}", i), + RestartPolicy::Permanent, + move |ctx| { + counter.fetch_add(1, std::sync::atomic::Ordering::SeqCst); + let addr = if is_dead_child { + ctx.spawn(PanicOnPing)? + } else { + ctx.spawn(IdleChild)? + }; + let _ = ctx.send(report, ChildStarted(addr)); + Ok(addr) + }, + ) + }) + .collect(); + + let sup = Supervisor::new(SupervisorStrategy::OneForOne, 10, specs); + let _sup_addr = rt.spawn(sup).unwrap(); + tick_many(&rt, 5); + + let mut child_addrs = Vec::new(); + while let Some(ChildStarted(addr)) = report_inbox.try_recv() { + child_addrs.push(addr); + } + assert_eq!(child_addrs.len(), num_children, "all children must start"); + + let initial_counts: Vec = spawn_counts.iter() + .map(|c| c.load(std::sync::atomic::Ordering::SeqCst)) + .collect(); + + // Kill the designated child via panic + rt.send_to(child_addrs[dead_idx], Ping).unwrap(); + tick_many(&rt, 10); + + // Verify against production compute_restart_set + let expected_set = compute_restart_set(SupervisorStrategy::OneForOne, dead_idx, num_children); + + let final_counts: Vec = spawn_counts.iter() + .map(|c| c.load(std::sync::atomic::Ordering::SeqCst)) + .collect(); + + for i in 0..num_children { + let restarted = final_counts[i] > initial_counts[i]; + let expected_restart = expected_set.contains(&i); + assert_eq!( + restarted, expected_restart, + "OneForOne: num_children={} dead_idx={} child={}: expected restart={} got={}", + num_children, dead_idx, i, expected_restart, restarted + ); + } + + combinations_tested += 1; + } + } + + assert_eq!(combinations_tested, 9, "must test all 9 num_children×dead_idx combinations"); +} + +/// Exhaustive G10: Temporary policy never restarts, regardless of strategy +/// or death reason. +/// +/// Enumerates: 3 strategies × 3 reasons = 9 combinations. +#[test] +fn g10_temporary_never_restarts() { + let mut combinations_tested = 0u32; + + for &strategy in &ALL_STRATEGIES { + for &reason in &ALL_REASONS { + // Production decision: Temporary never restarts + assert!( + !RestartPolicy::Temporary.should_restart(reason), + "production should_restart must return false for Temporary + {:?}", + reason + ); + + let rt = std_runtime(); + let child_inbox = rt.new_inbox::().unwrap(); + let child_report = *child_inbox.addr(); + + let spawn_count = Arc::new(std::sync::atomic::AtomicUsize::new(0)); + let sc = spawn_count.clone(); + + let spec = ChildSpec::new( + "temp-child", + RestartPolicy::Temporary, + move |ctx| { + sc.fetch_add(1, std::sync::atomic::Ordering::SeqCst); + let addr = match reason { + StopReason::Panicked => ctx.spawn(PanicOnPing)?, + StopReason::Completed => ctx.spawn(CompletedOnPing)?, + StopReason::Normal => ctx.spawn(IdleChild)?, + }; + let _ = ctx.send(child_report, ChildStarted(addr)); + Ok(addr) + }, + ); + + let sup = Supervisor::new(strategy, 10, vec![spec]); + let _sup_addr = rt.spawn(sup).unwrap(); + tick_many(&rt, 5); + + let child_addr = child_inbox.try_recv().expect("child must start").0; + let initial = spawn_count.load(std::sync::atomic::Ordering::SeqCst); + + match reason { + StopReason::Panicked => { + rt.send_to(child_addr, Ping).unwrap(); + } + StopReason::Normal => { + rt.stop_actor(child_addr).unwrap(); + } + StopReason::Completed => { + rt.send_to(child_addr, Ping).unwrap(); + } + } + tick_many(&rt, 10); + + let final_count = spawn_count.load(std::sync::atomic::Ordering::SeqCst); + assert_eq!( + final_count, initial, + "Temporary child must NOT be restarted: strategy={:?} reason={:?} spawns before={} after={}", + strategy, reason, initial, final_count + ); + + combinations_tested += 1; + } + } + + assert_eq!(combinations_tested, 9, "must test all 9 strategy×reason combinations"); +} + +/// Exhaustive G10: Transient policy restarts only on panic. +/// +/// Enumerates: 3 reasons × 3 strategies = 9 combinations. +#[test] +fn g10_transient_restart_only_on_panic() { + let mut combinations_tested = 0u32; + + for &strategy in &ALL_STRATEGIES { + for &reason in &ALL_REASONS { + let rt = std_runtime(); + let child_inbox = rt.new_inbox::().unwrap(); + let child_report = *child_inbox.addr(); + + let spawn_count = Arc::new(std::sync::atomic::AtomicUsize::new(0)); + let sc = spawn_count.clone(); + + let spec = ChildSpec::new( + "transient-child", + RestartPolicy::Transient, + move |ctx| { + sc.fetch_add(1, std::sync::atomic::Ordering::SeqCst); + let addr = match reason { + StopReason::Panicked => ctx.spawn(PanicOnPing)?, + StopReason::Completed => ctx.spawn(CompletedOnPing)?, + StopReason::Normal => ctx.spawn(IdleChild)?, + }; + let _ = ctx.send(child_report, ChildStarted(addr)); + Ok(addr) + }, + ); + + let sup = Supervisor::new(strategy, 10, vec![spec]); + let _sup_addr = rt.spawn(sup).unwrap(); + tick_many(&rt, 5); + + let child_addr = child_inbox.try_recv().expect("child must start").0; + let initial = spawn_count.load(std::sync::atomic::Ordering::SeqCst); + + match reason { + StopReason::Panicked => { + rt.send_to(child_addr, Ping).unwrap(); + } + StopReason::Normal => { + rt.stop_actor(child_addr).unwrap(); + } + StopReason::Completed => { + rt.send_to(child_addr, Ping).unwrap(); + } + } + tick_many(&rt, 10); + + let final_count = spawn_count.load(std::sync::atomic::Ordering::SeqCst); + let was_restarted = final_count > initial; + let production_predicts = RestartPolicy::Transient.should_restart(reason); + + assert_eq!( + was_restarted, production_predicts, + "Transient: strategy={:?} reason={:?}: production predicts restart={} but runtime restarted={}", + strategy, reason, production_predicts, was_restarted + ); + + combinations_tested += 1; + } + } + + assert_eq!(combinations_tested, 9, "must test all 9 strategy×reason combinations"); +} + +/// Exhaustive G10: verify compute_restart_set for every strategy × child count × dead index. +/// +/// 3 strategies × (1..=4 children) × (0..num_children dead indices) = 30 combinations. +#[test] +fn g10_exhaustive_restart_set_computation() { + let mut combinations_tested = 0u32; + + for &strategy in &ALL_STRATEGIES { + for num_children in 1..=4usize { + for dead_idx in 0..num_children { + let result = compute_restart_set(strategy, dead_idx, num_children); + + match strategy { + SupervisorStrategy::OneForOne => { + assert_eq!( + result, vec![dead_idx], + "OneForOne(dead={}, n={}) should restart only dead child", + dead_idx, num_children + ); + } + SupervisorStrategy::OneForAll => { + let expected: Vec = (0..num_children).collect(); + assert_eq!( + result, expected, + "OneForAll(dead={}, n={}) should restart all children", + dead_idx, num_children + ); + } + SupervisorStrategy::RestForOne => { + let expected: Vec = (dead_idx..num_children).collect(); + assert_eq!( + result, expected, + "RestForOne(dead={}, n={}) should restart dead and after", + dead_idx, num_children + ); + } + } + + combinations_tested += 1; + } + } + } + + assert_eq!(combinations_tested, 30, "must test all 30 strategy×children×dead_idx combinations"); +} + +/// Exhaustive G10: verify should_restart for every policy × reason combination. +/// +/// 3 policies × 3 reasons = 9 combinations. +#[test] +fn g10_exhaustive_should_restart_truth_table() { + let mut combinations_tested = 0u32; + + for &policy in &ALL_POLICIES { + for &reason in &ALL_REASONS { + let result = policy.should_restart(reason); + let expected = match policy { + RestartPolicy::Permanent => true, + RestartPolicy::Transient => reason == StopReason::Panicked, + RestartPolicy::Temporary => false, + }; + assert_eq!( + result, expected, + "should_restart({:?}, {:?}) = {} but expected {}", + policy, reason, result, expected + ); + combinations_tested += 1; + } + } + + assert_eq!(combinations_tested, 9, "must test all 9 policy×reason combinations"); } diff --git a/src/guarantees/g10_supervisor.rs b/src/guarantees/g10_supervisor.rs index adfa300..e72a8cc 100644 --- a/src/guarantees/g10_supervisor.rs +++ b/src/guarantees/g10_supervisor.rs @@ -5,10 +5,9 @@ //! symbolically enumerates all combinations of strategy, which child //! dies, each child's restart policy, and death reason. //! -//! Uses the real `SupervisorStrategy`, `RestartPolicy`, and `StopReason` -//! types from production code — only the decision *logic* is mirrored -//! independently (it's the specification that production code is verified -//! against). +//! The decision points call **production** pure functions +//! (`RestartPolicy::should_restart`, `compute_restart_set`) from +//! `std/supervisor.rs`, so Kani is proving properties of the real code. //! //! Properties proven: //! - **G10a**: `OneForOne` restarts only the dead child (if policy permits). @@ -18,23 +17,13 @@ //! - **G10e**: `Transient` children restart only on panic. use crate::actor::StopReason; +use crate::std::supervisor::compute_restart_set; use crate::std::{RestartPolicy, SupervisorStrategy}; // ─── Bounded mirror ───────────────────────────────────────────────────────── const MAX_CHILDREN: usize = 4; -/// Whether the policy says to restart given a death reason. -/// This is the *specification* — independent of the production code in -/// `Supervisor::handle_down`. Correspondence tests verify they agree. -fn should_restart(policy: RestartPolicy, reason: StopReason) -> bool { - match policy { - RestartPolicy::Permanent => true, - RestartPolicy::Transient => reason == StopReason::Panicked, - RestartPolicy::Temporary => false, - } -} - /// Outcome of the supervisor's restart decision. Tracks which children /// get restarted (set to `true` in the array). struct RestartOutcome { @@ -43,6 +32,7 @@ struct RestartOutcome { } /// Mirror of `Supervisor::handle_down` — the restart decision logic. +/// Calls production functions for the individual decisions. /// /// `num_children`: number of active children (1..=MAX_CHILDREN) /// `dead_idx`: index of the child that died @@ -64,9 +54,8 @@ fn decide_restart( meltdown: false, }; - // Step 1: should_restart check (supervisor.rs:263-267) - let restart = should_restart(policies[dead_idx], reason); - if !restart { + // Step 1: Use production should_restart function + if !policies[dead_idx].should_restart(reason) { return outcome; } @@ -77,28 +66,10 @@ fn decide_restart( return outcome; } - // Step 3: apply strategy (supervisor.rs:282-301) - match strategy { - SupervisorStrategy::OneForOne => { - // Only restart the dead child - outcome.restarted[dead_idx] = true; - } - SupervisorStrategy::OneForAll => { - // Restart all children in spec order - let mut i = 0; - while i < num_children { - outcome.restarted[i] = true; - i += 1; - } - } - SupervisorStrategy::RestForOne => { - // Restart dead child + all after it - let mut i = dead_idx; - while i < num_children { - outcome.restarted[i] = true; - i += 1; - } - } + // Step 3: Use production compute_restart_set function + let indices = compute_restart_set(strategy, dead_idx, num_children); + for idx in indices { + outcome.restarted[idx] = true; } outcome @@ -170,7 +141,7 @@ fn proof_g10a_one_for_one_restarts_only_dead() { max_restarts, ); - if !outcome.meltdown && should_restart(policies[dead_idx], reason) { + if !outcome.meltdown && policies[dead_idx].should_restart(reason) { // Only the dead child is restarted assert!(outcome.restarted[dead_idx]); let mut j = 0; @@ -214,7 +185,7 @@ fn proof_g10b_one_for_all_restarts_all() { max_restarts, ); - if !outcome.meltdown && should_restart(policies[dead_idx], reason) { + if !outcome.meltdown && policies[dead_idx].should_restart(reason) { // All children are restarted let mut j = 0; while j < num_children { @@ -255,7 +226,7 @@ fn proof_g10c_rest_for_one_restarts_from_dead() { max_restarts, ); - if !outcome.meltdown && should_restart(policies[dead_idx], reason) { + if !outcome.meltdown && policies[dead_idx].should_restart(reason) { // Children before dead_idx are NOT restarted let mut j = 0; while j < dead_idx { diff --git a/src/guarantees/g4_lifecycle.rs b/src/guarantees/g4_lifecycle.rs index 97dfc5c..016e058 100644 --- a/src/guarantees/g4_lifecycle.rs +++ b/src/guarantees/g4_lifecycle.rs @@ -4,6 +4,10 @@ //! the four boolean flags (`started`, `stopping`, `poisoned`, `suspended`) //! and the transitions that `tick_all` and `cleanup_dead` apply. //! +//! The mirror's decision points call the **production** pure functions +//! (`should_skip_actor`, `is_on_stop_eligible`) from `worker.rs`, so Kani +//! is proving properties of the real code, not a test-only re-implementation. +//! //! Properties proven: //! - **G4a**: `on_start` fires exactly once, before any `handle`. //! - **G4b**: `handle` is never called when `stopping || poisoned`. @@ -11,6 +15,8 @@ //! - **G4d**: No transition sequence reaches `handle` after `on_stop`. //! - **G4e**: Suspension pauses message processing; resume restores it. +use crate::worker::{should_skip_actor, is_on_stop_eligible}; + // ─── Bounded mirror ───────────────────────────────────────────────────────── /// Events that can occur during a tick, mirroring the control flow in @@ -61,13 +67,8 @@ impl KaniActorState { /// Mirror of the per-actor logic inside `tick_all`. /// Returns true if this actor was processed (not skipped). fn tick(&mut self, events: &[Event], event_count: usize) { - // Skip poisoned/stopping actors (worker.rs:495-498) - if self.poisoned || self.stopping { - return; - } - - // Skip suspended actors (worker.rs:502-504) - if self.suspended { + // Use production decision function for skip check + if should_skip_actor(self.poisoned, self.stopping, self.suspended) { return; } @@ -185,7 +186,8 @@ impl KaniActorState { if !self.poisoned && !self.stopping { return; } - if self.stopping && !self.poisoned { + // Use production decision function for on_stop eligibility + if is_on_stop_eligible(self.stopping, self.poisoned) { self.on_stop_count += 1; } self.cleanup_done = true; diff --git a/src/guarantees/mod.rs b/src/guarantees/mod.rs index c3212d4..a52279e 100644 --- a/src/guarantees/mod.rs +++ b/src/guarantees/mod.rs @@ -1,13 +1,13 @@ //! Runtime guarantee verification modules. //! //! Consolidates all formal verification (Kani bounded model checking) -//! and property-based testing (proptest) into a single module tree. +//! and exhaustive correspondence testing into a single module tree. //! //! - `g4_lifecycle`: Kani proofs for lifecycle ordering (G4) -//! - `g5_fault_isolation`: Proptest for fault isolation (G5) -//! - `g6_g7_death_orphan`: Proptest for death notifications (G6) and orphan cleanup (G7) +//! - `g5_fault_isolation`: Tests for fault isolation (G5) +//! - `g6_g7_death_orphan`: Tests for death notifications (G6) and orphan cleanup (G7) //! - `g10_supervisor`: Kani proofs for supervisor restart decisions (G10) -//! - `correspondence`: Property-based tests verifying kani mirrors match production code +//! - `correspondence`: Exhaustive deterministic tests verifying production decision functions match runtime behavior #[cfg(kani)] mod g4_lifecycle; @@ -23,3 +23,15 @@ mod g6_g7_death_orphan; #[cfg(test)] mod correspondence; + +#[cfg(test)] +mod model_checker; + +#[cfg(test)] +mod stateright_lifecycle; + +#[cfg(test)] +mod stateright_death_orphan; + +#[cfg(test)] +mod stateright_supervisor; diff --git a/src/guarantees/model_checker.rs b/src/guarantees/model_checker.rs new file mode 100644 index 0000000..a150e1f --- /dev/null +++ b/src/guarantees/model_checker.rs @@ -0,0 +1,221 @@ +//! Minimal exhaustive DFS model checker. +//! +//! Provides the same core API surface as `stateright` — [`Model`] trait, +//! [`Property`] (always/sometimes), and a [`Checker`] with DFS exploration — +//! without requiring an external crate dependency. +//! +//! This keeps Cargo.lock unchanged while still providing genuine exhaustive +//! state-space exploration for the runtime guarantee proofs. + +use std::collections::HashSet; +use std::fmt::Debug; +use std::hash::Hash; +use std::marker::PhantomData; + +// ── Model trait ────────────────────────────────────────────────────────────── + +/// A finite-state model suitable for exhaustive exploration. +pub trait Model: Sized { + type State: Clone + Debug + Hash + Eq; + type Action: Clone + Debug + Hash + Eq; + + /// Initial states to begin exploration from. + fn init_states(&self) -> Vec; + + /// Enumerate all enabled actions in `state`, pushing them into `actions`. + fn actions(&self, state: &Self::State, actions: &mut Vec); + + /// Compute the successor state after applying `action`. Return `None` if + /// the action is a no-op (state unchanged). + fn next_state(&self, state: &Self::State, action: Self::Action) -> Option; + + /// Properties to verify across all reachable states. + fn properties(&self) -> Vec>; + + /// Create a checker for this model. + fn checker(&self) -> Checker<'_, Self> { + Checker { model: self } + } +} + +// ── Property ───────────────────────────────────────────────────────────────── + +/// The kind of temporal property. +enum PropertyKind { + /// Must hold in every reachable state. + Always, + /// Must hold in at least one reachable state (liveness canary). + Sometimes, +} + +/// A named property checked during model exploration. +pub struct Property { + name: String, + kind: PropertyKind, + checker_fn: Box bool>, +} + +impl Property { + /// Safety invariant: must hold in every reachable state. + pub fn always(name: &str, f: impl Fn(&M, &M::State) -> bool + 'static) -> Self { + Self { + name: name.to_string(), + kind: PropertyKind::Always, + checker_fn: Box::new(f), + } + } + + /// Liveness canary: must hold in at least one reachable state. + pub fn sometimes(name: &str, f: impl Fn(&M, &M::State) -> bool + 'static) -> Self { + Self { + name: name.to_string(), + kind: PropertyKind::Sometimes, + checker_fn: Box::new(f), + } + } +} + +// ── Checker & DFS ──────────────────────────────────────────────────────────── + +/// Builder that holds a reference to the model. +pub struct Checker<'a, M: Model> { + model: &'a M, +} + +impl<'a, M: Model> Checker<'a, M> { + /// Run exhaustive DFS. Named `spawn_dfs` for API compatibility, but runs + /// synchronously (no threads needed for our bounded models). + pub fn spawn_dfs(self) -> DfsHandle { + let properties = self.model.properties(); + let mut visited: HashSet = HashSet::new(); + let mut stack: Vec<(M::State, usize)> = Vec::new(); // (state, depth) + let mut max_depth: usize = 0; + let mut actions_buf: Vec = Vec::new(); + + // Track property results + let mut always_violated: Vec> = properties + .iter() + .map(|_| None) + .collect(); + let mut sometimes_satisfied: Vec = properties + .iter() + .map(|_| false) + .collect(); + + // Seed with init states + for s in self.model.init_states() { + if visited.insert(s.clone()) { + stack.push((s, 0)); + } + } + + while let Some((state, depth)) = stack.pop() { + if depth > max_depth { + max_depth = depth; + } + + // Check all properties against this state + for (i, prop) in properties.iter().enumerate() { + let holds = (prop.checker_fn)(self.model, &state); + match prop.kind { + PropertyKind::Always => { + if !holds && always_violated[i].is_none() { + always_violated[i] = Some(format!( + "ALWAYS property {:?} violated in state: {:?}", + prop.name, state + )); + } + } + PropertyKind::Sometimes => { + if holds { + sometimes_satisfied[i] = true; + } + } + } + } + + // Expand successors + actions_buf.clear(); + self.model.actions(&state, &mut actions_buf); + + for action in actions_buf.drain(..) { + if let Some(next) = self.model.next_state(&state, action) { + if visited.insert(next.clone()) { + stack.push((next, depth + 1)); + } + } + } + } + + // Build failures list + let mut failures = Vec::new(); + for (i, prop) in properties.iter().enumerate() { + match prop.kind { + PropertyKind::Always => { + if let Some(msg) = &always_violated[i] { + failures.push(msg.clone()); + } + } + PropertyKind::Sometimes => { + if !sometimes_satisfied[i] { + failures.push(format!( + "SOMETIMES property {:?} was never satisfied across {} states", + prop.name, + visited.len() + )); + } + } + } + } + + DfsHandle { + result: CheckResult { + unique_states: visited.len(), + max_depth, + failures, + }, + _phantom: PhantomData, + } + } +} + +/// Handle returned by `spawn_dfs`. Call `.join()` to get the result. +pub struct DfsHandle { + result: CheckResult, + _phantom: PhantomData, +} + +// Suppress unused type parameter warning +impl DfsHandle { + /// Consume the handle and return the exploration result. + pub fn join(self) -> CheckResult { + self.result + } +} + +/// Result of an exhaustive DFS exploration. +pub struct CheckResult { + unique_states: usize, + max_depth: usize, + failures: Vec, +} + +impl CheckResult { + /// Number of unique states explored. + pub fn unique_state_count(&self) -> usize { + self.unique_states + } + + /// Maximum DFS depth reached. + pub fn max_depth(&self) -> usize { + self.max_depth + } + + /// Panic if any property was violated. + pub fn assert_properties(&self) { + if !self.failures.is_empty() { + let msg = self.failures.join("\n"); + panic!("Property violations:\n{msg}"); + } + } +} diff --git a/src/guarantees/stateright_death_orphan.rs b/src/guarantees/stateright_death_orphan.rs new file mode 100644 index 0000000..e2c4821 --- /dev/null +++ b/src/guarantees/stateright_death_orphan.rs @@ -0,0 +1,439 @@ +//! Stateright model-checking of death notifications (G6) and orphan cleanup (G7). +//! +//! Two focused models keep the state space tractable: +//! +//! 1. **MonitorModel** (G6): 3 actors with monitor/demonitor/kill. Proves +//! notification exactness, no-notification-for-alive, demonitor suppression. +//! +//! 2. **OrphanModel** (G7): 4 actors with parent-child/kill/orphan-cleanup. +//! Proves unsupervised children stop, supervised survive, cascading cleanup. + +use super::model_checker::{Model, Property}; + +// ═══════════════════════════════════════════════════════════════════════════ +// G6: Monitor Model +// ═══════════════════════════════════════════════════════════════════════════ + +const MON_N: usize = 3; +const MON_PAIRS: usize = MON_N * (MON_N - 1); // 6 + +fn mon_pair(i: usize, j: usize) -> usize { + debug_assert!(i < MON_N && j < MON_N && i != j); + if j < i { i * (MON_N - 1) + j } else { i * (MON_N - 1) + j - 1 } +} + +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +struct MonitorState { + alive: [bool; MON_N], + /// Active monitor from i to j. + active: [bool; MON_PAIRS], + /// Demonitored while target was still alive (the meaningful demonitor case). + deactivated_while_alive: [bool; MON_PAIRS], + /// Notification count (capped at 2 to detect duplicates). + notif: [u8; MON_PAIRS], +} + +impl MonitorState { + fn init() -> Self { + Self { + alive: [true; MON_N], + active: [false; MON_PAIRS], + deactivated_while_alive: [false; MON_PAIRS], + notif: [0; MON_PAIRS], + } + } +} + +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +enum MonAction { + Monitor(usize, usize), + Demonitor(usize, usize), + Kill(usize), +} + +#[derive(Clone)] +struct MonitorModel; + +impl Model for MonitorModel { + type State = MonitorState; + type Action = MonAction; + + fn init_states(&self) -> Vec { + vec![MonitorState::init()] + } + + fn actions(&self, s: &Self::State, actions: &mut Vec) { + for i in 0..MON_N { + if !s.alive[i] { continue; } + + for j in 0..MON_N { + if i == j { continue; } + let idx = mon_pair(i, j); + + if s.alive[j] && !s.active[idx] { + actions.push(MonAction::Monitor(i, j)); + } + if s.active[idx] { + actions.push(MonAction::Demonitor(i, j)); + } + } + + actions.push(MonAction::Kill(i)); + } + } + + fn next_state(&self, s: &Self::State, action: Self::Action) -> Option { + let mut n = s.clone(); + match action { + MonAction::Monitor(w, t) => { + let idx = mon_pair(w, t); + n.active[idx] = true; + n.deactivated_while_alive[idx] = false; + } + MonAction::Demonitor(w, t) => { + let idx = mon_pair(w, t); + n.active[idx] = false; + if n.alive[t] { + n.deactivated_while_alive[idx] = true; + } + } + MonAction::Kill(t) => { + if !n.alive[t] { return None; } + n.alive[t] = false; + for w in 0..MON_N { + if w == t { continue; } + let idx = mon_pair(w, t); + if n.alive[w] && n.active[idx] && n.notif[idx] < 2 { + n.notif[idx] += 1; + } + } + } + } + if n == *s { None } else { Some(n) } + } + + fn properties(&self) -> Vec> { + vec![ + Property::::always("G6a: exactly one notification per active monitor on dead target", |_, s| { + for w in 0..MON_N { + if !s.alive[w] { continue; } + for t in 0..MON_N { + if w == t { continue; } + let idx = mon_pair(w, t); + if s.active[idx] && !s.alive[t] && s.notif[idx] != 1 { + return false; + } + } + } + true + }), + Property::::always("G6b: no notification for alive targets", |_, s| { + for w in 0..MON_N { + for t in 0..MON_N { + if w == t { continue; } + if s.alive[t] && s.notif[mon_pair(w, t)] > 0 { + return false; + } + } + } + true + }), + Property::::always("G6c: demonitor before death suppresses notification", |_, s| { + for w in 0..MON_N { + for t in 0..MON_N { + if w == t { continue; } + let idx = mon_pair(w, t); + // If demonitored while target was alive, no notification should exist + if s.deactivated_while_alive[idx] && s.notif[idx] > 0 { + return false; + } + } + } + true + }), + // Liveness + Property::::sometimes("L1: monitor fires", |_, s| { + s.notif.iter().any(|&c| c > 0) + }), + Property::::sometimes("L2: demonitor suppression reachable", |_, s| { + (0..MON_N).any(|w| (0..MON_N).any(|t| { + w != t && { + let idx = mon_pair(w, t); + s.deactivated_while_alive[idx] && !s.alive[t] && s.notif[idx] == 0 + } + })) + }), + Property::::sometimes("L3: multiple monitors on same target", |_, s| { + (0..MON_N).any(|t| { + let watchers: usize = (0..MON_N) + .filter(|&w| w != t && s.notif[mon_pair(w, t)] > 0) + .count(); + watchers >= 2 + }) + }), + ] + } +} + +// ═══════════════════════════════════════════════════════════════════════════ +// G7: Orphan Model +// ═══════════════════════════════════════════════════════════════════════════ + +/// 4 actors: enough for parent → child → grandchild chains (3 deep) plus +/// a sibling to test supervised vs unsupervised. +const ORP_N: usize = 4; +const ORP_PAIRS: usize = ORP_N * (ORP_N - 1); // 12 + +fn orp_pair(i: usize, j: usize) -> usize { + debug_assert!(i < ORP_N && j < ORP_N && i != j); + if j < i { i * (ORP_N - 1) + j } else { i * (ORP_N - 1) + j - 1 } +} + +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +struct OrphanState { + alive: [bool; ORP_N], + /// Unsupervised parent→child. + parent_unsup: [bool; ORP_PAIRS], + /// Supervised parent→child. + parent_sup: [bool; ORP_PAIRS], + /// Orphan cleanup propagated for actor i. + orphan_cleaned: [bool; ORP_N], + /// Whether actor was killed by OrphanCleanup (not by explicit Kill). + orphan_killed: [bool; ORP_N], + /// How many parent-child links have been set (cap to limit state space). + link_count: u8, +} + +/// Max parent-child links to prevent state explosion. +const MAX_LINKS: u8 = 3; + +impl OrphanState { + fn init() -> Self { + Self { + alive: [true; ORP_N], + parent_unsup: [false; ORP_PAIRS], + parent_sup: [false; ORP_PAIRS], + orphan_cleaned: [false; ORP_N], + orphan_killed: [false; ORP_N], + link_count: 0, + } + } + + fn has_parent(&self, c: usize) -> bool { + (0..ORP_N).any(|p| p != c && { + let idx = orp_pair(p, c); + self.parent_unsup[idx] || self.parent_sup[idx] + }) + } + + fn has_children(&self, p: usize) -> bool { + (0..ORP_N).any(|c| c != p && { + let idx = orp_pair(p, c); + self.parent_unsup[idx] || self.parent_sup[idx] + }) + } +} + +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +enum OrpAction { + SetParentUnsup(usize, usize), + SetParentSup(usize, usize), + Kill(usize), + OrphanCleanup(usize), +} + +#[derive(Clone)] +struct OrphanModel; + +impl Model for OrphanModel { + type State = OrphanState; + type Action = OrpAction; + + fn init_states(&self) -> Vec { + vec![OrphanState::init()] + } + + fn actions(&self, s: &Self::State, actions: &mut Vec) { + // SetParent actions only if under link cap + if s.link_count < MAX_LINKS { + for p in 0..ORP_N { + if !s.alive[p] { continue; } + for c in 0..ORP_N { + if p == c || !s.alive[c] { continue; } + if s.has_parent(c) { continue; } + // Prevent cycles: c must not be an ancestor of p + if is_ancestor(s, c, p) { continue; } + actions.push(OrpAction::SetParentUnsup(p, c)); + actions.push(OrpAction::SetParentSup(p, c)); + } + } + } + + for i in 0..ORP_N { + if s.alive[i] { + actions.push(OrpAction::Kill(i)); + } + if !s.alive[i] && !s.orphan_cleaned[i] && s.has_children(i) { + actions.push(OrpAction::OrphanCleanup(i)); + } + } + } + + fn next_state(&self, s: &Self::State, action: Self::Action) -> Option { + let mut n = s.clone(); + match action { + OrpAction::SetParentUnsup(p, c) => { + n.parent_unsup[orp_pair(p, c)] = true; + n.link_count += 1; + } + OrpAction::SetParentSup(p, c) => { + n.parent_sup[orp_pair(p, c)] = true; + n.link_count += 1; + } + OrpAction::Kill(i) => { + if !n.alive[i] { return None; } + n.alive[i] = false; + } + OrpAction::OrphanCleanup(dead_parent) => { + n.orphan_cleaned[dead_parent] = true; + // Kill unsupervised children + for c in 0..ORP_N { + if c == dead_parent { continue; } + if n.parent_unsup[orp_pair(dead_parent, c)] && n.alive[c] { + n.alive[c] = false; + n.orphan_killed[c] = true; + } + } + } + } + if n == *s { None } else { Some(n) } + } + + fn properties(&self) -> Vec> { + vec![ + // G7a: After orphan cleanup, all unsupervised children are dead + Property::::always("G7a: orphan cleanup stops unsupervised children", |_, s| { + for p in 0..ORP_N { + if !s.alive[p] && s.orphan_cleaned[p] { + for c in 0..ORP_N { + if c == p { continue; } + if s.parent_unsup[orp_pair(p, c)] && s.alive[c] { + return false; + } + } + } + } + true + }), + + // G7b: OrphanCleanup never kills supervised-only children. + // If orphan_killed[c] is true, there must be a parent p with an + // unsupervised link (parent_unsup[p→c]) that was orphan-cleaned. + // A supervised-only child has no parent_unsup link, so orphan_killed + // being true for it would violate this property. + Property::::always("G7b: supervised children survive orphan cleanup", |_, s| { + for c in 0..ORP_N { + if s.orphan_killed[c] { + // There must exist a dead, cleaned parent with unsup link to c + let has_unsup_cleaned_parent = (0..ORP_N).any(|p| { + p != c + && s.parent_unsup[orp_pair(p, c)] + && s.orphan_cleaned[p] + }); + if !has_unsup_cleaned_parent { + return false; + } + } + } + true + }), + + // G7c: Cascading — if orphan-cleaned parent's child also died and was + // orphan-cleaned, its unsupervised children are dead too + Property::::always("G7c: cascading orphan cleanup", |_, s| { + for p in 0..ORP_N { + if s.orphan_cleaned[p] { + for c in 0..ORP_N { + if c == p { continue; } + if s.parent_unsup[orp_pair(p, c)] + && !s.alive[c] + && s.orphan_cleaned[c] + { + for gc in 0..ORP_N { + if gc == c { continue; } + if s.parent_unsup[orp_pair(c, gc)] && s.alive[gc] { + return false; + } + } + } + } + } + } + true + }), + + // Liveness + Property::::sometimes("L1: orphan cleanup triggers", |_, s| { + s.orphan_cleaned.iter().any(|&c| c) + }), + Property::::sometimes("L2: cascading cleanup reachable", |_, s| { + // Parent cleaned → child died → child cleaned + (0..ORP_N).any(|p| s.orphan_cleaned[p] && (0..ORP_N).any(|c| { + c != p + && s.parent_unsup[orp_pair(p, c)] + && !s.alive[c] + && s.orphan_cleaned[c] + })) + }), + Property::::sometimes("L3: supervised child survives cleanup", |_, s| { + (0..ORP_N).any(|p| s.orphan_cleaned[p] && (0..ORP_N).any(|c| { + c != p && s.parent_sup[orp_pair(p, c)] && s.alive[c] + })) + }), + ] + } +} + +/// Check if `ancestor` is an ancestor of `descendant` via parent links. +fn is_ancestor(s: &OrphanState, ancestor: usize, descendant: usize) -> bool { + // Walk up from descendant + let mut current = descendant; + for _ in 0..ORP_N { + let parent = (0..ORP_N).find(|&p| { + p != current && { + let idx = orp_pair(p, current); + s.parent_unsup[idx] || s.parent_sup[idx] + } + }); + match parent { + Some(p) if p == ancestor => return true, + Some(p) => current = p, + None => return false, + } + } + false +} + +// ── Tests ──────────────────────────────────────────────────────────────────── + +#[test] +#[ignore] // Exhaustive proof — run deliberately with `cargo test -- --ignored` +fn g6_monitor_model_check() { + let result = MonitorModel.checker().spawn_dfs().join(); + let unique = result.unique_state_count(); + let depth = result.max_depth(); + println!("Stateright G6 (Monitor): {} unique states, max depth {}", unique, depth); + result.assert_properties(); + assert!(unique > 100, "Too few states ({unique})"); +} + +#[test] +#[ignore] // Exhaustive proof — run deliberately with `cargo test -- --ignored` +fn g7_orphan_model_check() { + let result = OrphanModel.checker().spawn_dfs().join(); + let unique = result.unique_state_count(); + let depth = result.max_depth(); + println!("Stateright G7 (Orphan): {} unique states, max depth {}", unique, depth); + result.assert_properties(); + assert!(unique > 100, "Too few states ({unique})"); +} diff --git a/src/guarantees/stateright_lifecycle.rs b/src/guarantees/stateright_lifecycle.rs new file mode 100644 index 0000000..add4e2e --- /dev/null +++ b/src/guarantees/stateright_lifecycle.rs @@ -0,0 +1,354 @@ +//! Stateright model-checking of the actor lifecycle state machine (G4, G5). +//! +//! Exhaustively explores all interleavings of lifecycle transitions across a +//! bounded runtime with 3 actors. Each action directly transitions one actor's +//! lifecycle state (no explicit mailbox — events are modeled as actions). +//! +//! Verifies: +//! +//! - **G4**: Lifecycle ordering (on_start once, no handle when stopping/poisoned, +//! on_stop conditions, no handle after on_stop, suspension pauses processing). +//! - **G5**: Fault isolation (a panic in one actor never affects another's flags +//! or counters; healthy actors process messages despite sibling panics). +//! +//! Uses production decision functions (`should_skip_actor`, `is_on_stop_eligible`) +//! from `worker.rs` so the model checks real code, not test-only mirrors. + +use super::model_checker::{Model, Property}; +use crate::worker::{is_on_stop_eligible, should_skip_actor}; + +// ── Bounded constants ──────────────────────────────────────────────────────── + +/// Number of actors. 3 is the minimum to exercise isolation between a poisoned +/// actor and multiple healthy siblings. +const NUM_ACTORS: usize = 3; + +/// Cap on handle_count. 2 is sufficient to verify "handle fires" and +/// "handle does not fire after stop/poison" without state explosion. +const MAX_HANDLE: u8 = 2; + +// ── Per-actor state ────────────────────────────────────────────────────────── + +/// Lifecycle state for one actor. No mailbox — events are modeled as actions. +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +struct ActorState { + started: bool, + stopping: bool, + poisoned: bool, + suspended: bool, + alive: bool, + + on_start_count: u8, + handle_count: u8, + on_stop_count: u8, +} + +impl ActorState { + fn new() -> Self { + Self { + started: false, + stopping: false, + poisoned: false, + suspended: false, + alive: true, + on_start_count: 0, + handle_count: 0, + on_stop_count: 0, + } + } +} + +// ── Runtime state ──────────────────────────────────────────────────────────── + +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +struct RuntimeState { + actors: [ActorState; NUM_ACTORS], +} + +impl RuntimeState { + fn init() -> Self { + Self { + actors: std::array::from_fn(|_| ActorState::new()), + } + } +} + +// ── Actions ────────────────────────────────────────────────────────────────── + +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +enum RuntimeAction { + /// Fire on_start for an actor (first tick). + Start(usize), + /// Deliver a message — increments handle_count. + Handle(usize), + /// Actor's handler panics — sets poisoned. + PanicHandle(usize), + /// Actor's on_start panics — sets started + poisoned, handle_count stays 0. + PanicStart(usize), + /// Stop signal arrives — sets stopping. + Stop(usize), + /// Suspend signal — sets suspended. + Suspend(usize), + /// Resume signal delivered to suspended actor. + Resume(usize), + /// Run cleanup_dead for an actor (fires on_stop if eligible, marks not alive). + Cleanup(usize), +} + +// ── Stateright Model ───────────────────────────────────────────────────────── + +#[derive(Clone)] +struct LifecycleModel; + +impl Model for LifecycleModel { + type State = RuntimeState; + type Action = RuntimeAction; + + fn init_states(&self) -> Vec { + vec![RuntimeState::init()] + } + + fn actions(&self, state: &Self::State, actions: &mut Vec) { + for idx in 0..NUM_ACTORS { + let a = &state.actors[idx]; + + if !a.alive { + continue; + } + + // Start: only if not yet started and not skipped by production logic + if !a.started && !should_skip_actor(a.poisoned, a.stopping, a.suspended) { + actions.push(RuntimeAction::Start(idx)); + actions.push(RuntimeAction::PanicStart(idx)); + } + + // Handle/PanicHandle: only if started, not skipped, handle under cap + if a.started && !should_skip_actor(a.poisoned, a.stopping, a.suspended) { + if a.handle_count < MAX_HANDLE { + actions.push(RuntimeAction::Handle(idx)); + actions.push(RuntimeAction::PanicHandle(idx)); + } + } + + // Stop: only if started and not already stopping. + // Production justification: StopSignal goes through mailbox, + // processed AFTER on_start; ctx.stop_self() requires started. + if a.started && !a.stopping { + actions.push(RuntimeAction::Stop(idx)); + } + + // Suspend: only if started, not suspended, not stopping/poisoned + if a.started && !a.suspended && !a.stopping && !a.poisoned { + actions.push(RuntimeAction::Suspend(idx)); + } + + // Resume: only if suspended + if a.suspended { + actions.push(RuntimeAction::Resume(idx)); + } + + // Cleanup: only if stopping or poisoned + if a.stopping || a.poisoned { + actions.push(RuntimeAction::Cleanup(idx)); + } + } + } + + fn next_state(&self, state: &Self::State, action: Self::Action) -> Option { + let mut next = state.clone(); + + match action { + RuntimeAction::Start(idx) => { + let a = &mut next.actors[idx]; + a.on_start_count += 1; + a.started = true; + } + RuntimeAction::Handle(idx) => { + let a = &mut next.actors[idx]; + a.handle_count += 1; + } + RuntimeAction::PanicHandle(idx) => { + let a = &mut next.actors[idx]; + a.handle_count += 1; + a.poisoned = true; + } + RuntimeAction::PanicStart(idx) => { + let a = &mut next.actors[idx]; + a.on_start_count += 1; + a.started = true; + a.poisoned = true; + } + RuntimeAction::Stop(idx) => { + next.actors[idx].stopping = true; + } + RuntimeAction::Suspend(idx) => { + next.actors[idx].suspended = true; + } + RuntimeAction::Resume(idx) => { + next.actors[idx].suspended = false; + } + RuntimeAction::Cleanup(idx) => { + let a = &mut next.actors[idx]; + // Use production decision function + if is_on_stop_eligible(a.stopping, a.poisoned) { + a.on_stop_count += 1; + } + a.alive = false; + } + } + + // Prune no-change transitions + if next == *state { + return None; + } + + Some(next) + } + + fn properties(&self) -> Vec> { + vec![ + // ── G4 Safety Properties ────────────────────────────────────── + + // G4a: on_start fires at most once per actor + Property::::always("G4a: on_start_count <= 1", |_, state| { + state.actors.iter().all(|a| a.on_start_count <= 1) + }), + // G4a: no handle before on_start + Property::::always("G4a: no handle before start", |_, state| { + state + .actors + .iter() + .all(|a| !(a.handle_count > 0 && a.on_start_count == 0)) + }), + // G4b: if poisoned or stopping, no further handle calls + // (encoded in action generation, verified here as invariant) + Property::::always("G4b: poisoned implies no on_stop", |_, state| { + state + .actors + .iter() + .all(|a| !(a.poisoned && a.on_stop_count > 0)) + }), + // G4c: on_stop fires at most once + Property::::always("G4c: on_stop_count <= 1", |_, state| { + state.actors.iter().all(|a| a.on_stop_count <= 1) + }), + // G4c: on_stop only fires when stopping && !poisoned + Property::::always("G4c: on_stop implies stopping && !poisoned", |_, state| { + state.actors.iter().all(|a| { + if a.on_stop_count == 1 { + a.stopping && !a.poisoned + } else { + true + } + }) + }), + // G4d: on_stop implies actor is removed (no further handle possible) + Property::::always("G4d: on_stop implies not alive", |_, state| { + state.actors.iter().all(|a| { + if a.on_stop_count > 0 { + !a.alive + } else { + true + } + }) + }), + // G4e: on_stop implies the actor was started (no cleanup of + // never-initialized actors). Enabled by the Stop guard requiring + // `started`, which mirrors production: StopSignal goes through + // the mailbox and is processed after on_start. + Property::::always("G4e: on_stop implies started", |_, state| { + state.actors.iter().all(|a| { + if a.on_stop_count > 0 { a.started } else { true } + }) + }), + + // ── G5 Safety Properties ────────────────────────────────────── + + // G5: every actor's lifecycle invariants hold independently, + // regardless of what happened to other actors. + Property::::always("G5: per-actor invariants hold", |_, state| { + for a in &state.actors { + // Each actor's lifecycle is self-consistent + if a.on_start_count > 1 || a.on_stop_count > 1 { + return false; + } + if a.handle_count > 0 && a.on_start_count == 0 { + return false; + } + if a.alive && a.on_stop_count > 0 { + return false; + } + if a.poisoned && a.on_stop_count > 0 { + return false; + } + } + true + }), + // G5: a panic on one actor doesn't corrupt another's started flag + Property::::always("G5: panic isolation on started", |_, state| { + for i in 0..NUM_ACTORS { + if state.actors[i].poisoned { + for j in 0..NUM_ACTORS { + if i != j { + let other = &state.actors[j]; + // Other actor's lifecycle must be internally consistent + if other.handle_count > 0 && !other.started { + return false; + } + } + } + } + } + true + }), + // ── Liveness Canaries ───────────────────────────────────────── + + // L1: handle_count > 0 is reachable + Property::::sometimes("L1: handle reachable", |_, state| { + state.actors.iter().any(|a| a.handle_count > 0) + }), + // L2: on_stop_count == 1 is reachable + Property::::sometimes("L2: on_stop reachable", |_, state| { + state.actors.iter().any(|a| a.on_stop_count == 1) + }), + // L3: one actor poisoned while another has handle_count > 0 + Property::::sometimes("L3: poison + sibling handle", |_, state| { + let any_poisoned = state.actors.iter().any(|a| a.poisoned); + let any_handled = state + .actors + .iter() + .any(|a| a.handle_count > 0 && !a.poisoned); + any_poisoned && any_handled + }), + // L4: on_start panic reachable (poisoned with handle_count == 0) + Property::::sometimes("L4: on_start panic reachable", |_, state| { + state.actors.iter().any(|a| { + a.poisoned && a.handle_count == 0 && a.on_start_count > 0 + }) + }), + ] + } +} + +// ── Test ───────────────────────────────────────────────────────────────────── + +#[test] +#[ignore] // Exhaustive proof — run deliberately with `cargo test -- --ignored` +fn lifecycle_fault_isolation_model_check() { + let result = LifecycleModel.checker().spawn_dfs().join(); + + let unique_states = result.unique_state_count(); + let max_depth = result.max_depth(); + println!( + "Stateright G4/G5: explored {} unique states, max depth {}", + unique_states, max_depth, + ); + + result.assert_properties(); + + // Sanity: the model explored a meaningful state space. + assert!( + unique_states > 100, + "Model explored too few states ({unique_states}); bounds may be too tight", + ); +} diff --git a/src/guarantees/stateright_supervisor.rs b/src/guarantees/stateright_supervisor.rs new file mode 100644 index 0000000..6f6c013 --- /dev/null +++ b/src/guarantees/stateright_supervisor.rs @@ -0,0 +1,403 @@ +//! Stateright model-checking of supervisor restart decisions (G8). +//! +//! Exhaustively explores all interleavings of child deaths and supervisor +//! restart responses across bounded parameter spaces. Uses production +//! decision functions (`RestartPolicy::should_restart`, `compute_restart_set`) +//! from `std/supervisor.rs`. +//! +//! The model tracks each death event's restart set in state, enabling +//! per-transition property verification: +//! +//! - **G8a**: `OneForOne` restarts only the dead child (if policy permits). +//! - **G8b**: `OneForAll` restarts all children (if policy permits). +//! - **G8c**: `RestForOne` restarts dead child + successors (if policy permits). +//! - **G8d**: `Temporary` dead child triggers no restart. +//! - **G8e**: `Transient` dead child + Normal death → no restart. +//! - **G8f**: `Transient` dead child + Panicked death → restart (if not meltdown). +//! - **G8g**: Meltdown stops supervisor when total_restarts > max_restarts. +//! +//! Liveness canaries prove non-vacuity: restarts occur, meltdowns are +//! reachable, and each strategy is exercised. + +use super::model_checker::{Model, Property}; +use crate::actor::StopReason; +use crate::std::supervisor::compute_restart_set; +use crate::std::{RestartPolicy, SupervisorStrategy}; + +// ── Bounded constants ──────────────────────────────────────────────────────── + +/// Number of supervised children. 4 exercises all strategies meaningfully +/// (RestForOne needs at least 3 to distinguish "rest" from "all"). +const NUM_CHILDREN: usize = 4; + +/// Maximum restarts before meltdown. Kept small (3) to make meltdown +/// reachable without state explosion. +const MAX_RESTARTS: u8 = 3; + +/// Maximum deaths to process. Bounds the exploration depth. +const MAX_DEATHS: u8 = 4; + +// ── State ──────────────────────────────────────────────────────────────────── + +/// Simplified death reason matching `StopReason` variants relevant to restart. +#[derive(Clone, Copy, Debug, Hash, PartialEq, Eq)] +enum DeathReason { + Normal, + Panicked, +} + +impl DeathReason { + fn to_stop_reason(self) -> StopReason { + match self { + DeathReason::Normal => StopReason::Normal, + DeathReason::Panicked => StopReason::Panicked, + } + } +} + +/// Per-child state within the supervisor. +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +struct ChildState { + alive: bool, + policy: RestartPolicy, + /// How many times this child has been restarted. + restart_count: u8, +} + +/// Record of the most recent death event's outcome. Stored in state so +/// that `always` properties can verify per-transition correctness. +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +struct LastEvent { + dead_idx: usize, + reason: DeathReason, + dead_policy: RestartPolicy, + /// Which children were restarted by this event. + restarted: [bool; NUM_CHILDREN], + /// Whether this event triggered meltdown. + triggered_meltdown: bool, +} + +/// Supervisor state machine for Stateright exploration. +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +struct SupervisorState { + strategy: SupervisorStrategy, + children: [ChildState; NUM_CHILDREN], + total_restarts: u8, + melted_down: bool, + /// How many death events have been processed (bounds exploration). + deaths_processed: u8, + /// The last death event's outcome, for per-transition property checks. + last_event: Option, +} + +// ── Actions ────────────────────────────────────────────────────────────────── + +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +enum SupAction { + /// A child dies with the given reason. The supervisor immediately + /// processes the death: checks policy, computes restart set, executes. + ChildDies(usize, DeathReason), +} + +// ── Model ──────────────────────────────────────────────────────────────────── + +#[derive(Clone)] +struct SupervisorModel; + +impl SupervisorModel { + /// Generate all initial states: every combination of strategy × per-child policy. + fn all_init_states() -> Vec { + let strategies = [ + SupervisorStrategy::OneForOne, + SupervisorStrategy::OneForAll, + SupervisorStrategy::RestForOne, + ]; + let policies = [ + RestartPolicy::Permanent, + RestartPolicy::Transient, + RestartPolicy::Temporary, + ]; + + let mut states = Vec::new(); + + for &strategy in &strategies { + // Enumerate all 3^NUM_CHILDREN policy assignments + for combo in 0..3u32.pow(NUM_CHILDREN as u32) { + let mut children: [ChildState; NUM_CHILDREN] = + std::array::from_fn(|_| ChildState { + alive: true, + policy: RestartPolicy::Permanent, + restart_count: 0, + }); + + let mut c = combo; + for child in children.iter_mut() { + child.policy = policies[(c % 3) as usize]; + c /= 3; + } + + states.push(SupervisorState { + strategy, + children, + total_restarts: 0, + melted_down: false, + deaths_processed: 0, + last_event: None, + }); + } + } + + states + } +} + +impl Model for SupervisorModel { + type State = SupervisorState; + type Action = SupAction; + + fn init_states(&self) -> Vec { + Self::all_init_states() + } + + fn actions(&self, s: &Self::State, actions: &mut Vec) { + if s.melted_down || s.deaths_processed >= MAX_DEATHS { + return; + } + + for idx in 0..NUM_CHILDREN { + if s.children[idx].alive { + actions.push(SupAction::ChildDies(idx, DeathReason::Normal)); + actions.push(SupAction::ChildDies(idx, DeathReason::Panicked)); + } + } + } + + fn next_state(&self, s: &Self::State, action: Self::Action) -> Option { + let SupAction::ChildDies(dead_idx, reason) = action; + + if !s.children[dead_idx].alive { + return None; + } + + let mut next = s.clone(); + next.deaths_processed += 1; + + let dead_policy = next.children[dead_idx].policy; + + // Mark dead + next.children[dead_idx].alive = false; + + let mut event = LastEvent { + dead_idx, + reason, + dead_policy, + restarted: [false; NUM_CHILDREN], + triggered_meltdown: false, + }; + + // Use production should_restart on the dead child's policy + let stop_reason = reason.to_stop_reason(); + if !dead_policy.should_restart(stop_reason) { + next.last_event = Some(event); + return if next == *s { None } else { Some(next) }; + } + + // Meltdown check + let new_total = next.total_restarts + 1; + if new_total > MAX_RESTARTS { + next.melted_down = true; + event.triggered_meltdown = true; + next.last_event = Some(event); + return Some(next); + } + next.total_restarts = new_total; + + // Use production compute_restart_set + let restart_indices = + compute_restart_set(next.strategy, dead_idx, NUM_CHILDREN); + + for &idx in &restart_indices { + if idx < NUM_CHILDREN { + next.children[idx].alive = true; + next.children[idx].restart_count = + next.children[idx].restart_count.saturating_add(1); + event.restarted[idx] = true; + } + } + + next.last_event = Some(event); + if next == *s { None } else { Some(next) } + } + + fn properties(&self) -> Vec> { + vec![ + // ── G8a: OneForOne restarts only the dead child ───────────── + Property::::always( + "G8a: OneForOne restarts only dead child", + |_, s| { + if s.strategy != SupervisorStrategy::OneForOne { + return true; + } + let Some(ev) = &s.last_event else { return true }; + if !ev.restarted.iter().any(|&r| r) { + return true; // no restart (policy denied or meltdown) + } + // Only the dead child should be in the restart set + for (i, &restarted) in ev.restarted.iter().enumerate() { + if i == ev.dead_idx { + if !restarted { return false; } + } else if restarted { + return false; + } + } + true + }, + ), + + // ── G8b: OneForAll restarts all children ──────────────────── + Property::::always( + "G8b: OneForAll restarts all children", + |_, s| { + if s.strategy != SupervisorStrategy::OneForAll { + return true; + } + let Some(ev) = &s.last_event else { return true }; + if !ev.restarted.iter().any(|&r| r) { + return true; + } + // All children must be in the restart set + ev.restarted.iter().all(|&r| r) + }, + ), + + // ── G8c: RestForOne restarts dead child + successors ──────── + Property::::always( + "G8c: RestForOne restarts dead + successors only", + |_, s| { + if s.strategy != SupervisorStrategy::RestForOne { + return true; + } + let Some(ev) = &s.last_event else { return true }; + if !ev.restarted.iter().any(|&r| r) { + return true; + } + // Children before dead_idx must NOT be restarted + for i in 0..ev.dead_idx { + if ev.restarted[i] { return false; } + } + // Dead child + all after must be restarted + for i in ev.dead_idx..NUM_CHILDREN { + if !ev.restarted[i] { return false; } + } + true + }, + ), + + // ── G8d: Temporary dead child triggers no restart ─────────── + // When the child that DIES has Temporary policy, should_restart + // returns false and no children are restarted at all. + Property::::always( + "G8d: Temporary dead child triggers no restart", + |_, s| { + let Some(ev) = &s.last_event else { return true }; + if ev.dead_policy != RestartPolicy::Temporary { + return true; + } + ev.restarted.iter().all(|&r| !r) + }, + ), + + // ── G8e: Transient + Normal death → no restart ────────────── + Property::::always( + "G8e: Transient + Normal triggers no restart", + |_, s| { + let Some(ev) = &s.last_event else { return true }; + if ev.dead_policy != RestartPolicy::Transient + || ev.reason != DeathReason::Normal + { + return true; + } + ev.restarted.iter().all(|&r| !r) + }, + ), + + // ── G8f: Transient + Panicked → restart (unless meltdown) ── + Property::::always( + "G8f: Transient + Panicked triggers restart unless meltdown", + |_, s| { + let Some(ev) = &s.last_event else { return true }; + if ev.dead_policy != RestartPolicy::Transient + || ev.reason != DeathReason::Panicked + || ev.triggered_meltdown + { + return true; + } + // A restart should have happened + ev.restarted.iter().any(|&r| r) + }, + ), + + // ── G8g: Meltdown bounds total restarts ───────────────────── + Property::::always( + "G8g: meltdown when total_restarts exceeds max", + |_, s| { + if s.melted_down { + true // no further actions (enforced by empty actions) + } else { + s.total_restarts <= MAX_RESTARTS + } + }, + ), + + // ── Liveness Canaries ─────────────────────────────────────── + Property::::sometimes( + "L1: a restart occurs", + |_, s| s.children.iter().any(|c| c.restart_count > 0), + ), + Property::::sometimes( + "L2: meltdown is reachable", + |_, s| s.melted_down, + ), + Property::::sometimes( + "L3: OneForOne exercised with restart", + |_, s| { + s.strategy == SupervisorStrategy::OneForOne + && s.children.iter().any(|c| c.restart_count > 0) + }, + ), + Property::::sometimes( + "L4: OneForAll exercised with restart", + |_, s| { + s.strategy == SupervisorStrategy::OneForAll + && s.children.iter().any(|c| c.restart_count > 0) + }, + ), + Property::::sometimes( + "L5: RestForOne exercised with restart", + |_, s| { + s.strategy == SupervisorStrategy::RestForOne + && s.children.iter().any(|c| c.restart_count > 0) + }, + ), + ] + } +} + +// ── Tests ──────────────────────────────────────────────────────────────────── + +#[test] +#[ignore] // Exhaustive proof — run deliberately with `cargo test -- --ignored` +fn g8_supervisor_restart_model_check() { + let result = SupervisorModel.checker().spawn_dfs().join(); + let unique = result.unique_state_count(); + let depth = result.max_depth(); + println!( + "Stateright G8 (Supervisor Restart): {} unique states, max depth {}", + unique, depth, + ); + result.assert_properties(); + assert!( + unique > 100, + "Model explored too few states ({unique}); bounds may be too tight", + ); +} diff --git a/src/std/mod.rs b/src/std/mod.rs index 1919048..74bb5c6 100644 --- a/src/std/mod.rs +++ b/src/std/mod.rs @@ -1,4 +1,4 @@ -mod supervisor; +pub(crate) mod supervisor; mod router; pub mod name_registry; pub mod monitor_registry; diff --git a/src/std/supervisor.rs b/src/std/supervisor.rs index 8b743c3..e98434c 100644 --- a/src/std/supervisor.rs +++ b/src/std/supervisor.rs @@ -7,7 +7,7 @@ use super::ctx_ext::get_ext; use super::CtxMonitoring; /// How a child should be restarted when it dies. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub enum RestartPolicy { /// Always restart, regardless of stop reason. Permanent, @@ -18,7 +18,7 @@ pub enum RestartPolicy { } /// Strategy for handling child failures. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub enum SupervisorStrategy { /// Only restart the failed child. Other children are unaffected. OneForOne, @@ -29,11 +29,33 @@ pub enum SupervisorStrategy { RestForOne, } +impl RestartPolicy { + // Pure functions for kani model checking + + /// Whether this policy permits restarting a child that died for the given reason. + pub fn should_restart(self, reason: StopReason) -> bool { + match self { + RestartPolicy::Permanent => true, + RestartPolicy::Transient => reason == StopReason::Panicked, + RestartPolicy::Temporary => false, + } + } +} + +/// Compute which child indices should be restarted given a supervision strategy +pub fn compute_restart_set( + strategy: SupervisorStrategy, + dead_idx: usize, + num_children: usize, +) -> Vec { + match strategy { + SupervisorStrategy::OneForOne => vec![dead_idx], + SupervisorStrategy::OneForAll => (0..num_children).collect(), + SupervisorStrategy::RestForOne => (dead_idx..num_children).collect(), + } +} + /// Specification for a supervised child actor. -/// -/// The `start` closure is called with `&Ctx` and should spawn the child actor -/// (typically via `ctx.spawn()`). The supervisor monitors the returned address -/// and applies the restart policy when the child dies. pub struct ChildSpec { /// Unique identifier for this child. pub id: String, @@ -260,13 +282,7 @@ impl ActorInterface for Supervisor { }; self.children[idx] = None; - let should_restart = match self.specs[idx].restart { - RestartPolicy::Permanent => true, - RestartPolicy::Transient => down.reason == StopReason::Panicked, - RestartPolicy::Temporary => false, - }; - - if !should_restart { + if !self.specs[idx].restart.should_restart(down.reason) { return; } @@ -279,6 +295,7 @@ impl ActorInterface for Supervisor { return; } + let restart_indices = compute_restart_set(self.strategy, idx, self.specs.len()); match self.strategy { SupervisorStrategy::OneForOne => { if let Err(e) = self.start_child(ctx, idx) { @@ -288,14 +305,7 @@ impl ActorInterface for Supervisor { ); } } - SupervisorStrategy::OneForAll => { - // Stop all other living children, then restart all in order. - let restart_indices: Vec = (0..self.specs.len()).collect(); - self.begin_coordinated_restart(ctx, restart_indices); - } - SupervisorStrategy::RestForOne => { - // Stop children after the failed one, then restart failed + rest. - let restart_indices: Vec = (idx..self.specs.len()).collect(); + _ => { self.begin_coordinated_restart(ctx, restart_indices); } } diff --git a/src/worker.rs b/src/worker.rs index 55f5612..6ea4295 100644 --- a/src/worker.rs +++ b/src/worker.rs @@ -14,6 +14,30 @@ use crate::Error; use crate::extension::WorkerExtension; + +// Extracted pure functions for use in kani to prove guarantees + +/// Whether an actor should be skipped during `tick_all`. +pub(crate) fn should_skip_actor(poisoned: bool, stopping: bool, suspended: bool) -> bool { + poisoned || stopping || suspended +} + +/// Whether `on_stop` should fire for an actor being cleaned up. +pub(crate) fn is_on_stop_eligible(stopping: bool, poisoned: bool) -> bool { + stopping && !poisoned +} + +/// Determine the `StopReason` for a dead actor based on its flags. +pub(crate) fn determine_stop_reason(poisoned: bool, has_exit_value: bool) -> StopReason { + if poisoned { + StopReason::Panicked + } else if has_exit_value { + StopReason::Completed + } else { + StopReason::Normal + } +} + /// Route a message: try local pool first, then address_map for cross-worker, /// then inbox_registry for external receivers. fn route_to_pool_or_remote( @@ -492,14 +516,11 @@ impl ActorPool { ) -> usize { let mut count = 0; for (&addr, slot) in self.actors.iter_mut() { - if slot.poisoned || slot.stopping { - // Discard all messages for poisoned/stopping actors - slot.mailbox.clear(); - continue; - } - - // Skip suspended actors — messages keep queueing - if slot.suspended { + if should_skip_actor(slot.poisoned, slot.stopping, slot.suspended) { + // Discard all messages for poisoned/stopping actors (not suspended — those queue) + if slot.poisoned || slot.stopping { + slot.mailbox.clear(); + } continue; } @@ -696,19 +717,13 @@ impl ActorPool { let mut dead = Vec::with_capacity(dead_addrs.len()); for addr in dead_addrs { if let Some(mut slot) = self.actors.remove(&addr) { - let reason = if slot.poisoned { - StopReason::Panicked - } else if slot.exit_value.is_some() { - StopReason::Completed - } else { - StopReason::Normal - }; + let reason = determine_stop_reason(slot.poisoned, slot.exit_value.is_some()); // Call on_stop for gracefully stopping actors only debug_assert!( slot.poisoned || slot.stopping, "G4: non-dead actor reached cleanup_dead" ); - if slot.stopping && !slot.poisoned { + if is_on_stop_eligible(slot.stopping, slot.poisoned) { let mut type_counts: Vec<(&'static str, u64)> = slot.msg_type_counts.iter().map(|(&k, &v)| (k, v)).collect(); type_counts.sort_by(|a, b| b.1.cmp(&a.1));