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

stash core pruning and test consolidation

Browse source
This commit is contained in:
Zachery Aaron Shores-Chmielewski 2026-06-24 15:04:39 +04:00
parent 0775901dfe
commit 9e3d581bf6
34 changed files with 865 additions and 9290 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
Cargo.lock generated
View file

@ -5001,6 +5001,7 @@ dependencies = [
"crossbeam-utils",
"getrandom 0.2.17",
"mvp-system",
"parking_lot",
"proptest",
"proptest-state-machine",
"serde",

1
Cargo.toml
View file

@ -46,6 +46,7 @@ tracing = { version = "0.1", optional = true }
web-time = { version = "0.2", optional = true }
crossbeam-queue = "0.3.12"
crossbeam-utils = "0.8.21"
parking_lot = "0.12"
[lints.rust]
unexpected_cfgs = { level = "allow", check-cfg = ['cfg(kani)'] }

280
crates/mvp-system/tests/gpu_worker_node_e2e.rs
View file

@ -27,6 +27,8 @@ const INGRESS_BASE: usize = 0;
const EGRESS_BASE: usize = 4096;
const RING_BYTES: usize = 1024;
const HEADER_LEN: usize = 48;
const PREFLIGHT_TIMEOUT: Duration = Duration::from_secs(45);
const EVENT_TIMEOUT: Duration = Duration::from_secs(60);
#[test]
fn gpu_worker_node_e2e_cuda() {
@ -53,33 +55,28 @@ fn build_and_run_docker_fixture() {
copy_workspace_context(&workspace, &context);
let dockerfile = context.join("crates/mvp-system/tests/gpu_worker_node_e2e/Dockerfile");
phase("building CUDA Docker fixture image");
let build = Command::new("docker")
.args(["build", "-f"])
.arg(&dockerfile)
.args(["-t", IMAGE])
.arg(&context)
.output()
.status()
.expect("run docker build");
assert!(
build.status.success(),
"docker build failed\nstdout:\n{}\nstderr:\n{}",
String::from_utf8_lossy(&build.stdout),
String::from_utf8_lossy(&build.stderr)
);
assert!(build.success(), "docker build failed with status {build}");
phase("running CUDA Docker fixture");
let run = Command::new("docker")
.args(["run", "--rm", "--gpus"])
.arg(std::env::var("MVP_CUDA_GPUS").unwrap_or_else(|_| "all".to_owned()))
.args(["-e", "MVP_SYSTEM_CUDA_E2E_IN_CONTAINER=1"])
.args(["-e", "CARGO_TARGET_DIR=/tmp/mvp-system-target"])
.arg(IMAGE)
.output()
.status()
.expect("run docker CUDA fixture");
assert!(
run.status.success(),
"docker CUDA fixture failed\nstdout:\n{}\nstderr:\n{}",
String::from_utf8_lossy(&run.stdout),
String::from_utf8_lossy(&run.stderr)
run.success(),
"docker CUDA fixture failed with status {run}"
);
}
@ -120,7 +117,80 @@ fn copy_context_entry(source: &Path, dest: &Path) {
}
}
fn phase(message: &str) {
eprintln!("gpu-worker-node-e2e: {message}");
}
fn run_cuda_preflight() {
let script = r#"
import os
print("cuda preflight: importing tinygrad", flush=True)
from tinygrad import Tensor, dtypes
print(f"cuda preflight: DEV={os.environ.get('DEV')}", flush=True)
print("cuda preflight: realizing Tensor([1])", flush=True)
value = Tensor([1], dtype=dtypes.int32).realize().numpy().tolist()
print(f"cuda preflight: ok {value}", flush=True)
"#;
let child = Command::new("python3")
.arg("-c")
.arg(script)
.env("DEV", "CUDA")
.stdout(Stdio::piped())
.stderr(Stdio::piped())
.spawn()
.expect("spawn CUDA preflight");
let pid = child.id();
let (tx, rx) = mpsc::channel();
thread::spawn(move || {
let _ = tx.send(child.wait_with_output());
});
match rx.recv_timeout(PREFLIGHT_TIMEOUT) {
Ok(output) => {
let output = output.expect("wait CUDA preflight");
eprintln!(
"gpu-worker-node-e2e: CUDA preflight stdout:\n{}",
String::from_utf8_lossy(&output.stdout)
);
assert!(
output.status.success(),
"CUDA preflight failed with status {}\nstdout:\n{}\nstderr:\n{}",
output.status,
String::from_utf8_lossy(&output.stdout),
String::from_utf8_lossy(&output.stderr)
);
}
Err(mpsc::RecvTimeoutError::Timeout) => {
unsafe {
libc::kill(pid as libc::pid_t, libc::SIGKILL);
}
let output = rx
.recv_timeout(Duration::from_secs(5))
.ok()
.and_then(Result::ok);
let (stdout, stderr) = output
.as_ref()
.map(|output| {
(
String::from_utf8_lossy(&output.stdout).into_owned(),
String::from_utf8_lossy(&output.stderr).into_owned(),
)
})
.unwrap_or_else(|| ("<unavailable>".to_owned(), "<unavailable>".to_owned()));
panic!(
"CUDA preflight timed out after {:?}; killed pid {pid}\nstdout:\n{stdout}\nstderr:\n{stderr}",
PREFLIGHT_TIMEOUT
);
}
Err(mpsc::RecvTimeoutError::Disconnected) => panic!("CUDA preflight waiter disconnected"),
}
}
fn run_integrated_node_harness() {
phase("running CUDA tinygrad preflight");
run_cuda_preflight();
phase("creating shared arena and telemetry socket");
let arena_fd = create_arena(ARENA_BYTES);
let worker_path = Path::new(env!("CARGO_MANIFEST_DIR"))
.join("tests/gpu_worker_node_e2e/mvp_tinygrad_worker.py");
@ -144,12 +214,14 @@ fn run_integrated_node_harness() {
Arc::clone(&ingest_alive),
);
phase("spawning Rust worker node actor");
let rt = Runtime::new(RuntimeConfig::default());
let reports = rt.new_inbox::<HarnessReport>().expect("report inbox");
let node = rt
.spawn(GpuWorkerNodeActor::new(rt.create_sender(), *reports.addr()))
.expect("spawn gpu worker node actor");
phase("spawning tinygrad worker process");
rt.send_to(
node,
NodeMsg::Start(StartWorker {
@ -160,17 +232,33 @@ fn run_integrated_node_harness() {
}),
)
.expect("send start");
wait_for_report(&rt, &mut emitter, &frame_rx, &reports, |report| {
matches!(report, HarnessReport::ProcessStarted)
});
wait_for_report(
&rt,
node,
&mut emitter,
&frame_rx,
&reports,
"worker process start",
|report| matches!(report, HarnessReport::ProcessStarted),
);
phase("initializing CUDA backend");
send_command(
&rt,
node,
json!({"type":"InitializeWorker","helper_abi_version":1}),
);
wait_for_control(&rt, &mut emitter, &frame_rx, &reports, "WorkerReady");
wait_for_control(
&rt,
node,
&mut emitter,
&frame_rx,
&reports,
"WorkerReady",
"worker ready",
);
phase("installing ingress and egress rings");
send_command(
&rt,
node,
@ -187,12 +275,38 @@ fn run_integrated_node_harness() {
node,
install_ring_command(EGRESS_RING_ID, EGRESS_EDGE_ID, "out", "egress", EGRESS_BASE),
);
wait_for_control(&rt, &mut emitter, &frame_rx, &reports, "RingInstalled");
wait_for_control(&rt, &mut emitter, &frame_rx, &reports, "RingInstalled");
wait_for_control(
&rt,
node,
&mut emitter,
&frame_rx,
&reports,
"RingInstalled",
"ingress ring installed",
);
wait_for_control(
&rt,
node,
&mut emitter,
&frame_rx,
&reports,
"RingInstalled",
"egress ring installed",
);
phase("configuring worker role");
send_command(&rt, node, json!({"type":"ConfigureRole","role_id":1}));
wait_for_control(&rt, &mut emitter, &frame_rx, &reports, "RoleLoaded");
wait_for_control(
&rt,
node,
&mut emitter,
&frame_rx,
&reports,
"RoleLoaded",
"role loaded",
);
phase("copying ingress object into CUDA tensor");
let input_record = object_record(9000, 0, &[1, 2, 3, 4]);
pwrite_all(arena_fd, INGRESS_BASE, &input_record);
send_command(
@ -200,9 +314,18 @@ fn run_integrated_node_harness() {
node,
json!({"type":"RingReadable","ring_id":INGRESS_RING_ID,"committed_bytes":input_record.len()}),
);
let loaded = wait_for_control(&rt, &mut emitter, &frame_rx, &reports, "ObjectLoaded");
let loaded = wait_for_control(
&rt,
node,
&mut emitter,
&frame_rx,
&reports,
"ObjectLoaded",
"object loaded",
);
let handle = loaded["handle"]["id"].as_u64().expect("device handle id");
phase("executing CUDA step and writing egress object");
send_command(
&rt,
node,
@ -214,8 +337,24 @@ fn run_integrated_node_harness() {
"output_object_id":9001
}),
);
let produced = wait_for_control(&rt, &mut emitter, &frame_rx, &reports, "ObjectProduced");
wait_for_control(&rt, &mut emitter, &frame_rx, &reports, "StepCompleted");
let produced = wait_for_control(
&rt,
node,
&mut emitter,
&frame_rx,
&reports,
"ObjectProduced",
"object produced",
);
wait_for_control(
&rt,
node,
&mut emitter,
&frame_rx,
&reports,
"StepCompleted",
"step completed",
);
let committed = produced["committed_bytes"]
.as_u64()
.expect("committed bytes") as usize;
@ -223,6 +362,7 @@ fn run_integrated_node_harness() {
pread_exact(arena_fd, EGRESS_BASE, &mut egress);
assert_eq!(decode_payload_words(&egress), vec![2, 4, 6, 8]);
phase("releasing device object");
send_command(
&rt,
node,
@ -230,19 +370,40 @@ fn run_integrated_node_harness() {
);
wait_for_control(
&rt,
node,
&mut emitter,
&frame_rx,
&reports,
"DeviceObjectReleased",
"device object released",
);
phase("shutting down worker process");
send_command(&rt, node, json!({"type":"ShutdownWorker"}));
wait_for_control(&rt, &mut emitter, &frame_rx, &reports, "WorkerStopped");
wait_for_report(&rt, &mut emitter, &frame_rx, &reports, |report| {
matches!(report, HarnessReport::ProcessExited(0))
});
wait_for_control(
&rt,
node,
&mut emitter,
&frame_rx,
&reports,
"WorkerStopped",
"worker stopped",
);
wait_for_report(
&rt,
node,
&mut emitter,
&frame_rx,
&reports,
"worker process exit",
|report| matches!(report, HarnessReport::ProcessExited(0)),
);
phase("asserting worker telemetry");
let telemetry = collect_telemetry(&mut emitter, &frame_rx, Duration::from_secs(1));
assert_has_worker_event(&telemetry, "importing_tinygrad");
assert_has_worker_event(&telemetry, "tinygrad_imported");
assert_has_worker_event(&telemetry, "realizing_cuda_probe");
assert_has_worker_event(&telemetry, "backend_initialized");
assert_has_worker_event(&telemetry, "worker_ready");
assert_has_worker_event(&telemetry, "ring_installed");
@ -292,6 +453,7 @@ enum NodeMsg {
ControlLine(String),
StderrLine(String),
ProcessExited(i32),
KillWorker(String),
}
#[derive(Clone, Debug)]
@ -306,6 +468,7 @@ struct GpuWorkerNodeActor {
sender: ExternalSender,
report_to: ActorAddress,
stdin: Option<std::process::ChildStdin>,
child_pid: Option<u32>,
}
impl GpuWorkerNodeActor {
@ -314,6 +477,7 @@ impl GpuWorkerNodeActor {
sender,
report_to,
stdin: None,
child_pid: None,
}
}
}
@ -340,9 +504,13 @@ impl ActorInterface for GpuWorkerNodeActor {
.expect("send stderr report");
}
NodeMsg::ProcessExited(code) => {
self.child_pid = None;
ctx.send(self.report_to, HarnessReport::ProcessExited(code))
.expect("send exit report");
}
NodeMsg::KillWorker(reason) => {
self.kill_worker(&reason);
}
}
}
}
@ -368,6 +536,7 @@ impl GpuWorkerNodeActor {
let stdout = child.stdout.take().expect("worker stdout");
let stderr = child.stderr.take().expect("worker stderr");
self.stdin = Some(child.stdin.take().expect("worker stdin"));
self.child_pid = Some(child.id());
let target = ctx.self_addr();
let sender = self.sender.clone();
@ -390,6 +559,7 @@ impl GpuWorkerNodeActor {
for line in BufReader::new(stderr).lines() {
match line {
Ok(line) => {
eprintln!("gpu-worker-node-e2e worker stderr: {line}");
if sender.send_to(target, NodeMsg::StderrLine(line)).is_err() {
break;
}
@ -413,6 +583,15 @@ impl GpuWorkerNodeActor {
ctx.send(self.report_to, HarnessReport::ProcessStarted)
.expect("send started report");
}
fn kill_worker(&mut self, reason: &str) {
if let Some(pid) = self.child_pid.take() {
eprintln!("gpu-worker-node-e2e: killing worker pid {pid}: {reason}");
unsafe {
libc::kill(pid as libc::pid_t, libc::SIGKILL);
}
}
}
}
fn spawn_worker_event_ingest(
@ -420,8 +599,10 @@ fn spawn_worker_event_ingest(
sink: datastream::emit::DatastreamEventSink,
alive: Arc<AtomicBool>,
) -> thread::JoinHandle<()> {
thread::spawn(move || {
let (ready_tx, ready_rx) = mpsc::channel();
let handle = thread::spawn(move || {
let socket = std::os::unix::net::UnixDatagram::bind(&socket_path).expect("bind UDS ingest");
ready_tx.send(()).expect("signal UDS ingest ready");
socket
.set_read_timeout(Some(Duration::from_millis(50)))
.expect("set UDS timeout");
@ -437,7 +618,11 @@ fn spawn_worker_event_ingest(
Err(_) => break,
}
}
})
});
ready_rx
.recv_timeout(Duration::from_secs(5))
.expect("UDS ingest socket ready");
handle
}
fn send_command(rt: &Runtime, node: ActorAddress, command: Value) {
@ -447,16 +632,20 @@ fn send_command(rt: &Runtime, node: ActorAddress, command: Value) {
fn wait_for_control(
rt: &Runtime,
node: ActorAddress,
emitter: &mut DatastreamEmitter,
frame_rx: &mpsc::Receiver<Frame>,
reports: &swactor::runtime::Inbox<HarnessReport>,
kind: &str,
phase_name: &str,
) -> Value {
match wait_for_report(
rt,
node,
emitter,
frame_rx,
reports,
phase_name,
|report| matches!(report, HarnessReport::ControlEvent(value) if value["type"] == kind),
) {
HarnessReport::ControlEvent(value) => value,
@ -466,26 +655,55 @@ fn wait_for_control(
fn wait_for_report(
rt: &Runtime,
node: ActorAddress,
emitter: &mut DatastreamEmitter,
_frame_rx: &mpsc::Receiver<Frame>,
reports: &swactor::runtime::Inbox<HarnessReport>,
phase_name: &str,
mut predicate: impl FnMut(&HarnessReport) -> bool,
) -> HarnessReport {
let started = Instant::now();
let mut stderr_lines = Vec::new();
while started.elapsed() < Duration::from_secs(60) {
while started.elapsed() < EVENT_TIMEOUT {
rt.tick();
emitter.tick();
while let Some(report) = reports.try_recv() {
if predicate(&report) {
return report;
}
match &report {
HarnessReport::StderrLine(line) => stderr_lines.push(line.clone()),
_ if predicate(&report) => return report,
HarnessReport::ControlEvent(value) if value["type"] == "WorkerFatal" => {
rt.send_to(
node,
NodeMsg::KillWorker(format!("fatal while waiting for {phase_name}")),
)
.expect("send kill after fatal");
rt.tick();
panic!(
"worker fatal while waiting for {phase_name}: {value}\nstderr={stderr_lines:?}"
);
}
HarnessReport::ProcessExited(code) if *code != 0 => {
panic!(
"worker exited with {code} while waiting for {phase_name}; stderr={stderr_lines:?}"
);
}
_ => {}
}
}
thread::sleep(Duration::from_millis(5));
}
panic!("timed out waiting for report; stderr={stderr_lines:?}");
rt.send_to(
node,
NodeMsg::KillWorker(format!("timeout while waiting for {phase_name}")),
)
.expect("send kill on timeout");
rt.tick();
panic!(
"timed out after {:?} waiting for {phase_name}; stderr={stderr_lines:?}",
EVENT_TIMEOUT
);
}
fn collect_telemetry(

8
crates/mvp-system/tests/gpu_worker_node_e2e/Dockerfile
View file

@ -7,8 +7,10 @@ RUN apt-get update && \
build-essential \
pkg-config \
python3 \
python3-pip && \
python3 -m pip install --no-cache-dir --break-system-packages tinygrad numpy && \
python3-pip \
cuda-cudart-dev-12-6 \
cuda-nvrtc-12-6 && \
python3 -m pip install --no-cache-dir --break-system-packages tinygrad==0.12.0 numpy && \
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal && \
apt-get clean && \
rm -rf /var/lib/apt/lists/*
@ -18,4 +20,4 @@ ENV DEV=CUDA
ENV PYTHONDONTWRITEBYTECODE=1
COPY . /workspace
WORKDIR /workspace
CMD ["cargo", "test", "-p", "mvp-system", "--features", "local-e2e", "--test", "gpu_worker_node_e2e", "--", "--nocapture"]
CMD ["sh", "-lc", "python3 -c 'import os; print(\"cuda preflight: importing tinygrad\", flush=True); from tinygrad import Tensor,dtypes; print(\"cuda preflight: DEV=\" + str(os.environ.get(\"DEV\")), flush=True); print(\"cuda preflight: realizing Tensor([1])\", flush=True); print(Tensor([1], dtype=dtypes.int32).realize().numpy().tolist(), flush=True)' && cargo test -p mvp-system --features local-e2e --test gpu_worker_node_e2e -- --nocapture"]

34
crates/mvp-system/tests/gpu_worker_node_e2e/mvp_tinygrad_worker.py
View file

@ -10,7 +10,6 @@ import sys
import time
from typing import Any
from tinygrad import Tensor, dtypes
HEADER_LEN = 48
GENERATION = 1
@ -21,6 +20,9 @@ telemetry_path = os.environ["SWACTOR_WORKER_EVENT_SOCK"]
rings: dict[int, dict[str, Any]] = {}
objects: dict[int, dict[str, Any]] = {}
role_configured = False
Tensor: Any = None
dtypes: Any = None
next_handle = 42
@ -28,6 +30,10 @@ def control(**event: Any) -> None:
print(json.dumps(event, separators=(",", ":")), flush=True)
def log(message: str) -> None:
print(f"mvp_tinygrad_worker: {message}", file=sys.stderr, flush=True)
def observe(kind: str, **fields: Any) -> None:
global telemetry
if telemetry is None:
@ -57,15 +63,34 @@ def require_arena() -> mmap.mmap:
return arena
def require_tinygrad() -> tuple[Any, Any]:
if Tensor is None or dtypes is None:
fatal("BackendNotInitialized")
return Tensor, dtypes
def initialize(cmd: dict[str, Any]) -> None:
global arena
global arena, Tensor, dtypes
if int(cmd["helper_abi_version"]) != 1:
fatal("UnsupportedHelperAbi", helper_abi_version=cmd["helper_abi_version"])
fd = int(os.environ["SWACTOR_ARENA_FD"])
size = int(os.environ["SWACTOR_ARENA_BYTES"])
arena = mmap.mmap(fd, size)
Tensor([1], dtype=dtypes.int32).realize()
observe("backend_initialized")
log("importing tinygrad")
observe("importing_tinygrad")
import_start = time.monotonic()
from tinygrad import Tensor as TinyTensor, dtypes as tiny_dtypes
Tensor = TinyTensor
dtypes = tiny_dtypes
observe("tinygrad_imported", elapsed_ms=int((time.monotonic() - import_start) * 1000))
log(f"realizing CUDA probe with DEV={os.environ.get('DEV')}")
observe("realizing_cuda_probe", dev=os.environ.get("DEV"))
probe_start = time.monotonic()
Tensor([1], dtype=dtypes.int32).realize().numpy().tolist()
observe("backend_initialized", elapsed_ms=int((time.monotonic() - probe_start) * 1000))
observe("worker_ready")
control(type="WorkerReady", generation=GENERATION)
@ -118,6 +143,7 @@ def parse_record(base: int, committed_bytes: int, ring: dict[str, Any]) -> tuple
def ring_readable(cmd: dict[str, Any]) -> None:
global next_handle
Tensor, dtypes = require_tinygrad()
ring_id = int(cmd["ring_id"])
ring = rings[ring_id]
if ring["direction"] != "ingress":

21
src/actor.rs
View file

@ -210,8 +210,8 @@ impl Environment {
/// Check if the environment contains a value with the given `TypeId`.
///
/// Type-erased version of [`contains`](Self::contains) — used by
/// `ServiceRegistry::inject_into` to skip keys already present.
/// Type-erased version of [`contains`](Self::contains) for extension code
/// that merges pre-built values without knowing their concrete types.
pub fn contains_type_id(&self, type_id: TypeId) -> bool {
self.inner.contains_key(&type_id)
}
@ -255,8 +255,8 @@ impl EnvironmentBuilder {
/// Insert a type-erased value by `TypeId`.
///
/// Used by `ServiceRegistry::inject_into` to merge pre-built bindings
/// without knowing concrete types at compile time.
/// Used by extension code to merge pre-built values without knowing concrete
/// types at compile time.
pub fn set_raw(&mut self, type_id: TypeId, value: Arc<dyn Any + Send + Sync>) -> &mut Self {
self.map.insert(type_id, value);
self
@ -279,13 +279,14 @@ impl Default for EnvironmentBuilder {
// ─── Well-Known Environment Keys ─────────────────────────────────────────────
/// Milliseconds since runtime creation when this actor was spawned.
/// Injected by StdExtension (opt-in at runtime level). Read via `ctx.env::<SpawnTimestamp>()`.
/// Uses the same time base as `SystemInfo::uptime_ms`.
///
/// Reserved environment key for custom extensions that want a spawn timestamp.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct SpawnTimestamp(pub u64);
/// Logical name assigned via `spawn_named()`. Read via `ctx.env::<LogicalName>()`.
/// None for unnamed actors.
/// Logical name assigned to an actor.
///
/// Reserved environment key for custom naming extensions.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct LogicalName(pub String);
@ -297,8 +298,8 @@ impl LogicalName {
/// A typed service binding stored in the environment.
///
/// `S` is a zero-sized marker type that identifies the service (e.g., `struct Datastore;`).
/// Stored via `ServiceRegistry` and read via `ctx.resource::<S>()`.
/// Reserved environment value for custom resource/service extensions. `S` is a
/// zero-sized marker type that identifies the service (e.g., `struct Datastore;`).
#[derive(Clone, Debug)]
pub struct ServiceBinding<S: 'static + Send + Sync> {
pub addr: ActorAddress,

4
src/extension.rs
View file

@ -20,11 +20,11 @@ pub trait RuntimeExtension: Send + Sync {
dead: &[(ActorAddress, StopReason, Option<ExitValue>)],
) -> Vec<(ActorAddress, Box<dyn Any + Send>)>;
/// Clean up extension state for dead actors (names, groups, monitors).
/// Clean up extension state for dead actors.
fn cleanup_dead(&self, dead: &[ActorAddress]);
/// Called for each newly spawned actor, before it enters the pool.
/// Extensions can enrich the actor's environment (e.g., inject SpawnTimestamp).
/// Extensions can enrich the actor's environment.
/// `child` is the address of the newly spawned actor.
/// `parent` is the address of the spawning actor, or `None` for runtime-spawned actors.
/// `uptime_ms` is milliseconds since runtime creation.

262
src/guarantees/RUNTIME_GUARANTEES.md
View file

@ -1,222 +1,90 @@
# 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)
This document describes the beta core-runtime guarantees that remain after the
alpha-only `std` features were pruned. Tests now separate core correctness from
optional library patterns.
## Abstract
## Verification layers
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.
1. Unit/integration tests exercise observable runtime behavior.
2. Kani/model-check modules cover core finite-state lifecycle decisions where
enabled.
3. Exhaustive correspondence tests enumerate production decision-function truth
tables and compare them with runtime behavior.
4. `tests/core_extension_seams.rs` verifies the generic extension seam without
depending on unused std features.
A guarantee listed here is a **promise**. Code that violates a guarantee is a bug in the runtime, not in the user's actor.
## Core decision functions
---
| Function | Defined in | Runtime use |
| --- | --- | --- |
| `should_skip_actor(poisoned, stopping, suspended) -> bool` | `worker.rs` | `tick_all` skips actors that must not process mailbox messages. |
| `is_on_stop_eligible(stopping, poisoned) -> bool` | `worker.rs` | Cleanup decides whether `on_stop` should run. |
| `determine_stop_reason(poisoned, has_exit_value) -> StopReason` | `worker.rs` | Cleanup reports normal, panic, or completed exits. |
## Enforcement Strategy
## Retained core guarantees
Four layers, ordered by strength:
### G4: Lifecycle ordering
1. **Compiler (type system)** — Make violations unrepresentable. `Send + 'static` bounds, ownership, lack of `&mut` aliasing. Zero runtime cost, impossible to bypass without `unsafe`.
Actors process messages only while eligible. Stopping actors do not handle later
mailbox messages, poisoned actors do not run `on_stop`, and graceful stops run
`on_stop` exactly once.
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.
Evidence:
- `src/guarantees/correspondence.rs`
- `src/guarantees/g4_lifecycle.rs` when Kani is enabled
- `src/guarantees/stateright_lifecycle.rs`
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.
### G5: Fault isolation
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 panicking actor is removed/poisoned without preventing unrelated actors from
continuing to process messages.
A guarantee is **fully contracted** when all applicable layers enforce it.
Evidence:
- `src/guarantees/g5_fault_isolation.rs`
- `tests/actor_lifecycle.rs`
---
### Core extension seam correctness
## Verification Architecture
The core runtime correctly invokes extension hooks independent of any specific
std feature:
### Production Decision Functions
- `RuntimeExtension::on_spawn` can mutate the spawned actor environment.
- `RuntimeExtension::on_actor_death` can return messages, and core routes them
normally.
- `RuntimeExtension::cleanup_dead` receives dead actor batches.
- `RuntimeExtension::create_worker_extension` installs a per-worker extension.
- `WorkerExtension::handle_request`, `on_tick`, `gc_dead`, and
`has_pending_work` participate in worker progress and message routing.
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:
Evidence:
- `tests/core_extension_seams.rs`
| 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` |
## Retained std beta guarantees
Kani proofs and Stateright models call these production functions directly — not test-only mirrors.
Only std code used by production crates remains in the beta surface:
### Model Bounds
- runtime naming registration, lookup, unregister, listing, and dead-actor cleanup
- runtime groups join, leave, publish, membership listing, and dead-actor cleanup
- actor-side `ctx.watch(target)` death notifications via `ActorExited`
- actor-side `ctx.join_group(group)` membership
| 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 |
Evidence:
- `tests/std_extension.rs`
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.
## Removed alpha-only guarantees
---
The following were tied to unused `std` features and are no longer part of the
beta guarantee set:
## Guarantee Catalog
- monitor/`Down` delivery and demonitor cancellation
- tick timers and interval timers
- supervisor restart policies and strategies
- router distribution/replacement/meltdown behavior
- service/resource injection and typed resource handles
- std wrapper traits for lifecycle, lineage, capabilities, system info,
self-stats, and environment access
- supervised-orphan distinction
### 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 |
If one of these features becomes production-used again, reintroduce it with a
focused beta API and fresh correctness tests for that feature.

633
src/guarantees/correspondence.rs
View file

@ -1,58 +1,20 @@
//! Exhaustive correspondence tests: verify that Kani bounded mirrors agree
//! with the real runtime across the *entire* finite input space.
//! Exhaustive correspondence tests for core runtime lifecycle decisions.
//!
//! These are the drift detectors. If someone changes `tick_all`'s skip logic
//! or `Supervisor::handle_down`'s restart decision without updating the Kani
//! mirrors, these tests fail.
//!
//! How they work:
//! - 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
//! - No random sampling — every combination is hit
use std::sync::Arc;
//! These tests enumerate finite input spaces for production decision functions and
//! compare them to observable runtime behavior. Pruned alpha std features are not
//! part of the beta guarantee set.
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 ────────────────────────────────────────────────────────────────
fn std_runtime() -> Runtime {
Runtime::new(RuntimeConfig::default()).with_extension(Arc::new(StdExtension::new()))
}
fn tick_many(rt: &Runtime, n: usize) {
for _ in 0..n {
rt.tick();
}
}
const ALL_POLICIES: [RestartPolicy; 3] = [
RestartPolicy::Permanent,
RestartPolicy::Transient,
RestartPolicy::Temporary,
];
const ALL_REASONS: [StopReason; 3] = [
StopReason::Normal,
StopReason::Panicked,
StopReason::Completed,
];
const ALL_STRATEGIES: [SupervisorStrategy; 3] = [
SupervisorStrategy::OneForOne,
SupervisorStrategy::OneForAll,
SupervisorStrategy::RestForOne,
];
// ─── Real runtime actors ────────────────────────────────────────────────────
#[derive(Clone, Debug)]
struct Ping;
@ -62,10 +24,6 @@ struct HandleCalled(#[allow(dead_code)] ActorAddress);
#[derive(Clone, Debug)]
struct OnStopCalled(#[allow(dead_code)] 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,
@ -84,7 +42,6 @@ impl ActorInterface for DualReporter {
}
}
/// Actor that panics in on_start.
struct OnStartPanicker {
handle_to: ActorAddress,
stop_to: ActorAddress,
@ -107,7 +64,6 @@ impl ActorInterface for OnStartPanicker {
}
}
/// Actor that panics on first handle call.
struct HandlePanicker {
stop_to: ActorAddress,
}
@ -125,48 +81,8 @@ impl ActorInterface for HandlePanicker {
}
}
/// Actor that panics on receiving Ping — used to trigger Panicked death.
struct PanicOnPing;
impl ActorInterface for PanicOnPing {
type Incoming = Ping;
type Response = ();
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {
panic!("intentional child panic");
}
}
/// 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 {
type Incoming = Ping;
type Response = ();
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
}
// ═══════════════════════════════════════════════════════════════════════════
// G4 Exhaustive Correspondence: lifecycle decisions vs real runtime
// ═══════════════════════════════════════════════════════════════════════════
/// 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 {
@ -177,35 +93,24 @@ fn g4_healthy_actor_handle_called() {
let addr = rt
.spawn(DualReporter {
handle_to: report_addr,
stop_to: report_addr, // unused for this test path
stop_to: report_addr,
})
.unwrap();
rt.tick(); // on_start
rt.tick();
// 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"
);
assert!(!should_skip_actor(false, false, false));
for _ in 0..msg_count {
rt.send_to(addr, Ping).unwrap();
}
tick_many(&rt, msg_count + 5);
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
);
let handle_count = std::iter::from_fn(|| h_inbox.try_recv()).count();
assert_eq!(handle_count, msg_count);
}
}
/// 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.
/// Exhaustive G4: a poisoned actor must not have handle or on_stop called.
#[test]
fn g4_poisoned_actor_no_handle_no_on_stop() {
for msg_count in 1..=5 {
@ -213,15 +118,8 @@ fn g4_poisoned_actor_no_handle_no_on_stop() {
let h_inbox = rt.new_inbox::<HandleCalled>().unwrap();
let s_inbox = rt.new_inbox::<OnStopCalled>().unwrap();
// 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)"
);
assert!(should_skip_actor(true, false, false));
assert!(!is_on_stop_eligible(false, true));
let addr = rt
.spawn(OnStartPanicker {
@ -229,45 +127,24 @@ fn g4_poisoned_actor_no_handle_no_on_stop() {
stop_to: *s_inbox.addr(),
})
.unwrap();
rt.tick(); // on_start panics → poisoned
rt.tick();
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
);
assert_eq!(std::iter::from_fn(|| h_inbox.try_recv()).count(), 0);
assert_eq!(std::iter::from_fn(|| s_inbox.try_recv()).count(), 0);
}
}
/// 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.
/// Exhaustive G4: a stopping actor skips later messages and calls on_stop once.
#[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)"
);
assert!(should_skip_actor(false, true, false));
assert!(is_on_stop_eligible(true, false));
let rt = Runtime::new(RuntimeConfig::default());
let h_inbox = rt.new_inbox::<HandleCalled>().unwrap();
@ -279,7 +156,7 @@ fn g4_stopping_actor_no_handle_yes_on_stop() {
stop_to: *s_inbox.addr(),
})
.unwrap();
rt.tick(); // on_start
rt.tick();
rt.stop_actor(addr).unwrap();
for _ in 0..msg_count {
@ -287,25 +164,12 @@ fn g4_stopping_actor_no_handle_yes_on_stop() {
}
tick_many(&rt, 5);
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
);
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
);
assert_eq!(std::iter::from_fn(|| h_inbox.try_recv()).count(), 0);
assert_eq!(std::iter::from_fn(|| s_inbox.try_recv()).count(), 1);
}
}
/// 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());
@ -316,85 +180,46 @@ fn g4_handle_panic_poisons_no_on_stop() {
stop_to: *s_inbox.addr(),
})
.unwrap();
rt.tick(); // on_start
rt.tick();
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");
assert!(!is_on_stop_eligible(false, true));
assert_eq!(std::iter::from_fn(|| s_inbox.try_recv()).count(), 0);
}
/// 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
/// Exhaustively enumerate core lifecycle decision function truth tables.
#[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)
let mut skip_combinations = 0;
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,
should_skip_actor(poisoned, stopping, suspended),
poisoned || stopping || suspended
);
combinations_tested += 1;
skip_combinations += 1;
}
}
}
assert_eq!(
combinations_tested, 8,
"must test all 8 flag combinations for should_skip_actor"
);
assert_eq!(skip_combinations, 8);
// is_on_stop_eligible: exhaustive over (stopping, poisoned)
let mut on_stop_combinations = 0u32;
let mut on_stop_combinations = 0;
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
);
assert_eq!(is_on_stop_eligible(stopping, poisoned), stopping && !poisoned);
on_stop_combinations += 1;
}
}
assert_eq!(
on_stop_combinations, 4,
"must test all 4 flag combinations for is_on_stop_eligible"
);
assert_eq!(on_stop_combinations, 4);
// determine_stop_reason: exhaustive over (poisoned, has_exit_value)
let mut reason_combinations = 0u32;
let mut reason_combinations = 0;
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 {
@ -402,397 +227,9 @@ fn g4_exhaustive_decision_function_truth_table() {
} else {
StopReason::Normal
};
assert_eq!(
reason, expected,
"determine_stop_reason({}, {}) = {:?} but expected {:?}",
poisoned, has_exit_value, reason, expected
);
assert_eq!(determine_stop_reason(poisoned, has_exit_value), expected);
reason_combinations += 1;
}
}
assert_eq!(
reason_combinations, 4,
"must test all 4 flag combinations for determine_stop_reason"
);
}
// ═══════════════════════════════════════════════════════════════════════════
// G10 Exhaustive Correspondence: restart decisions vs real supervisor
// ═══════════════════════════════════════════════════════════════════════════
/// 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 &policy in &ALL_POLICIES {
for &reason in &ALL_REASONS {
let rt = std_runtime();
let child_inbox = rt.new_inbox::<ChildStarted>().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| {
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(SupervisorStrategy::OneForOne, 10, vec![spec]);
let _sup_addr = rt.spawn(sup).unwrap();
tick_many(&rt, 3);
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");
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_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;
}
}
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::<ChildStarted>().unwrap();
let report_addr = *report_inbox.addr();
let spawn_counts: Vec<Arc<std::sync::atomic::AtomicUsize>> = (0..num_children)
.map(|_| Arc::new(std::sync::atomic::AtomicUsize::new(0)))
.collect();
let specs: Vec<ChildSpec> = (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<usize> = 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<usize> = 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::<ChildStarted>().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::<ChildStarted>().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<usize> = (0..num_children).collect();
assert_eq!(
result, expected,
"OneForAll(dead={}, n={}) should restart all children",
dead_idx, num_children
);
}
SupervisorStrategy::RestForOne => {
let expected: Vec<usize> = (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"
);
assert_eq!(reason_combinations, 4);
}

335
src/guarantees/g10_supervisor.rs
View file

@ -1,335 +0,0 @@
//! Kani proof harnesses for G10 — Supervisor Restart Decisions.
//!
//! Bounded mirror of the supervisor restart decision logic from
//! `std/supervisor.rs`. For bounded child counts (4 children),
//! symbolically enumerates all combinations of strategy, which child
//! dies, each child's restart policy, and death reason.
//!
//! 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).
//! - **G10b**: `OneForAll` restarts all children (respecting policies).
//! - **G10c**: `RestForOne` restarts dead child + all after it (respecting policies).
//! - **G10d**: `Temporary` children are never restarted.
//! - **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;
/// Outcome of the supervisor's restart decision. Tracks which children
/// get restarted (set to `true` in the array).
struct RestartOutcome {
restarted: [bool; MAX_CHILDREN],
meltdown: bool,
}
/// 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
/// `strategy`: supervision strategy
/// `policies`: restart policy per child
/// `reason`: why the child died
/// `total_restarts` / `max_restarts`: meltdown tracking
fn decide_restart(
num_children: usize,
dead_idx: usize,
strategy: SupervisorStrategy,
policies: &[RestartPolicy; MAX_CHILDREN],
reason: StopReason,
total_restarts: u32,
max_restarts: u32,
) -> RestartOutcome {
let mut outcome = RestartOutcome {
restarted: [false; MAX_CHILDREN],
meltdown: false,
};
// Step 1: Use production should_restart function
if !policies[dead_idx].should_restart(reason) {
return outcome;
}
// Step 2: meltdown check (supervisor.rs:273-280)
let new_total = total_restarts + 1;
if new_total > max_restarts {
outcome.meltdown = true;
return outcome;
}
// 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
}
// ─── Helper: symbolic enum generation ───────────────────────────────────────
fn symbolic_strategy() -> SupervisorStrategy {
let v: u8 = kani::any();
kani::assume(v < 3);
match v {
0 => SupervisorStrategy::OneForOne,
1 => SupervisorStrategy::OneForAll,
_ => SupervisorStrategy::RestForOne,
}
}
fn symbolic_policy() -> RestartPolicy {
let v: u8 = kani::any();
kani::assume(v < 3);
match v {
0 => RestartPolicy::Permanent,
1 => RestartPolicy::Transient,
_ => RestartPolicy::Temporary,
}
}
fn symbolic_reason() -> StopReason {
let v: u8 = kani::any();
kani::assume(v < 2);
// Only Normal and Panicked are relevant for restart decisions.
// Completed behaves identically to Normal (non-panic).
match v {
0 => StopReason::Normal,
_ => StopReason::Panicked,
}
}
// ─── Proof harnesses ────────────────────────────────────────────────────────
/// **G10a**: `OneForOne` restarts only the dead child (if policy permits).
#[kani::proof]
#[kani::unwind(5)]
fn proof_g10a_one_for_one_restarts_only_dead() {
let num_children: usize = kani::any();
kani::assume(num_children >= 1 && num_children <= MAX_CHILDREN);
let dead_idx: usize = kani::any();
kani::assume(dead_idx < num_children);
let mut policies = [RestartPolicy::Permanent; MAX_CHILDREN];
let mut i = 0;
while i < num_children {
policies[i] = symbolic_policy();
i += 1;
}
let reason = symbolic_reason();
let max_restarts: u32 = kani::any();
kani::assume(max_restarts >= 1);
let outcome = decide_restart(
num_children,
dead_idx,
SupervisorStrategy::OneForOne,
&policies,
reason,
0, // fresh supervisor
max_restarts,
);
if !outcome.meltdown && policies[dead_idx].should_restart(reason) {
// Only the dead child is restarted
assert!(outcome.restarted[dead_idx]);
let mut j = 0;
while j < num_children {
if j != dead_idx {
assert!(!outcome.restarted[j]);
}
j += 1;
}
}
}
/// **G10b**: `OneForAll` restarts all children (respecting policies).
#[kani::proof]
#[kani::unwind(5)]
fn proof_g10b_one_for_all_restarts_all() {
let num_children: usize = kani::any();
kani::assume(num_children >= 1 && num_children <= MAX_CHILDREN);
let dead_idx: usize = kani::any();
kani::assume(dead_idx < num_children);
let mut policies = [RestartPolicy::Permanent; MAX_CHILDREN];
let mut i = 0;
while i < num_children {
policies[i] = symbolic_policy();
i += 1;
}
let reason = symbolic_reason();
let max_restarts: u32 = kani::any();
kani::assume(max_restarts >= 1);
let outcome = decide_restart(
num_children,
dead_idx,
SupervisorStrategy::OneForAll,
&policies,
reason,
0,
max_restarts,
);
if !outcome.meltdown && policies[dead_idx].should_restart(reason) {
// All children are restarted
let mut j = 0;
while j < num_children {
assert!(outcome.restarted[j]);
j += 1;
}
}
}
/// **G10c**: `RestForOne` restarts dead child + all after it.
#[kani::proof]
#[kani::unwind(5)]
fn proof_g10c_rest_for_one_restarts_from_dead() {
let num_children: usize = kani::any();
kani::assume(num_children >= 1 && num_children <= MAX_CHILDREN);
let dead_idx: usize = kani::any();
kani::assume(dead_idx < num_children);
let mut policies = [RestartPolicy::Permanent; MAX_CHILDREN];
let mut i = 0;
while i < num_children {
policies[i] = symbolic_policy();
i += 1;
}
let reason = symbolic_reason();
let max_restarts: u32 = kani::any();
kani::assume(max_restarts >= 1);
let outcome = decide_restart(
num_children,
dead_idx,
SupervisorStrategy::RestForOne,
&policies,
reason,
0,
max_restarts,
);
if !outcome.meltdown && policies[dead_idx].should_restart(reason) {
// Children before dead_idx are NOT restarted
let mut j = 0;
while j < dead_idx {
assert!(!outcome.restarted[j]);
j += 1;
}
// Dead child and all after it ARE restarted
let mut k = dead_idx;
while k < num_children {
assert!(outcome.restarted[k]);
k += 1;
}
}
}
/// **G10d**: `Temporary` children are never restarted.
#[kani::proof]
#[kani::unwind(5)]
fn proof_g10d_temporary_never_restarted() {
let num_children: usize = kani::any();
kani::assume(num_children >= 1 && num_children <= MAX_CHILDREN);
let dead_idx: usize = kani::any();
kani::assume(dead_idx < num_children);
let strategy = symbolic_strategy();
let reason = symbolic_reason();
// Force the dead child to Temporary
let mut policies = [RestartPolicy::Permanent; MAX_CHILDREN];
let mut i = 0;
while i < num_children {
policies[i] = symbolic_policy();
i += 1;
}
policies[dead_idx] = RestartPolicy::Temporary;
let max_restarts: u32 = kani::any();
kani::assume(max_restarts >= 1);
let outcome = decide_restart(
num_children,
dead_idx,
strategy,
&policies,
reason,
0,
max_restarts,
);
// Temporary child triggers no restart at all (should_restart returns false)
// so no children should be restarted
let mut j = 0;
while j < num_children {
assert!(!outcome.restarted[j]);
j += 1;
}
assert!(!outcome.meltdown);
}
/// **G10e**: `Transient` children restart only on panic.
#[kani::proof]
#[kani::unwind(5)]
fn proof_g10e_transient_only_on_panic() {
let num_children: usize = kani::any();
kani::assume(num_children >= 1 && num_children <= MAX_CHILDREN);
let dead_idx: usize = kani::any();
kani::assume(dead_idx < num_children);
let strategy = symbolic_strategy();
let reason = symbolic_reason();
// Force the dead child to Transient
let mut policies = [RestartPolicy::Permanent; MAX_CHILDREN];
let mut i = 0;
while i < num_children {
policies[i] = symbolic_policy();
i += 1;
}
policies[dead_idx] = RestartPolicy::Transient;
let max_restarts: u32 = kani::any();
kani::assume(max_restarts >= 1);
let outcome = decide_restart(
num_children,
dead_idx,
strategy,
&policies,
reason,
0,
max_restarts,
);
if reason == StopReason::Normal {
// Normal stop: transient child should NOT trigger restarts
let mut j = 0;
while j < num_children {
assert!(!outcome.restarted[j]);
j += 1;
}
assert!(!outcome.meltdown);
}
// On panic: restarts happen (covered by strategy-specific proofs)
}

690
src/guarantees/g6_g7_death_orphan.rs
View file

@ -1,690 +0,0 @@
//! Property-based tests for G6 (Death Notification Completeness)
//! and G7 (Orphan Cleanup).
//!
//! G6: For every (monitor, monitored) pair where the monitored actor dies,
//! exactly one `Down` or `ActorExited` is delivered. No notifications
//! for actors still alive. Demonitored relationships produce no notification.
//!
//! G7: When a parent dies, all unsupervised children eventually stop.
//! Supervised children are handled by their supervisor, not orphan-killed.
use std::sync::Arc;
use proptest::prelude::*;
use crate::actor::{ActorAddress, ActorExited, ActorInterface, Down, ExitReason, StopReason};
use crate::config::RuntimeConfig;
use crate::runtime::{Ctx, Runtime};
use crate::std::{
ChildSpec, CtxMonitoring, CtxWatching, RestartPolicy, StdExtension, Supervisor,
SupervisorStrategy,
};
// ─── Helpers ────────────────────────────────────────────────────────────────
fn std_runtime() -> Runtime {
Runtime::new(RuntimeConfig::default()).with_extension(Arc::new(StdExtension::new()))
}
fn tick_many(rt: &Runtime, n: usize) {
for _ in 0..n {
rt.tick();
}
}
// ─── Message Types ──────────────────────────────────────────────────────────
#[derive(Clone, Debug)]
struct Ping;
#[derive(Clone, Debug)]
struct DownReport {
dead: ActorAddress,
reason: StopReason,
}
#[derive(Clone, Debug)]
struct ExitReport {
dead: ActorAddress,
reason: ExitReason,
}
#[derive(Clone, Debug)]
struct StoppedReport(ActorAddress);
// ─── Actor Types ────────────────────────────────────────────────────────────
/// An actor that monitors a set of targets in on_start and reports Down
/// messages to an external inbox.
struct MonitorActor {
targets: Vec<ActorAddress>,
report_to: ActorAddress,
}
impl ActorInterface for MonitorActor {
type Incoming = Ping;
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
for &target in &self.targets {
let _ = ctx.monitor(target);
}
}
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
fn handle_down(&mut self, ctx: &Ctx, down: Down) {
let _ = ctx.send(
self.report_to,
DownReport {
dead: down.addr,
reason: down.reason,
},
);
}
}
/// An actor that watches a set of targets in on_start and reports ActorExited
/// messages to an external inbox.
struct WatchActor {
targets: Vec<ActorAddress>,
report_to: ActorAddress,
}
impl ActorInterface for WatchActor {
type Incoming = Ping;
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
for &target in &self.targets {
ctx.watch(target);
}
}
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
fn on_actor_exit(&mut self, ctx: &Ctx, exited: ActorExited) {
let _ = ctx.send(
self.report_to,
ExitReport {
dead: exited.addr,
reason: exited.reason,
},
);
}
}
/// An actor that monitors targets, then demonitors some before they die.
struct DemonitorActor {
targets: Vec<ActorAddress>,
/// Indices into `targets` to demonitor after setup.
demonitor_indices: Vec<usize>,
report_to: ActorAddress,
}
impl ActorInterface for DemonitorActor {
type Incoming = Ping;
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
let mut refs = Vec::new();
for &target in &self.targets {
refs.push(ctx.monitor(target).unwrap());
}
// Demonitor selected targets
for &idx in &self.demonitor_indices {
if idx < refs.len() {
ctx.demonitor(refs[idx]);
}
}
}
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
fn handle_down(&mut self, ctx: &Ctx, down: Down) {
let _ = ctx.send(
self.report_to,
DownReport {
dead: down.addr,
reason: down.reason,
},
);
}
}
/// Simple actor that panics on first message.
struct PanicOnMsg;
impl ActorInterface for PanicOnMsg {
type Incoming = Ping;
type Response = ();
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {
panic!("intentional panic");
}
}
/// Actor that does nothing, just stays alive.
struct IdleActor;
impl ActorInterface for IdleActor {
type Incoming = Ping;
type Response = ();
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
}
#[derive(Clone, Debug)]
struct SpawnReport {
children: Vec<ActorAddress>,
}
/// Reports when on_stop fires.
struct StopReportActor {
report_to: ActorAddress,
}
impl ActorInterface for StopReportActor {
type Incoming = Ping;
type Response = ();
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
fn on_stop(&mut self, ctx: &Ctx) {
let _ = ctx.send(self.report_to, StoppedReport(ctx.self_addr()));
}
}
// ─── Property Tests ─────────────────────────────────────────────────────────
proptest! {
#![proptest_config(ProptestConfig::with_cases(60))]
// ═══════════════════════════════════════════════════════════════════════
// G6: Death Notification Completeness — Monitor (Down)
// ═══════════════════════════════════════════════════════════════════════
/// Spawn N targets. Kill a random subset. A single monitoring actor monitors
/// all targets. Assert: exactly one Down per dead target, zero for alive ones.
#[test]
fn monitor_exactly_one_down_per_dead_target(
num_targets in 2usize..=10,
kill_mask in prop::collection::vec(prop::bool::ANY, 2..=10),
) {
let rt = std_runtime();
let down_inbox = rt.new_inbox::<DownReport>().unwrap();
// Spawn targets
let mut targets = Vec::new();
for _ in 0..num_targets {
targets.push(rt.spawn(PanicOnMsg).unwrap());
}
// Spawn the monitoring actor
let _monitor = rt.spawn(MonitorActor {
targets: targets.clone(),
report_to: *down_inbox.addr(),
}).unwrap();
// Tick so on_start runs (monitors registered)
tick_many(&rt, 2);
// Kill targets according to mask
let kill_mask: Vec<bool> = kill_mask.into_iter().take(num_targets).collect();
let expected_dead: Vec<ActorAddress> = targets.iter()
.zip(kill_mask.iter())
.filter(|&(_, kill)| *kill)
.map(|(&addr, _)| addr)
.collect();
for &addr in &expected_dead {
rt.send_to(addr, Ping).unwrap();
}
tick_many(&rt, 5);
// Collect Down reports
let mut reports: Vec<DownReport> = Vec::new();
while let Some(r) = down_inbox.try_recv() {
reports.push(r);
}
// Exactly one Down per dead target
let dead_count = expected_dead.len();
prop_assert_eq!(
reports.len(), dead_count,
"expected {} Down messages, got {}", dead_count, reports.len()
);
// Each dead target appears exactly once
for &dead_addr in &expected_dead {
let count = reports.iter().filter(|r| r.dead == dead_addr).count();
prop_assert_eq!(count, 1, "dead target should appear exactly once in Down reports");
}
// Reason should be Panicked for panic-killed actors
for r in &reports {
prop_assert_eq!(r.reason, StopReason::Panicked);
}
}
// ═══════════════════════════════════════════════════════════════════════
// G6: Death Notification Completeness — Watch (ActorExited)
// ═══════════════════════════════════════════════════════════════════════
/// Same scenario but using watch + on_actor_exit instead of monitor + handle_down.
#[test]
fn watch_exactly_one_exited_per_dead_target(
num_targets in 2usize..=10,
kill_mask in prop::collection::vec(prop::bool::ANY, 2..=10),
) {
let rt = std_runtime();
let exit_inbox = rt.new_inbox::<ExitReport>().unwrap();
let mut targets = Vec::new();
for _ in 0..num_targets {
targets.push(rt.spawn(PanicOnMsg).unwrap());
}
let _watcher = rt.spawn(WatchActor {
targets: targets.clone(),
report_to: *exit_inbox.addr(),
}).unwrap();
tick_many(&rt, 2);
let kill_mask: Vec<bool> = kill_mask.into_iter().take(num_targets).collect();
let expected_dead: Vec<ActorAddress> = targets.iter()
.zip(kill_mask.iter())
.filter(|&(_, kill)| *kill)
.map(|(&addr, _)| addr)
.collect();
for &addr in &expected_dead {
rt.send_to(addr, Ping).unwrap();
}
tick_many(&rt, 5);
let mut reports: Vec<ExitReport> = Vec::new();
while let Some(r) = exit_inbox.try_recv() {
reports.push(r);
}
let dead_count = expected_dead.len();
prop_assert_eq!(
reports.len(), dead_count,
"expected {} ActorExited, got {}", dead_count, reports.len()
);
for &dead_addr in &expected_dead {
let count = reports.iter().filter(|r| r.dead == dead_addr).count();
prop_assert_eq!(count, 1, "dead target should appear exactly once in ActorExited reports");
}
for r in &reports {
prop_assert_eq!(r.reason.clone(), ExitReason::Panicked);
}
}
// ═══════════════════════════════════════════════════════════════════════
// G6: Demonitor produces no notification
// ═══════════════════════════════════════════════════════════════════════
/// Monitor N targets, demonitor a random subset, kill all targets.
/// Assert: only non-demonitored targets produce Down messages.
#[test]
fn demonitor_suppresses_notification(
num_targets in 2usize..=8,
demonitor_mask in prop::collection::vec(prop::bool::ANY, 2..=8),
) {
let rt = std_runtime();
let down_inbox = rt.new_inbox::<DownReport>().unwrap();
let mut targets = Vec::new();
for _ in 0..num_targets {
targets.push(rt.spawn(PanicOnMsg).unwrap());
}
let demonitor_mask: Vec<bool> = demonitor_mask.into_iter().take(num_targets).collect();
let demonitor_indices: Vec<usize> = demonitor_mask.iter()
.enumerate()
.filter(|&(_, d)| *d)
.map(|(i, _)| i)
.collect();
let _monitor = rt.spawn(DemonitorActor {
targets: targets.clone(),
demonitor_indices: demonitor_indices.clone(),
report_to: *down_inbox.addr(),
}).unwrap();
tick_many(&rt, 2);
// Kill all targets
for &addr in &targets {
rt.send_to(addr, Ping).unwrap();
}
tick_many(&rt, 5);
let mut reports: Vec<DownReport> = Vec::new();
while let Some(r) = down_inbox.try_recv() {
reports.push(r);
}
// Targets that were demonitored should NOT appear
let demonitor_set: std::collections::HashSet<usize> =
demonitor_indices.iter().copied().collect();
let expected_count = (0..num_targets)
.filter(|i| !demonitor_set.contains(i))
.count();
prop_assert_eq!(
reports.len(), expected_count,
"expected {} Down (non-demonitored), got {}", expected_count, reports.len()
);
// Verify no demonitored target appears in reports
for &idx in &demonitor_indices {
if idx < num_targets {
let count = reports.iter().filter(|r| r.dead == targets[idx]).count();
prop_assert_eq!(count, 0, "demonitored target should not produce Down");
}
}
}
// ═══════════════════════════════════════════════════════════════════════
// G6: No notification for alive actors
// ═══════════════════════════════════════════════════════════════════════
/// Monitor N targets, kill none. Assert: zero Down messages after many ticks.
#[test]
fn no_notification_for_alive_actors(
num_targets in 2usize..=10,
) {
let rt = std_runtime();
let down_inbox = rt.new_inbox::<DownReport>().unwrap();
let mut targets = Vec::new();
for _ in 0..num_targets {
targets.push(rt.spawn(IdleActor).unwrap());
}
let _monitor = rt.spawn(MonitorActor {
targets: targets.clone(),
report_to: *down_inbox.addr(),
}).unwrap();
tick_many(&rt, 10);
let count = std::iter::from_fn(|| down_inbox.try_recv()).count();
prop_assert_eq!(count, 0, "no Down for alive actors");
}
// ═══════════════════════════════════════════════════════════════════════
// G6: Multiple monitors on same target — each gets exactly one Down
// ═══════════════════════════════════════════════════════════════════════
/// N watchers monitor the same target. Kill the target. Each watcher gets
/// exactly one Down.
#[test]
fn multiple_monitors_each_get_one_down(
num_watchers in 2usize..=8,
) {
let rt = std_runtime();
let down_inbox = rt.new_inbox::<DownReport>().unwrap();
let target = rt.spawn(PanicOnMsg).unwrap();
for _ in 0..num_watchers {
rt.spawn(MonitorActor {
targets: vec![target],
report_to: *down_inbox.addr(),
}).unwrap();
}
tick_many(&rt, 2);
// Kill target
rt.send_to(target, Ping).unwrap();
tick_many(&rt, 5);
let reports: Vec<DownReport> = std::iter::from_fn(|| down_inbox.try_recv()).collect();
prop_assert_eq!(
reports.len(), num_watchers,
"each watcher should get exactly one Down"
);
for r in &reports {
prop_assert_eq!(r.dead, target);
}
}
// ═══════════════════════════════════════════════════════════════════════
// G7: Orphan Cleanup — unsupervised children stop when parent dies
// ═══════════════════════════════════════════════════════════════════════
/// Parent spawns N unsupervised children. Kill the parent. Assert all children
/// eventually stop (verified via on_stop reports and failed send attempts).
#[test]
fn orphan_unsupervised_children_stop_on_parent_death(
num_children in 1usize..=8,
) {
let rt = std_runtime();
let spawn_inbox = rt.new_inbox::<SpawnReport>().unwrap();
let stop_inbox = rt.new_inbox::<StoppedReport>().unwrap();
// Spawn a parent that will spawn children (using StopReportActor as children
// so we can observe on_stop). We need a custom parent for this.
struct StopReportParent {
num_children: usize,
spawn_report_to: ActorAddress,
stop_report_to: ActorAddress,
}
impl ActorInterface for StopReportParent {
type Incoming = Ping;
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
let mut children = Vec::new();
for _ in 0..self.num_children {
let child = ctx.spawn(StopReportActor {
report_to: self.stop_report_to,
}).unwrap();
children.push(child);
}
let _ = ctx.send(
self.spawn_report_to,
SpawnReport { children },
);
}
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
}
let parent = rt.spawn(StopReportParent {
num_children,
spawn_report_to: *spawn_inbox.addr(),
stop_report_to: *stop_inbox.addr(),
}).unwrap();
tick_many(&rt, 3);
// Get spawn report
let report = spawn_inbox.try_recv().expect("should receive spawn report");
let children = report.children;
prop_assert_eq!(children.len(), num_children);
// Kill parent
rt.stop_actor(parent).unwrap();
tick_many(&rt, 10);
// All children should have received on_stop
let stopped: Vec<StoppedReport> = std::iter::from_fn(|| stop_inbox.try_recv()).collect();
let stopped_addrs: std::collections::HashSet<ActorAddress> =
stopped.iter().map(|s| s.0).collect();
prop_assert_eq!(
stopped_addrs.len(), num_children,
"all {} unsupervised children should stop, got {} stops",
num_children, stopped_addrs.len()
);
for &child in &children {
prop_assert!(
stopped_addrs.contains(&child),
"child {:?} should have been stopped", child
);
}
}
// ═══════════════════════════════════════════════════════════════════════
// G7: Supervised children are NOT orphan-killed
// ═══════════════════════════════════════════════════════════════════════
/// Spawn a supervisor with N children. Kill the supervisor's parent (which
/// is the runtime — so stop the supervisor). The supervisor's on_stop should
/// handle children, not the orphan mechanism.
///
/// We verify that supervised children survive their grandparent's death
/// (i.e., the supervisor manages them, not the orphan killer).
#[test]
fn supervised_children_not_orphan_killed(
num_children in 1usize..=5,
) {
let rt = std_runtime();
// Build a supervisor with permanent children
let specs: Vec<ChildSpec> = (0..num_children)
.map(|i| {
ChildSpec::new(
format!("child-{}", i),
RestartPolicy::Permanent,
move |ctx| {
ctx.spawn(IdleActor)
},
)
})
.collect();
let sup = Supervisor::new(SupervisorStrategy::OneForOne, 10, specs);
let sup_addr = rt.spawn(sup).unwrap();
tick_many(&rt, 3);
// Verify children are alive by sending Ping to each
// We need to discover children addresses — send a ping to check
// Actually, we can verify the actor count
let stats = rt.stats();
let total_before = stats.workers.iter().map(|w| w.num_actors).sum::<usize>();
// 1 supervisor + N children = N+1
prop_assert!(
total_before >= num_children + 1,
"expected at least {} actors, got {}", num_children + 1, total_before
);
// Stop the supervisor — it should gracefully stop its children via on_stop
rt.stop_actor(sup_addr).unwrap();
tick_many(&rt, 10);
// All actors (sup + children) should be gone
let stats = rt.stats();
let total_after = stats.workers.iter().map(|w| w.num_actors).sum::<usize>();
prop_assert_eq!(
total_after, 0,
"all actors should be stopped after supervisor stops"
);
}
// ═══════════════════════════════════════════════════════════════════════
// G7: Cascading orphan cleanup — parent with grandchildren
// ═══════════════════════════════════════════════════════════════════════
/// Parent spawns children, each child spawns grandchildren. Kill the parent.
/// Assert: all descendants eventually stop (cascading orphan cleanup).
#[test]
fn cascading_orphan_cleanup(
num_children in 1usize..=4,
grandchildren_each in 1usize..=3,
) {
let rt = std_runtime();
let stop_inbox = rt.new_inbox::<StoppedReport>().unwrap();
let stop_addr = *stop_inbox.addr();
/// Parent that spawns ChildWithGrandchildren
struct TreeParent {
num_children: usize,
grandchildren_each: usize,
stop_report_to: ActorAddress,
}
impl ActorInterface for TreeParent {
type Incoming = Ping;
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
for _ in 0..self.num_children {
let _ = ctx.spawn(ChildWithGrandchildren {
num_grandchildren: self.grandchildren_each,
stop_report_to: self.stop_report_to,
});
}
}
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
fn on_stop(&mut self, ctx: &Ctx) {
let _ = ctx.send(self.stop_report_to, StoppedReport(ctx.self_addr()));
}
}
struct ChildWithGrandchildren {
num_grandchildren: usize,
stop_report_to: ActorAddress,
}
impl ActorInterface for ChildWithGrandchildren {
type Incoming = Ping;
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
for _ in 0..self.num_grandchildren {
let _ = ctx.spawn(StopReportActor {
report_to: self.stop_report_to,
});
}
}
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
fn on_stop(&mut self, ctx: &Ctx) {
let _ = ctx.send(self.stop_report_to, StoppedReport(ctx.self_addr()));
}
}
let parent = rt.spawn(TreeParent {
num_children,
grandchildren_each,
stop_report_to: stop_addr,
}).unwrap();
tick_many(&rt, 5);
// Kill parent
rt.stop_actor(parent).unwrap();
tick_many(&rt, 15);
// Count stopped reports: parent + children + grandchildren
let expected_total = 1 + num_children + (num_children * grandchildren_each);
let stopped: Vec<StoppedReport> = std::iter::from_fn(|| stop_inbox.try_recv()).collect();
prop_assert_eq!(
stopped.len(), expected_total,
"expected {} stop reports (1 parent + {} children + {} grandchildren), got {}",
expected_total, num_children, num_children * grandchildren_each, stopped.len()
);
// All actors should be gone
let stats = rt.stats();
let total = stats.workers.iter().map(|w| w.num_actors).sum::<usize>();
prop_assert_eq!(total, 0, "all actors should be stopped");
}
}

20
src/guarantees/mod.rs
View file

@ -1,26 +1,15 @@
//! Runtime guarantee verification modules.
//!
//! Consolidates all formal verification (Kani bounded model checking)
//! and exhaustive correspondence testing into a single module tree.
//!
//! - `g4_lifecycle`: Kani proofs for lifecycle ordering (G4)
//! - `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`: Exhaustive deterministic tests verifying production decision functions match runtime behavior
//! Formal and exhaustive checks now cover core runtime behavior only. Alpha std
//! features that are not used by production crates were pruned from the beta
//! surface, so their feature-specific guarantee modules are no longer compiled.
#[cfg(kani)]
mod g4_lifecycle;
#[cfg(kani)]
mod g10_supervisor;
#[cfg(test)]
mod g5_fault_isolation;
#[cfg(test)]
mod g6_g7_death_orphan;
#[cfg(test)]
mod correspondence;
@ -32,6 +21,3 @@ mod stateright_lifecycle;
#[cfg(test)]
mod stateright_death_orphan;
#[cfg(test)]
mod stateright_supervisor;

368
src/guarantees/stateright_supervisor.rs
View file

@ -1,368 +0,0 @@
//! 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",
);
}

62
src/std/children_registry.rs
View file

@ -1,62 +0,0 @@
use std::sync::RwLock;
use crate::actor::ActorAddress;
use crate::{AddrMap, AddrSet};
/// Tracks parent → children relationships for orphan cleanup.
///
/// When a parent dies, unsupervised children are stopped automatically.
/// Entries are added in `on_spawn` and cleaned up on actor death.
pub struct ChildrenRegistry {
/// parent_addr → set of child addresses
children: RwLock<AddrMap<AddrSet>>,
}
impl Default for ChildrenRegistry {
fn default() -> Self {
Self::new()
}
}
impl ChildrenRegistry {
pub fn new() -> Self {
Self {
children: RwLock::new(AddrMap::default()),
}
}
/// Register a parent → child relationship.
pub fn register(&self, parent: ActorAddress, child: ActorAddress) {
self.children
.write()
.unwrap()
.entry(parent)
.or_default()
.insert(child);
}
/// Remove and return all children of a parent (for orphan handling).
pub fn take_children(&self, parent: &ActorAddress) -> Vec<ActorAddress> {
self.children
.write()
.unwrap()
.remove(parent)
.map(|set| set.into_iter().collect())
.unwrap_or_default()
}
/// Clean up entries for dead actors (as both parent and child).
pub fn cleanup(&self, dead: &[ActorAddress]) {
let mut map = self.children.write().unwrap();
for addr in dead {
// Remove as parent
map.remove(addr);
// Remove as child from any parent's set
for set in map.values_mut() {
set.remove(addr);
}
}
// Remove empty parent entries
map.retain(|_, set| !set.is_empty());
}
}

386
src/std/ctx_ext.rs
View file

@ -1,11 +1,6 @@
use crate::Error;
use crate::actor::{
ActorAddress, ActorInterface, Ctx, Environment, LogicalName, Message, MonitorRef, SystemInfo,
};
use crate::actor::{ActorAddress, Ctx};
use super::StdExtension;
use super::resource_handle::ResourceHandle;
use super::timer_wheel::{CloneMsg, TimerRequest};
pub(crate) fn get_ext<'a>(ctx: &'a Ctx) -> &'a StdExtension {
ctx.extension()
@ -15,165 +10,27 @@ pub(crate) fn get_ext<'a>(ctx: &'a Ctx) -> &'a StdExtension {
.expect("Extension is not StdExtension")
}
/// Monitoring extension for [`Ctx`].
///
/// Provides `monitor` / `demonitor` via the [`StdExtension`] monitor registry.
pub trait CtxMonitoring {
/// Subscribe to death notifications from `target`. Returns a [`MonitorRef`]
/// that can be used to cancel the subscription.
fn monitor(&self, target: ActorAddress) -> Result<MonitorRef, Error>;
/// Cancel a monitor subscription.
fn demonitor(&self, mref: MonitorRef);
}
impl CtxMonitoring for Ctx<'_> {
fn monitor(&self, target: ActorAddress) -> Result<MonitorRef, Error> {
if let Some(caps) = self.env::<crate::CapabilitySet>() {
caps.check_monitor(target)?;
}
Ok(get_ext(self)
.monitor_registry
.register(self.self_addr(), target))
}
fn demonitor(&self, mref: MonitorRef) {
get_ext(self).monitor_registry.deregister(mref);
}
}
/// Naming extension for [`Ctx`].
///
/// Provides `where_is`, `register_name`, and `spawn_named` via the [`StdExtension`]
/// name registry.
pub trait CtxNaming {
/// Look up an actor address by its registered name.
fn where_is(&self, name: &str) -> Option<ActorAddress>;
/// Register a name for the given address.
fn register_name(&self, name: impl Into<String>, addr: ActorAddress) -> Result<(), Error>;
/// Spawn an actor with a registered name, returning its address.
fn spawn_named<A: ActorInterface>(
&self,
name: impl Into<String>,
actor: A,
) -> Result<ActorAddress, Error>;
}
impl CtxNaming for Ctx<'_> {
fn where_is(&self, name: &str) -> Option<ActorAddress> {
get_ext(self).name_registry.lookup(name)
}
fn register_name(&self, name: impl Into<String>, addr: ActorAddress) -> Result<(), Error> {
get_ext(self).name_registry.register(name.into(), addr)
}
fn spawn_named<A: ActorInterface>(
&self,
name: impl Into<String>,
actor: A,
) -> Result<ActorAddress, Error> {
let name = name.into();
let addr = self
.spawn_builder(actor)
.env(LogicalName(name.clone()))
.finish()?;
if let Err(e) = get_ext(self).name_registry.register(name, addr) {
let _ = self.stop_actor(addr);
return Err(e);
}
Ok(addr)
}
}
/// Watching extension for [`Ctx`].
///
/// Provides `watch` / `unwatch` via the [`StdExtension`] watch registry.
/// When a watched actor dies, the watcher receives an [`ActorExited`] message
/// delivered to its `on_actor_exit()` callback.
/// Provides actor-side death notification via [`StdExtension`]'s watch registry.
pub trait CtxWatching {
/// Watch another actor's liveness. If the target dies, this actor
/// receives an `ActorExited` message.
///
/// Calling watch() multiple times on the same target is idempotent —
/// only one notification is delivered.
/// Watch another actor's liveness. If the target dies, this actor receives an
/// [`crate::actor::ActorExited`] message through `on_actor_exit`.
fn watch(&self, target: ActorAddress);
/// Stop watching an actor. No notification will be delivered if the
/// target subsequently dies.
fn unwatch(&self, target: ActorAddress);
}
impl CtxWatching for Ctx<'_> {
fn watch(&self, target: ActorAddress) {
get_ext(self).watch_registry.watch(self.self_addr(), target);
}
fn unwatch(&self, target: ActorAddress) {
get_ext(self)
.watch_registry
.unwatch(self.self_addr(), target);
}
}
/// Timer extension for [`Ctx`].
///
/// Provides `send_after_ticks` / `send_interval_ticks` via the per-worker
/// [`TimerWheel`](super::timer_wheel::TimerWheel).
pub trait CtxTimers {
/// Schedule a one-shot timer: deliver `msg` to `addr` after `ticks` worker ticks.
///
/// The message is delivered as a normal mailbox message during the fire tick,
/// before `tick_all` processes messages. The timer is tick-counted (deterministic),
/// not wall-clock based.
fn send_after_ticks<M: Message>(&self, addr: ActorAddress, msg: M, ticks: u64);
/// Schedule a repeating timer: deliver a clone of `msg` to `addr` every `period` ticks.
///
/// The first delivery happens after `period` ticks. The message is cloned for each
/// delivery. The timer continues until the target actor is stopped/poisoned.
fn send_interval_ticks<M: Message>(&self, addr: ActorAddress, msg: M, period: u64);
}
impl CtxTimers for Ctx<'_> {
fn send_after_ticks<M: Message>(&self, addr: ActorAddress, msg: M, ticks: u64) {
self.raw_inner()
.post_worker_request(Box::new(TimerRequest::Once {
dest: addr,
msg: Box::new(msg),
ticks,
}));
}
fn send_interval_ticks<M: Message>(&self, addr: ActorAddress, msg: M, period: u64) {
self.raw_inner()
.post_worker_request(Box::new(TimerRequest::Interval {
dest: addr,
msg: Box::new(msg) as Box<dyn CloneMsg>,
period,
}));
}
}
/// Group extension for [`Ctx`].
///
/// Provides `join_group`, `leave_group`, `publish`, and `group_members` via
/// the [`StdExtension`] group registry.
/// Provides actor-side group membership via [`StdExtension`]'s group registry.
pub trait CtxGroups {
/// Add this actor to a named group.
fn join_group(&self, group: impl Into<String>);
/// Remove this actor from a named group.
fn leave_group(&self, group: &str);
/// Broadcast a message to all members of a named group.
/// Returns the number of messages successfully enqueued.
fn publish<M: Message>(&self, group: &str, msg: M) -> usize;
/// Return all members of a named group.
fn group_members(&self, group: &str) -> Vec<ActorAddress>;
}
impl CtxGroups for Ctx<'_> {
@ -182,237 +39,4 @@ impl CtxGroups for Ctx<'_> {
.group_registry
.join(group.into(), self.self_addr());
}
fn leave_group(&self, group: &str) {
get_ext(self).group_registry.leave(group, &self.self_addr());
}
fn publish<M: Message>(&self, group: &str, msg: M) -> usize {
let members = get_ext(self).group_registry.members(group);
let mut count = 0;
for member in &members {
if self.send(*member, msg.clone()).is_ok() {
count += 1;
}
}
count
}
fn group_members(&self, group: &str) -> Vec<ActorAddress> {
get_ext(self).group_registry.members(group)
}
}
/// System introspection extension for [`Ctx`].
///
/// Provides convenience accessors for system-level information. Does NOT
/// require [`StdExtension`] — the data comes from the core runtime.
pub trait CtxSystem {
/// Returns the full [`SystemInfo`] snapshot.
fn system_info(&self) -> SystemInfo;
/// Index of the worker thread this actor is running on.
fn worker_id(&self) -> usize;
/// Total number of worker threads in the runtime.
fn num_workers(&self) -> usize;
/// Total number of live actors across all workers.
fn total_actors(&self) -> usize;
/// Milliseconds since the runtime was created.
fn uptime_ms(&self) -> u64;
}
impl CtxSystem for Ctx<'_> {
fn system_info(&self) -> SystemInfo {
Ctx::system_info(self)
}
fn worker_id(&self) -> usize {
Ctx::system_info(self).worker_id
}
fn num_workers(&self) -> usize {
Ctx::system_info(self).num_workers
}
fn total_actors(&self) -> usize {
Ctx::system_info(self).total_actors
}
fn uptime_ms(&self) -> u64 {
Ctx::system_info(self).uptime_ms
}
}
/// Lineage extension for [`Ctx`].
///
/// Exposes the actor's parent and supervisor. `parent()` does NOT require
/// [`StdExtension`] — the data is stored in core per-actor state.
/// `supervisor()` returns `None` gracefully when StdExtension is absent.
pub trait CtxLineage {
/// Returns the address of the actor that spawned this one, or `None`
/// if this actor was spawned externally via `Runtime::spawn`.
fn parent(&self) -> Option<ActorAddress>;
/// Returns the address of this actor's supervisor, or `None` if
/// unsupervised or StdExtension is not installed.
fn supervisor(&self) -> Option<ActorAddress>;
}
impl CtxLineage for Ctx<'_> {
fn parent(&self) -> Option<ActorAddress> {
Ctx::parent(self)
}
fn supervisor(&self) -> Option<ActorAddress> {
let ext = self.extension()?.as_any().downcast_ref::<StdExtension>()?;
ext.supervisor_registry.lookup(&self.self_addr())
}
}
/// Per-actor self-introspection extension for [`Ctx`].
///
/// Exposes the actor's own operational metrics. Does NOT require
/// [`StdExtension`] — the data is snapshotted from core before each tick.
pub trait CtxSelfStats {
/// Total messages this actor has successfully processed (before the current tick).
fn messages_processed(&self) -> u64;
/// Number of messages in this actor's mailbox at the start of the current tick.
fn mailbox_depth(&self) -> usize;
/// Per-message-type counts for this actor, sorted descending by count.
fn message_type_counts(&self) -> &[(&'static str, u64)];
}
impl CtxSelfStats for Ctx<'_> {
fn messages_processed(&self) -> u64 {
Ctx::messages_processed(self)
}
fn mailbox_depth(&self) -> usize {
Ctx::mailbox_depth(self)
}
fn message_type_counts(&self) -> &[(&'static str, u64)] {
Ctx::message_type_counts(self)
}
}
/// Service resource extension for [`Ctx`].
///
/// Provides typed service discovery via the environment. Does NOT require
/// [`StdExtension`] — reads from the core environment (same as [`CtxEnvironment`]).
pub trait CtxResources {
/// Look up a service address by marker type `S`.
///
/// Returns `None` if no `ServiceBinding<S>` is present in the environment.
fn resource<S: 'static + Send + Sync>(&self) -> Option<ActorAddress>;
}
impl CtxResources for Ctx<'_> {
fn resource<S: 'static + Send + Sync>(&self) -> Option<ActorAddress> {
if let Some(caps) = self.env::<crate::CapabilitySet>()
&& caps.check_service::<S>().is_err()
{
return None;
}
self.env::<crate::ServiceBinding<S>>().map(|b| b.addr)
}
}
/// Environment extension for [`Ctx`].
///
/// Provides access to the actor's inherited typed key-value environment.
/// Does NOT require [`StdExtension`] — the data is stored in core per-actor state.
pub trait CtxEnvironment {
/// Read a typed value from this actor's environment.
fn env<T: std::any::Any + Send + Sync>(&self) -> Option<&T>;
/// Access this actor's full environment.
fn environment(&self) -> &Environment;
}
impl CtxEnvironment for Ctx<'_> {
fn env<T: std::any::Any + Send + Sync>(&self) -> Option<&T> {
Ctx::env(self)
}
fn environment(&self) -> &Environment {
Ctx::environment(self)
}
}
/// Resource handle extension for [`Ctx`].
///
/// Provides `handle::<H>()` to construct typed proxy structs wrapping service
/// addresses for ergonomic domain-specific APIs. See [`ResourceHandle`] for
/// how to define a handle type.
pub trait CtxHandles {
/// Construct a typed resource handle from the service registry.
///
/// Returns `None` if no `ServiceBinding<H::Service>` is present in the
/// actor's environment (consistent with `ctx.resource()`, `ctx.where_is()`, etc).
fn handle<H: ResourceHandle>(&self) -> Option<H>;
}
impl CtxHandles for Ctx<'_> {
fn handle<H: ResourceHandle>(&self) -> Option<H> {
let binding = self.env::<crate::ServiceBinding<H::Service>>()?;
Some(H::from_parts(binding.addr, self.self_addr()))
}
}
/// Lifecycle extension for [`Ctx`].
///
/// Provides suspend/resume capabilities with authorization:
/// only the actor itself or its supervisor can resume it.
pub trait CtxLifecycle {
/// Suspend this actor. Messages continue to queue but are not processed
/// until resumed by self or supervisor.
fn suspend_self(&self);
/// Resume a suspended actor. Only the actor itself or its supervisor
/// may call this. Returns `Err` if the caller is not authorized.
fn resume(&self, target: ActorAddress) -> Result<(), Error>;
}
impl CtxLifecycle for Ctx<'_> {
fn suspend_self(&self) {
Ctx::suspend_self(self);
}
fn resume(&self, target: ActorAddress) -> Result<(), Error> {
// Self-resume is always allowed
if target == self.self_addr() {
self.raw_inner().request_resume(target);
return Ok(());
}
// Supervisor can resume its child
let ext = get_ext(self);
if ext.supervisor_registry.lookup(&target) == Some(self.self_addr()) {
self.raw_inner().request_resume(target);
return Ok(());
}
Err(Error::from(
"resume denied: caller is not self or supervisor",
))
}
}
/// Capability introspection extension for [`Ctx`].
pub trait CtxCapabilities {
fn capabilities(&self) -> Option<&crate::CapabilitySet>;
fn is_restricted(&self) -> bool;
}
impl CtxCapabilities for Ctx<'_> {
fn capabilities(&self) -> Option<&crate::CapabilitySet> {
Ctx::env(self)
}
fn is_restricted(&self) -> bool {
self.env::<crate::CapabilitySet>().is_some()
}
}

103
src/std/extension.rs
View file

@ -1,58 +1,29 @@
use std::any::Any;
use crate::actor::{
ActorAddress, Down, Environment, EnvironmentBuilder, ExitReason, ExitValue, SpawnTimestamp,
StopReason, StopSignal,
};
use crate::extension::{RuntimeExtension, WorkerExtension};
use crate::actor::{ActorAddress, Environment, ExitReason, ExitValue, StopReason};
use crate::extension::RuntimeExtension;
use super::children_registry::ChildrenRegistry;
use super::group_registry::GroupRegistry;
use super::monitor_registry::MonitorRegistry;
use super::name_registry::NameRegistry;
use super::service_registry::ServiceRegistry;
use super::supervisor_registry::SupervisorRegistry;
use super::timer_wheel::TimerWheel;
use super::watch_registry::WatchRegistry;
/// Standard library extension — provides naming, monitoring, watching, and group registries.
/// Standard library extension — provides naming, watching, and group registries.
///
/// Install on a `Runtime` via `runtime.with_extension(Arc::new(StdExtension::new()))`.
pub struct StdExtension {
pub(crate) name_registry: NameRegistry,
pub(crate) monitor_registry: MonitorRegistry,
pub(crate) watch_registry: WatchRegistry,
pub(crate) group_registry: GroupRegistry,
pub(crate) supervisor_registry: SupervisorRegistry,
pub(crate) service_registry: ServiceRegistry,
pub(crate) children_registry: ChildrenRegistry,
}
impl StdExtension {
pub fn new() -> Self {
Self {
name_registry: NameRegistry::new(),
monitor_registry: MonitorRegistry::new(),
watch_registry: WatchRegistry::new(),
group_registry: GroupRegistry::new(),
supervisor_registry: SupervisorRegistry::new(),
service_registry: ServiceRegistry::new(),
children_registry: ChildrenRegistry::new(),
}
}
/// Resolve a human-readable name for an actor address (reverse lookup).
pub fn resolve_name(&self, addr: &ActorAddress) -> Option<String> {
self.name_registry.lookup_by_addr(addr)
}
/// Register a supervisor → child relationship.
///
/// This is used by the built-in [`Supervisor`](super::Supervisor) and can
/// also be called by custom supervisor implementations.
pub fn register_supervisor(&self, supervisor: ActorAddress, child: ActorAddress) {
self.supervisor_registry.register(supervisor, child);
}
}
impl Default for StdExtension {
@ -64,9 +35,8 @@ impl Default for StdExtension {
/// Map StopReason → ExitReason for watch notifications.
fn stop_to_exit(reason: StopReason) -> ExitReason {
match reason {
StopReason::Normal => ExitReason::Stopped,
StopReason::Normal | StopReason::Completed => ExitReason::Completed,
StopReason::Panicked => ExitReason::Panicked,
StopReason::Completed => ExitReason::Completed,
}
}
@ -78,73 +48,38 @@ impl RuntimeExtension for StdExtension {
let mut notifications = Vec::new();
for (addr, reason, exit_value) in dead {
let addr = *addr;
let reason = *reason;
// Monitor notifications (Down)
let watchers = self.monitor_registry.take_monitors(&addr);
for (_mref, watcher) in watchers {
let down = Down {
addr,
reason,
exit_value: exit_value.clone(),
};
notifications.push((watcher, Box::new(down) as Box<dyn Any + Send>));
}
// Watch notifications (ActorExited)
let watch_notifications =
self.watch_registry
.notify_death(addr, stop_to_exit(reason), exit_value.clone());
let watch_notifications = self.watch_registry.notify_death(
*addr,
stop_to_exit(*reason),
exit_value.clone(),
);
for (watcher, exited) in watch_notifications {
notifications.push((watcher, Box::new(exited) as Box<dyn Any + Send>));
}
// Orphan handling: kill unsupervised children
let children = self.children_registry.take_children(&addr);
for child in children {
if self.supervisor_registry.lookup(&child).is_none() {
notifications.push((child, Box::new(StopSignal) as Box<dyn Any + Send>));
}
}
}
notifications
}
fn cleanup_dead(&self, dead: &[ActorAddress]) {
self.children_registry.cleanup(dead);
for addr in dead {
self.name_registry.unregister_by_addr(addr);
self.group_registry.cleanup(addr);
self.monitor_registry.remove_watcher(addr);
self.watch_registry.cleanup_watcher(addr);
self.supervisor_registry.cleanup(addr);
}
}
fn on_spawn(
&self,
_child: ActorAddress,
_parent: Option<ActorAddress>,
env: Environment,
_uptime_ms: u64,
) -> Environment {
env
}
fn as_any(&self) -> &dyn Any {
self
}
fn on_spawn(
&self,
child: ActorAddress,
parent: Option<ActorAddress>,
env: Environment,
uptime_ms: u64,
) -> Environment {
// Register parent → child relationship for orphan cleanup
if let Some(parent_addr) = parent {
self.children_registry.register(parent_addr, child);
}
let env = self.service_registry.inject_into(env);
EnvironmentBuilder::from_env(&env)
.set(SpawnTimestamp(uptime_ms))
.build()
}
fn create_worker_extension(&self) -> Option<Box<dyn WorkerExtension>> {
Some(Box::new(TimerWheel::new()))
}
}

24
src/std/group_registry.rs
View file

@ -1,13 +1,12 @@
use std::collections::{HashMap, HashSet};
use std::sync::RwLock;
use parking_lot::RwLock;
use crate::actor::ActorAddress;
use crate::{AddrBuildHasher, AddrMap, AddrSet};
/// Actor groups (pub-sub). Actors join/leave named groups; messages can be
/// broadcast to all members of a group.
///
/// Groups are created lazily on first join and removed when empty.
pub struct GroupRegistry {
/// group_name → set of member addresses
groups: RwLock<HashMap<String, AddrSet>>,
@ -33,21 +32,15 @@ impl GroupRegistry {
pub fn join(&self, group: String, addr: ActorAddress) {
self.groups
.write()
.unwrap()
.entry(group.clone())
.or_insert_with(|| HashSet::with_hasher(AddrBuildHasher))
.insert(addr);
self.memberships
.write()
.unwrap()
.entry(addr)
.or_default()
.insert(group);
self.memberships.write().entry(addr).or_default().insert(group);
}
/// Remove an actor from a named group. Empty groups are auto-deleted.
pub fn leave(&self, group: &str, addr: &ActorAddress) {
let mut groups = self.groups.write().unwrap();
let mut groups = self.groups.write();
if let Some(members) = groups.get_mut(group) {
members.remove(addr);
if members.is_empty() {
@ -55,7 +48,7 @@ impl GroupRegistry {
}
}
drop(groups);
if let Some(membership) = self.memberships.write().unwrap().get_mut(addr) {
if let Some(membership) = self.memberships.write().get_mut(addr) {
membership.remove(group);
}
}
@ -64,7 +57,6 @@ impl GroupRegistry {
pub fn members(&self, group: &str) -> Vec<ActorAddress> {
self.groups
.read()
.unwrap()
.get(group)
.map(|s| s.iter().copied().collect())
.unwrap_or_default()
@ -72,9 +64,9 @@ impl GroupRegistry {
/// Remove a dead actor from all its groups.
pub fn cleanup(&self, addr: &ActorAddress) {
let group_names = self.memberships.write().unwrap().remove(addr);
let group_names = self.memberships.write().remove(addr);
if let Some(names) = group_names {
let mut groups = self.groups.write().unwrap();
let mut groups = self.groups.write();
for name in names {
if let Some(members) = groups.get_mut(&name) {
members.remove(addr);
@ -88,6 +80,6 @@ impl GroupRegistry {
/// Return all active group names.
pub fn group_names(&self) -> Vec<String> {
self.groups.read().unwrap().keys().cloned().collect()
self.groups.read().keys().cloned().collect()
}
}

18
src/std/mod.rs
View file

@ -1,24 +1,10 @@
pub mod children_registry;
mod ctx_ext;
mod extension;
pub mod group_registry;
pub mod monitor_registry;
pub mod name_registry;
pub mod resource_handle;
mod router;
mod runtime_ext;
pub mod service_registry;
pub(crate) mod supervisor;
pub mod supervisor_registry;
pub(crate) mod timer_wheel;
pub mod watch_registry;
pub use ctx_ext::{
CtxCapabilities, CtxEnvironment, CtxGroups, CtxHandles, CtxLifecycle, CtxLineage,
CtxMonitoring, CtxNaming, CtxResources, CtxSelfStats, CtxSystem, CtxTimers, CtxWatching,
};
pub use ctx_ext::{CtxGroups, CtxWatching};
pub use extension::StdExtension;
pub use resource_handle::ResourceHandle;
pub use router::{Router, RoutingStrategy};
pub use runtime_ext::{RuntimeGroups, RuntimeNaming, RuntimeResources, RuntimeWatching};
pub use supervisor::{ChildSpec, RestartPolicy, Supervisor, SupervisorStrategy};
pub use runtime_ext::{RuntimeGroups, RuntimeNaming};

92
src/std/monitor_registry.rs
View file

@ -1,92 +0,0 @@
use std::collections::HashMap;
use std::sync::RwLock;
use std::sync::atomic::{AtomicU64, Ordering};
use crate::actor::{ActorAddress, MonitorRef};
use crate::{AddrBuildHasher, AddrMap};
/// Tracks monitor subscriptions: watched actor → list of (MonitorRef, watcher address).
///
/// Write-rare (monitor/demonitor/death), read at cleanup time.
pub struct MonitorRegistry {
/// watched_addr → [(mref, watcher_addr)]
monitors: RwLock<AddrMap<Vec<(MonitorRef, ActorAddress)>>>,
/// mref → watched_addr (for O(1) demonitor)
ref_to_target: RwLock<HashMap<MonitorRef, ActorAddress>>,
next_ref: AtomicU64,
}
impl Default for MonitorRegistry {
fn default() -> Self {
Self::new()
}
}
impl MonitorRegistry {
pub fn new() -> Self {
Self {
monitors: RwLock::new(HashMap::with_hasher(AddrBuildHasher)),
ref_to_target: RwLock::new(HashMap::new()),
next_ref: AtomicU64::new(1),
}
}
/// Register a monitor: `watcher` wants to know when `target` dies.
pub fn register(&self, watcher: ActorAddress, target: ActorAddress) -> MonitorRef {
let id = self.next_ref.fetch_add(1, Ordering::Relaxed);
let mref = MonitorRef::from_raw(id);
self.monitors
.write()
.unwrap()
.entry(target)
.or_default()
.push((mref, watcher));
self.ref_to_target.write().unwrap().insert(mref, target);
mref
}
/// Cancel a monitor by its ref.
pub fn deregister(&self, mref: MonitorRef) {
if let Some(target) = self.ref_to_target.write().unwrap().remove(&mref) {
let mut monitors = self.monitors.write().unwrap();
if let Some(watchers) = monitors.get_mut(&target) {
watchers.retain(|(r, _)| *r != mref);
if watchers.is_empty() {
monitors.remove(&target);
}
}
}
}
/// Remove and return all monitors for a dead actor.
pub fn take_monitors(&self, target: &ActorAddress) -> Vec<(MonitorRef, ActorAddress)> {
let watchers = self
.monitors
.write()
.unwrap()
.remove(target)
.unwrap_or_default();
let mut ref_map = self.ref_to_target.write().unwrap();
for (mref, _) in &watchers {
ref_map.remove(mref);
}
watchers
}
/// Remove all monitor subscriptions where `addr` is the watcher (dead watcher cleanup).
pub fn remove_watcher(&self, addr: &ActorAddress) {
let mut monitors = self.monitors.write().unwrap();
let mut ref_map = self.ref_to_target.write().unwrap();
monitors.retain(|_target, watchers| {
watchers.retain(|(mref, watcher)| {
if watcher == addr {
ref_map.remove(mref);
false
} else {
true
}
});
!watchers.is_empty()
});
}
}

27
src/std/name_registry.rs
View file

@ -1,13 +1,11 @@
use std::collections::HashMap;
use std::sync::RwLock;
use parking_lot::RwLock;
use crate::actor::ActorAddress;
use crate::{AddrBuildHasher, AddrMap};
/// Named actor registry — maps human-readable names to actor addresses.
///
/// `RwLock<HashMap>` — same pattern as `AddressMap`. Write-rare (spawn/death),
/// read-often (lookup). A reverse map enables O(1) cleanup on actor death.
pub struct NameRegistry {
names: RwLock<HashMap<String, ActorAddress>>,
reverse: RwLock<AddrMap<String>>,
@ -29,42 +27,37 @@ impl NameRegistry {
/// Register a name → address mapping. Returns `Err` if the name is already taken.
pub fn register(&self, name: String, addr: ActorAddress) -> Result<(), crate::Error> {
let mut names = self.names.write().unwrap();
let mut names = self.names.write();
if names.contains_key(&name) {
return Err(crate::Error::from("Name already registered"));
}
names.insert(name.clone(), addr);
drop(names);
self.reverse.write().unwrap().insert(addr, name);
self.reverse.write().insert(addr, name);
Ok(())
}
/// Look up an actor address by name.
pub fn lookup(&self, name: &str) -> Option<ActorAddress> {
self.names.read().unwrap().get(name).copied()
self.names.read().get(name).copied()
}
/// Unregister a name, returning the address it was bound to.
pub fn unregister(&self, name: &str) -> Option<ActorAddress> {
let addr = self.names.write().unwrap().remove(name)?;
self.reverse.write().unwrap().remove(&addr);
let addr = self.names.write().remove(name)?;
self.reverse.write().remove(&addr);
Some(addr)
}
/// Remove a name by address (called on actor death for auto-cleanup).
pub fn unregister_by_addr(&self, addr: &ActorAddress) {
if let Some(name) = self.reverse.write().unwrap().remove(addr) {
self.names.write().unwrap().remove(&name);
if let Some(name) = self.reverse.write().remove(addr) {
self.names.write().remove(&name);
}
}
/// Look up the name bound to an actor address (reverse lookup).
pub fn lookup_by_addr(&self, addr: &ActorAddress) -> Option<String> {
self.reverse.read().unwrap().get(addr).cloned()
}
/// Return all registered names.
pub fn registered_names(&self) -> Vec<String> {
self.names.read().unwrap().keys().cloned().collect()
self.names.read().keys().cloned().collect()
}
}

44
src/std/resource_handle.rs
View file

@ -1,44 +0,0 @@
use crate::actor::ActorAddress;
/// Typed proxy wrapping a service address for ergonomic domain-specific APIs.
///
/// Implement this trait on a struct that wraps a service address and provides
/// domain-specific methods. Methods take `&self` + `&Ctx` (not stored `&Ctx` —
/// avoids lifetime issues with `&mut self` in handlers).
///
/// # Example
///
/// ```ignore
/// struct CounterHandle {
/// service: ActorAddress,
/// self_addr: ActorAddress,
/// }
///
/// impl ResourceHandle for CounterHandle {
/// type Service = CounterService;
/// fn from_parts(service_addr: ActorAddress, self_addr: ActorAddress) -> Self {
/// Self { service: service_addr, self_addr }
/// }
/// fn service_addr(&self) -> ActorAddress { self.service }
/// fn self_addr(&self) -> ActorAddress { self.self_addr }
/// }
///
/// impl CounterHandle {
/// pub fn increment(&self, ctx: &Ctx) -> Result<(), Error> {
/// ctx.send(self.service_addr(), Increment { reply_to: self.self_addr() })
/// }
/// }
/// ```
pub trait ResourceHandle: Sized {
/// Marker type identifying the service (same `S` used with `ServiceRegistry`).
type Service: 'static + Send + Sync;
/// Construct a handle from a service address and the calling actor's address.
fn from_parts(service_addr: ActorAddress, self_addr: ActorAddress) -> Self;
/// The address of the underlying service actor.
fn service_addr(&self) -> ActorAddress;
/// The address of the actor holding this handle (for reply_to patterns).
fn self_addr(&self) -> ActorAddress;
}

179
src/std/router.rs
View file

@ -1,179 +0,0 @@
use std::marker::PhantomData;
use std::sync::Arc;
use crate::Error;
use crate::actor::{ActorAddress, ActorInterface, Ctx, Down, Message};
use super::CtxMonitoring;
use super::supervisor::ActiveChild;
/// Strategy for distributing messages across pool workers.
#[derive(Debug, Clone)]
pub enum RoutingStrategy {
/// Sequential round-robin distribution.
RoundRobin,
/// Random worker selection.
Random,
/// Send to all workers (message is cloned to each).
Broadcast,
}
/// A router actor that manages a pool of identical workers and distributes
/// incoming messages across them according to a [`RoutingStrategy`].
///
/// Workers are spawned during `on_start`, monitored for failures, and
/// automatically replaced to maintain the target pool size. Meltdown
/// protection stops the router when total restarts exceed `max_restarts`.
///
/// # Example
///
/// ```ignore
/// let router = Router::new(
/// RoutingStrategy::RoundRobin,
/// 5,
/// |ctx| ctx.spawn(MyWorker::new()),
/// 10,
/// );
/// let router_addr = rt.spawn(router)?;
/// rt.send_to(router_addr, WorkerMessage::DoWork(42))?;
/// ```
pub struct Router<M: Message> {
strategy: RoutingStrategy,
pool_size: usize,
factory: Arc<dyn Fn(&Ctx) -> Result<ActorAddress, Error> + Send + Sync>,
workers: Vec<Option<ActiveChild>>,
rr_index: usize,
total_restarts: u32,
max_restarts: u32,
_marker: PhantomData<M>,
}
impl<M: Message> Router<M> {
pub fn new(
strategy: RoutingStrategy,
pool_size: usize,
factory: impl Fn(&Ctx) -> Result<ActorAddress, Error> + Send + Sync + 'static,
max_restarts: u32,
) -> Self {
Self {
strategy,
pool_size,
factory: Arc::new(factory),
workers: (0..pool_size).map(|_| None).collect(),
rr_index: 0,
total_restarts: 0,
max_restarts,
_marker: PhantomData,
}
}
fn start_worker(&mut self, ctx: &Ctx, idx: usize) -> Result<(), Error> {
let addr = (self.factory)(ctx)?;
let mref = ctx.monitor(addr)?;
self.workers[idx] = Some(ActiveChild {
addr,
_monitor_ref: mref,
});
Ok(())
}
fn find_worker_idx(&self, addr: ActorAddress) -> Option<usize> {
self.workers
.iter()
.position(|w| w.as_ref().is_some_and(|ac| ac.addr == addr))
}
fn live_workers(&self) -> Vec<ActorAddress> {
self.workers
.iter()
.filter_map(|w| w.as_ref().map(|ac| ac.addr))
.collect()
}
fn select_one(&mut self) -> Option<ActorAddress> {
let live = self.live_workers();
if live.is_empty() {
return None;
}
match self.strategy {
RoutingStrategy::RoundRobin => {
let idx = self.rr_index % live.len();
self.rr_index = self.rr_index.wrapping_add(1);
Some(live[idx])
}
RoutingStrategy::Random => {
#[cfg(feature = "getrandom")]
{
let mut buf = [0u8; 8];
getrandom::getrandom(&mut buf).expect("getrandom failed");
let r = u64::from_ne_bytes(buf) as usize;
Some(live[r % live.len()])
}
#[cfg(not(feature = "getrandom"))]
{
// Fallback to round-robin when getrandom is unavailable (wasm)
let idx = self.rr_index % live.len();
self.rr_index = self.rr_index.wrapping_add(1);
Some(live[idx])
}
}
RoutingStrategy::Broadcast => None, // handled separately
}
}
}
impl<M: Message> ActorInterface for Router<M> {
type Incoming = M;
type Response = ();
fn handle(&mut self, ctx: &Ctx, msg: M) {
match self.strategy {
RoutingStrategy::Broadcast => {
let live = self.live_workers();
for addr in live {
let _ = ctx.send(addr, msg.clone());
}
}
_ => {
if let Some(addr) = self.select_one() {
let _ = ctx.send(addr, msg);
}
}
}
}
fn on_start(&mut self, ctx: &Ctx) {
for idx in 0..self.pool_size {
if let Err(e) = self.start_worker(ctx, idx) {
eprintln!("swactor: router failed to start worker {idx}: {e}");
}
}
}
fn on_stop(&mut self, ctx: &Ctx) {
for child in self.workers.iter().flatten() {
let _ = ctx.stop_actor(child.addr);
}
}
fn handle_down(&mut self, ctx: &Ctx, down: Down) {
let Some(idx) = self.find_worker_idx(down.addr) else {
return;
};
self.workers[idx] = None;
self.total_restarts += 1;
if self.total_restarts > self.max_restarts {
eprintln!(
"swactor: router reached max restarts ({}), shutting down",
self.max_restarts
);
ctx.stop_self();
return;
}
if let Err(e) = self.start_worker(ctx, idx) {
eprintln!("swactor: router failed to restart worker {idx}: {e}");
}
}
}

72
src/std/runtime_ext.rs
View file

@ -1,5 +1,5 @@
use crate::Error;
use crate::actor::{ActorAddress, ActorInterface, EnvironmentBuilder, LogicalName, Message};
use crate::actor::{ActorAddress, Message};
use crate::runtime::Runtime;
use super::StdExtension;
@ -14,19 +14,11 @@ fn get_ext(rt: &Runtime) -> &StdExtension {
/// Naming extension for [`Runtime`].
///
/// Provides `spawn_named`, `where_is`, `unregister`, and `registered_names`
/// via the [`StdExtension`] name registry.
/// Provides explicit name registration and lookup via [`StdExtension`]'s name registry.
pub trait RuntimeNaming {
/// Register a name for an already-spawned actor. Returns `Err` if name is taken.
fn register_name(&self, name: impl Into<String>, addr: ActorAddress) -> Result<(), Error>;
/// Spawn an actor with a registered name, returning its address.
fn spawn_named<A: ActorInterface>(
&self,
name: impl Into<String>,
actor: A,
) -> Result<ActorAddress, Error>;
/// Look up an actor address by its registered name.
fn where_is(&self, name: &str) -> Option<ActorAddress>;
@ -42,23 +34,6 @@ impl RuntimeNaming for Runtime {
get_ext(self).name_registry.register(name.into(), addr)
}
fn spawn_named<A: ActorInterface>(
&self,
name: impl Into<String>,
actor: A,
) -> Result<ActorAddress, Error> {
let name = name.into();
let env = EnvironmentBuilder::new()
.set(LogicalName(name.clone()))
.build();
let addr = self.spawn_with_env(actor, env)?;
if let Err(e) = get_ext(self).name_registry.register(name, addr) {
let _ = self.stop_actor(addr);
return Err(e);
}
Ok(addr)
}
fn where_is(&self, name: &str) -> Option<ActorAddress> {
get_ext(self).name_registry.lookup(name)
}
@ -72,31 +47,10 @@ impl RuntimeNaming for Runtime {
}
}
/// Watching extension for [`Runtime`].
///
/// Provides `watch` / `unwatch` via the [`StdExtension`] watch registry.
pub trait RuntimeWatching {
/// Register a watch: `watcher` receives `ActorExited` when `target` dies.
fn watch(&self, watcher: ActorAddress, target: ActorAddress);
/// Cancel a watch.
fn unwatch(&self, watcher: ActorAddress, target: ActorAddress);
}
impl RuntimeWatching for Runtime {
fn watch(&self, watcher: ActorAddress, target: ActorAddress) {
get_ext(self).watch_registry.watch(watcher, target);
}
fn unwatch(&self, watcher: ActorAddress, target: ActorAddress) {
get_ext(self).watch_registry.unwatch(watcher, target);
}
}
/// Group extension for [`Runtime`].
///
/// Provides `join_group`, `leave_group`, `publish_to`, `group_members`,
/// and `groups` via the [`StdExtension`] group registry.
/// Provides runtime-level group membership and publication via [`StdExtension`]'s
/// group registry.
pub trait RuntimeGroups {
/// Add an actor to a named group. The group is created if it doesn't exist.
fn join_group(&self, addr: ActorAddress, group: impl Into<String>);
@ -143,21 +97,3 @@ impl RuntimeGroups for Runtime {
get_ext(self).group_registry.group_names()
}
}
/// Service registry extension for [`Runtime`].
///
/// Allows registering typed service bindings that are automatically injected
/// into every actor's environment at spawn time.
pub trait RuntimeResources {
/// Register a service address under marker type `S`.
///
/// All actors spawned after this call will have `ServiceBinding<S>` in
/// their environment (unless overridden via `spawn_builder`).
fn register_service<S: 'static + Send + Sync>(&self, addr: ActorAddress);
}
impl RuntimeResources for Runtime {
fn register_service<S: 'static + Send + Sync>(&self, addr: ActorAddress) {
get_ext(self).service_registry.register::<S>(addr);
}
}

58
src/std/service_registry.rs
View file

@ -1,58 +0,0 @@
use std::any::{Any, TypeId};
use std::collections::HashMap;
use std::sync::{Arc, RwLock};
use crate::actor::{Environment, EnvironmentBuilder};
/// Stores typed service bindings for injection into actor environments.
///
/// Bindings are registered at the runtime level (e.g., during startup) and
/// automatically injected into every actor's environment via the `on_spawn`
/// hook. Existing environment keys are **not** overwritten — this preserves
/// per-subtree overrides set via `spawn_builder`.
pub struct ServiceRegistry {
bindings: RwLock<HashMap<TypeId, Arc<dyn Any + Send + Sync>>>,
}
impl Default for ServiceRegistry {
fn default() -> Self {
Self::new()
}
}
impl ServiceRegistry {
pub fn new() -> Self {
Self {
bindings: RwLock::new(HashMap::new()),
}
}
/// Register a service binding by marker type `S`.
///
/// Overwrites any previous binding for the same marker type.
pub fn register<S: 'static + Send + Sync>(&self, addr: crate::actor::ActorAddress) {
let binding = crate::actor::ServiceBinding::<S>::new(addr);
let type_id = TypeId::of::<crate::actor::ServiceBinding<S>>();
self.bindings
.write()
.unwrap()
.insert(type_id, Arc::new(binding));
}
/// Merge all registered bindings into an environment, skipping keys
/// that are already present (preserves spawn_builder overrides).
pub fn inject_into(&self, env: Environment) -> Environment {
let bindings = self.bindings.read().unwrap();
if bindings.is_empty() {
return env;
}
let mut builder = EnvironmentBuilder::from_env(&env);
for (&type_id, value) in bindings.iter() {
if !env.contains_type_id(type_id) {
builder.set_raw(type_id, Arc::clone(value));
}
}
builder.build()
}
}

309
src/std/supervisor.rs
View file

@ -1,309 +0,0 @@
use std::sync::Arc;
use crate::Error;
use crate::actor::{ActorAddress, ActorInterface, Ctx, Down, MonitorRef, StopReason};
use super::CtxMonitoring;
use super::ctx_ext::get_ext;
/// How a child should be restarted when it dies.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum RestartPolicy {
/// Always restart, regardless of stop reason.
Permanent,
/// Restart only on abnormal exit (Panicked). Normal stops are final.
Transient,
/// Never restart. The child is removed on any exit.
Temporary,
}
/// Strategy for handling child failures.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum SupervisorStrategy {
/// Only restart the failed child. Other children are unaffected.
OneForOne,
/// Terminate all children and restart them all in spec order.
OneForAll,
/// Terminate children started after the failed child, then restart
/// the failed child and all terminated children in spec order.
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.
pub struct ChildSpec {
/// Unique identifier for this child.
pub id: String,
/// How to restart this child.
pub restart: RestartPolicy,
/// Factory to spawn the child. Called with `&Ctx`, returns the child's address.
pub start: Arc<dyn Fn(&Ctx) -> Result<ActorAddress, Error> + Send + Sync>,
}
impl ChildSpec {
pub fn new(
id: impl Into<String>,
restart: RestartPolicy,
start: impl Fn(&Ctx) -> Result<ActorAddress, Error> + Send + Sync + 'static,
) -> Self {
Self {
id: id.into(),
restart,
start: Arc::new(start),
}
}
}
/// Tracked state for an active child within a supervisor or router.
pub(crate) struct ActiveChild {
pub(crate) addr: ActorAddress,
pub(crate) _monitor_ref: MonitorRef,
}
/// Internal phase for coordinating multi-child restart (OneForAll, RestForOne).
///
/// In `Normal` phase, the supervisor processes Down messages and applies the strategy.
/// When a coordinated restart is needed, it transitions to `Stopping` (sends stop
/// signals, waits for Down confirmations) then restarts all affected children.
enum SupervisorPhase {
/// Normal operation — process Down messages and apply strategy.
Normal,
/// Waiting for children to confirm death before restarting.
Stopping {
/// Children we're still waiting for Down confirmation.
awaiting: Vec<ActorAddress>,
/// Spec indices to restart once all confirmations received.
restart_set: Vec<usize>,
},
}
/// A supervisor actor that manages child actors according to a restart strategy.
///
/// Children are spawned during `on_start`. When a child dies, the supervisor
/// receives a [`Down`] notification via [`ActorInterface::handle_down`] and
/// applies the configured strategy and restart policy.
///
/// # Strategies
///
/// - **OneForOne**: Only the failed child is restarted.
/// - **OneForAll**: All children are stopped, then all restarted in spec order.
/// - **RestForOne**: The failed child and all children started after it are
/// stopped, then restarted in spec order.
///
/// # Restart Intensity
///
/// The supervisor tracks total restarts. When `total_restarts > max_restarts`,
/// the supervisor stops itself (meltdown protection), escalating the failure
/// to its own supervisor if one exists.
///
/// # Example
///
/// ```ignore
/// let sup = Supervisor::new(
/// SupervisorStrategy::OneForOne,
/// 5, // max 5 restarts before meltdown
/// vec![
/// ChildSpec::new("worker", RestartPolicy::Permanent, |ctx| {
/// ctx.spawn(MyWorker::new())
/// }),
/// ],
/// );
/// let sup_addr = rt.spawn(sup)?;
/// ```
pub struct Supervisor {
strategy: SupervisorStrategy,
max_restarts: u32,
specs: Vec<ChildSpec>,
children: Vec<Option<ActiveChild>>,
total_restarts: u32,
phase: SupervisorPhase,
}
impl Supervisor {
pub fn new(strategy: SupervisorStrategy, max_restarts: u32, specs: Vec<ChildSpec>) -> Self {
let children = (0..specs.len()).map(|_| None).collect();
Self {
strategy,
max_restarts,
specs,
children,
total_restarts: 0,
phase: SupervisorPhase::Normal,
}
}
fn start_child(&mut self, ctx: &Ctx, idx: usize) -> Result<(), Error> {
let addr = (self.specs[idx].start)(ctx)?;
let mref = ctx.monitor(addr)?;
get_ext(ctx)
.supervisor_registry
.register(ctx.self_addr(), addr);
self.children[idx] = Some(ActiveChild {
addr,
_monitor_ref: mref,
});
Ok(())
}
fn find_child_idx(&self, addr: ActorAddress) -> Option<usize> {
self.children
.iter()
.position(|c| c.as_ref().is_some_and(|ac| ac.addr == addr))
}
/// Check meltdown intensity — returns true if we should stop.
fn check_intensity(&mut self) -> bool {
self.total_restarts += 1;
self.total_restarts > self.max_restarts
}
/// Try to finish the coordinated restart: restart all children in `restart_set`.
fn finish_restart(&mut self, ctx: &Ctx) {
let restart_set = match &mut self.phase {
SupervisorPhase::Stopping { restart_set, .. } => std::mem::take(restart_set),
_ => return,
};
self.phase = SupervisorPhase::Normal;
for idx in restart_set {
if let Err(e) = self.start_child(ctx, idx) {
eprintln!(
"swactor: supervisor failed to restart child '{}': {}",
self.specs[idx].id, e
);
}
}
}
/// Begin a coordinated restart for the given spec indices.
/// Stops any living children in the set, then waits for their Down messages.
fn begin_coordinated_restart(&mut self, ctx: &Ctx, restart_indices: Vec<usize>) {
let mut awaiting = Vec::new();
for &idx in &restart_indices {
if let Some(child) = self.children[idx].take() {
let _ = ctx.stop_actor(child.addr);
awaiting.push(child.addr);
}
}
if awaiting.is_empty() {
// All children already dead — restart immediately.
for idx in &restart_indices {
if let Err(e) = self.start_child(ctx, *idx) {
eprintln!(
"swactor: supervisor failed to restart child '{}': {}",
self.specs[*idx].id, e
);
}
}
} else {
self.phase = SupervisorPhase::Stopping {
awaiting,
restart_set: restart_indices,
};
}
}
}
impl ActorInterface for Supervisor {
type Incoming = ();
type Response = ();
fn handle(&mut self, _ctx: &Ctx, _msg: ()) {}
fn on_start(&mut self, ctx: &Ctx) {
for idx in 0..self.specs.len() {
if let Err(e) = self.start_child(ctx, idx) {
eprintln!(
"swactor: supervisor failed to start child '{}': {}",
self.specs[idx].id, e
);
}
}
}
fn on_stop(&mut self, ctx: &Ctx) {
for child in self.children.iter().flatten() {
let _ = ctx.stop_actor(child.addr);
}
}
fn handle_down(&mut self, ctx: &Ctx, down: Down) {
// During coordinated restart: track Down confirmations.
if matches!(self.phase, SupervisorPhase::Stopping { .. }) {
// Clear from children tracking
if let Some(idx) = self.find_child_idx(down.addr) {
self.children[idx] = None;
}
// Remove from awaiting list
if let SupervisorPhase::Stopping { awaiting, .. } = &mut self.phase {
awaiting.retain(|a| *a != down.addr);
}
let done = matches!(&self.phase,
SupervisorPhase::Stopping { awaiting, .. } if awaiting.is_empty());
if done {
self.finish_restart(ctx);
}
return;
}
// Normal phase: handle child death.
let Some(idx) = self.find_child_idx(down.addr) else {
return;
};
self.children[idx] = None;
if !self.specs[idx].restart.should_restart(down.reason) {
return;
}
if self.check_intensity() {
eprintln!(
"swactor: supervisor reached max restarts ({}), shutting down",
self.max_restarts
);
ctx.stop_self();
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) {
eprintln!(
"swactor: supervisor failed to restart child '{}': {}",
self.specs[idx].id, e
);
}
}
_ => {
self.begin_coordinated_restart(ctx, restart_indices);
}
}
}
}

46
src/std/supervisor_registry.rs
View file

@ -1,46 +0,0 @@
use std::sync::RwLock;
use crate::AddrMap;
use crate::actor::ActorAddress;
/// Maps supervised children to their supervisor.
///
/// Follows the same pattern as `MonitorRegistry`, `GroupRegistry`, etc.
/// Entries are added in `Supervisor::start_child` and cleaned up on actor death.
pub struct SupervisorRegistry {
/// child_addr → supervisor_addr
children: RwLock<AddrMap<ActorAddress>>,
}
impl Default for SupervisorRegistry {
fn default() -> Self {
Self::new()
}
}
impl SupervisorRegistry {
pub fn new() -> Self {
Self {
children: RwLock::new(AddrMap::default()),
}
}
/// Register a supervisor → child relationship.
pub fn register(&self, supervisor: ActorAddress, child: ActorAddress) {
self.children.write().unwrap().insert(child, supervisor);
}
/// Look up the supervisor of a child actor.
pub fn lookup(&self, child: &ActorAddress) -> Option<ActorAddress> {
self.children.read().unwrap().get(child).copied()
}
/// Remove entries where `dead_addr` is either a child or a supervisor.
pub fn cleanup(&self, dead_addr: &ActorAddress) {
let mut map = self.children.write().unwrap();
// Remove the dead actor as a child
map.remove(dead_addr);
// Remove all children supervised by the dead actor
map.retain(|_, supervisor| supervisor != dead_addr);
}
}

154
src/std/timer_wheel.rs
View file

@ -1,154 +0,0 @@
use std::any::Any;
use crate::actor::{ActorAddress, Message};
use crate::extension::WorkerExtension;
// ─── Cloneable Message Trait ────────────────────────────────────────────────
/// Type-erased cloneable message for interval timers.
/// Since `Message: Clone`, all actor messages implement this.
pub(crate) trait CloneMsg: Send {
fn clone_boxed(&self) -> Box<dyn Any + Send>;
}
impl<M: Message> CloneMsg for M {
fn clone_boxed(&self) -> Box<dyn Any + Send> {
Box::new(self.clone())
}
}
// ─── Timer Request ──────────────────────────────────────────────────────────
/// Timer request from a handler, queued for processing after tick_all.
pub(crate) enum TimerRequest {
/// One-shot: deliver `msg` to `dest` after `ticks` worker ticks.
Once {
dest: ActorAddress,
msg: Box<dyn Any + Send>,
ticks: u64,
},
/// Repeating: deliver a clone of `msg` to `dest` every `period` ticks.
Interval {
dest: ActorAddress,
msg: Box<dyn CloneMsg>,
period: u64,
},
}
// ─── Timer Wheel ────────────────────────────────────────────────────────────
struct OnceTimer {
fire_at: u64,
dest: ActorAddress,
msg: Box<dyn Any + Send>,
}
struct IntervalTimer {
next_fire: u64,
period: u64,
dest: ActorAddress,
msg: Box<dyn CloneMsg>,
}
/// Per-worker tick-counting timer wheel.
///
/// Timers are deterministic (tick-counted, not wall-clock). One-shot timers
/// fire once and are consumed; interval timers fire repeatedly every N ticks.
pub struct TimerWheel {
current_tick: u64,
once_timers: Vec<OnceTimer>,
interval_timers: Vec<IntervalTimer>,
}
impl TimerWheel {
pub fn new() -> Self {
Self {
current_tick: 0,
once_timers: Vec::new(),
interval_timers: Vec::new(),
}
}
/// Advance the tick counter and collect all due timer messages.
fn fire(&mut self) -> Vec<(ActorAddress, Box<dyn Any + Send>)> {
self.current_tick += 1;
let tick = self.current_tick;
let mut result = Vec::new();
// Fire one-shot timers (swap-remove for O(1) removal)
let mut i = 0;
while i < self.once_timers.len() {
if self.once_timers[i].fire_at <= tick {
let timer = self.once_timers.swap_remove(i);
result.push((timer.dest, timer.msg));
} else {
i += 1;
}
}
// Fire interval timers
for timer in &mut self.interval_timers {
if timer.next_fire <= tick {
let msg = timer.msg.clone_boxed();
result.push((timer.dest, msg));
timer.next_fire = tick + timer.period;
}
}
result
}
/// Remove interval timers whose target was just removed from the worker.
fn gc_dead_intervals(&mut self, dead: &[ActorAddress]) {
if dead.is_empty() {
return;
}
self.interval_timers.retain(|t| !dead.contains(&t.dest));
}
fn add_once(&mut self, dest: ActorAddress, msg: Box<dyn Any + Send>, ticks: u64) {
self.once_timers.push(OnceTimer {
fire_at: self.current_tick + ticks,
dest,
msg,
});
}
fn add_interval(&mut self, dest: ActorAddress, msg: Box<dyn CloneMsg>, period: u64) {
let period = period.max(1); // prevent zero-period infinite loop
self.interval_timers.push(IntervalTimer {
next_fire: self.current_tick + period,
period,
dest,
msg,
});
}
}
impl WorkerExtension for TimerWheel {
fn has_pending_work(&self) -> bool {
!self.once_timers.is_empty() || !self.interval_timers.is_empty()
}
fn on_tick(&mut self) -> Vec<(ActorAddress, Box<dyn Any + Send>)> {
if self.once_timers.is_empty() && self.interval_timers.is_empty() {
return Vec::new();
}
self.fire()
}
fn handle_request(&mut self, request: Box<dyn Any + Send>) {
if let Ok(req) = request.downcast::<TimerRequest>() {
match *req {
TimerRequest::Once { dest, msg, ticks } => self.add_once(dest, msg, ticks),
TimerRequest::Interval { dest, msg, period } => {
self.add_interval(dest, msg, period)
}
}
}
}
fn gc_dead(&mut self, dead: &[ActorAddress]) {
self.gc_dead_intervals(dead);
}
}

69
src/std/watch_registry.rs
View file

@ -1,12 +1,10 @@
use std::collections::{HashMap, HashSet};
use std::sync::Mutex;
use parking_lot::Mutex;
use crate::actor::{ActorAddress, ActorExited, ExitReason, ExitValue};
/// Tracks watch relationships between actors.
///
/// Thread-safe via interior `Mutex`. Watch/unwatch operations are rare
/// relative to message sends, so contention is negligible.
pub struct WatchRegistry {
inner: Mutex<WatchState>,
}
@ -35,27 +33,11 @@ impl WatchRegistry {
}
pub fn watch(&self, watcher: ActorAddress, target: ActorAddress) {
let mut state = self.inner.lock().unwrap();
let mut state = self.inner.lock();
state.watchers.entry(target).or_default().insert(watcher);
state.watching.entry(watcher).or_default().insert(target);
}
pub fn unwatch(&self, watcher: ActorAddress, target: ActorAddress) {
let mut state = self.inner.lock().unwrap();
if let Some(set) = state.watchers.get_mut(&target) {
set.remove(&watcher);
if set.is_empty() {
state.watchers.remove(&target);
}
}
if let Some(set) = state.watching.get_mut(&watcher) {
set.remove(&target);
if set.is_empty() {
state.watching.remove(&watcher);
}
}
}
/// Called when an actor dies. Returns (watcher_addr, ActorExited) pairs.
pub fn notify_death(
&self,
@ -63,37 +45,36 @@ impl WatchRegistry {
reason: ExitReason,
exit_value: Option<ExitValue>,
) -> Vec<(ActorAddress, ActorExited)> {
let mut state = self.inner.lock().unwrap();
let notification = ActorExited {
addr: target,
reason,
exit_value,
};
let mut result = Vec::new();
if let Some(watcher_set) = state.watchers.remove(&target) {
for watcher in &watcher_set {
result.push((*watcher, notification.clone()));
if let Some(set) = state.watching.get_mut(watcher) {
set.remove(&target);
if set.is_empty() {
state.watching.remove(watcher);
}
}
let mut state = self.inner.lock();
let watchers = state.watchers.remove(&target).unwrap_or_default();
for watcher in &watchers {
if let Some(targets) = state.watching.get_mut(watcher) {
targets.remove(&target);
}
}
result
watchers
.into_iter()
.map(|watcher| {
(
watcher,
ActorExited {
addr: target,
reason: reason.clone(),
exit_value: exit_value.clone(),
},
)
})
.collect()
}
/// Called when a watcher itself dies. Cleans up all its watching entries.
pub fn cleanup_watcher(&self, watcher: &ActorAddress) {
let mut state = self.inner.lock().unwrap();
let mut state = self.inner.lock();
if let Some(targets) = state.watching.remove(watcher) {
for target in targets {
if let Some(set) = state.watchers.get_mut(&target) {
set.remove(watcher);
if set.is_empty() {
if let Some(watchers) = state.watchers.get_mut(&target) {
watchers.remove(watcher);
if watchers.is_empty() {
state.watchers.remove(&target);
}
}

319
tests/actor_lifecycle.rs
View file

@ -1,13 +1,13 @@
//! Actor Lifecycle Tests — birth, life, death of individual actors.
//!
//! Covers: spawning, on_start, parent-child delegation, graceful stop,
//! panic isolation, dead actor cleanup, watching (ActorExited), and
//! monitoring (Down notifications).
//! panic isolation, dead actor cleanup, and watching (ActorExited).
mod common;
use common::*;
use std::sync::Arc;
use parking_lot::Mutex;
use std::sync::atomic::{AtomicUsize, Ordering};
// ── Local actors ────────────────────────────────────────────────────────────
@ -157,14 +157,13 @@ impl ActorInterface for StopOnTrigger {
/// Watches targets and counts exit notifications via on_actor_exit.
struct ExitWatcher {
exit_count: Arc<AtomicUsize>,
last_reason: Arc<std::sync::Mutex<Option<ExitReason>>>,
last_addr: Arc<std::sync::Mutex<Option<ActorAddress>>>,
last_reason: Arc<Mutex<Option<ExitReason>>>,
last_addr: Arc<Mutex<Option<ActorAddress>>>,
}
#[derive(Clone)]
enum WatcherCmd {
WatchThis(ActorAddress),
UnwatchThis(ActorAddress),
}
impl ActorInterface for ExitWatcher {
@ -173,19 +172,18 @@ impl ActorInterface for ExitWatcher {
fn handle(&mut self, ctx: &Ctx, msg: WatcherCmd) {
match msg {
WatcherCmd::WatchThis(target) => ctx.watch(target),
WatcherCmd::UnwatchThis(target) => ctx.unwatch(target),
}
}
fn on_actor_exit(&mut self, _ctx: &Ctx, exited: ActorExited) {
self.exit_count.fetch_add(1, Ordering::SeqCst);
*self.last_reason.lock().unwrap() = Some(exited.reason);
*self.last_addr.lock().unwrap() = Some(exited.addr);
*self.last_reason.lock() = Some(exited.reason);
*self.last_addr.lock() = Some(exited.addr);
}
}
struct WatcherState {
exit_count: Arc<AtomicUsize>,
last_reason: Arc<std::sync::Mutex<Option<ExitReason>>>,
last_reason: Arc<Mutex<Option<ExitReason>>>,
}
impl WatcherState {
@ -193,14 +191,14 @@ impl WatcherState {
self.exit_count.load(Ordering::SeqCst)
}
fn last_reason(&self) -> Option<ExitReason> {
self.last_reason.lock().unwrap().clone()
self.last_reason.lock().clone()
}
}
fn new_exit_watcher() -> (ExitWatcher, WatcherState) {
let exit_count = Arc::new(AtomicUsize::new(0));
let last_reason = Arc::new(std::sync::Mutex::new(None));
let last_addr = Arc::new(std::sync::Mutex::new(None));
let last_reason = Arc::new(Mutex::new(None));
let last_addr = Arc::new(Mutex::new(None));
let state = WatcherState {
exit_count: exit_count.clone(),
last_reason: last_reason.clone(),
@ -215,43 +213,6 @@ fn new_exit_watcher() -> (ExitWatcher, WatcherState) {
)
}
/// Monitors a target and forwards Down to a reply address.
struct MonitorWatcherActor {
watch_target: ActorAddress,
reply_to: ActorAddress,
mref: Option<MonitorRef>,
}
impl ActorInterface for MonitorWatcherActor {
type Incoming = Down;
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
self.mref = Some(ctx.monitor(self.watch_target).unwrap());
}
fn handle(&mut self, ctx: &Ctx, msg: Down) {
ctx.send(self.reply_to, msg).unwrap();
}
}
/// Demonitors on Ping.
struct DemonitorActor {
watch_target: ActorAddress,
mref: Option<MonitorRef>,
}
impl ActorInterface for DemonitorActor {
type Incoming = Ping;
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
self.mref = Some(ctx.monitor(self.watch_target).unwrap());
}
fn handle(&mut self, ctx: &Ctx, _msg: Ping) {
if let Some(mref) = self.mref.take() {
ctx.demonitor(mref);
}
}
}
/// A silent actor that does nothing (target for watching tests).
struct Sleeper;
#[derive(Clone)]
@ -688,71 +649,37 @@ fn panic_isolation_and_cleanup() {
fn watch_notification_contract() {
let rt = std_runtime(RuntimeConfig::default());
// Spawn target + 3 watchers + 1 that unwatches
let target = rt.spawn(PanicActor).unwrap();
let (w1, s1) = new_exit_watcher();
let (w2, s2) = new_exit_watcher();
let (w3, s3) = new_exit_watcher();
let (w4, s4) = new_exit_watcher(); // will unwatch
let w1_addr = rt.spawn(w1).unwrap();
let w2_addr = rt.spawn(w2).unwrap();
let w3_addr = rt.spawn(w3).unwrap();
let w4_addr = rt.spawn(w4).unwrap();
// All watch the target
rt.send_to(w1_addr, WatcherCmd::WatchThis(target)).unwrap();
rt.send_to(w2_addr, WatcherCmd::WatchThis(target)).unwrap();
rt.send_to(w3_addr, WatcherCmd::WatchThis(target)).unwrap();
rt.send_to(w4_addr, WatcherCmd::WatchThis(target)).unwrap();
tick_n(&rt, 3);
// w2 double-watches (idempotent test)
// w2 double-watches: registration is idempotent.
rt.send_to(w2_addr, WatcherCmd::WatchThis(target)).unwrap();
tick_n(&rt, 3);
// w4 unwatches
rt.send_to(w4_addr, WatcherCmd::UnwatchThis(target))
.unwrap();
tick_n(&rt, 3);
// Kill target
rt.send_to(target, PanicMsg).unwrap();
tick_n(&rt, 5);
assert_eq!(s1.count(), 1, "watcher 1 notified");
assert_eq!(s2.count(), 1, "double-watch still only one notification");
assert_eq!(s3.count(), 1, "watcher 3 notified");
assert_eq!(s4.count(), 0, "unwatched watcher not notified");
assert_eq!(s1.last_reason(), Some(ExitReason::Panicked));
// --- Runtime-level watch ---
let rt = std_runtime(RuntimeConfig::default());
let target = rt.spawn(PanicActor).unwrap();
let (w, s) = new_exit_watcher();
let w_addr = rt.spawn(w).unwrap();
tick_n(&rt, 2);
rt.watch(w_addr, target);
rt.send_to(target, PanicMsg).unwrap();
tick_n(&rt, 5);
assert_eq!(s.count(), 1, "runtime-level watch delivers notification");
}
/// Watch edge cases: watcher dies before target (no crash), self-watch (no
/// crash), watcher reacts to death by spawning a replacement.
#[test]
fn watch_edge_cases() {
// Watcher dies before target — no crash
let rt = std_runtime(RuntimeConfig::default());
let target = rt.spawn(PanicActor).unwrap();
let target2 = rt.spawn(PanicActor).unwrap();
rt.watch(target2, target);
tick_n(&rt, 3);
rt.send_to(target2, PanicMsg).unwrap(); // kill watcher first
tick_n(&rt, 5);
rt.send_to(target, PanicMsg).unwrap(); // kill target — no crash
tick_n(&rt, 5);
// Self-watch — no crash
let rt = std_runtime(RuntimeConfig::default());
let (w, _s) = new_exit_watcher();
@ -804,227 +731,3 @@ fn watch_edge_cases() {
);
}
/// Monitor API contract: Down on stop (Normal) and panic (Panicked), multiple
/// monitors, demonitor cancels, dead watcher cleanup, stacked monitors,
/// external inbox, handle_down dispatch.
#[test]
fn monitor_death_notification_contract() {
let rt = std_runtime(RuntimeConfig::default());
// --- Stop → Down(Normal) ---
let inbox = rt.new_inbox::<Down>().unwrap();
let target = rt.spawn(PingPongActor).unwrap();
rt.spawn(MonitorWatcherActor {
watch_target: target,
reply_to: *inbox.addr(),
mref: None,
})
.unwrap();
rt.tick();
rt.stop_actor(target).unwrap();
tick_n(&rt, 3);
let down = inbox.try_recv().expect("Down on graceful stop");
assert_eq!(down.addr, target);
assert_eq!(down.reason, StopReason::Normal);
// --- Panic → Down(Panicked) ---
let rt = std_runtime(RuntimeConfig::default());
let inbox = rt.new_inbox::<Down>().unwrap();
let target = rt.spawn(PanicActor).unwrap();
rt.spawn(MonitorWatcherActor {
watch_target: target,
reply_to: *inbox.addr(),
mref: None,
})
.unwrap();
rt.tick();
rt.send_to(target, PanicMsg).unwrap();
tick_n(&rt, 3);
let down = inbox.try_recv().expect("Down on panic");
assert_eq!(down.reason, StopReason::Panicked);
// --- Multiple monitors ---
let rt = std_runtime(RuntimeConfig::default());
let inbox1 = rt.new_inbox::<Down>().unwrap();
let inbox2 = rt.new_inbox::<Down>().unwrap();
let target = rt.spawn(PingPongActor).unwrap();
rt.spawn(MonitorWatcherActor {
watch_target: target,
reply_to: *inbox1.addr(),
mref: None,
})
.unwrap();
rt.spawn(MonitorWatcherActor {
watch_target: target,
reply_to: *inbox2.addr(),
mref: None,
})
.unwrap();
rt.tick();
rt.stop_actor(target).unwrap();
tick_n(&rt, 3);
assert!(inbox1.try_recv().is_some(), "watcher 1 notified");
assert!(inbox2.try_recv().is_some(), "watcher 2 notified");
// --- Demonitor cancels ---
let rt = std_runtime(RuntimeConfig::default());
let down_inbox = rt.new_inbox::<Down>().unwrap();
let target = rt.spawn(PingPongActor).unwrap();
let watcher = rt
.spawn(DemonitorActor {
watch_target: target,
mref: None,
})
.unwrap();
rt.tick();
rt.send_to(
watcher,
Ping {
reply_to: ActorAddress::default(),
},
)
.unwrap();
rt.tick(); // demonitor
rt.stop_actor(target).unwrap();
tick_n(&rt, 3);
assert!(
down_inbox.try_recv().is_none(),
"demonitored: no Down delivered"
);
// --- Dead watcher cleaned up ---
let rt = std_runtime(RuntimeConfig::default());
let target = rt.spawn(PingPongActor).unwrap();
let watcher = rt
.spawn(MonitorWatcherActor {
watch_target: target,
reply_to: ActorAddress::default(),
mref: None,
})
.unwrap();
rt.tick();
rt.stop_actor(watcher).unwrap();
rt.tick(); // watcher dies
rt.stop_actor(target).unwrap();
tick_n(&rt, 3); // target dies — no crash trying to deliver to dead watcher
// --- Stacked monitors produce multiple notifications ---
struct DoubleMonitor {
target: ActorAddress,
reply_to: ActorAddress,
}
impl ActorInterface for DoubleMonitor {
type Incoming = Down;
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
ctx.monitor(self.target).unwrap();
ctx.monitor(self.target).unwrap();
}
fn handle(&mut self, ctx: &Ctx, msg: Down) {
ctx.send(self.reply_to, msg).unwrap();
}
}
let rt = std_runtime(RuntimeConfig::default());
let inbox = rt.new_inbox::<Down>().unwrap();
let target = rt.spawn(PingPongActor).unwrap();
rt.spawn(DoubleMonitor {
target,
reply_to: *inbox.addr(),
})
.unwrap();
rt.tick();
rt.stop_actor(target).unwrap();
tick_n(&rt, 3);
assert!(
inbox.try_recv().is_some(),
"first Down from stacked monitor"
);
assert!(
inbox.try_recv().is_some(),
"second Down from stacked monitor"
);
assert!(inbox.try_recv().is_none(), "no more");
// --- handle_down dispatch ---
struct MonitoringTracker {
target: ActorAddress,
downs: Vec<Down>,
inbox: ActorAddress,
}
impl ActorInterface for MonitoringTracker {
type Incoming = Ping;
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
ctx.monitor(self.target).unwrap();
}
fn handle(&mut self, ctx: &Ctx, _msg: Ping) {
let _ = ctx.send(self.inbox, Count(self.downs.len()));
}
fn handle_down(&mut self, _ctx: &Ctx, down: Down) {
self.downs.push(down);
}
}
let rt = std_runtime(RuntimeConfig::default());
let inbox = rt.new_inbox::<Count>().unwrap();
let target = rt.spawn(PanicActor).unwrap();
let tracker = rt
.spawn(MonitoringTracker {
target,
downs: vec![],
inbox: *inbox.addr(),
})
.unwrap();
rt.tick();
rt.send_to(target, PanicMsg).unwrap();
tick_n(&rt, 3);
rt.send_to(
tracker,
Ping {
reply_to: ActorAddress::default(),
},
)
.unwrap();
rt.tick();
assert_eq!(
inbox.try_recv(),
Some(Count(1)),
"handle_down received exactly one Down"
);
// --- When Incoming=Down, handle_down is NOT called ---
struct DownAsIncoming {
target: ActorAddress,
inbox: ActorAddress,
}
impl ActorInterface for DownAsIncoming {
type Incoming = Down;
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
ctx.monitor(self.target).unwrap();
}
fn handle(&mut self, ctx: &Ctx, msg: Down) {
let _ = ctx.send(self.inbox, msg);
}
fn handle_down(&mut self, _ctx: &Ctx, _down: Down) {
panic!("handle_down must not be called when Incoming=Down");
}
}
let rt = std_runtime(RuntimeConfig::default());
let inbox = rt.new_inbox::<Down>().unwrap();
let target = rt.spawn(PanicActor).unwrap();
rt.spawn(DownAsIncoming {
target,
inbox: *inbox.addr(),
})
.unwrap();
rt.tick();
rt.send_to(target, PanicMsg).unwrap();
tick_n(&rt, 3);
let received = inbox
.try_recv()
.expect("Down delivered via handle(), not handle_down");
assert_eq!(received.reason, StopReason::Panicked);
}

7
tests/common/mod.rs
View file

@ -11,12 +11,7 @@ pub use swactor::actor::{
SpawnBuilder, SpawnTimestamp, StopReason,
};
pub use swactor::runtime::{Ctx, Inbox, Runtime, RuntimeConfig};
pub use swactor::std::{
ChildSpec, CtxCapabilities, CtxEnvironment, CtxGroups, CtxHandles, CtxLifecycle, CtxLineage,
CtxMonitoring, CtxNaming, CtxResources, CtxSelfStats, CtxSystem, CtxTimers, CtxWatching,
ResourceHandle, RestartPolicy, Router, RoutingStrategy, RuntimeGroups, RuntimeNaming,
RuntimeResources, RuntimeWatching, StdExtension, Supervisor, SupervisorStrategy,
};
pub use swactor::std::{CtxGroups, CtxWatching, RuntimeGroups, RuntimeNaming, StdExtension};
// ── Messages ────────────────────────────────────────────────────────────────

277
tests/core_extension_seams.rs Normal file
View file

@ -0,0 +1,277 @@
use std::any::Any;
use std::sync::Arc;
use parking_lot::Mutex;
use swactor::actor::{ActorAddress, ActorInterface, Ctx, Environment, EnvironmentBuilder, ExitValue, StopReason};
use swactor::config::RuntimeConfig;
use swactor::extension::{RuntimeExtension, WorkerExtension};
use swactor::runtime::Runtime;
#[derive(Clone, Debug, PartialEq, Eq)]
struct SpawnMarker(&'static str);
#[derive(Clone, Debug, PartialEq, Eq)]
struct SpawnMarkerSeen(Option<&'static str>);
#[derive(Clone, Debug, PartialEq, Eq)]
struct DeathSeen(ActorAddress);
#[derive(Clone, Debug, PartialEq, Eq)]
struct WorkerExtFired;
struct WorkerRequest {
target: ActorAddress,
}
#[derive(Default)]
struct SeamState {
death_report_to: Mutex<Option<ActorAddress>>,
cleaned: Mutex<Vec<ActorAddress>>,
worker_pending: Mutex<Vec<ActorAddress>>,
}
struct SeamExtension {
state: Arc<SeamState>,
inject_spawn_marker: bool,
enable_worker_extension: bool,
}
impl SeamExtension {
fn new(state: Arc<SeamState>) -> Self {
Self {
state,
inject_spawn_marker: false,
enable_worker_extension: false,
}
}
fn with_spawn_marker(mut self) -> Self {
self.inject_spawn_marker = true;
self
}
fn with_worker_extension(mut self) -> Self {
self.enable_worker_extension = true;
self
}
}
impl RuntimeExtension for SeamExtension {
fn on_actor_death(
&self,
dead: &[(ActorAddress, StopReason, Option<ExitValue>)],
) -> Vec<(ActorAddress, Box<dyn Any + Send>)> {
let _ = dead.iter().map(|(_, reason, value)| (reason, value)).count();
let Some(report_to) = *self.state.death_report_to.lock() else {
return Vec::new();
};
dead.iter()
.map(|(addr, _, _)| {
(
report_to,
Box::new(DeathSeen(*addr)) as Box<dyn Any + Send>,
)
})
.collect()
}
fn cleanup_dead(&self, dead: &[ActorAddress]) {
self.state.cleaned.lock().extend_from_slice(dead);
}
fn on_spawn(
&self,
_child: ActorAddress,
_parent: Option<ActorAddress>,
env: Environment,
_uptime_ms: u64,
) -> Environment {
if self.inject_spawn_marker {
EnvironmentBuilder::from_env(&env)
.set(SpawnMarker("from-extension"))
.build()
} else {
env
}
}
fn as_any(&self) -> &dyn Any {
self
}
fn create_worker_extension(&self) -> Option<Box<dyn WorkerExtension>> {
self.enable_worker_extension.then(|| {
Box::new(SeamWorkerExtension {
state: Arc::clone(&self.state),
}) as Box<dyn WorkerExtension>
})
}
}
struct SeamWorkerExtension {
state: Arc<SeamState>,
}
impl WorkerExtension for SeamWorkerExtension {
fn has_pending_work(&self) -> bool {
!self.state.worker_pending.lock().is_empty()
}
fn on_tick(&mut self) -> Vec<(ActorAddress, Box<dyn Any + Send>)> {
self.state
.worker_pending
.lock()
.pop()
.map(|target| {
(
target,
Box::new(WorkerExtFired) as Box<dyn Any + Send>,
)
})
.into_iter()
.collect()
}
fn handle_request(&mut self, request: Box<dyn Any + Send>) {
if let Ok(request) = request.downcast::<WorkerRequest>() {
self.state.worker_pending.lock().push(request.target);
}
}
fn gc_dead(&mut self, dead: &[ActorAddress]) {
self.state
.worker_pending
.lock()
.retain(|target| !dead.contains(target));
}
}
fn tick_n(rt: &Runtime, n: usize) {
for _ in 0..n {
rt.tick();
}
}
struct MarkerReporter {
report_to: ActorAddress,
}
impl ActorInterface for MarkerReporter {
type Incoming = ();
type Response = ();
fn on_start(&mut self, ctx: &Ctx) {
let marker = ctx.env::<SpawnMarker>().map(|marker| marker.0);
ctx.send(self.report_to, SpawnMarkerSeen(marker)).unwrap();
}
fn handle(&mut self, _ctx: &Ctx, _msg: ()) {}
}
#[test]
fn on_spawn_environment_mutation_is_visible_to_actor() {
let state = Arc::new(SeamState::default());
let rt = Runtime::new(RuntimeConfig::default()).with_extension(Arc::new(
SeamExtension::new(Arc::clone(&state)).with_spawn_marker(),
));
let inbox = rt.new_inbox::<SpawnMarkerSeen>().unwrap();
rt.spawn(MarkerReporter {
report_to: *inbox.addr(),
})
.unwrap();
tick_n(&rt, 2);
assert_eq!(
inbox.try_recv(),
Some(SpawnMarkerSeen(Some("from-extension")))
);
}
struct PanicOnPing;
impl ActorInterface for PanicOnPing {
type Incoming = ();
type Response = ();
fn handle(&mut self, _ctx: &Ctx, _msg: ()) {
panic!("intentional seam-test panic");
}
}
#[test]
fn on_actor_death_messages_are_routed() {
let state = Arc::new(SeamState::default());
let rt = Runtime::new(RuntimeConfig::default())
.with_extension(Arc::new(SeamExtension::new(Arc::clone(&state))));
let inbox = rt.new_inbox::<DeathSeen>().unwrap();
*state.death_report_to.lock() = Some(*inbox.addr());
let target = rt.spawn(PanicOnPing).unwrap();
rt.send_to(target, ()).unwrap();
tick_n(&rt, 4);
assert_eq!(inbox.try_recv(), Some(DeathSeen(target)));
}
#[test]
fn cleanup_dead_receives_dead_actor_batch() {
let state = Arc::new(SeamState::default());
let rt = Runtime::new(RuntimeConfig::default())
.with_extension(Arc::new(SeamExtension::new(Arc::clone(&state))));
let target = rt.spawn(PanicOnPing).unwrap();
rt.send_to(target, ()).unwrap();
tick_n(&rt, 4);
assert!(state.cleaned.lock().contains(&target));
}
struct WorkerRequestActor {
target: ActorAddress,
}
impl ActorInterface for WorkerRequestActor {
type Incoming = ();
type Response = ();
fn handle(&mut self, ctx: &Ctx, _msg: ()) {
ctx.raw_inner()
.post_worker_request(Box::new(WorkerRequest { target: self.target }));
}
}
#[test]
fn worker_extension_request_is_handled_and_emits_message() {
let state = Arc::new(SeamState::default());
let rt = Runtime::new(RuntimeConfig::default()).with_extension(Arc::new(
SeamExtension::new(Arc::clone(&state)).with_worker_extension(),
));
let inbox = rt.new_inbox::<WorkerExtFired>().unwrap();
let actor = rt
.spawn(WorkerRequestActor {
target: *inbox.addr(),
})
.unwrap();
rt.send_to(actor, ()).unwrap();
tick_n(&rt, 4);
assert_eq!(inbox.try_recv(), Some(WorkerExtFired));
}
#[test]
fn worker_extension_pending_work_keeps_runtime_progressing() {
let state = Arc::new(SeamState::default());
let rt = Runtime::new(RuntimeConfig::default()).with_extension(Arc::new(
SeamExtension::new(Arc::clone(&state)).with_worker_extension(),
));
let inbox = rt.new_inbox::<WorkerExtFired>().unwrap();
state.worker_pending.lock().push(*inbox.addr());
rt.tick();
assert_eq!(inbox.try_recv(), Some(WorkerExtFired));
}

170
tests/message_delivery.rs
View file

@ -1,7 +1,7 @@
//! Message Routing and Handler Behavior Tests.
//!
//! Covers: routing correctness at scale, send-from-within-handler patterns,
//! address error handling, fairness/budgets, and timers.
//! address error handling, and fairness/budgets.
mod common;
use common::*;
@ -38,59 +38,6 @@ impl ActorInterface for SelfSendActor {
}
}
/// Schedules a one-shot timer in on_start.
struct TimerStartActor {
target: ActorAddress,
delay_ticks: u64,
}
impl ActorInterface for TimerStartActor {
type Incoming = Ping;
type Response = Pong;
fn on_start(&mut self, ctx: &Ctx) {
ctx.send_after_ticks(
self.target,
Ping {
reply_to: ctx.self_addr(),
},
self.delay_ticks,
);
}
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
}
/// Schedules a one-shot timer from a handler.
struct DelayPingPongActor;
impl ActorInterface for DelayPingPongActor {
type Incoming = Forward;
type Response = Done;
fn handle(&mut self, ctx: &Ctx, msg: Forward) {
ctx.send_after_ticks(msg.reply_to, Done(msg.value), 3);
}
}
/// Schedules an interval timer on start.
struct HeartbeatActor {
target: ActorAddress,
period: u64,
}
impl ActorInterface for HeartbeatActor {
type Incoming = Ping;
type Response = Pong;
fn on_start(&mut self, ctx: &Ctx) {
ctx.send_interval_ticks(
self.target,
Ping {
reply_to: ctx.self_addr(),
},
self.period,
);
}
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
}
/// NumberedMsg/Reply for routing correctness tests.
#[derive(Clone)]
struct NumberedMsg {
@ -452,118 +399,3 @@ fn fairness_budget_prevents_starvation() {
);
}
/// One-shot timers fire at the right tick and only once. Interval timers fire
/// repeatedly at the right period. Timers are cleaned up when actors die.
#[test]
fn timer_one_shot_and_interval() {
// One-shot: delay=3 from on_start
let rt = std_runtime(RuntimeConfig::default());
let inbox = rt.new_inbox::<Ping>().unwrap();
rt.spawn(TimerStartActor {
target: *inbox.addr(),
delay_ticks: 3,
})
.unwrap();
rt.tick(); // tick 1: on_start schedules
assert!(inbox.try_recv().is_none(), "no delivery tick 1");
rt.tick(); // tick 2
assert!(inbox.try_recv().is_none(), "no delivery tick 2");
rt.tick(); // tick 3
assert!(inbox.try_recv().is_none(), "no delivery tick 3");
rt.tick(); // tick 4: fires
assert!(inbox.try_recv().is_some(), "timer fires after 3-tick delay");
// One-shot from handler
let rt = std_runtime(RuntimeConfig::default());
let inbox = rt.new_inbox::<Done>().unwrap();
let addr = rt.spawn(DelayPingPongActor).unwrap();
rt.send_to(
addr,
Forward {
value: 42,
reply_to: *inbox.addr(),
},
)
.unwrap();
rt.tick(); // process Forward, schedule timer
assert!(inbox.try_recv().is_none());
rt.tick(); // tick 2
rt.tick(); // tick 3
assert!(inbox.try_recv().is_none());
rt.tick(); // tick 4: fires
assert_eq!(
inbox.try_recv(),
Some(Done(42)),
"delayed reply from handler timer"
);
// One-shot does NOT repeat
let rt = std_runtime(RuntimeConfig::default());
let inbox = rt.new_inbox::<Ping>().unwrap();
rt.spawn(TimerStartActor {
target: *inbox.addr(),
delay_ticks: 1,
})
.unwrap();
rt.tick(); // schedule
rt.tick(); // fires
assert!(inbox.try_recv().is_some(), "first fire");
tick_n(&rt, 5);
assert!(inbox.try_recv().is_none(), "one-shot doesn't repeat");
// Zero-delay fires next tick
let rt = std_runtime(RuntimeConfig::default());
let inbox = rt.new_inbox::<Ping>().unwrap();
rt.spawn(TimerStartActor {
target: *inbox.addr(),
delay_ticks: 0,
})
.unwrap();
rt.tick(); // schedule
assert!(
inbox.try_recv().is_none(),
"not immediate — fires next tick"
);
rt.tick(); // fires
assert!(inbox.try_recv().is_some(), "zero-delay fires next tick");
// Interval: period=2, fires on ticks 3, 5, 7
let rt = std_runtime(RuntimeConfig::default());
let inbox = rt.new_inbox::<Ping>().unwrap();
rt.spawn(HeartbeatActor {
target: *inbox.addr(),
period: 2,
})
.unwrap();
rt.tick(); // tick 1: schedule
assert!(inbox.try_recv().is_none());
rt.tick(); // tick 2
assert!(inbox.try_recv().is_none());
rt.tick(); // tick 3: first fire
assert!(inbox.try_recv().is_some(), "fire on tick 3");
rt.tick(); // tick 4
assert!(inbox.try_recv().is_none());
rt.tick(); // tick 5: second fire
assert!(inbox.try_recv().is_some(), "fire on tick 5");
rt.tick(); // tick 6
assert!(inbox.try_recv().is_none());
rt.tick(); // tick 7: third fire
assert!(inbox.try_recv().is_some(), "fire on tick 7");
// Timer cleanup when target actor dies
let rt = std_runtime(RuntimeConfig::default());
let counter_addr = rt.spawn(CounterActor { count: 0 }).unwrap();
rt.spawn(HeartbeatActor {
target: counter_addr,
period: 1,
})
.unwrap();
tick_n(&rt, 3);
rt.stop_actor(counter_addr).unwrap();
tick_n(&rt, 5);
let stats = rt.stats();
assert_eq!(
stats.workers[0].num_actors, 1,
"only heartbeat actor remains"
);
}

74
tests/proptest_runtime.rs
View file

@ -8,12 +8,9 @@ use std::collections::HashMap;
use proptest::prelude::*;
use proptest_state_machine::{ReferenceStateMachine, StateMachineTest, prop_state_machine};
use std::sync::Arc;
use swactor::actor::{ActorAddress, ActorInterface};
use swactor::config::RuntimeConfig;
use swactor::runtime::{Ctx, Inbox, Runtime};
use swactor::std::{CtxTimers, StdExtension};
// ─── Shared Actor Types ────────────────────────────────────────────────────
@ -114,77 +111,6 @@ proptest! {
);
}
/// One-shot timer fires at exactly the right tick for any delay.
#[test]
fn one_shot_timer_fires_at_correct_tick(delay in 1u64..20) {
let rt = Runtime::new(RuntimeConfig::default())
.with_extension(Arc::new(StdExtension::new()));
let inbox = rt.new_inbox::<Ping>().unwrap();
struct TimerActor { target: ActorAddress, delay: u64 }
impl ActorInterface for TimerActor {
type Incoming = Ping;
type Response = ();
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
fn on_start(&mut self, ctx: &Ctx) {
ctx.send_after_ticks(self.target, Ping(42), self.delay);
}
}
let _addr = rt.spawn(TimerActor { target: *inbox.addr(), delay }).unwrap();
// Tick up to the expected fire tick
for tick in 1..=(delay + 1) {
rt.tick();
let msg = inbox.try_recv();
if tick <= delay {
prop_assert!(msg.is_none(), "Timer fired too early at tick {}", tick);
} else {
prop_assert!(msg.is_some(), "Timer should have fired at tick {}", tick);
}
}
// No second fire (one-shot)
rt.tick();
prop_assert!(inbox.try_recv().is_none(), "One-shot timer fired twice");
}
/// Interval timer fires at correct periodic ticks for any period.
#[test]
fn interval_timer_fires_at_correct_period(period in 1u64..10) {
let rt = Runtime::new(RuntimeConfig::default())
.with_extension(Arc::new(StdExtension::new()));
let inbox = rt.new_inbox::<Ping>().unwrap();
struct IntervalActor { target: ActorAddress, period: u64 }
impl ActorInterface for IntervalActor {
type Incoming = Ping;
type Response = ();
fn handle(&mut self, _ctx: &Ctx, _msg: Ping) {}
fn on_start(&mut self, ctx: &Ctx) {
ctx.send_interval_ticks(self.target, Ping(1), self.period);
}
}
let _addr = rt.spawn(IntervalActor { target: *inbox.addr(), period }).unwrap();
// Verify 3 consecutive fires
let mut fire_count = 0;
// Timer scheduled on tick 1 (on_start). First fire at tick 1+period.
for tick in 1..=(period * 3 + 2) {
rt.tick();
if let Some(_) = inbox.try_recv() {
fire_count += 1;
// First fire should be at tick (period + 1)
// Subsequent fires every `period` ticks after that
let expected_tick = period + 1 + (fire_count - 1) * period;
prop_assert_eq!(tick, expected_tick,
"Fire #{} at wrong tick (period={})", fire_count, period);
}
}
prop_assert!(fire_count >= 3, "Expected 3+ fires, got {} (period={})", fire_count, period);
}
/// Spawn N actors and verify all get unique addresses and appear in stats.
#[test]
fn spawn_n_actors_all_tracked(n in 1usize..50) {

5008
tests/std_extension.rs
View file

File diff suppressed because it is too large Load diff