zacheryasc/swactor
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: runtime guarantees and checks

Browse source 
Exhaustive checks of the statespace that enable us to give formal
guarantees about runtime properties.
This commit is contained in:
Zachery Aaron Shores-Chmielewski 2026-03-28 12:07:08 +07:00
parent 05379928d6
commit 672a23ba42
13 changed files with 2348 additions and 812 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

157
src/RUNTIME_GUARANTEES.md
View file

@ -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<dyn AnyActor>` 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<Mutex<ActorSlot>>` — 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<ActorAddress, WorkerId>` — 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 |

222
src/guarantees/RUNTIME_GUARANTEES.md Normal file
View file

@ -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<usize>` | `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<dyn AnyActor>` 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<Mutex<ActorSlot>>` — 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<ActorAddress, WorkerId>` — 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 |

1168
src/guarantees/correspondence.rs
View file

File diff suppressed because it is too large Load diff

57
src/guarantees/g10_supervisor.rs
View file

@ -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 {

18
src/guarantees/g4_lifecycle.rs
View file

@ -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;

20
src/guarantees/mod.rs
View file

@ -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;

221
src/guarantees/model_checker.rs Normal file
View file

@ -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<Self::State>;
/// Enumerate all enabled actions in `state`, pushing them into `actions`.
fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>);
/// 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<Self::State>;
/// Properties to verify across all reachable states.
fn properties(&self) -> Vec<Property<Self>>;
/// 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<M: Model> {
name: String,
kind: PropertyKind,
checker_fn: Box<dyn Fn(&M, &M::State) -> bool>,
}
impl<M: Model> Property<M> {
/// 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<M> {
let properties = self.model.properties();
let mut visited: HashSet<M::State> = HashSet::new();
let mut stack: Vec<(M::State, usize)> = Vec::new(); // (state, depth)
let mut max_depth: usize = 0;
let mut actions_buf: Vec<M::Action> = Vec::new();
// Track property results
let mut always_violated: Vec<Option<String>> = properties
.iter()
.map(|_| None)
.collect();
let mut sometimes_satisfied: Vec<bool> = 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<M: Model> {
result: CheckResult,
_phantom: PhantomData<M>,
}
// Suppress unused type parameter warning
impl<M: Model> DfsHandle<M> {
/// 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<String>,
}
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}");
}
}
}

439
src/guarantees/stateright_death_orphan.rs Normal file
View file

@ -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<Self::State> {
vec![MonitorState::init()]
}
fn actions(&self, s: &Self::State, actions: &mut Vec<Self::Action>) {
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<Self::State> {
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<Property<Self>> {
vec![
Property::<Self>::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::<Self>::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::<Self>::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::<Self>::sometimes("L1: monitor fires", |_, s| {
s.notif.iter().any(|&c| c > 0)
}),
Property::<Self>::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::<Self>::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<Self::State> {
vec![OrphanState::init()]
}
fn actions(&self, s: &Self::State, actions: &mut Vec<Self::Action>) {
// 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<Self::State> {
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<Property<Self>> {
vec![
// G7a: After orphan cleanup, all unsupervised children are dead
Property::<Self>::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::<Self>::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::<Self>::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::<Self>::sometimes("L1: orphan cleanup triggers", |_, s| {
s.orphan_cleaned.iter().any(|&c| c)
}),
Property::<Self>::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::<Self>::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})");
}

354
src/guarantees/stateright_lifecycle.rs Normal file
View file

@ -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<Self::State> {
vec![RuntimeState::init()]
}
fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>) {
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<Self::State> {
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<Property<Self>> {
vec![
// ── G4 Safety Properties ──────────────────────────────────────
// G4a: on_start fires at most once per actor
Property::<Self>::always("G4a: on_start_count <= 1", |_, state| {
state.actors.iter().all(|a| a.on_start_count <= 1)
}),
// G4a: no handle before on_start
Property::<Self>::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::<Self>::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::<Self>::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::<Self>::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::<Self>::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::<Self>::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::<Self>::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::<Self>::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::<Self>::sometimes("L1: handle reachable", |_, state| {
state.actors.iter().any(|a| a.handle_count > 0)
}),
// L2: on_stop_count == 1 is reachable
Property::<Self>::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::<Self>::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::<Self>::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",
);
}

403
src/guarantees/stateright_supervisor.rs Normal file
View file

@ -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<LastEvent>,
}
// ── 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<SupervisorState> {
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::State> {
Self::all_init_states()
}
fn actions(&self, s: &Self::State, actions: &mut Vec<Self::Action>) {
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<Self::State> {
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<Property<Self>> {
vec![
// ── G8a: OneForOne restarts only the dead child ─────────────
Property::<Self>::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::<Self>::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::<Self>::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::<Self>::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::<Self>::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::<Self>::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::<Self>::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::<Self>::sometimes(
"L1: a restart occurs",
|_, s| s.children.iter().any(|c| c.restart_count > 0),
),
Property::<Self>::sometimes(
"L2: meltdown is reachable",
|_, s| s.melted_down,
),
Property::<Self>::sometimes(
"L3: OneForOne exercised with restart",
|_, s| {
s.strategy == SupervisorStrategy::OneForOne
&& s.children.iter().any(|c| c.restart_count > 0)
},
),
Property::<Self>::sometimes(
"L4: OneForAll exercised with restart",
|_, s| {
s.strategy == SupervisorStrategy::OneForAll
&& s.children.iter().any(|c| c.restart_count > 0)
},
),
Property::<Self>::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",
);
}

2
src/std/mod.rs
View file

@ -1,4 +1,4 @@
mod supervisor;
pub(crate) mod supervisor;
mod router;
pub mod name_registry;
pub mod monitor_registry;

52
src/std/supervisor.rs
View file

@ -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<usize> {
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<usize> = (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<usize> = (idx..self.specs.len()).collect();
_ => {
self.begin_coordinated_restart(ctx, restart_indices);
}
}

47
src/worker.rs
View file

@ -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));