diff --git a/.github/workflows/verification.yml b/.github/workflows/verification.yml index 27e0d137..f3fa506e 100644 --- a/.github/workflows/verification.yml +++ b/.github/workflows/verification.yml @@ -36,10 +36,14 @@ jobs: select: --only 'MCLifecycle*' - leg: deferred select: --only 'MCDeferred*' + - leg: dynamic-safety + select: --only 'MCDynamicSupervisor,MCDynamicSupervisorBackoff,MCDynamicSupervisorZero,MCDynamicSupervisorThree' + - leg: dynamic-liveness + select: --only 'MCDynamicSupervisorCallers,MCDynamicSupervisorLive,MCDynamicSupervisorAbort' - leg: start select: --only 'MCStart*' - leg: other - select: --exclude 'MCSupervision,MCLifecycle*,MCDeferred*,MCStart*' + select: --exclude 'MCSupervision,MCLifecycle*,MCDeferred*,MCDynamicSupervisor*,MCStart*' steps: - uses: actions/checkout@v4 - uses: DeterminateSystems/nix-installer-action@v16 @@ -114,6 +118,10 @@ jobs: - MCLifecycleWideDeep - MCLifecycleLiveDeep - MCLifecycleDeep + - MCDynamicSupervisorDeep + - MCDynamicSupervisorWideDeep + - MCDynamicSupervisorBackoffDeep + - MCDynamicSupervisorCallersDeep - MCStartDeep steps: - uses: actions/checkout@v4 diff --git a/CHANGELOG.md b/CHANGELOG.md index 22f39dfc..e2053c34 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -205,6 +205,25 @@ gauges into a CSV, fails on growth per hour after warm-up or on any count not returning to its baseline after quiesce, and has a `--inject-leak` negative control. Run it before each release (`docs/TESTING.md`). +- Design (not implementation) for rank 12a, the dynamic supervisor + (`DynamicSupervisor` / `simple_one_for_one`, PR #245): + `docs/design/dynamic-supervisor.md`, the ethrex/ethlambda client mapping + and the `DynamicSupervisor` TLA+ model (per-PR, zero-budget and weekly + configurations). Revision 2 applies the maintainer's decisions (OTP-style + serialised starts, Elixir's 3-in-5 s budget with opt-in backoff, + `Shutdown` on exhaustion, arguments returned on rejection) and both + reviews (stuck-child isolation, reservation protocol, history-based + invariants), with 27 named negative controls. Revision 3 applies the + second reviews and the round-two decisions: one FIFO operation queue, + terminate lookup when the loop handles the call, stuck classification by + exit reason, caller liveness without assuming cleanup ends, `ignore`, a + trace-validation test plan, a fenced `terminate_slot(.., expect)` for + introspection, the shared shapes with unified start (#259: + `StartOutcome>`, `ChildStartError`, `Init::continue_with`, + `StartOptions`), and 41 negative controls. Round 3: slot finalization + and ignored-attempt cleanup kept in the model, FIFO checked at selection, + queued terminate calls `Stopped` at shutdown, mempool reservations held by + an owning registration, 44 negative controls; approved for implementation. - Determinism D1-D3 (priority tier 3). Under `--cfg spawned_sim`: wall-clock and OS-entropy reads made inside a simulated run return virtual diff --git a/ROADMAP.md b/ROADMAP.md index 2931b4e0..582ba9fc 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -744,7 +744,7 @@ the first start (semantics §11; found reviewing #233). Behaviour change: extend | 11a | Design inputs to rank 11: promise pipelining and transactional turns | Decide within the rank 11 design, not as a separate API: (1) whether a pipelined send ("on reply to R, send M to the target R names") is expressible without an extra handler turn, with M failing like R rather than being dropped (E/Cap'n Proto/Goblins pipelining; the main latency tool if rank 44 ever ships); (2) whether deferred replies and completions are sent at the end of a turn or immediately, and an opt-in Goblins-style transactional turn that holds a handler's sends until it returns and discards them on panic (state rollback only for snapshot-able state; external effects are never rolled back); (3) whether per-turn snapshots can serve ranks 21 and 30 too. The rank 11 TLA+ model must cover a reply sent by a turn that then panics. See [request semantics references](docs/research/request-semantics-references.md); STM's "effects only on commit" is the same idea restricted to one actor, while its `retry` is selective receive and stays out ([STM note](docs/research/concurrency-models.md#5-software-transactional-memory)). | | 11b | Managed compute pool (CPU offload with pipe-to-self) | **Client evidence:** ethrex's four hand-built rayon pools, 50 `spawn_blocking` calls and the L2 import deadlock at 0% CPU (535647e45); synchronous cell serving that occupied every runtime worker (d958dcba4); ethlambda's hand-owned aggregation worker and semaphore-bounded, `catch_unwind`-guarded gossip checks ([evidence](docs/research/concurrency-models.md#who-uses-it)). One bounded CPU pool per `ActorSystem` or group, never on Tokio workers; `ctx.compute(job, map)` (name illustrative) delivers the result to the submitting actor as a message; per-actor and per-pool admission caps that reject at once or follow rank 17; cancellation tied to owner stop, restart and scope close (rank 15a) with generation fencing; a panic becomes an error message, exactly once; metrics for queue depth, wait, run time and rejections. Document that jobs must not wait on their own pool and gang jobs need a dedicated pool. Rayon behind a feature first; a fixed native pool as the alternative. Built on rank 11's completion contract; shares admission design with rank 34. Prior art: Akka dispatchers, Orleans `Task.Run`, Ray tasks, BEAM dirty schedulers ([concurrency models](docs/research/concurrency-models.md#1-cpu-parallel-compute-pools-integrated-with-actors)). | | 12 | Scoped, lifecycle-owned registries | **Client evidence:** ethrex's per-peer connection map and its `ConnectionId` guard (#7435). Keyed registration that owns the actor's lifetime, with generations so an old cleanup cannot remove its replacement. Also scope the registry to an `ActorSystem` instead of the process-global static, so parallel tests and multi-node simulations do not share names. Prerequisite for groups/pub-sub. Orleans keeps the same one-live-instance-per-key invariant ([virtual actors](docs/research/virtual-actors.md#what-it-means-for-spawned)). | -| 12a | Dynamic supervisor (`DynamicSupervisor` / `simple_one_for_one`) | **Client evidence:** ethrex starts one connection actor per peer at runtime and cleans it up by hand (see [per-key actor maps](#client-search-results)); today's `Supervisor` only owns the fixed child list declared at build time. Proposed contract: children are started at runtime from one `ChildSpec` template with per-call arguments, sharing its restart mode (Elixir-style heterogeneous specs only if a user needs them). The restart budget is supervisor-wide, as in OTP: exhausting it fails the supervisor and escalates to its parent, so a flapping child cannot restart forever. `max_children` counts restarting children, so a new start cannot take a slot mid-restart, and rejects with a typed error rather than queueing. `start_child` after shutdown begins is rejected, never dropped or leaked. Explicitly stopping a child does not restart it. Shutdown stops all live children concurrently under one supervisor deadline (OTP does not order dynamic children; sequential stops would multiply per-child timeouts). Usable inside a nested tree. Independent of rank 12 (`start_child` returns a handle); when combined, a restarted child re-registers under a new generation so an old cleanup cannot remove it. Planned after v0.7, not part of it; extend the TLA+ model (start/stop racing restart and shutdown, cap including restarting children) before release, as for OneForAll/RestForOne. The other OTP variants stay out: `Task.Supervisor` folds into ranks 11/15, `PartitionSupervisor` is sharding, and significant children/`auto_shutdown` wait for a user. **Research ([supervision models](docs/research/supervision-models.md)):** counting restarting children against `max_children` goes beyond Elixir; add `terminate_child` (stop without restart; today an individually stopped Permanent child is restarted) and consider it on static supervisors too. Significant children/`auto_shutdown` would be a trigger for draining (rank 13). Document why Spawned's default budget (5 restarts in 30 s) is looser than OTP's (1 in 5 s): per-child backoff already spreads restarts. Non-goals: an Akka-style Resume directive (keep state after a failure) and buffering messages during backoff, because references are instance-bound. | +| 12a | Dynamic supervisor (`DynamicSupervisor` / `simple_one_for_one`) | **Design in review** (PR #245, not implemented): [design contract](docs/design/dynamic-supervisor.md), [client mapping](docs/design/dynamic-supervisor-client-mapping.md), TLA+ model `DynamicSupervisor.tla` (starts racing crashes, restarts, `terminate_child`, `max_children`, budget exhaustion and shutdown) with 27 negative controls; revision 2 settles the open questions as OTP/Elixir (serialised starts, 3 restarts in 5 s with opt-in backoff, `Shutdown` on exhaustion) and isolates children stuck while retiring. Follow-ups: static nested supervisors exit `Shutdown` on exhaustion, static `terminate_child`. Registry-owned lookup stays in rank 12. **Client evidence:** ethrex starts one connection actor per peer at runtime and cleans it up by hand (see [per-key actor maps](#client-search-results)); today's `Supervisor` only owns the fixed child list declared at build time. Proposed contract: children are started at runtime from one `ChildSpec` template with per-call arguments, sharing its restart mode (Elixir-style heterogeneous specs only if a user needs them). The restart budget is supervisor-wide, as in OTP: exhausting it fails the supervisor and escalates to its parent, so a flapping child cannot restart forever. `max_children` counts restarting children, so a new start cannot take a slot mid-restart, and rejects with a typed error rather than queueing. `start_child` after shutdown begins is rejected, never dropped or leaked. Explicitly stopping a child does not restart it. Shutdown stops all live children concurrently under one supervisor deadline (OTP does not order dynamic children; sequential stops would multiply per-child timeouts). Usable inside a nested tree. Independent of rank 12 (`start_child` returns a handle); when combined, a restarted child re-registers under a new generation so an old cleanup cannot remove it. Planned after v0.7, not part of it; extend the TLA+ model (start/stop racing restart and shutdown, cap including restarting children) before release, as for OneForAll/RestForOne. The other OTP variants stay out: `Task.Supervisor` folds into ranks 11/15, `PartitionSupervisor` is sharding, and significant children/`auto_shutdown` wait for a user. **Research ([supervision models](docs/research/supervision-models.md)):** counting restarting children against `max_children` matches Elixir, which keeps a restarting child in its map (corrected by the design; this said it went beyond Elixir); add `terminate_child` (stop without restart; today an individually stopped Permanent child is restarted) and consider it on static supervisors too. Significant children/`auto_shutdown` would be a trigger for draining (rank 13). The dynamic supervisor uses Elixir's defaults (3 restarts in 5 s, no backoff unless configured). Non-goals: an Akka-style Resume directive (keep state after a failure) and buffering messages during backoff, because references are instance-bound. | | 13 | Coordinated shutdown and bounded draining | Ordered stop exists; add explicit draining as a policy: close admission, handle queued work by policy, join helpers and report unfinished work. Standalone scopes currently use reverse admission order; explore declared dependencies with cycle/unknown-edge rejection and model-checked deadline propagation. Keep current stop/discard as the default. Design with rank 15a: draining is closing the actor's scope under its deadline. Keep "stuck cleanup fails the tree" instead of OTP's `brutal_kill`; add only reporting of unfinished work ([supervision models](docs/research/supervision-models.md)). | | 14 | Separate fair control path | Part of supervision/shutdown design; defer a generic public priority API. Non-trapping actors already receive abnormal exits through cancellation; queued `ExitEnvelope` only matters for trapping actors. Specify boundedness and per-sender ordering for startup, monitor and trapped-exit events. Priority cannot preempt a running handler or starve user work. | | 15 | Actor-owned helper completion scopes | **Client evidence:** ethlambda hand-owns its aggregation worker; add cancel-previous, generation fencing and join-with-deadline. Managed helpers require ActorSystem; explore standalone ownership without detached fallback or changing actor-join guarantees implicitly. Gate new helper registration, cancel, then explicitly join; helpers depending on their stopped owner can deadlock. | diff --git a/docs/TESTING.md b/docs/TESTING.md index 1d7fd39c..fd41ee6e 100644 --- a/docs/TESTING.md +++ b/docs/TESTING.md @@ -177,7 +177,7 @@ Status of each layer. "Planned" items are tracked in the | Layer | Tool | Catches | Status | |---|---|---|---| -| Design | TLA+ and TLC | Holes in lifecycle, restart and shutdown rules | `Supervision`, `Cohorts`, `NestedSupervision` and `Coordinator` models in `verification/tla`, run in CI | +| Design | TLA+ and TLC | Holes in lifecycle, restart and shutdown rules | `Supervision`, `Cohorts`, `NestedSupervision` and `Coordinator` models in `verification/tla`, run in CI; design models `Lifecycle` (v0.8 exit signals), `DeferredReplies`/`DeferredJobs` (rank 11) and `DynamicSupervisor` (rank 12a), each with named negative controls | | Design, unbounded depth | Apalache inductive invariants | An invariant that a state TLC never reached would break | Safety invariants of all four models proven inductive at fixed sizes, with negative controls; `tla-apalache` CI job | | Design, any size | TLAPS or Veil | An invariant that fails only for larger configurations | Planned ([verification tools](research/verification-tools.md)) | | Spec and code | Trace validation | The implementation doing something the model forbids | Real OneForOne, cohort and nested traces plus invalid-trace and model-mutation controls | @@ -1263,6 +1263,18 @@ model. Hand-edited traces are rejected at the edited event. Trace validation found one model gap (a running child may exit with `Shutdown` while the supervisor is open, via `ChildHandle::shutdown`); no implementation deviation. +`verification/tla/DynamicSupervisor.tla` models the rank 12a design (not +implemented, revision 3): OTP's serialised control loop with one FIFO queue, +`start_child` and `terminate_child` racing crashes, restarts, `max_children`, +the budget reservation protocol, ignore, stuck children and shutdown. TLC +checks 23 safety invariants, two action properties and five liveness +properties (callers answered even if cleanup never ends; shutdown and +recovery complete when it does). Six configurations run on every PR and one +weekly; 44 named negative controls each fail their property. The design's +[test plan](design/dynamic-supervisor.md#test-plan-relating-the-model-to-the-code) +specifies the trace events and trace-validation tests the implementation +must ship. + Apalache checks that the safety invariants of `Supervision`, `Cohorts`, `NestedSupervision` and `Coordinator` are inductive (`Init => IndInv`, `IndInv /\ Next => IndInv'`), so they hold at any depth, for the configured diff --git a/docs/design/README.md b/docs/design/README.md index 98ef6283..4b96466f 100644 --- a/docs/design/README.md +++ b/docs/design/README.md @@ -19,6 +19,14 @@ Active design contracts. Usage is documented in the [guide](../GUIDE.md). implemented) for exit signals, `Killed`/`NoProc`, supervisor startup and runtime-dropped actors as in OTP (ROADMAP ranks 5e, 5f, 5g), with the base actor lifecycle model `Lifecycle.tla`. +- **[dynamic-supervisor.md](dynamic-supervisor.md)** (rank 12a, approved for + implementation after review round 3, not implemented): OTP's `simple_one_for_one` / Elixir's + `DynamicSupervisor`: runtime `start_child` from a typed template, + `terminate_child`, `max_children` counting restarting children, a + supervisor-wide budget and concurrent shutdown. Model: + `verification/tla/DynamicSupervisor.tla`. Client mapping (ethrex's + per-peer connections): [dynamic-supervisor-client-mapping.md](dynamic-supervisor-client-mapping.md). + - **[introspection.md](introspection.md)** (0.9, design in review, not implemented): `info()` readable while a handler is wedged, `get_state`/`get_status` between turns, supervision and system snapshots, diff --git a/docs/design/dynamic-supervisor-client-mapping.md b/docs/design/dynamic-supervisor-client-mapping.md new file mode 100644 index 00000000..120c22ea --- /dev/null +++ b/docs/design/dynamic-supervisor-client-mapping.md @@ -0,0 +1,338 @@ +# Dynamic supervisor: client mapping + +Companion to the [dynamic supervisor design](dynamic-supervisor.md) (ROADMAP +rank 12a). Maps the one runtime-spawned actor population in the clients, +ethrex's per-peer connection actors, onto the proposed API, and records that +ethlambda has none. Sketches are illustrative, not patches; nothing in either +client was changed. + +Revisions read (source reading only, nothing built or run): + +| Repository | Ref | Commit | spawned | +|---|---|---|---| +| ethrex | `main` | [`fd5c57dd`](https://github.com/lambdaclass/ethrex/tree/fd5c57ddada097952660f6b749c739119e4de852) | 0.5.0 | +| ethrex | `spawned-v0.7` | [`0dd4c105`](https://github.com/lambdaclass/ethrex/tree/0dd4c105f65d544b0fb5e92d8634a1699127f826) | 0.7.3 | +| ethrex | PR [#7435](https://github.com/lambdaclass/ethrex/pull/7435) (`ConnectionId` guard) | merge [`fc44a9fb`](https://github.com/lambdaclass/ethrex/commit/fc44a9fb25451a17656e88e8e15b4443f747f661) | | +| ethlambda | `main` | [`c3f5f566`](https://github.com/lambdaclass/ethlambda/tree/c3f5f566cb3a61e3d388c66ce21794c18a6618ce) | 0.5.0 | +| ethlambda | `spawned-v0.7` | [`6a12bc75`](https://github.com/lambdaclass/ethlambda/tree/6a12bc753ae18c9d63f3dbf930edc700c4c4704c) | 0.7.3 | + +`crates/networking/p2p/rlpx/connection/server.rs` and `handshake.rs` are +identical on both ethrex branches; their links below use `spawned-v0.7`. +Short forms: **V** = `https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826`, +**M** = `https://github.com/lambdaclass/ethrex/blob/fd5c57ddada097952660f6b749c739119e4de852`. + +## ethrex today + +### Who starts connections + +One `PeerConnectionServer` actor per TCP connection, started with a bare +`.start()` (unmanaged, S6) and owned by nothing: + +- **Accept:** `PeerConnection::spawn_as_receiver(context, peer_addr, stream, permit)` + ([V server.rs:191-209](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/rlpx/connection/server.rs#L191-L209)), + called from the accept loop `serve_p2p_requests`, which discards the result + ([V network.rs:253-290](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/network.rs#L253-L290)). +- **Dial:** `PeerConnection::spawn_as_initiator(context, &node)` + ([V server.rs:211-224](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/rlpx/connection/server.rs#L211-L224)), + called by the `RLPxInitiator` actor + ([V initiator.rs:91-120](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/rlpx/initiator.rs#L91-L120)), + result also discarded. + +```rust +// server.rs:191-224 (both branches) +pub fn spawn_as_receiver(context: P2PContext, peer_addr: SocketAddr, stream: TcpStream, + admission_permit: tokio::sync::OwnedSemaphorePermit) -> PeerConnection { + let state = ConnectionState::Receiver(Receiver { context, peer_addr, stream: Arc::new(stream) }); + let connection = PeerConnectionServer { state, _admission_permit: Some(admission_permit) }; + Self { handle: connection.start() } +} +pub fn spawn_as_initiator(context: P2PContext, node: &Node) -> PeerConnection { + let state = ConnectionState::Initiator(Initiator { context, node: node.clone() }); + // Outbound dials are not admission-capped (we initiate them); inbound is the attack surface. + let connection = PeerConnectionServer { state, _admission_permit: None }; + Self { handle: connection.start() } +} +``` + +On `spawned-v0.7` the singletons (peer table, initiator, broadcaster, +subscription manager) moved onto an `ActorSystem` group and discovery under a +OneForOne supervisor, but connections did not; the comment says why: +"Per-connection actors (`PeerConnectionServer`) are not admitted: they are +created and dropped per peer, and the system only owns a fixed set" +([V initializers.rs:1041-1042](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/cmd/ethrex/initializers.rs#L1041-L1042)). +So connections run on whatever runtime is current at the call site, and +system shutdown does not stop them. + +### How they are tracked + +After the handshake the connection registers itself with the peer table, +`IndexMap` +([V peer_table.rs:546](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/peer_table.rs#L546)), +passing its own `ActorRef` and a `ConnectionId` +([server.rs:1074-1101](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/rlpx/connection/server.rs#L1074-L1101)). +The first connection to a node wins; a duplicate gets `false`, sends +Disconnect(AlreadyConnected) and stops. + +`ConnectionId` is a process-global counter added by #7435 after a duplicate +connection's cleanup removed the live entry +([server.rs:176-188](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/rlpx/connection/server.rs#L176-L188)): + +```rust +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct ConnectionId(u64); +impl ConnectionId { + pub(crate) fn next() -> Self { + static NEXT: std::sync::atomic::AtomicU64 = std::sync::atomic::AtomicU64::new(0); + Self(NEXT.fetch_add(1, std::sync::atomic::Ordering::Relaxed)) + } +} +``` + +### How they are cleaned up + +Nothing monitors or links a connection. It reports its own death from its +`stopped()` hook +([server.rs:623-671](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/rlpx/connection/server.rs#L623-L671)): + +```rust +// The peer table removes the node only if it lists this connection for it, so +// a duplicate connection to an already-connected node leaves the live one +// listed. Sent even when registration failed: a registration the peer table +// applied after this connection stopped waiting for it is undone here. +if let Err(e) = established_state.peer_table.remove_peer( + established_state.node.node_id(), + established_state.connection_id, +) { debug!("Failed to remove peer from table: {e}"); } +if established_state.registered_in_peer_table + && let Err(e) = established_state.tx_broadcaster.remove_peer(established_state.node.node_id()) +{ debug!("Failed to remove peer from tx broadcaster: {e}"); } +established_state.teardown().await; +``` + +and the table checks the guard +([V peer_table.rs:693-711](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/peer_table.rs#L693-L711)): + +```rust +if let Some(peer) = self.peers.get(&msg.node_id) { + if peer.connection_id != Some(msg.connection_id) { return; } + self.peers.swap_remove(&msg.node_id); +} +self.sessions.remove(&msg.node_id); +``` + +Gaps in this scheme: + +- If `stopped()` does not run, the entry is never removed. Today that is a + panic in `started()`; under v0.8 it is also a kill, an untrapped exit + signal and the supervisor's or system's shutdown of a non-trapping actor + (exit-signals design, decision 2). +- A registration that timed out on the connection side but was applied by + the table is undone only because `stopped()` sends `remove_peer` + unconditionally; the comment above exists for this case. +- At node shutdown nothing stops connections; their `remove_peer` sends fail + silently once the table is gone ([V shutdown.rs:81-153](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/cmd/ethrex/shutdown.rs#L81-L153) + stops the system's actors only). + +### Limits + +- Inbound: a semaphore of `MAX_INBOUND_CONNECTIONS = 150` + ([V network.rs:68](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/network.rs#L68)), + `try_acquire_owned()` in the accept loop; when full the stream is dropped + before any actor exists. The permit lives in actor state + (`_admission_permit`) and is released when the state drops. +- Outbound dials are not capped by it; `target_peers` (100) gates dialing and + registration (`TooManyPeers`). + +### Restarts + +None. A dead connection is removed; the node may be re-dialed later through +discovery. In supervision terms every connection is **Temporary**. + +## Mapping + +Revision 2 of the design changes three things for ethrex: the supervisor +serialises starts like OTP (so the RLPx handshake must leave `started()`), +rejections return the arguments, and a connection whose cleanup gets stuck +fails only itself. + +| ethrex today | With the dynamic supervisor | +|---|---| +| `.start()`, unmanaged, on the caller's runtime | `start_child(args)` on a `DynamicSupervisor`, placed on the `p2p` group | +| handshake inside `started()` (up to `HANDSHAKE_TIMEOUT`, 10 s) | **required change:** the handshake moves to the post-start continuation of the unified-start design (0.9, OTP's `handle_continue`): it runs right after `started()` returns and before any message, still under `HANDSHAKE_TIMEOUT`, and a failure ends the actor (a Temporary exit, not a start failure). Otherwise one silent peer would hold the supervisor's control loop, and with it every accept and dial, for the whole `startup_timeout`. A self-sent first message is not equivalent: a message enqueued by another actor first would run before it. The continuation precedes messages but cannot prevent termination: `terminate_child` or shutdown can end the connection before or during the handshake, which then ends it without registering in the peer table (nothing to clean up there) | +| no owner; shutdown does not stop connections | the supervisors are owned by the system, nested under the p2p supervisor (recommended) or as roots admitted after the peer table; connections stop before the table, all at once, each killed after its `shutdown_timeout` | +| `Semaphore(150)` plus `_admission_permit` in actor state | `max_children = Some(150)` on an inbound supervisor; `Rejected { MaxChildren, args }` returns the `ConnArgs`, so the accept loop can still send an RLPx Disconnect or just drop the stream, as today | +| outbound uncapped | a second supervisor for dials without `max_children` | +| `ConnectionId` (process-global counter) | the table's `MonitorRef` (or the connection's `ActorId`, never reused, M4) | +| `stopped()` sends `remove_peer(node_id, connection_id)` | the peer table monitors the connection when it registers it; `Handler` removes the entry only if it still holds that monitor. `Down` arrives exactly once whatever ends the actor (X1), including kills and a skipped `stopped()` | +| timed-out registration undone by an unconditional `remove_peer` | the table's monitor fires for that registration too; a monitor installed after the connection died gets `Down { NoProc }` at once (E4) | +| connections never restarted | `DynamicChildSpec::temporary(..)`, chosen deliberately over the Permanent default: a dropped peer must not be redialled by the supervisor (the TCP stream is gone and discovery decides whom to dial), so the connection is one-shot. No restarts, no budget use, arguments (the `TcpStream`, the `Node`) moved without `Clone` | +| first-wins on duplicates | unchanged: domain policy in the table (rank 12 may later own it) | +| `teardown()` and `tx_broadcaster.remove_peer` in `stopped()` | moved to owners that act on the `Down` (below): `stopped()` is skipped for a non-trapping connection on `terminate_child`, on shutdown and after a kill | +| raw `tokio::spawn` outbound writer holding the socket sink ([server.rs:1530-1557](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/rlpx/connection/server.rs#L1530-L1557)) | **required change:** an owned helper (`ctx.spawn_helper`), cancelled at exit and joined within the cleanup deadline, with an explicit policy for frames still queued (drop them; the peer is being disconnected). Until then the writer can outlive the actor and keep the socket open after the supervisor freed the slot, so `max_children` would bound slots, not sockets | + +### After (sketch) + +```rust +// Wiring (initializers.rs): nested under the p2p supervisor, so a failure +// of the connection supervisor is restarted instead of disabling accepts. +let inbound = p2p_tree.add_dynamic_supervisor(DynamicSupervisorSpec::new( + "rlpx-inbound", + DynamicSupervisorConfig { max_children: Some(MAX_INBOUND_CONNECTIONS), ..Default::default() }, + DynamicChildSpec::temporary("rlpx-inbound", &p2p_group, |_ctx, args: ConnArgs| async move { + Ok::<_, Infallible>(PeerConnectionServer::new(args)) + }) + .shutdown_timeout(Duration::from_secs(2)), +))?; +// `outbound` likewise, without max_children. + +// Accept loop (network.rs): the semaphore and the permit plumbing go away. +// start_child resolves as soon as started() returns, which is now immediate. +match inbound.current()?.start_child(ConnArgs::receiver(context.clone(), peer_addr, stream)).await { + Ok(_) => {} + Err(StartChildError::Rejected { reason: RejectReason::MaxChildren, args }) => { + debug!(peer = %peer_addr, "Inbound connection cap reached"); + drop(args); // closes the stream, as today + } + Err(e) => debug!(peer = %peer_addr, "Inbound connection not started: {}", e.without_args()), +} + +// Connection actor (server.rs): the handshake leaves started(). +// Handshake as the post-start continuation (unified start #259, 0.9): +// runs after the readiness commit and before any message. +async fn started(&mut self, _ctx: &Context) -> Init { + Init::continue_with(Handshake) +} +impl Handler for PeerConnectionServer { + async fn handle(&mut self, _: Handshake, ctx: &Context) { /* existing handshake code */ } +} + +// Peer table (peer_table.rs): registration installs the monitor... +async fn handle_new_connected_peer(&mut self, msg: NewConnectedPeer, ctx: &Context) -> bool { + let id = msg.node.node_id(); + if self.peers.contains_key(&id) { return false; } + let monitor = ctx.monitor(&msg.connection.handle.child_handle()); + self.by_monitor.insert(monitor, id); + self.peers.insert(id, PeerData::new(/* … */).with_monitor(monitor)); + true +} +// ...and removal is the Down, guarded by the entry's own monitor (agy 8): +impl Handler for PeerTableServer { + async fn handle(&mut self, down: Down, _ctx: &Context) { + let Some(id) = self.by_monitor.remove(&down.monitor_ref) else { return }; + if self.peers.get(&id).is_some_and(|p| p.monitor == down.monitor_ref) { + self.peers.swap_remove(&id); + self.sessions.remove(&id); + self.on_connection_gone(id, down.monitor_ref); // see "Skipped teardown" + } + } +} +``` + +### Skipped teardown: who releases what + +`stopped()` does not run for a non-trapping connection that is terminated, +shut down or killed (v0.8, decision 2), and `trap_exit` does not cover a +kill. So each resource the hook releases today needs an owner whose +lifetime covers it. Two kinds: + +- **Records an actor keeps in its own state** (peer-table entries, the + broadcaster's index) live and die with that actor. Their owner monitors + the connection and releases on `Down`, guarded by the identity it stored. + If the owner itself stops or restarts first, the records go with it, so + nothing leaks. +- **Persistent reservations outside any actor** (the mempool's in-flight + hashes, cell availability, the announced-hash budget) would outlive a + monitor whose owner stops before handling `Down` (Codex round 3: the peer + table can begin a non-trapping shutdown with the `Down` still queued). + They are held by an **owning registration**: a value the mempool hands + out when the connection reserves, kept in the connection's state, whose + destruction releases exactly that connection's entries synchronously, + under the mempool's lock, with no message and no `.await`. State + destruction runs on every exit path, kills and runtime drops included + (exit phase 5), before the connection's slot is freed, so the release + cannot be lost whoever else is alive. + +Nothing is sent from `Drop`: a message would reach the peer table before the +`Down` (phase 5 before 6) and could pick the dying peer as an alternate +(agy round 2), and an enqueued message is not a completed release. + +| Released in `stopped()` today | Owner and registration | Release | +|---|---|---| +| peer-table entry and discv5 session | peer table; `new_connected_peer` stores the monitor reference in `PeerData` | on `Down`, only if the entry still holds that monitor; gone anyway if the peer table stops | +| tx-broadcaster index | broadcaster; its `add_peer` records the connection's `ActorId` and monitors it | on `Down`, only if the index is still owned by that `ActorId`; gone anyway if the broadcaster stops | +| in-flight transaction reservations (`clear_in_flight_txs`) | mempool registration `InFlightLease`, held in the connection's state; the mempool records each in-flight hash against the lease's `ActorId` | the lease's destruction removes the hashes still recorded against it, synchronously | +| cell availability and announced-hash budget (`clear_peer_cell_availability`, `forget_peer_announcements`) | the same lease, keyed by (node id, connection `ActorId`) instead of node id plus a "started session" check | the lease's destruction, for that `ActorId` only; a second session of the same node keeps its own | +| re-request to alternates (`retry_on_alternates`) | peer table, best effort | on `Down`, after removing the entry, with a local lookup of live peers (no request to itself). Suppressed by explicit shutdown state, the node's shutdown token that `shutdown_l1` cancels first, not by `Down.reason`: a connection killed at its shutdown deadline ends `Killed`. Lost if the peer table stops first, which is acceptable for a retry | +| disconnect metrics | peer table's `Down` handler (it has the final reason) | best effort | + +### What disappears + +About 45-60 of the ~135 hand-written lines (counted on `main`): + +| Code | Lines | Fate | +|---|---|---| +| `ConnectionId` type and `next()` ([server.rs:176-188](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/rlpx/connection/server.rs#L176-L188)) | 13 | removed | +| `connection_id` in `Established`, `PeerData` and the handshake ([server.rs:432-437](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/rlpx/connection/server.rs#L432-L437), [handshake.rs:177](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/rlpx/connection/handshake.rs#L177), [M peer_table.rs:324-326](https://github.com/lambdaclass/ethrex/blob/fd5c57ddada097952660f6b749c739119e4de852/crates/networking/p2p/peer_table.rs#L324-L326)) | ~8 | removed (replaced by the monitor) | +| `remove_peer` protocol method and `handle_remove_peer` with its guard ([V peer_table.rs:693-711](https://github.com/lambdaclass/ethrex/blob/0dd4c105f65d544b0fb5e92d8634a1699127f826/crates/networking/p2p/peer_table.rs#L693-L711)) | ~22 | replaced by a ~12-line `Handler` | +| `remove_peer` send in `stopped()` | ~6 | removed | +| inbound semaphore, `try_acquire_owned`, `_admission_permit` field and parameter | ~15 | replaced by `max_children` | +| "connections are not admitted" comment and unmanaged `.start()` | | connections owned by the system | + +Added: the handshake as a post-start continuation (moving existing code), +the writer as an owned helper, the mempool's `InFlightLease` (an owning +registration released by its destruction), the broadcaster's identity check +and the release logic in the `Down` handlers. Net lines are +roughly even; what changes is that every path out of a connection is +covered. #7435's integration test (171 lines) stays as a regression test, +now exercising the monitor guard. + +### Bugs and gaps it closes + +- **Stale entries when `stopped()` does not run** (panic in `started()` + today; kills, `terminate_child` and shutdown under v0.8): the `Down` still + comes. +- **The #7435 class**: removal is keyed by the registered connection's + monitor and re-checked against the entry, not by node id. +- **Unowned connections at shutdown**: stopped within the system deadline, + before the peer table, instead of dying with the process. +- **Unowned writer tasks**: joined before the slot frees. +- **Placement**: connections run on the `p2p` group. + +### Things to watch in a migration + +- **Serialised starts.** Anything slow left in `started()` holds every + accept and dial. Keep `started()` to state setup; the handshake is the continuation. +- **Stuck cleanup.** A connection's own exit gets one `shutdown_timeout` + for its owned cleanup (E3 row 4, no kill); a terminated or shut-down one + gets the signal, the kill after `shutdown_timeout` and a second interval. + A connection that misses them is stuck: its slot stays counted until its + code returns, it is reported, and **nothing else is affected**, since + connections are Temporary (design: stuck children). Only budget + exhaustion (impossible for Temporary children) or a closed group fails + the supervisor; nesting it under the p2p supervisor still restarts it in + that case instead of leaving accepts disabled (agy P0). +- **Caps count slots until owned cleanup ends**, writer helper included, + so a slow socket close keeps its slot a little longer than the permit did. +- **Rejected arguments come back**, so the accept loop decides what to do + with the stream. + +## ethlambda + +No dynamic per-X actors on either branch. + +- `main`: two singletons, `BlockChainServer` (`start_with_backend(Backend::Thread)`, + [crates/blockchain/src/lib.rs:434](https://github.com/lambdaclass/ethlambda/blob/c3f5f566cb3a61e3d388c66ce21794c18a6618ce/crates/blockchain/src/lib.rs#L434)) + and `P2PServer` (`start()`, + [crates/net/p2p/src/lib.rs:1271](https://github.com/lambdaclass/ethlambda/blob/c3f5f566cb3a61e3d388c66ce21794c18a6618ce/crates/net/p2p/src/lib.rs#L1271)), + plus one `PeerTableServer` and one `DiscoveryServer` from ethrex. Peers + are libp2p connections handled inside the swarm, not actors. No maps of + `ActorRef`. +- `spawned-v0.7`: the same singletons placed with `start_on(group)` + ([lib.rs:1268](https://github.com/lambdaclass/ethlambda/blob/6a12bc753ae18c9d63f3dbf930edc700c4c4704c/crates/net/p2p/src/lib.rs#L1268), + [blockchain lib.rs:449](https://github.com/lambdaclass/ethlambda/blob/6a12bc753ae18c9d63f3dbf930edc700c4c4704c/crates/blockchain/src/lib.rs#L449)) + and the HTTP server under a static supervisor + ([main.rs:977-989](https://github.com/lambdaclass/ethlambda/blob/6a12bc753ae18c9d63f3dbf930edc700c4c4704c/bin/ethlambda/src/main.rs#L977-L989)). + +Per-request and per-check concurrency is plain `tokio::spawn`/`spawn_blocking` +(gossip checks, aggregation), which belongs to ranks 11b and 15, not to a +dynamic supervisor. diff --git a/docs/design/dynamic-supervisor.md b/docs/design/dynamic-supervisor.md new file mode 100644 index 00000000..f25f3714 --- /dev/null +++ b/docs/design/dynamic-supervisor.md @@ -0,0 +1,1273 @@ +# Dynamic supervisor: design contract + +**Status: approved for implementation after review round 3 (revision 3), not implemented.** ROADMAP rank 12a. +Draft PR [#245](https://github.com/lambdaclass/spawned/pull/245). Revision 2 +applied the maintainer's decisions on revision 1's open questions and the +first reviews; revision 3 applies the decisions on round two's questions and +the second reviews (Codex, agy), plus the OTP/Elixir/Gleam comparison. See +[Decisions](#decisions) and [Review resolutions](#review-resolutions). + +- Covers OTP's `simple_one_for_one` and Elixir's `DynamicSupervisor`: children + started at runtime from one template, supervised one for one, terminated + individually, and all stopped concurrently when the supervisor stops. +- Builds on the v0.8 exit-signal contract ([otp-exit-signals.md](otp-exit-signals.md), + accepted, implementation in #240): the single death point D, `Killed`, + `NoProc`, the parent exit signal (E3), first-start failure as + `SupervisorError::FailedToStartChild` (S1, S2) and `stopped()` skipped for a + non-trapping child whose parent sends `Shutdown`. It also builds on rank 11 + ([deferred-replies.md](deferred-replies.md), #239) for what callers of a + dying child see. +- Model: [`DynamicSupervisor.tla`](../../verification/tla/DynamicSupervisor.tla); + see [What the model establishes](#what-the-model-establishes). +- Client mapping: [dynamic-supervisor-client-mapping.md](dynamic-supervisor-client-mapping.md) + (ethrex's per-peer connection actors; ethlambda has none). +- Illustrative API shapes are not copyable code. + +**Project rule.** Match Erlang/OTP. Deviate only where: + +- **R:** Rust forces it; +- **T:** Rust types add strictness; or +- **B:** Spawned adds a bound OTP lacks. + +## Contents + +- [Sources](#sources) +- [Goals and non-goals](#goals-and-non-goals) +- [Decisions](#decisions) +- [API](#api) +- [Semantics](#semantics) +- [Erlang alignment](#erlang-alignment) +- [Non-guarantees](#non-guarantees) +- [Semantics contract: what this adds and touches](#semantics-contract-what-this-adds-and-touches) +- [Interaction with rank 12 (scoped registries)](#interaction-with-rank-12-scoped-registries) +- [What the model establishes](#what-the-model-establishes) +- [Test plan: relating the model to the code](#test-plan-relating-the-model-to-the-code) +- [Alternatives considered](#alternatives-considered) +- [Follow-ups](#follow-ups) +- [Review resolutions](#review-resolutions) + +## Sources + +Read for this design (line numbers refer to these revisions): + +- OTP `lib/stdlib/src/supervisor.erl` at master + [`186c0b94`](https://github.com/erlang/otp/blob/186c0b94da565e4cd234685307b3c3ea41c4af1c/lib/stdlib/src/supervisor.erl) + (OTP 29 development; compared with `OTP-28.5.0.8`, no behavioural difference + for dynamic children). +- Elixir `lib/elixir/lib/dynamic_supervisor.ex` at main + [`b57b70bd`](https://github.com/elixir-lang/elixir/blob/b57b70bd96e2e76d66cb81eba6b39c172fa8e8e4/lib/elixir/lib/dynamic_supervisor.ex) + (compared with `v1.19.7`; only the shutdown code differs). + +What OTP and Elixir do, in short: + +| Topic | OTP `simple_one_for_one` | Elixir `DynamicSupervisor` | +|---|---|---| +| `start_child` | `gen_server:call(Sup, …, infinity)`; the supervisor runs the start function, which normally waits for the child's `init` (proc_lib), so starts are serialised with each other and with `'EXIT'` handling ([L652](https://github.com/erlang/otp/blob/186c0b94da565e4cd234685307b3c3ea41c4af1c/lib/stdlib/src/supervisor.erl#L652), [L1077-1092](https://github.com/erlang/otp/blob/186c0b94da565e4cd234685307b3c3ea41c4af1c/lib/stdlib/src/supervisor.erl#L1077-L1092)) | same; "will block the `DynamicSupervisor` until the child initializes" ([L359](https://github.com/elixir-lang/elixir/blob/b57b70bd96e2e76d66cb81eba6b39c172fa8e8e4/lib/elixir/lib/dynamic_supervisor.ex#L359)) | +| Arguments | `ExtraArgs` appended to the template's | `extra_arguments` (fixed per supervisor) prepended to each spec's args ([L752](https://github.com/elixir-lang/elixir/blob/b57b70bd96e2e76d66cb81eba6b39c172fa8e8e4/lib/elixir/lib/dynamic_supervisor.ex#L752)) | +| Specs | one template | any child spec per call | +| Start result | `{ok, Pid}`, `{ok, Pid, Info}`, `{ok, undefined}` on `ignore` (nothing stored), `{error, Reason}` unwrapped | same, but `:ignore` bare | +| Start failure and the budget | not counted: `add_restart` runs only in `restart/2` | not counted | +| `terminate_child` | by pid; any restart type; removed, never restarted; an unknown dead pid returns `ok` ([L1108-1115](https://github.com/erlang/otp/blob/186c0b94da565e4cd234685307b3c3ea41c4af1c/lib/stdlib/src/supervisor.erl#L1108-L1115), [L1861-1875](https://github.com/erlang/otp/blob/186c0b94da565e4cd234685307b3c3ea41c4af1c/lib/stdlib/src/supervisor.erl#L1861-L1875)) | by pid; unknown pid `{:error, :not_found}` ([L712-721](https://github.com/elixir-lang/elixir/blob/b57b70bd96e2e76d66cb81eba6b39c172fa8e8e4/lib/elixir/lib/dynamic_supervisor.ex#L712-L721)) | +| `restart_child`, `delete_child` | `{error, simple_one_for_one}` | not provided | +| `which_children` | `{undefined, Pid \| restarting, Type, Mods}`, unordered | same | +| `count_children` | `specs` always 1; `active` excludes restarting; `workers`/`supervisors` include them ([L1218-1229](https://github.com/erlang/otp/blob/186c0b94da565e4cd234685307b3c3ea41c4af1c/lib/stdlib/src/supervisor.erl#L1218-L1229)) | `specs` = number of children; otherwise the same | +| Default restart type | `permanent` ([L449](https://github.com/erlang/otp/blob/186c0b94da565e4cd234685307b3c3ea41c4af1c/lib/stdlib/src/supervisor.erl#L449)) | `:permanent` ([L404-413](https://github.com/elixir-lang/elixir/blob/b57b70bd96e2e76d66cb81eba6b39c172fa8e8e4/lib/elixir/lib/dynamic_supervisor.ex#L404-L413)); `Task.Supervisor` defaults to `:temporary` | +| Temporary children | start args not kept (`mapsets`), "it could become very costly" ([L1813-1817](https://github.com/erlang/otp/blob/186c0b94da565e4cd234685307b3c3ea41c4af1c/lib/stdlib/src/supervisor.erl#L1813-L1817)) | args dropped (`mfa_for_restart`, [L784](https://github.com/elixir-lang/elixir/blob/b57b70bd96e2e76d66cb81eba6b39c172fa8e8e4/lib/elixir/lib/dynamic_supervisor.ex#L784)) | +| Restart intensity | default 1 in 5 s; `add_restart` before every restart attempt, also each `try_again_restart` retry ([L1477-1531](https://github.com/erlang/otp/blob/186c0b94da565e4cd234685307b3c3ea41c4af1c/lib/stdlib/src/supervisor.erl#L1477-L1531)) | default 3 in 5 s; each `$gen_restart` retry counts | +| Exhaustion | logs `reached_max_restart_intensity`, terminates every child, exits `shutdown` | same | +| `max_children` | none | `:infinity` by default; checked only in `start_child`, `map_size(children) < max_children`, which includes restarting entries; restarts never re-check ([L742](https://github.com/elixir-lang/elixir/blob/b57b70bd96e2e76d66cb81eba6b39c172fa8e8e4/lib/elixir/lib/dynamic_supervisor.ex#L742)) | +| `terminate_child` duration | blocks the supervisor until the child is gone: `shutdown` then `kill` after the timeout, or forever with `infinity` (the default for supervisor children) | same | +| Shutdown | `terminate_dynamic_children`: monitor and `exit(P, shutdown)` to every child first, one timer for the template's shutdown value, then `kill` to every child still alive; order "is not defined" ([L1701-1799](https://github.com/erlang/otp/blob/186c0b94da565e4cd234685307b3c3ea41c4af1c/lib/stdlib/src/supervisor.erl#L1701-L1799)) | same, one timer per distinct shutdown value | +| Static strategies, for contrast | children stopped one at a time in reverse start order, each waited for | | +| Restarted supervisor | starts with no children | same | +| `auto_shutdown`, significant children | rejected for `simple_one_for_one` | only `:never` | + +The ROADMAP entry says counting restarting children against `max_children` +"goes beyond Elixir". It does not: Elixir keeps a restarting child in its +`children` map under the old pid, so it counts. This design matches Elixir +there, and the ROADMAP row is corrected in this PR. + +## Goals and non-goals + +Goals: + +1. Start supervised children at runtime, each from a template plus per-call + arguments, with a synchronous `start_child` that returns the child or a + typed error. +2. OTP's operation order: one control loop serialises starts, restart + decisions and terminations, as the supervisor process does. +3. OTP's restart types, supervisor-wide restart budget and escalation. +4. Terminate one child without restarting it. +5. Optional `max_children` that rejects at once, counting restarting + children. +6. Stop every child concurrently on shutdown, bounded by the per-child + shutdown timeout and the kill, not by the number of children. +7. One child that cannot finish its cleanup never takes healthy siblings + down unless OTP would also stop them. +8. Placement on one `ExecutionGroup`; ownership by an `ActorSystem`; + nesting under a static supervisor. + +Non-goals (v1): + +- Heterogeneous children (Elixir's any-spec `start_child`): decision Q2. +- A keyed registry owned by the supervisor (rank 12; see + [Interaction with rank 12](#interaction-with-rank-12-scoped-registries)). +- Supervisor-type dynamic children (a template that builds a nested + supervisor per call). Possible later through the nested adapter. +- `Task.Supervisor` (ranks 11 and 15), `PartitionSupervisor` (sharding), + significant children and `auto_shutdown` (OTP rejects them for + `simple_one_for_one`). +- Draining children on shutdown (rank 13), bounded mailboxes (rank 17). +- `terminate_child` on static supervisors (decision Q6, a follow-up). + +## Decisions + +The maintainer settled revision 1's open questions under the match-Erlang +rule: + +| # | Question | Decision | +|---|---|---| +| Q1 | Concurrent or serialised construction | **Serialised, as OTP.** One control loop runs each start (admission, factory, `started()`) to completion before the next operation. Factories still run on the target group. Long work (ethrex's RLPx handshake) moves out of `started()` into the post-start continuation, OTP's `handle_continue` (decision G1) | +| Q2 | Heterogeneous children | The typed template is enough for v1 | +| Q3 | Defaults | Elixir's: `max_restarts = 3`, `restart_window = 5 s`; backoff **opt-in** (`None` by default); `max_children = None` | +| Q4 | Group capacity across restarts | The slot holds a **transferable native-capacity reservation** from admission to removal, separate from any generation's scope lease | +| Q5 | Exit reason of an exhausted supervisor | `Shutdown`, as OTP, keeping the diagnostic in `failure()`. Static nested supervisors need the same change: a separate follow-up PR | +| Q6 | `terminate_child` on static supervisors | Separate follow-up | +| Q7 | Arguments on rejection | Returned on pre-admission rejection (`MaxChildren`, `Stopped`, placement); a distinct error for a start aborted after construction began | + +Round two (revision 3): + +| # | Question | Decision | +|---|---|---| +| R1 | Loop blocked during `terminate_child` | **Kept, as OTP and Elixir:** the loop is held through the child's removal or its deadline | +| R2 | Stuck child that must restart | **Fails the supervisor**, after fixing the Transient classification (a stall is not a recorded cleanup failure). Escalation cannot make an unkillable computation disappear (see [Stuck children](#stuck-children)) | +| R3 | Atomic fan-out in the model | Kept as an ownership abstraction; a small interleaved refinement configuration checks that the fan-out completes even when siblings never finish | +| R4 | Two slots | Fast checks keep two slots; targeted three-slot instances check admission order, the cap and the shared budget. Bounded checks, no cutoff claimed | +| R5 | ethrex teardown | No message from `Drop`. Each resource's owner monitors the connection and releases on `Down`, as an Erlang owner would | +| G1 | Post-start work | Depends on the post-start continuation (a `handle_continue` equivalent) of the unified-start design (0.9), not on "the first message", which other messages could overtake | +| G2 | Restart type for connections | The ethrex mapping and the example use `temporary()` (a dropped peer must not be redialled by the supervisor); the default stays Permanent (OTP) | +| G3 | `ignore` | Accepted from the factory and from `Init::ignore()`: nothing is kept once cleaned up, `start_child` returns `Ignored { pending }` (OTP `{ok, undefined}`) | +| G4 | Start data | Deferred, as in unified start (#259): `gen_server` returns only `{ok, Pid}`; `Started` is `{ actor, child }` | +| G5 | Introspection | `ChildInfo` and `ChildCounts` are the types introspection v1 exposes for static supervisors too; names agreed across both designs | +| U1 | Shared shapes with unified start (#259 rev. 2-3, section 18) | `StartOutcome>` with `Ignored { pending: Option }` as an `Ok` outcome; a failed init never runs `stopped()`; `FailedToStart { cause: ChildStartError, cleanup_stuck }`; `ChildStart`; `StartOptions` through `DynamicChildSpec::options`; the continuation is `Init::continue_with(msg)`, which precedes messages but is no termination barrier | +| I1 | Fenced termination (introspection #256 rev. 3) | `terminate_slot` takes an optional `expect: ActorId@generation`; a mismatch returns `Stale { current }` and does nothing, checked at the supervisor operation itself, so the console's `terminate --expect` cannot kill a child that moved on | + +## API + +### Template + +```rust +/// One template for every child: placement, factory, restart type, limits. +/// The factory gets the per-call arguments (OTP's ExtraArgs). +pub struct DynamicChildSpec { /* name, group, factory, restart, timeouts */ } + +impl DynamicChildSpec { + /// Permanent, as OTP's default. A restartable child is rebuilt from its + /// arguments, hence `Clone`. + pub fn new(name: impl Into, group: &ExecutionGroup, factory: F) -> Self + where + F: Fn(FactoryContext, Args) -> U + Send + Sync + 'static, + U: Future> + Send + 'static, + S: Into>, // `A` (via From) or `ChildStart::Ignore` (#259) + E: std::fmt::Display; + pub fn restart(self, restart: RestartMode) -> Self; +} + +impl DynamicChildSpec { + /// A Temporary template. Arguments are moved into the only generation + /// and never kept (OTP stores no arguments for temporary children), so + /// they need not be `Clone`: a `TcpStream` works. + pub fn temporary(name: impl Into, group: &ExecutionGroup, factory: F) -> Self; +} + +impl DynamicChildSpec { + /// Covers the factory and `started()` together (#259); default 5 s; + /// `Timeout::Infinity` allowed. + pub fn startup_timeout(self, limit: impl Into) -> Self; + pub fn shutdown_timeout(self, limit: Duration) -> Self; // default 5 s + /// Per-child start options shared with unified start (#259 section 2.4): + /// name, label, stack size, per-instance bounds. The template's group + /// stays the positional argument of `new`/`temporary`; a `backend` here + /// is rejected (`InvalidOptions`), as for a `ChildSpec`. + pub fn options(self, options: StartOptions) -> Self; +} +``` + +- Two constructors is a Rust-forced shape (R): a restartable child must be + rebuilt from its arguments, a temporary one must accept move-only values. + `RestartMode::Temporary` passed to `restart()` is allowed and never + clones. The restart type is per template, as in `simple_one_for_one`. +- `Args` needs `Send + 'static`, plus `Clone` for restartable templates; not + `Sync` (one owner holds the retained copy). +- `DynamicChildSpec`, `DynamicSupervisor`, `SupervisedDynamicSupervisor` and + `DynamicChild` implement `Clone` without requiring `A: Clone` or + `Args: Clone` (shared handles), so a supervisor of move-only arguments can + be stored in a cloneable context. + +### Starting the supervisor + +```rust +pub struct DynamicSupervisorConfig { + pub max_restarts: usize, // default 3 (Elixir) + pub restart_window: Duration, // default 5 s (Elixir) + pub max_children: Option, // default None (Elixir :infinity); Some(0) allowed + pub backoff: Option, // default None: restart at once, as OTP +} + +// Root, owned by the system (a shutdown unit in admission order, S2): +let peers: DynamicSupervisor = + system.dynamic_supervisor(config, spec)?.start().await?; + +// Nested under a static supervisor, as `add_supervisor` (V8): +let slot: SupervisedDynamicSupervisor = + builder.add_dynamic_supervisor(DynamicSupervisorSpec::new("peers", config, spec))?; +let peers = slot.current()?; // re-resolve after the parent restarts it +``` + +- `start()` returns once the supervisor is admitted; it has no children to + start, so it cannot fail with `FailedToStartChild`. +- Configuration errors (zero window, `backoff.maximum < initial`, zero + timeouts, a foreign group) are `SupervisorError::Configuration` or + `System(ForeignGroup)` at construction. `max_children = Some(0)` is valid + and rejects every start, as Elixir's `max_children: 0`. The static + supervisor's `max_children <= 65536` ceiling does not apply. +- `DynamicSupervisorSpec::new(name, config, spec)` takes the template; the + adapter runs on the template's group. Its `shutdown_timeout` (how long the + parent waits for the whole dynamic supervisor) defaults to waiting for + the inner supervisor to finish, as OTP's `infinity` for supervisor + children; see [Nesting](#nesting-and-the-system). + +### Operations + +```rust +impl DynamicSupervisor { + /// OTP start_child(Sup, ExtraArgs). Queued on the control loop; resolves + /// when the first generation is ready, was ignored, or failed. + pub async fn start_child(&self, args: Args) + -> Result>, StartChildError>; + /// OTP terminate_child(Sup, Pid): the actor id is looked up when the loop + /// handles the call; it names the slot only if it is the slot's last + /// published id at that moment. + pub async fn terminate_child(&self, id: ActorId) -> Result<(), TerminateChildError>; + /// The same by slot. With `expect`, only if the slot's current published + /// child is still that `ActorId@generation`; otherwise `Stale` and + /// nothing is done (introspection's `terminate --expect`, #256). + pub async fn terminate_slot(&self, id: DynamicChildId, expect: Option) + -> Result<(), TerminateChildError>; + pub fn which_children(&self) -> Vec; + pub fn count_children(&self) -> ChildCounts; + pub fn stop(&self); + pub async fn shutdown(&self, deadline: Duration) -> SupervisorReport; + pub async fn join(&self); + pub fn failure(&self) -> Option; +} + +/// Shared with unified start (#259 section 18): `T` is `ActorRef` there. +pub enum StartOutcome { + Started(T), + /// The factory returned `ChildStart::Ignore`, or `started()` returned + /// `Init::ignore()` (OTP {ok, undefined}). `pending` is `None` once the + /// ignoring instance was cleaned up and the slot freed; `Some(handle)` + /// when the answer came at the cleanup deadline first: the slot still + /// counts (state `Stopping`) until the instance is published and the slot + /// finalized, and `handle.wait_exit()` reaches that end (#259 rev. 3). + Ignored { pending: Option }, +} + +pub struct Started { + pub actor: ActorRef, // the first generation, as OTP's Pid + pub child: DynamicChild, // the slot, across restarts +} + +/// Like `SupervisedChild` for a dynamic slot. Holds no arguments and no +/// scope; after removal it keeps only terminal metadata. +impl DynamicChild { + pub fn id(&self) -> DynamicChildId; + pub fn current(&self) -> Result, ChildUnavailable>; + pub async fn wait_for_generation(&self, after: u64) -> Result, ChildUnavailable>; + pub fn snapshot(&self) -> ChildSnapshot; + pub async fn terminate(&self) -> Result<(), TerminateChildError>; // = terminate_slot(id, None) +} + +/// Nested form, as `SupervisedSupervisor`. +impl SupervisedDynamicSupervisor { + pub fn current(&self) -> Result, ChildUnavailable>; + pub async fn wait_ready(&self) -> Result, ChildUnavailable>; + pub async fn wait_for_generation(&self, after: u64) + -> Result, ChildUnavailable>; + pub fn snapshot(&self) -> ChildSnapshot; +} +impl DynamicSupervisorSpec { + pub fn new(name: impl Into, config: DynamicSupervisorConfig, + spec: DynamicChildSpec) -> Self; // Permanent + pub fn restart(self, restart: RestartMode) -> Self; + pub fn startup_timeout(self, limit: Duration) -> Self; + /// Default: wait for the inner supervisor to finish (OTP's `infinity` + /// for supervisor children); a finite value is a reporting bound only. + pub fn shutdown_timeout(self, limit: Duration) -> Self; +} + +#[non_exhaustive] +pub enum StartChildError { + /// Not admitted: nothing was constructed and the arguments come back. + Rejected { reason: RejectReason, args: Args }, + /// Admitted, then the supervisor began shutting down before readiness + /// committed. The arguments were consumed by the factory. + Aborted, + /// The first generation failed: factory error or panic, panic or stop + /// in started(), or startup_timeout. Not retried, not charged. + /// `ChildStartError` is #259's: `Factory`, `Start(StartError)` (with + /// `InitFailed`/`InitExited { reason }`), `StartupTimeout { pending }`. + FailedToStart { cause: ChildStartError, cleanup_stuck: bool }, +} + +#[non_exhaustive] +pub enum RejectReason { + MaxChildren, // Elixir {:error, :max_children} + Stopped, // shutting down or stopped (OTP: the call exits) + Placement(SystemError), // the group is closed or out of native capacity +} + +/// The slot's last published child: its `ActorId` and the generation at +/// which it was published. Failed replacement attempts do not change it +/// (they advance `ChildInfo::generation`, the attempt count, but publish +/// nothing), so an `expect` taken during backoff still matches. +pub struct ExpectedChild { pub actor: ActorId, pub generation: u64 } + +#[non_exhaustive] +pub enum TerminateChildError { + NotFound, // no current child with that id or slot (Elixir {:error, :not_found}) + /// `expect` did not match: the slot's current published child moved on. + Stale { current: Option }, + Stopped, // shutdown began before the loop handled the call + CleanupStuck, // the child missed its deadlines; see "Stuck children" +} + +/// Shared with introspection v1 (static and dynamic supervisors). +pub struct ChildInfo { + pub key: ChildKey, // DynamicChildId here; the name for static children + pub actor: Option, // last published id; None before the first readiness + pub ready: bool, // true iff state == Running + pub state: ChildState, + pub generation: u64, +} + +pub struct ChildCounts { + pub specs: usize, // 1, as OTP simple_one_for_one + pub active: usize, // children with a live, ready generation + pub supervisors: usize, // 0 in v1 + pub workers: usize, // every child held, restarting and stuck included +} +``` + +- An ignored attempt is cleaned up like any exit before anything is + released: `Init::ignore()` drops the constructed state and joins its owned + work; a factory ignore has nothing to drop. Then the slot is finalized + (retained arguments dropped) and only then freed and answered + `Ok(StartOutcome::Ignored { pending: None })`. If that cleanup misses its + deadline the start is answered `Ok(Ignored { pending: Some(handle) })` at + the deadline (the outcome was decided when the child ignored) and the slot + stays counted, `Stopping`, until the instance is published and the slot + finalized, as for any stuck retiring child (control `IgnoreFreesEarly`; + Codex round 3; #259 rev. 3). +- The factory returns `Result, E>` with + `ChildStart::Actor(a) | ChildStart::Ignore` (`From`), and `started()` + may return `Init::ignore()`; both are unified start's shapes (#259). An + ignore on a first start returns `Ok(StartOutcome::Ignored { .. })` and + keeps nothing once cleaned up; on a restart it removes the child (OTP drops it), without charge + beyond the attempt already stamped. +- Typed start data (`Started::data`) is deferred, as in #259: `gen_server` + returns only `{ok, Pid}`. +- `StartChildError` implements `Error` when `Args: Debug`; + `into_args()` returns the arguments of a `Rejected`, and `without_args()` + maps to `StartChildError<()>` for `?`. +- `FailedToStart` carries #259's `ChildStartError`, so the generation's + `ExitReason` (`InitExited { reason }`) or cause (`InitFailed`, + `Factory`) is typed, not a string. +- `ChildState` gains no variant: a dynamic child is `Starting`, `Running`, + `Backoff` (restart pending), `Stopping` (including stuck), then leaves + `which_children`, which is a snapshot in no particular order. +- Removed slots are evicted from the supervisor's table after slot + finalization ([Retained arguments](#retained-arguments)): memory is + O(children held). +- `ChildInfo`, `ChildCounts` and `ChildKey` are introspection v1's types + (#256); the implementation uses its canonical declarations, which have + more fields than the ones shown here, which are those this design + depends on. + +### Restart types + +| | OTP | This design | +|---|---|---| +| Default | `permanent` | `Permanent` (`DynamicChildSpec::new`); `temporary()` for one-shot children | +| Table | `do_restart/3` | V1 with the v0.8 rule: Permanent always; Transient on an abnormal reason (`Panic`, `Kill`, `Killed`, `NoProc`) or a recorded cleanup failure (cleanup that *finished* and reported a destructor or helper failure; a cleanup that is still running past its deadline is not one); Temporary never | +| A replacement failing before readiness | `try_again_restart`, retried | retried unless Temporary, each attempt charged | +| `terminate_child` | never restarted | never restarted, any type | + +### Restart budget + +- **Scope:** one rolling window per supervisor, as OTP's intensity and + period. Defaults 3 per 5 s (Elixir). +- **What counts:** every restart attempt: the factory call of every + generation after a child's first, including retries of a replacement that + failed before readiness (OTP's `add_restart` before each restart and each + `try_again_restart`). There are no collateral restarts, so v0.7's "every + factory call" and rank 5f's "recovery rounds" count the same here. +- **What does not count:** a failed `start_child`, a Temporary child's exit, + an exit after `terminate_child`, exits during shutdown. +- **Reservation protocol** (as V5, modelled here): when the loop decides a + restart, it reserves one grant; if none is left the supervisor fails at + once (no backoff is entered). The reservation is stamped into the window + when the restart attempt is admitted, and refunded if the pending restart + is cancelled by `terminate_child` or shutdown. Window expiry releases only + stamped grants, never reservations. +- **Backoff** is opt-in (`backoff: Some(..)`). Without it (the default) the + loop reserves, stamps and runs the restart attempt in the same turn in + which it handles the exit, as OTP's `restart/2` does; a failed attempt + re-queues the exit at the tail of the loop's queue (OTP's + `try_again_restart` cast) and is decided again there. With backoff the + loop reserves, releases the loop, and the timer queues a retry that the + loop takes in order. With it, the + per-child jitter stream is seeded from the supervisor seed mixed with the + slot's `DynamicChildId`, not only the shared template name, so siblings do + not draw identical delays (agy 9). +- **Exhaustion:** the supervisor fails (`failure()` records "restart + intensity reached" with the child and its last reason, as OTP's + `reached_max_restart_intensity` report), closes admission, stops every + child as in a shutdown, and **exits `Shutdown`** (OTP): a nested dynamic + supervisor under a Transient parent is then not restarted; under a + Permanent parent it is (decision Q5). Stuck cleanups and coordinator + faults still exit abnormally. + +### `max_children` + +- `None` by default. `Some(n)` caps the children held: starting, running, + cleaning up, in backoff, constructing a replacement, or stuck. A slot is + freed only when its child is removed: its last generation finished owned + cleanup (milestone 7 of the exit phases), its retained arguments were + dropped, and no restart follows. +- Checked only when the loop admits a start; a full supervisor answers + `Rejected { MaxChildren, args }` and nothing waits. Restarts are never + re-checked (Elixir) and never need to be: their slot was never freed. +- The slot frees after cleanup, not at the exit signal as OTP removes the + child at `'EXIT'` (B: the cap bounds what is really held). + +### Placement and capacity + +- Every child and every factory runs on the template's `ExecutionGroup`. + The group must belong to the supervisor's `ActorSystem`. +- Async groups: children share the group's workers; nothing is reserved. + The supervisor's control loop runs on the system's control runtime, + outside every group budget, as today. +- Native groups (`thread_group(n)`, one thread per live actor): each slot + takes a **transferable native-capacity reservation** at admission and + keeps it until removal. A generation's scope draws its thread from that + reservation and returns it when the generation's scope has joined; the + replacement draws it again. The reservation is a separate permit owned by + the slot, not the old scope's completion lease, so it never keeps a + finished scope from joining (decision Q4). A start that cannot reserve + answers `Rejected { Placement(Capacity), args }`. +- Pinned groups multiplex actors on a shard and have no per-actor native + capacity; the slot keeps its shard (affinity) across restarts and + reserves nothing. +- A closed group rejects starts (`Placement(Closed)`) and fails restarts, + which fails the supervisor, as static supervisors treat group closure. + +### Nesting and the system + +- Root: `system.dynamic_supervisor(config, spec)` is a shutdown unit in + admission order, stopped in its turn by `ActorSystem::shutdown` (S2); its + children stop concurrently in that turn. +- Under a static supervisor: `add_dynamic_supervisor` uses the nested + adapter (V8), with its join barrier over every descendant. A restart by + the parent creates a new, empty dynamic supervisor (OTP). Old handles + return `Stopped`; `SupervisedDynamicSupervisor::current()` resolves the new + one. +- The adapter's own `shutdown_timeout` defaults to waiting for the inner + supervisor to finish, which its own deadlines already bound (OTP's + `infinity` for supervisor children). A finite value is a reporting bound: + when it expires the parent records a cleanup failure but keeps the + descendant join barrier. A fixed margin such as 2 × child timeout + 1 s + (revision 2) cannot cover an unbounded fan-out and the cleanup this + contract allows (Codex F7). + +## Semantics + +### The control loop + +One logical control loop per supervisor, as OTP's supervisor process. It +owns one FIFO queue holding, in arrival order: + +- `start_child` requests; +- `terminate_child` / `terminate_slot` calls; +- exit notices of children whose owned cleanup finished (OTP's `'EXIT'`); +- backoff retries, when backoff is configured (OTP's `try_again_restart` + cast is the no-backoff counterpart: a failed attempt's exit is queued at + the tail). + +The loop takes the head and runs it to completion before the next: + +- a start: admission (gate, `max_children`, capacity), then the first + generation's factory and `started()`, until readiness commits, the factory + ignores, or the attempt failed and was cleaned up (or reached its + deadline); +- an exit notice: the restart decision, the reservation and, without + backoff, the restart attempt until readiness or failure; +- a retry: stamping and the restart attempt; +- a terminate call: lookup, signal, kill escalation and removal, or the + deadline. + +The exit of the child an operation is waiting for (the first generation of +a failing start, the child being terminated) is consumed by that operation +directly, as OTP's `start_child` returns the start function's error and +`shutdown/2` consumes the `'EXIT'` with `unlink_flush`. Every other exit +waits its turn in the queue. + +Not serialised: children run, exit and clean up concurrently; deadlines and +the backoff timer run off the loop; `which_children`, `count_children` and +`current()` read a snapshot; shutdown closes admission at once, answers the +queued requests and cancels the operation in progress (alignment row 21, +B). Factories run on the target group even though the loop awaits them. + +Consequences, as in OTP: + +- Requests are served in arrival order: with `max_children = 1`, of two + queued starts the first is admitted and the second gets `MaxChildren`, + never the reverse (model: `FifoOrder`, control `LaterOp`). +- A start arriving while another constructs waits; if the first fails, the + second is admitted. +- A slow `started()` delays every later operation. Slow initialisation goes + in the post-start continuation (below). +- A slow-to-stop child holds the loop during its `terminate_child`, at most + until its deadline; the stall watchdog and introspection report "blocked + in terminate_child(id) for T" (decision R1). + +**Post-start continuation.** Slow initialisation (ethrex's RLPx handshake) +belongs in unified start's continuation (#259 section 8, OTP's +`handle_continue`): `started()` returns `Init::continue_with(msg)` and +`Handler` runs it as the first turn after the readiness commit, before +any mailbox entry. "Send yourself a message in `started()`" is not +equivalent, because a message enqueued by someone else first would run +first. The continuation is not a termination barrier: readiness is already +committed, so `terminate_child`, a kill or shutdown can end the child before +or during it, as fatal signals end an OTP process in `handle_continue`. +This design depends on #259 (0.9). + +### `start_child` + +1. **Queued** on the loop, in arrival order. If the supervisor is already + closed: `Rejected { Stopped, args }` at once. +2. **Admission** when the loop reaches it: closed → `Rejected { Stopped, args }` + (also for a request still queued when shutdown begins); cap reached → + `Rejected { MaxChildren, args }`; native capacity → `Rejected { Placement, args }`. + Otherwise the slot is created (`Starting`), counted from now on. +3. **Construction**: arguments are moved (Temporary) or cloned (restartable; + the original is retained by the slot) inside the tracked attempt, on the + target group, outside framework locks. The factory runs, then + `started()`, bounded together by `startup_timeout`. A panicking `clone()` + is a failed attempt like a factory panic. +4. **Commit.** Readiness commits under the gate, only while it is open. The + commit is the success: from then on `start_child` returns + `Ok(Started)`, even if shutdown begins before the caller observes it + (success is historical, like `ActorRef::ready()` and `start()`'s + readiness, `supervision.rs` `start_owned`). An ignore answers + `Ok(Ignored { pending })` after cleanup and finalization (above). The returned `actor` may + already be dead: if the child crashed between the commit and the caller's + wake-up, it is handled by the restart table and `child.current()` + resolves the replacement (Codex 2). +5. **First-start failure.** Factory error or panic, panic or stop in + `started()`, `Init::error`/`Init::stop`, or `startup_timeout`: the + generation is stopped and cleaned up without `stopped()` (a failed init + never runs it, as OTP never calls `terminate/2` after a failed `init/1`; + #259 rev. 3: `stopped()` runs only after a ready commit), its state is + dropped and its owned work joined, the slot finalized and removed, and + `FailedToStart { cause: ChildStartError, cleanup_stuck: false }` returned. Never retried, never charged (OTP). If the cleanup misses its + deadlines (E3 rows 3-4), `FailedToStart { .., cleanup_stuck: true }` is + returned at the deadline; the slot stays counted and its work stays owned + by the system until it really ends, as S2 releases `start()`'s waiter + (Codex 4, agy 7). The supervisor is not failed: see + [Stuck children](#stuck-children). +6. **Shutdown during construction**: the attempt is cancelled (state dropped + without hooks if `started()` had not begun, L2; otherwise the parent exit + signal, applied when `started()` returns, and still no `stopped()`, since + the child never committed ready); `Aborted` is returned after its cleanup or deadline. The error + reflects what ended the attempt: a factory failure recorded before + shutdown stays `FailedToStart` (agy 7). +7. **Cancellation** of the `start_child` future does not cancel the start + (R4); a child that becomes ready is supervised and listed. OTP behaves the + same when the caller dies. + +### Races + +| Race | Outcome | +|---|---| +| two `start_child` calls, cap reached by the first | served in arrival order: the first is admitted, the second gets `Rejected { MaxChildren, args }` | +| `start_child` vs shutdown, while queued | `Rejected { Stopped, args }` | +| `start_child` vs shutdown, during construction | `Aborted`; never `Ok` unless readiness committed first (`NoStartAfterShutdown`) | +| `start_child` vs shutdown, after the commit | `Ok`; the child is then stopped with the others | +| `start_child` vs a sibling's crash | the crashed child keeps its slot through cleanup, backoff and the replacement (`MaxChildrenBound`, control `UncountedRestart`) | +| `start_child` vs a sibling's removal | the slot frees only after the removed child's cleanup and slot finalization | +| `terminate_slot` vs a crash of that child | the loop takes them in order. Exit first: a pending restart is cancelled and refunded, or the restart attempt (which holds the loop) finishes and the call then terminates the new generation. Terminate first: the crash is consumed by the termination, no restart. Either way the child is removed and never restarted (`TerminatedNeverRestarted`, `NoPublishAfterStop`) | +| `terminate_child(id)` vs a crash of that child | the id is looked up when the loop handles the call. If the slot's last published id is still `id` (cleanup, backoff, a failed replacement), the child is terminated as above. If a replacement committed readiness before the call reached the head, `id` is stale: `NotFound`, and the replacement keeps running (Elixir; `TermResultsSound`, control `SlotLookup`) | +| `terminate_slot(id, expect)` vs a restart | the expectation is compared when the loop handles the call, under the same order as everything else: if the slot's last published child is no longer `expect`, `Stale { current }` and nothing is done; a child in cleanup or backoff whose last published id still matches is terminated (`TermResultsSound`, control `IgnoreExpect`) | +| `terminate_child` vs shutdown | a call still queued when shutdown begins gets `Stopped`; a call in progress resolves when the child is removed (`Ok`) or at its deadline (`CleanupStuck`) (control `QueuedTermOk`) | +| two calls for one child | the second is handled after the first completed: `NotFound` if the child was removed, `CleanupStuck` if it is stuck (Elixir; no shared waiters) | +| a terminate whose child gets stuck | `CleanupStuck` is committed at the deadline and never changes, even if the work ends later (`TermResultsSound`, `TermResultStable`, control `StuckResultLost`) | + +### Restart identity and termination keys + +- Every generation has a new `ActorId`, mailbox and state (M4). The slot's + `DynamicChildId` never changes. `current()` returns the latest ready + generation; `wait_for_generation(n)` waits for a newer one (V4). +- The **termination key** of a slot is its **last published** `ActorId`, + compared when the loop handles the call (not when it was made). + It is kept through cleanup, backoff and failed replacement attempts, and + switches only when a replacement's readiness commits, as OTP keeps the + original pid as the `restarting` entry's key and Elixir keeps + `current_pid` (Codex 3, agy 5). A call with an older id after a + successful replacement gets `NotFound`; only a slot-based call + (`terminate_slot`, `DynamicChild::terminate`) is guaranteed to reach the + child whatever its generation. +- `which_children` reports that key and whether the child is ready, so a + child seen restarting can be terminated by key or by slot. +- Callers that find children by a domain key keep their own map until rank + 12 ([below](#interaction-with-rank-12-scoped-registries)). + +### Terminating one child + +`terminate_child` is OTP's `shutdown/2` for one child, run by the loop: + +1. Look the target up (id or slot, above). Not found: `NotFound`. Already + stuck: `CleanupStuck`. +2. Mark the slot terminated (no restart from now on); cancel a pending + restart and refund its reservation. +3. Send the parent exit signal `Shutdown`: a non-trapping child begins exit + after its current handler and skips `stopped()` (E2, decision 2); a + trapping child handles the messages queued before the signal, then runs + `stopped()` (E3). +4. After `shutdown_timeout` without reaching its death point, kill it + (`Killed`, E1). OTP's kill ends the process at that point. Spawned's kill + is cooperative (R), so Spawned adds a second `shutdown_timeout` after the + kill; a child that misses it, or whose owned cleanup misses its deadline, + is stuck and the call returns `CleanupStuck` at that moment. +5. Otherwise `Ok` once the child is removed. + +The loop is held for the whole call, through removal or the deadline (as +OTP's supervisor is blocked in `terminate_child` and Elixir's handles it in +its call handler); deadline monitoring and the child's cleanup run off the +loop. + +### Stuck children + +OTP's `kill` always ends a process, so an OTP supervisor never waits past +the shutdown timeout (except with `infinity`). Spawned's kill is +cooperative (R): a child can stay in a handler, in `stopped()` or in owned +cleanup past every deadline. A child is **stuck** when, after its stop +signal, it misses the kill and the second interval, or when its owned +cleanup misses its deadline (`shutdown_timeout` from exit begin for a child +that ended on its own, E3 row 4: one interval, no kill). + +The classification uses the exit reason only: a cleanup that is still +running is not a recorded cleanup failure, so it does not make a Transient +child restartable (revision 2 contradicted itself here; Codex F3, agy 1). + +| The stuck child | Effect | +|---|---| +| would not be restarted: Temporary; Transient after a normal exit (`Normal`, `Shutdown`); removed by `terminate_child`; a failed first start | **only that child is affected.** Its slot stays counted and its work owned until it really ends, then the slot is removed. The failure is in its `ChildSnapshot::last_error` and the report; a waiting `terminate_child` gets `CleanupStuck`, a waiting `start_child` gets `FailedToStart { cleanup_stuck: true }`. The supervisor and its siblings are unaffected | +| would be restarted: Permanent; Transient after an abnormal exit; a failed replacement of a restartable child | the supervisor **fails** and exits abnormally: it cannot start the replacement while the old generation lives (V3), and OTP would have restarted it (decision R2) | +| being stopped by shutdown | the shutdown report is incomplete and records the failure (V9, S3); "done" waits for it | + +Escalation cannot make an unkillable computation disappear. The failed +dynamic supervisor's parent restarts the subtree only after the descendant +barrier (V8): the stuck generation still holds its slot, its group capacity +and whatever it touches until its code returns. What escalation gives is +visibility (the parent and the report know) and the OTP restart policy once +the work ends. Model: `StuckIsolated` checks the classification against the +table, not against the label the action chose (controls `StuckFailsAll`, +`MisclassifyStuck`). + +### Shutdown of all children + +When the supervisor closes (`stop`, `shutdown(deadline)`, system shutdown, +its parent, or a failure): + +1. Admission closes: queued starts get `Rejected { Stopped, args }`, the + construction in progress is cancelled (`Aborted`), pending restarts are + cancelled and refunded. +2. **Fan-out:** the supervisor sends every live child the parent exit + signal, one after another without awaiting any child's completion, then + waits. Children have no order (OTP: "not defined"). Model: + `ConcurrentShutdown`, control `Sequential`. +3. **Deadlines:** each child's intervals are measured from its own signal + (E3): kill after `shutdown_timeout`, stuck after a second one. OTP arms + one timer after the whole fan-out, so a child signalled early gets the + fan-out time on top of its interval there; here it does not. This is an + inherited E3 deviation (B: per-child bounds independent of N), listed in + the alignment table. Shutdown takes at most the fan-out time plus + 2 × `shutdown_timeout` plus owned cleanup up to its deadline. +4. **Done** means every slot was removed: every generation reached + publication and its owned cleanup finished, its arguments dropped (V9; + `NoChildOutlivesSupervisor`, `ClosedLeadsToDone`). +5. `shutdown(deadline)` keeps the static meaning: `deadline` is the report + deadline; children still running then stay owned by the system (S3). + +The model's main configurations take the fan-out as one step, an ownership +abstraction: it establishes that every admitted child is signalled before +the supervisor waits, not timer epochs or scheduling bounds (time is +abstract). The refinement configuration `MCDynamicSupervisorCallers` runs +the fan-out one signal per step, interleaved with the children, with no +cleanup ever assumed to finish, and checks `FanoutCompletes`: every +admitted child is signalled even while signalled siblings never end +(control `Sequential` waits for each sibling and fails it). Timing claims +are for the implementation's tests. + +### Retained arguments + +- Restartable slots keep the original `Args`; each attempt receives a clone + made inside the attempt (on the target group, outside framework locks, + within `startup_timeout`). A panicking or hanging clone is a failed + attempt. +- **Generation cleanup and slot finalization are distinct.** Generation + cleanup (the actor's death, its state and queued messages, its helpers) + ends every generation; a failure recorded there feeds the Transient rule. + Slot finalization runs once, only after the loop decided to remove the + slot (no restart can follow): it drops the retained arguments and then + releases the native-capacity reservation and the `max_children` slot. +- Finalization runs as a tracked task on the template's group, never on the + control loop's executor and never under a supervisor lock, bounded by + `shutdown_timeout`. The loop awaits it (as it awaits factories) before it + takes the next operation, so a start queued behind a removal sees the + slot freed, not a transient `MaxChildren` (agy round 3). The slot stays + counted, and its native-capacity reservation held, until finalization + ended (model: state `finalizing`, invariant `RemovedAfterFinalize`, + control `EarlyFree`). A panicking destructor is recorded as a finalization + failure in the report (no restart: the decision was already made). A + destructor that hangs past the deadline makes the slot stuck as a + retiring child: it stays counted, it is reported, nothing else is + affected (Codex F8). +- `DynamicChild` handles hold no arguments and no scopes. + +### In-flight requests and deferred replies of a dying child + +As for any actor (exit-signals design, phases of an exit, with rank 11): + +- At the child's death point D every queued request and every open + `ReplyTo` token is answered `ActorStopped(final reason)`: `Shutdown` after + a clean stop, `Killed` after the kill, the crash reason after a crash. A + request or registration after D gets `NoProc`. +- A non-trapping child stopped by its supervisor (`terminate_child` or + shutdown) skips `stopped()`, so cleanup that must always run belongs in + `Drop`, in an owner that monitors the child, or needs `trap_exit` (and + even then not after a kill). +- Pipe jobs of the child are cancelled at exit begin and joined after + publication (rank 11 step 4) within the cleanup deadline; the slot frees + only after that join. +- A replacement never receives the old generation's queue, tokens or jobs + (V4; rank 11 `ActorId` fencing). + +### Links and monitors + +- The supervisor is the parent of every child generation (E3). It is not an + actor: it observes children through internal completion state, not links + or a mailbox (V9), so a child's backlog never delays its exit handling and + a child cannot unlink itself from supervision. (OTP links to children and + uses a monitor only while shutting one down, so that a child that called + `unlink(Sup)` cannot hang the supervisor; Codex 14.) +- Children can link to and monitor each other and outside actors as usual. +- Owners that track children should monitor them; the `Down` arrives exactly + once with the final reason, also after a kill or a skipped `stopped()`. + +## Erlang alignment + +| # | Rule | OTP / Elixir | This design | Reason for any deviation | +|---|---|---|---|---| +| 1 | `start_child` is synchronous and returns the child | `{ok, Pid}` after the start function returns | `Ok(Started { actor, child })` after `started()` | aligned; `child` is an addition (row 9) | +| 2 | Operations serialised by the supervisor | one process: calls and `'EXIT'` messages handled in mailbox order, one at a time | one control loop over one FIFO queue of starts, terminate calls, exits and retries | aligned (decisions Q1, R1) | +| 3 | Template plus per-call args | `ExtraArgs` appended (Elixir: fixed `extra_arguments` prepended) | typed `Args` passed to the factory | T | +| 4 | `ignore` | `{ok, undefined}`, nothing stored; on restart the child is dropped | `Ok(Ignored { pending })`, nothing kept after cleanup; on restart the child is removed | aligned (decision G3); `pending` is R (cleanup can outlive the answer) | +| 5 | Start failure | `{error, Reason}`, not counted, not retried | `FailedToStart`, not counted, not retried, after cleanup or at its deadline | aligned; the deadline release is R (S2) | +| 6 | Default restart type | `permanent` | `Permanent` | aligned | +| 7 | Temporary children keep no args | `mapsets` | `temporary()` moves args once, no `Clone` | aligned; R for the separate constructor | +| 8 | `terminate_child` key | pid, looked up when the call is handled, kept through failed restarts | last published `ActorId`, looked up when the loop handles the call; `NotFound` (Elixir) otherwise, including for a second call | aligned with Elixir; OTP's `ok` for a dead unknown pid is a `find_child` artefact | +| 9 | Restart identity | new pid, found through names | new `ActorId`; stable `DynamicChildId`, `current()`, `terminate_slot` | addition, consistent with `SupervisedChild` (instance-bound references) | +| 10 | `restart_child`, `delete_child` | `{error, simple_one_for_one}` | not provided | aligned (absent at compile time: T) | +| 11 | `which_children` | pid or `restarting`, unordered | last published id plus `ready`, unordered | aligned plus fields | +| 12 | `count_children` | `specs` 1, `active` excludes restarting | same | aligned with OTP | +| 13 | `max_children` | Elixir: default infinity, `0` allowed, start only, counts restarting | same; frees after cleanup | aligned; B for freeing after cleanup | +| 14 | Restart budget | every restart attempt counts; Elixir default 3 in 5 s | same rule and defaults | aligned (decision Q3) | +| 15 | Exhaustion | terminate children, exit `shutdown` | terminate children concurrently, exit `Shutdown`, diagnostic in `failure()` | aligned (decision Q5); static nested supervisors follow in a separate PR | +| 16 | Shutdown order and timer | parallel, undefined order, one timer armed after the fan-out, then `kill` | parallel, each child's interval from its own signal, `kill`, then a second interval and stuck | timer epoch: inherited E3 deviation (B), early children get no fan-out time on top; the second interval is R | +| 17 | Shutdown signal | `exit(Child, shutdown)`; a trapping child runs `terminate` | parent exit signal; trapping child runs `stopped()` after its backlog; non-trapping skips it | aligned (E2, E3) | +| 18 | `start_child` during shutdown | the queued call exits with the supervisor's reason or `noproc` | `Rejected { Stopped, args }` or `Aborted` | R: no caller exit in Rust; T: the arguments come back | +| 19 | Restarted dynamic supervisor | empty | empty | aligned | +| 20 | Backoff | none | none by default; opt-in per supervisor | aligned by default (decision Q3) | +| 21 | Shutdown admission | the supervisor processes its queue in order; a start queued behind the shutdown is never handled | admission closes at once, the construction in progress is cancelled | B (exit-signals design) | +| 22 | When a slot frees | at `'EXIT'` | after owned cleanup and the argument drop (V3) | R and B: destructors and owned helpers outlive the last hook | +| 23 | A child that ignores `shutdown` | killed after the timeout; the kill always ends it | killed cooperatively after the timeout; if it misses a second interval it is stuck, isolated unless it would restart | R: Rust cannot kill a thread; policy in [Stuck children](#stuck-children) | +| 24 | Calls in flight to a dying child | `'EXIT'`/monitor tells callers | `ActorStopped(reason)` at D, `NoProc` after | aligned (rank 11, v0.8) | +| 25 | Heterogeneous specs | Elixir: any spec per call | one typed template | T; decision Q2 | +| 26 | Nested supervisor's shutdown wait | `infinity` by default for supervisor children | waits for the inner supervisor by default; a finite value only reports | aligned | + +## Non-guarantees + +- **No order** among dynamic children, at start (beyond arrival order on the + loop) or shutdown, and none in `which_children`. +- **No queueing** at `max_children`: a full supervisor rejects. Waiting for + a slot is rank 17's admission. +- **No parallel construction:** one slow `started()` delays the supervisor's + other operations (OTP's behaviour). Use the post-start continuation for slow work. +- **No exactly-once start under cancellation:** a dropped `start_child` + future may still produce a supervised child. +- **No state or queue carried across a restart** (V4). +- **No transparent reference:** `Started::actor` is the first generation + only and may already be dead when observed. +- **No preemption:** a stuck child keeps its slot and its resources until + its code returns; Spawned only reports it. +- **`which_children`/`count_children` are snapshots.** +- **No bounded memory per child** (rank 18a) or per mailbox (rank 17). + +## Semantics contract: what this adds and touches + +New guarantees (section 6 of [semantics.md](semantics.md), ids proposed): + +| Id | Guarantee | Checked by (planned) | +|---|---|---| +| V10 | **Dynamic admission.** One control loop takes starts, terminate calls, exits and retries from one FIFO queue, one at a time. A start is admitted atomically with the gate and the count; success commits only while admission is open and is then historical; a rejected start returns its arguments; an ignored start stores nothing; a first-start failure is returned after cleanup or at its deadline, uncharged and unretried; every call is answered even if cleanup never ends. | `DynamicSupervisor!FifoOrder`, `!SerialConstruction`, `!NoStartAfterShutdown`, `!OkMeansReady`, `!FirstStartNeverRetried`, `!FailedAfterCleanup`, `!FailureCauseKept`, `!StartAnswered` (CallerSpec); trace validation | +| V11 | **Cap counts restarting children.** A child holds its slot from admission until removal, through cleanup, backoff, replacement and a stuck cleanup. | `!MaxChildrenBound` | +| V12 | **Terminated means removed.** The target is looked up when the loop handles the call; after a found `terminate_child` the child is never restarted or republished, a pending restart is cancelled and refunded, `Ok` means removed, `CleanupStuck` is committed at the deadline and never changes; a call still queued at shutdown gets `Stopped`. | `!TerminatedNeverRestarted`, `!NoPublishAfterStop`, `!ReservationsMatch`, `!TermResultsSound`, `TermResultStable`, `!TerminateAnswered` (CallerSpec) | +| V13 | **Concurrent shutdown.** Every admitted child is signalled without awaiting another; the supervisor is done only after every child finished. | `!ConcurrentShutdown`, `!FanoutCompletes` (refinement, CallerSpec), `!NoChildOutlivesSupervisor`, `!ClosedLeadsToDone` | +| V14 | **Stuck isolation.** A child stuck while retiring (by the exit reason; a stall is not a recorded cleanup failure) fails only itself; the supervisor fails only for a stuck child the table would restart, budget exhaustion, or during shutdown. | `!StuckIsolated` | + +Touched: + +- **V1** (restart table) per child, including the cleanup-failure rule: + `!RestartFollowsPolicy` (both directions, checked at the decision: + reservation, attempt or exhaustion; no retirement of a restartable child + while open), `!TemporaryNeverRestarted`, + `!RecoveryProgress`. +- **V3, V4** per slot: `!AtMostOneGeneration`, `!PublishedIsLive` (also + requiring readiness). +- **V5** (budget): supervisor-wide, start failures excluded, reservations + modelled: `!ChargedRestarts`, `!ReservationsMatch`, `!BudgetBounded`, + `!ExhaustionCloses`. Exhaustion stops all children concurrently and exits + `Shutdown`. +- **V8** (escalation): a dynamic supervisor is a nestable subtree. +- **V9** (shutdown): concurrent instead of reverse order for dynamic + children; `!NoGenerationAfterClose`. +- **S1, S2**: the dynamic supervisor is a shutdown unit; its admission + closes with the tree. +- **§10** gains the non-guarantees above; **§11** gains rows 16, 21, 22, 23 + and 26. + +No guarantee in sections 1-5 changes. + +## Interaction with rank 12 (scoped registries) + +**Registry-owned lookup is deferred to rank 12.** Rank 12a ships +`start_child` returning a handle and nothing keyed: + +- The two are independent: a dynamic supervisor is useful without keys (one + actor per accepted socket counted by `max_children`), and a keyed registry + is useful without supervision. +- Conflict policy for a key is domain policy (ethrex keeps the first + connection; another user may replace-and-stop), which belongs in the + registry's design. +- Keys in 12a would make it depend on rank 12's scoping before it exists. + +Until rank 12, the pattern depends on the restart type (Codex 13): + +**Temporary children** (one generation): the owner's map plus a monitor of +that generation, guarded by the monitor reference. + +```rust +let StartOutcome::Started(started) = peers.start_child(args).await? else { + return Ok(()); // the factory or started() ignored: nothing to track +}; +let mref = ctx.monitor(&started.actor.child_handle()); +self.by_key.insert(key, Entry { child: started.child, monitor: mref }); +// Handler: remove the entry only if it still holds this monitor. +fn on_down(&mut self, down: Down) { + if let Some(key) = self.by_monitor.remove(&down.monitor_ref) { + if self.by_key.get(&key).is_some_and(|e| e.monitor == down.monitor_ref) { + self.by_key.remove(&key); + } + } +} +``` + +**Restartable children:** the entry belongs to the slot, not to a +generation. Keep the `DynamicChild` in the map until the slot is removed +(learned from `terminate_child`'s result, or from `child.snapshot()` being +terminal), and resolve the current generation with `child.current()` on +each use; or let each generation register itself (`ctx.register_name` in +`started()`, generation-owned, S5). A monitor of one generation only says +that generation died, not that the slot is gone. + +**Composition once rank 12 lands:** + +- A keyed start is `start_child` plus a generation-owned registration made + by the child or by the supervisor on readiness, released when that + generation's cleanup finishes, so an old cleanup can never remove a + replacement (S5, the ethrex #7435 bug). +- Restartable children re-register per generation; lookups between a crash + and the replacement's readiness find nothing (V4). +- Duplicate policy is the registry's; `max_children` and the budget stay the + supervisor's. + +## What the model establishes + +[`DynamicSupervisor.tla`](../../verification/tla/DynamicSupervisor.tla) +(revision 3) models one dynamic supervisor, `start_child` calls made at any +moment, and `terminate_child` calls, each aimed at a slot by the id the caller +saw, by slot, or by slot fenced with `expect` (the id@generation the caller +saw). The control loop takes starts, terminate calls, +exit notices and backoff retries from one FIFO queue; the exit of the child +an operation waits for is consumed by that operation. Each slot's restart +type is chosen in `Init`. Budget reservations, stamping, refunds and window +expiry are explicit; backoff is a constant (off: the attempt runs in the +exit's turn and a failed one re-queues; on: reserve, timer, retry through +the queue). Children can ignore, fail, time out, exit, be stopped (Shutdown, +or Killed after the kill), record a cleanup failure, or get stuck before or +after their death point. + +Event invariants (late commits, publications and generations; forbidden +restart decisions or retirements; restart attempts; queue order) read +history variables that `GhostUpdate` computes from each step's state change, +separately from the actions. `alive` keeps every live generation. + +Two fairness sets. `CallerSpec` assumes only the loop's work and deadlines +(startup timeout, cleanup deadline) progress; no user code is assumed to +finish. `StartAnswered`, `TerminateAnswered` and `FanoutCompletes` hold +under it (Codex F4). `Spec` adds progress of readiness, stops, cleanup and +stuck children, for `ClosedLeadsToDone` and `RecoveryProgress`. + +| Invariant | Meaning | +|---|---| +| `AtMostOneGeneration` | a slot never has two live generations | +| `PublishedIsLive` | `current()` returns only the running, live, latest, ready generation | +| `NoChildOutlivesSupervisor` | done means every child finished and was removed | +| `MaxChildrenBound` | children held never exceed `max_children` | +| `SerialConstruction` | at most one generation is being constructed | +| `FifoOrder` | every operation the loop selects is the head of the queue at selection (not merely a non-decreasing ticket: a later operation served first, then the earlier one rejected at close, is caught) | +| `TemporaryNeverRestarted` | a Temporary child has one generation | +| `TerminatedNeverRestarted` | no generation begins after a found `terminate_child` | +| `NoGenerationAfterClose` | no generation begins after admission closed | +| `NoPublishAfterStop` | no generation is published after close or termination | +| `NoStartAfterShutdown` | no `start_child` outcome (`Ok` or the ignore decision) commits after admission closed | +| `RestartFollowsPolicy` | every restart decision (reservation, attempt, exhaustion) is allowed by the table; no restartable exit is retired while open | +| `FirstStartNeverRetried` | a failed first start is never retried | +| `FailedAfterCleanup` | `FailedToStart`/`Aborted` only once cleanup really finished (removed, no live generation) or with the deadline failure recorded | +| `FailureCauseKept` | the start error reflects what ended the attempt | +| `ChargedRestarts` | every restart attempt is charged exactly once; first starts never | +| `ReservationsMatch` | reservations are exactly the pending restarts | +| `BudgetBounded` | stamped grants plus reservations stay within `max_restarts` | +| `ExhaustionCloses` | exhaustion fails and closes the supervisor | +| `StuckIsolated` | the supervisor fails only by exhaustion, a stuck child the table would restart (checked against the table), or while closing | +| `ConcurrentShutdown` | once waiting, every running child has its stop signal | +| `OkMeansReady` | `Ok` only for a child that became ready | +| `QueuedTermStopped` | a terminate call still queued when shutdown began is answered `Stopped` and stays so | +| `RemovedAfterFinalize` | a slot is freed only after slot finalization (and an ignored attempt's cleanup) | +| `TermResultsSound` | `Ok` only after removal; a call in progress when its child got stuck reports `CleanupStuck`; a pending call holds the loop; an id call or a fenced slot call reaches only the generation it named | + +Action properties: `NeverReopens`, `TermResultStable` (a committed terminate +result never changes). Liveness: `StartAnswered`, `TerminateAnswered`, +`FanoutCompletes` (CallerSpec), `ShutdownAnswersStarts` (CallerSpec without +startup deadlines, `MCDynamicSupervisorAbort`); `ClosedLeadsToDone`, `RecoveryProgress` +(Spec). + +Configurations (TLC 2.19, fede, 4 workers, `nice -n 19`). These are +bounded checks: two slots for the broad instances, three for the targeted +one; no cutoff argument is claimed (Codex F10). + +| Configuration | Instance | Distinct states | Depth | Time | +|---|---|---|---|---| +| `MCDynamicSupervisor` (per PR; safety, action properties; `Spec`) | 2 slots, every pair of restart types, two terminate calls (by id, by slot fenced with `expect`), `max_children` 1, budget 1, one window release, no backoff, exits `Normal`/`Panic`, start failures factory/`Normal`/timeout, ignore, cleanup failures | 8,488,736 | 30 | 1m26s | +| `MCDynamicSupervisorBackoff` (per PR; safety) | as above with backoff | 9,878,333 | 36 | 1m48s | +| `MCDynamicSupervisorZero` (per PR; safety) | as the first with budget 0 | 1,170,745 | 21 | 12 s | +| `MCDynamicSupervisorThree` (per PR; safety) | 3 Permanent crashing children, `max_children` 2, shared budget 1, FIFO with three arrivals | 442,239 | 30 | 7 s | +| `MCDynamicSupervisorCallers` (per PR; `StartAnswered`, `TerminateAnswered`, `FanoutCompletes` under `CallerSpec`) | 2 slots, `max_children` 2, one call, fan-out as separate steps | 3,380,536 | 29 | 6m33s | +| `MCDynamicSupervisorLive` (per PR; `ClosedLeadsToDone`, `RecoveryProgress` under `Spec`) | 2 slots, one call by slot, backoff | 581,563 | 34 | 55 s | +| `MCDynamicSupervisorDeep` (weekly; safety) | budget 2, two releases, `max_children` 2, backoff, one call | 9,992,213 | 45 | 1m35s | + +Negative controls (`negative_checks.py`, run one at a time; each checks +`TypeOK` and only the named property). Every invariant and liveness +property above has at least one; the two action properties do not. + +| `Fault` | Mutation | Fails | Config | +|---|---|---|---| +| `IgnoreMax` | admission ignores the cap | `MaxChildrenBound` | main | +| `UncountedRestart` | a crashed child frees its slot until it restarts | `MaxChildrenBound` | main | +| `RestartTemporary` | Temporary follows the Permanent rule | `TemporaryNeverRestarted` | main | +| `RestartTerminated` | termination does not stop a restart | `TerminatedNeverRestarted` | main | +| `AcceptDuringShutdown` | a start admitted and committed after close | `NoStartAfterShutdown` | main | +| `RestartAfterClose` | a pending restart proceeds after close | `NoGenerationAfterClose` | backoff | +| `NoEscalate` | exhaustion drops only that child | `ExhaustionCloses` | main | +| `EarlyDone` | done before every child finished | `NoChildOutlivesSupervisor` | main | +| `SkipSignal` | the fan-out skips a child | `ConcurrentShutdown` | main | +| `ConcurrentStart` | constructions not serialised | `SerialConstruction` | main, cap 2 | +| `LaterOp` | the loop admits a later start first | `FifoOrder` | main | +| `StuckFailsAll` | any stuck child fails the supervisor | `StuckIsolated` | main | +| `MisclassifyStuck` | a retiring stuck child classified as restartable | `StuckIsolated` | main | +| `PublishAfterClose` | a replacement publishes after close | `NoPublishAfterStop` | main | +| `PublishAfterExit` | a generation stays published after it exits | `PublishedIsLive` | main | +| `OverlapGeneration` | the replacement starts before the old cleanup ended | `AtMostOneGeneration` | main | +| `PublishBeforeReady` | a replacement is published at construction | `PublishedIsLive` | main | +| `PrematureOk` | `Ok` committed at admission | `OkMeansReady` | main | +| `UnchargedRetry` | a failed replacement's retry is not charged | `ChargedRestarts` | main | +| `ChargeFirstStart` | a first start is charged | `ChargedRestarts` | main | +| `TransientNormalRestart` | Transient restarts after a normal exit | `RestartFollowsPolicy` | main | +| `TransientNormalRestart` | the same at zero budget: a normal exit exhausts the budget | `RestartFollowsPolicy` | main, budget 0 | +| `PermanentRetires` | Permanent is not restarted | `RestartFollowsPolicy` | main | +| `RetryFirstStart` | a failed first start is retried | `FirstStartNeverRetried` | main | +| `EarlyFailedReply` | `FailedToStart` before cleanup | `FailedAfterCleanup` | main | +| `EarlyRemove` | a failed start removed with its generation still alive | `FailedAfterCleanup` | main | +| `LateFailedOverwrite` | a pre-shutdown failure reported as `Aborted` | `FailureCauseKept` | main | +| `NoRefund` | a cancelled restart keeps its reservation | `ReservationsMatch` | backoff | +| `ExpireReserved` | window expiry releases a reservation | `ReservationsMatch` | backoff | +| `OverReserve` | a restart reserved beyond the budget | `BudgetBounded` | main | +| `TermReplyEarly` | `terminate_child` returns before removal | `TermResultsSound` | main | +| `SlotLookup` | an id call reaches a newer generation | `TermResultsSound` | main | +| `QueuedTermOk` | shutdown answers a queued call `Ok` | `QueuedTermStopped` | main | +| `EarlyFree` | removal frees the slot before finalization | `RemovedAfterFinalize` | main | +| `IgnoreAfterClose` | an ignore decided after shutdown began | `NoStartAfterShutdown` | main | +| `IgnoreFreesEarly` | an ignored attempt frees the slot at once | `RemovedAfterFinalize` | main | +| `StuckResultLost` | `CleanupStuck` not committed; later turns into `Ok` | `TermResultsSound` | main | +| `IgnoreExpect` | a fenced call terminates a child that moved on | `TermResultsSound` | main | +| `NoAbort` | a start racing shutdown is not cancelled | `ShutdownAnswersStarts` | abort: `CallerSpec` without startup deadlines, which passes unmutated (with deadlines the timeout would answer the start and mask the mutation) | +| `NoDeadline` | no cleanup deadline | `StartAnswered` | callers | +| `TermLost` | a found call never signals the child | `TerminateAnswered` | callers | +| `Sequential` | the fan-out waits for each signalled child | `FanoutCompletes` | callers | +| `StuckBackoff` | shutdown does not cancel a pending restart | `ClosedLeadsToDone` | live | +| `LostRestart` | a decided restart is never attempted | `RecoveryProgress` | live | + +CONTROLS_NOTE + +Not modelled: handler bodies, mailboxes and requests (`Lifecycle.tla`; +rank 11's models); real time; native-capacity reservations and slot +finalization as separate steps (a counted slot and its removal stand for +them); nesting (one child of `NestedSupervision.tla`'s parent); repeated +churn of one slot (each slot is one start call; a reusable-slot model would +need fresh identities). Apalache inductive invariants are a follow-up. + +## Test plan: relating the model to the code + +Standing rule: a model counts only once real runs are checked against it. +The implementation must emit lifecycle-trace events (feature +`lifecycle-trace`, as `TraceSupervision.tla` uses today) that map one to one +onto `DynamicSupervisor.tla` actions, and ship trace-validation tests that +replay real runs as model behaviours. + +**Events.** Each carries the supervisor's trace id, the slot (`DynamicChildId`), +the generation, and where noted the queue ticket or call id. + +| Event | Emitted when | Model action | +|---|---|---| +| `DReq` (slot, ticket) | `start_child` queued, or rejected because closed | `Request` | +| `DAdmit` (slot, ticket, outcome: admitted / max) | the loop takes a start | `LoopAdmit` | +| `DReject` (slot) | shutdown answers a queued start | `RejectQueued` | +| `DReady` (slot, gen) | readiness commits | `Ready` | +| `DIgnore` (slot, gen) | the factory returned `ChildStart::Ignore` or `started()` returned `Init::ignore()` (cleanup follows, as for an exit) | `Ignore` | +| `DStartFail` (slot, gen, reason) | factory error or panic, stop or panic in `started()` | `StartFail` | +| `DStartTimeout` (slot, gen) | `startup_timeout` fired | `StartTimeout` | +| `DAbort` (slot, gen) | shutdown cancelled a construction | `AbortStart` | +| `DExit` (slot, gen, reason) | a running generation began exiting on its own | `SelfExit` | +| `DStopSeen` (slot, gen, reason) | a signalled generation began exiting (Shutdown/Killed) | `StopObserved` | +| `DCleaned` (slot, gen, cleanup_failure, ticket?) | owned cleanup finished; the exit notice is queued with a ticket, or carries none when the start or terminate waiting for this child consumes it directly | `CleanupDone` | +| `DStuck` (slot, gen, kind) | a deadline was missed | `CleanupStuck` | +| `DStuckDone` (slot) | a stuck child or finalization finally ended (after `DStuck`, the generation's later end emits only this, never `DCleaned`) | `StuckDone` | +| `DFinalized` (slot) | slot finalization ended: retained arguments dropped, capacity and the slot released; a pending start answered | `Finalize` | +| `DDecide` (slot, ticket?, outcome: finalize / backoff / restart / exhausted) | the loop handled an exit; "finalize" starts slot finalization, which `DFinalized` (or `DStuck`) ends | `Decide` | +| `DRetryQueued` (slot, ticket) | the backoff timer fired | `BackoffFire` | +| `DRetry` (slot, gen, ticket) | the loop took a retry | `BackoffDone` | +| `DCancel` (slot) | a pending restart was cancelled and refunded; finalization starts | `CancelBackoff` | +| `DTermCall` (call, slot, named gen, ticket) | `terminate_child`/`terminate_slot` called; the named generation is whatever the caller passed, current or superseded | `TermCall` | +| `DTermLookup` (call, outcome: found / notfound / stuck / stale) | the loop handled the call | `LoopTerm` | +| `DTermReject` (call) | shutdown answered a queued call | `RejectQueuedTerm` | +| `DTermDone` (call, result) | the call resolved `Ok` | `TermResolve` | +| `DClose`, `DSignal` (slot), `DDone` | external or parent shutdown began (exhaustion and a restart-required or closing stuck child close admission themselves, inside `DDecide`/`DStuck`); a child was signalled (the last signal ends the fan-out); all children finished | `Close`, `SupSignal`/`SupSignalStep`, `SupDone` | +| `DExpire` | a grant left the window | `WindowExpire` | + +The trace checker (`trace_check.py`) learns a `dynamic-v1` schema that +replays these events as a `TraceDynamic.tla` behaviour, with the instance +constants taken from the run (slots, modes, calls, cap, budget, backoff). +The fan-out is emitted as one `DSignal` per child; the checker accepts the +signals of one shutdown as a single `SupSignal` step when no child event +falls between them, and checks the refinement configuration otherwise. + +**Tests the implementation must ship** (`concurrency/tests/dynamic_trace.rs`, +recorded in the `tla-traces` CI job, plus generated scripts in +`supervisor_policies`): + +1. Admission order: two starts at the cap; the second rejected with its + arguments. +2. First-start failures: factory error, panic in `started()`, startup + timeout, `Init::error`, ignore (factory and `Init::ignore()`); each + answered after cleanup with its `ChildStartError`; one with a stuck + cleanup. +3. Restart table per type and reason, with and without backoff, including a + failed replacement re-queued and retried, and a recorded cleanup failure + restarting a Transient child. +4. Budget: exhaustion at zero and at one, reservation refund on terminate + and on shutdown during backoff. +5. Terminate: by id, by slot, a stale id after a successful replacement, a + second call, a call during a restart attempt, a call queued at + shutdown, a stuck child, a fenced call whose child moved on (`Stale`). +6. Shutdown with several children, one stuck; a start racing shutdown; a + commit racing shutdown. +7. Seeded random scripts (as `supervision_trace`) for coverage. + +**Expected action coverage** (`trace_coverage.py`): every action of +`DynamicSupervisor.tla` reached by the dedicated tests, except the fault +branches; `WindowExpire` only in paused-time tests. The coverage baseline +must list them so that a regression fails CI, as for the static models. + +## Alternatives considered + +1. **Concurrent construction with atomic admission** (revision 1). + Rejected (Q1, Codex 1): it changes outcomes, not only timing (with a cap + of one, a start arriving during a failing start is rejected instead of + admitted), and OTP's own idiom for slow initialisation is to leave it out + of `init`. +2. **Heterogeneous children as the primary API.** Rejected for v1 (Q2); can + be added as a separate untyped handle without changing this contract. +3. **`max_children` that waits.** Rejected: Elixir rejects; waiting is rank + 17's admission. +4. **Free the slot at the exit signal.** Rejected: owned cleanup still holds + resources (B). +5. **Stop children in reverse start order.** Rejected: OTP does not order + them, and sequential stops multiply shutdown time. +6. **Fail the supervisor on any stuck child** (revision 1, as static V3). + Rejected (agy P0): a retiring child needs no replacement, so V3 does not + force it, and OTP's supervisor carries on after killing such a child. +7. **Terminate by slot only.** Rejected: OTP and Elixir terminate by pid; + both forms are offered. +8. **Keyed registration in 12a.** Rejected; see rank 12 above. +9. **Hold the old scope's capacity lease across a restart** (one reading of + revision 1's Q4). Rejected (Codex): it would keep the finished scope from + joining; the reservation is a separate permit owned by the slot. +10. **Return the arguments from every error.** Not possible after the + factory consumed them; only pre-admission rejections return them. +11. **A `try_reserve()` permit before `start_child`.** Not needed for the + ethrex migration once rejections return the arguments; it adds permit + lifetime and cancellation semantics. Later if a user needs it. + +## Follow-ups + +- **Static nested supervisors exit `Shutdown` on budget exhaustion** (Q5): + separate PR, changing `nested.rs`'s failure path; `NestedSupervision.tla` + and semantics V8 accordingly. The nested adapter's default + `shutdown_timeout` collision (agy 6) applies to static nested supervisors + too and belongs in that PR. +- **`terminate_child` on static supervisors** (Q6): separate design (OTP + keeps the spec, `restart_child`, `delete_child`; `Supervision.tla` and + `Cohorts.tla` changes). +- **Apalache inductive invariants** for `DynamicSupervisor.tla`. +- **Unified start (0.9):** the post-start continuation, `ChildStart::Ignore` + and `Init` start data are that design's; this design consumes them. +- **Introspection v1:** owns `ChildInfo`, `ChildCounts`, `ChildKey` and the + "blocked in terminate_child" report. +- **Implementation acceptance:** the [test plan](#test-plan-relating-the-model-to-the-code), evidence that dynamic tables, retained arguments and capacity + reservations add nothing to the ordinary actor and message paths (Codex + closing note). + +## Review resolutions + +Round 1: Codex (1 P0, 12 P1, 1 P2) and agy (1 P0, 7 P1, 1 P2), both "approve +after the listed changes", run without the author's answers. Each finding +was checked against the code and sources before acting on it. + +### Codex + +| # | Finding | Resolution | +|---|---|---| +| 1 (P0) | Concurrent construction changes outcomes (cap of one, a failing start), not only timing; not Rust-forced. Also: OTP's supervisor runs the start function, not `init` | **Accepted** (decision Q1). [The control loop](#the-control-loop) serialises starts, exit handling and terminations; model `SerialConstruction`, control `ConcurrentStart`. Sources row corrected | +| 2 | "Never `Ok` after shutdown" conflates commit with observation; `start()` keeps readiness historical | **Accepted.** Success commits only while open and is then historical, possibly with a dead first-generation reference ([`start_child`](#start_child) step 4). The model separates the commit (`Ready`) from anything the caller does later; `NoStartAfterShutdown` is about the commit | +| 3 | Termination identity must survive failed replacement attempts | **Accepted.** The termination key is the last published `ActorId`, kept until a replacement's readiness commits, as OTP and Elixir ([Restart identity](#restart-identity-and-termination-keys)); duplicates and stale ids specified in [Races](#races) | +| 4 | A failed start whose cleanup never joins leaves `start_child` unanswered | **Accepted.** `FailedToStart { cleanup_stuck: true }` at the deadline, slot still counted, work still owned (S2's rule). Model: `StuckDone` is fair only for liveness; `StartAnswered` holds because the stuck step answers | +| 5 | Exhaustion must exit `Shutdown`, not abnormally | **Accepted** (decision Q5): exits `Shutdown` with the diagnostic in `failure()`; static nested supervisors in a follow-up PR | +| 6 | The model omits reservation, stamping and refund | **Accepted.** Explicit `reserved`, `stamped`, `windowed`; reservation at the decision with immediate exhaustion; refund on cancel; expiry only of stamped grants. `ReservationsMatch`, `ChargedRestarts`, `BudgetBounded` (no longer implied by `TypeOK`); controls `NoRefund`, `ExpireReserved`, `UnchargedRetry`, `ChargeFirstStart`, and the per-PR `MCDynamicSupervisorZero` (budget 0) | +| 7 | Invariants too weak: `alive` overwritten, `BudgetBounded` implied by `TypeOK`, `PublishedIsLive` ignores readiness | **Accepted.** `alive` accumulates and loses only the cleaned generation; restart attempts are counted by a history variable; publication requires readiness. Controls `OverlapGeneration`, `UnchargedRetry`, `PublishBeforeReady`, `PrematureOk`. The point that controls prove sensitivity only for their mutation stands; every named invariant now has at least one control | +| 8 | Restart table and progress unverified; configs miss normal pre-readiness replacement failures and the cleanup-failure rule | **Accepted.** `RestartFollowsPolicy` in both directions, `RecoveryProgress`; `StartFails` includes `Normal`, `CleanupFails = {FALSE, TRUE}`, a zero-budget configuration. Controls `TransientNormalRestart`, `PermanentRetires`. "Fence asynchronous events by attempt identity": the model's per-slot generation plays that role; the implementation keeps the existing generation fencing | +| 9 | Concurrent shutdown needs a fan-out and deadline contract; stuck detection before D | **Accepted in the doc, kept abstract in the model.** Fan-out without awaits, each child's intervals from its own signal, timing including the fan-out ([Shutdown](#shutdown-of-all-children)); stuck detection before D (signalled but still running) and after D (cleanup) are both `CleanupStuck` in the model. The one-step fan-out is a documented abstraction, to be checked by trace validation | +| 10 | Retained arguments: clone can panic or block, drop can panic or hang | **Accepted.** [Retained arguments](#retained-arguments); `Sync` dropped | +| 11 | ethrex: the raw `tokio::spawn` writer (`server.rs:1542`) and framework listeners/timers are not covered; "no helpers" is wrong | **Accepted, confirmed in the code.** The client mapping now migrates the writer into an owned helper with a pending-frame policy and states that until then `max_children` bounds slots, not sockets | +| 12 | Monitoring fixes peer-table removal but not `teardown()`'s mempool and announcement cleanup when `stopped()` is skipped | **Accepted, confirmed** (`teardown()` clears in-flight transaction hashes). The mapping assigns each resource an owner that releases it on the `Down`, guarded by the connection's identity | +| 13 | The map-plus-monitor example only works for Temporary children | **Accepted.** Labelled Temporary-only, with the restartable pattern ([rank 12](#interaction-with-rank-12-scoped-registries)) | +| 14 (P2) | Elixir allows `max_children = 0`; pinned groups have no per-actor capacity; OTP's monitors are only for shutdown; termination by slot | **Accepted.** `Some(0)` allowed; pinned groups keep affinity only; links text corrected; `terminate_slot` added | + +### agy + +| # | Finding | Resolution | +|---|---|---| +| 1 (P0) | One stuck child (even retiring) fails the whole supervisor; a root ethrex supervisor would be bricked. The ethrex text also misstated self-exit timing (one interval, no kill) | **Accepted.** [Stuck children](#stuck-children): a retiring stuck child fails only itself; the supervisor fails only for a stuck child it would restart (V3) or during shutdown. `StuckIsolated`, control `StuckFailsAll`. The mapping's timing statement is corrected and recommends nesting the connection supervisors under the p2p supervisor anyway | +| 2 | No `RestartFollowsPolicy`; first-start rules unchecked | **Accepted.** `RestartFollowsPolicy`, `FirstStartNeverRetried`, `FailedAfterCleanup`, `ChargedRestarts` (covers "uncharged"), with controls. agy's `FailedAfterCleanup` required `alive = {}`; it is `removed` or `stuck`, because of Codex 4 | +| 3 | A constructing replacement can publish after `TerminateChild` or `Close` undetected; `lateOk` only covered first starts and was set by the guarded action | **Accepted in part.** History variables are computed outside the actions (`GhostUpdate`) for commits, publications and generations; `NoPublishAfterStop`, control `PublishAfterClose`. The `TerminateChild` half no longer arises: with the serialised loop, `terminate_child` cannot run while a replacement is being constructed (it waits behind it), which `SerialConstruction` and the loop's ownership enforce | +| 4 | Budget charged after backoff in the model; refund unchecked | **Accepted**, as Codex 6 | +| 5 | `terminate_child` target resolution: contradictions during replacement construction and `Starting`; no way to terminate from `which_children` | **Accepted.** Last-published key; serialisation answers the `Starting` case (a terminate queued behind a start finds the child); `terminate_slot`; `DynamicChildInfo` reports the key and readiness | +| 6 | The nested adapter's 5 s wait collides with the inner 2 × `shutdown_timeout`; redundant constructor arguments | **Accepted.** `DynamicSupervisorSpec::new(name, config, spec)`; default wait 2 × child `shutdown_timeout` + 1 s. The same collision in static nested supervisors goes to the follow-up PR | +| 7 | Stuck first-start cleanup must release `start_child`; a pre-shutdown failure must not be reported as shutdown; in-flight and duplicate terminates | **Accepted.** As Codex 4; `cause` recorded when the attempt ends (`FailureCauseKept`, control `LateFailedOverwrite`); terminate resolution modelled (`TermOkMeansRemoved`, `TerminateAnswered`, control `TermReplyEarly`) | +| 8 | ethrex `Handler` lacks the monitor check on the entry; awaiting `start_child` stalls accepts; `terminate_child` also skips `stopped()` | **Accepted.** The guard is in both sketches; the handshake moves out of `started()` (required now that starts are serialised); the `stopped()` note covers `terminate_child` | +| 9 (P2) | Jitter seed per slot; drop `Sync`; unconditional `Clone`, slot eviction; structured `FailedToStart` | **Accepted**, all four | + +### Round 1 open questions (decided as R1-R5) + +1. **Holding the loop during `terminate_child`** (OTP blocks the supervisor + up to 2 × `shutdown_timeout`): faithful, but a slow-to-stop child delays + every start meanwhile. Keep, or let the loop continue while the + termination completes? +2. **Stuck children that would restart** fail the supervisor (V3). An + alternative is to retire such a slot instead (no restart, no failure). + Failing matches the static supervisor and escalates; retiring would + silently weaken Permanent. +3. **The one-step fan-out abstraction** in the model: acceptable with trace + validation, or should the model interleave signals with child steps? + +### Round 2 + +Codex (F1-F9 P1, F10 P2) and agy (1-5 P1, 6 P2), both "approve after the +listed changes", no P0. Each was checked against the model and the doc. + +| Finding | Resolution | +|---|---| +| **Codex F1 = agy 2**: id calls looked up at call time in prose but not in the model; queued call at shutdown could become `Ok`; `Release` freed the loop before the terminate resolved; `CleanupStuck` could later become `Ok` | **Accepted.** Lookup happens when the loop handles the call; the model carries the generation the caller named and two calls (by id and by slot). A call still queued at shutdown gets `Stopped`. The loop stays held until the call resolves. `CleanupStuck` is committed at the deadline and never changes. Duplicates are not shared waiters: a second call is handled after the first and gets `NotFound` or `CleanupStuck` (Elixir). `TermResultsSound`, `TermResultStable`; controls `SlotLookup`, `QueuedTermOk`, `StuckResultLost`, `TermReplyEarly` | +| **Codex F2**: serialisation checked, arrival order not | **Accepted.** One FIFO queue of starts, terminate calls, exit notices and retries; history variable on the served ticket; `FifoOrder`, control `LaterOp`. The three-slot targeted instance has more arrivals | +| **Codex F3 = agy 1**: Transient normal exit with stalled cleanup listed as both isolated and restartable; `StuckIsolated` trusted the action's label; a wrong decision that exhausts the budget escaped `RestartFollowsPolicy` | **Accepted.** A stall is not a recorded cleanup failure: classification by exit reason only, Transient-normal stuck children are isolated. `StuckIsolated` re-derives "restart" from the table. `RestartFollowsPolicy` checks every decision (reservation, attempt, exhaustion). Controls `MisclassifyStuck` and `TransientNormalRestart` at zero budget | +| **Codex F4**: caller liveness assumed cleanup finishes | **Accepted.** `CallerSpec` gives progress only to loop work and deadlines; `StartAnswered` and `TerminateAnswered` hold under it; `ClosedLeadsToDone` and `RecoveryProgress` keep `Spec`. Control `NoDeadline` | +| **Codex F5 = agy 3**: `FailedAfterCleanup` checked a label | **Accepted.** It now requires removal with no live generation, or a recorded deadline failure; control `EarlyRemove` | +| **Codex F6 = agy 3**: `Sequential`'s witness signalled a queued, unadmitted start | **Accepted.** Fan-out targets admitted children only. `Sequential` now runs on the interleaved refinement with two admitted children (`max_children` 2) against `FanoutCompletes`; `ConcurrentShutdown` gets its own control `SkipSignal` | +| **agy 3**: `PublishedIsLive` ignored the slot state; `BudgetBounded`, `RecoveryProgress`, `TerminateAnswered` had no controls | **Accepted.** `PublishedIsLive` requires `running` (control `PublishAfterExit`); controls `OverReserve`, `LostRestart`, `TermLost`. Every invariant and liveness property now has a control; the two action properties do not, and the doc says so | +| **Codex F7**: 2 × T + 1 s cannot cover an unbounded fan-out; timer epoch is a deviation | **Accepted.** The nested adapter waits for the inner supervisor by default (OTP's `infinity`); a finite value is a reporting bound keeping the barrier. The per-child timer epoch is listed as an inherited E3 deviation (alignment row 16) | +| **Codex F8**: destruction of retained arguments | **Accepted.** Slot finalization is distinct from generation cleanup, runs as a tracked task on the group (never on the loop or under a lock), after the removal decision, so its failure never triggers a restart; a hang makes the slot stuck as retiring | +| **Codex F9 = agy 5**: teardown protocol incomplete; a message from `Drop` arrives before `Down` | **Accepted, with decision R5.** No message from `Drop`. Each owner (peer table, broadcaster, mempool records) stores the connection's identity at registration and releases exactly on `Down`; re-requests are best effort, after removal, with local lookup, skipped during shutdown | +| **agy 4**: backoff `None` in the model always went through a backoff state | **Accepted.** `BackoffOn` constant: without backoff the decision reserves, stamps and runs the attempt in the same turn; a failed attempt re-queues its exit at the tail (`try_again_restart`). Both variants are checked | +| **Codex F10 (P2)**: two slots are bounded evidence | **Accepted.** No sufficiency claim; a three-slot targeted instance (FIFO, cap with a restarting child, shared budget); repeated churn of one slot stays out of scope (it would need fresh identities) | +| **agy 6 (P2)** | **Accepted.** `SupervisedDynamicSupervisor` and spec builder methods shown; `ready` documented as "state is Running"; `latePub` catches any change to a non-zero value | + +Also from the OTP/Elixir/Gleam comparison: decisions G1-G5 (continuation, +`temporary()` for connections, `ignore`, start data, shared introspection +types), and the standing rule that models are related to the code: the +[test plan](#test-plan-relating-the-model-to-the-code) lists the events, their +action mapping, the required tests and the expected coverage. + +**Introspection dependency (#256 revision 3).** The console's +`terminate --expect id@generation` is fenced at the supervisor operation: +`terminate_slot` takes `expect` and answers `Stale { current }` without +acting when the slot's published child moved on. Modelled as a third call +kind (`expect`) in `LoopTerm`, with control `IgnoreExpect`. `ChildInfo`, +`ChildCounts` and `ChildKey` are shared with introspection v1. + +### Round 3 (confirmation) + +Codex (3 P1) and agy (2 P1, P2s), both "approve after the listed changes", +no P0. Each fixed in its own commit. + +| Finding | Resolution | +|---|---| +| **Codex 1**: `Ignore` and removal erased cleanup the contract keeps (an `Init::ignore()` attempt's state and helpers; slot finalization of retained arguments), so real interleavings could not replay | **Accepted.** An ignored attempt goes through cleanup like any exit; every removal goes through a `finalizing` state that keeps the slot counted and its capacity held until finalization ends (or is stuck), and the loop awaits it. New events `DFinalized`, `DDecide(finalize)`. Invariant `RemovedAfterFinalize`; controls `EarlyFree`, `IgnoreFreesEarly`. An ignored start whose cleanup misses its deadline is answered `Ignored` at the deadline, the slot stays counted | +| **Codex 2**: `FifoOrder` accepted serve-2-then-reject-1; a queued terminate answered `Ok` at shutdown passed; `NoAbort` failed on a config where `StartAnswered` fails without the mutation | **Accepted.** `FifoOrder` checks that every selection is the head at selection. `QueuedTermStopped` (history of calls queued when admission closed) with `QueuedTermOk` mutating the real wrong `Ok`. `ShutdownAnswersStarts` on `MCDynamicSupervisorAbort` (no startup deadlines), which passes unmutated; `NoAbort` fails there | +| **Codex 3**: mempool reservations released on the peer table's `Down` could be lost if the peer table stopped first; `Down.reason == Shutdown` cannot detect shutdown (escalation kills) | **Accepted.** Reservations outside actors are held by an owning registration (`InFlightLease`) in the connection's state, released synchronously by its destruction on every exit path before the slot frees. Records inside an actor's state die with it. Retries are suppressed by the node's shutdown token | +| **agy 1**: `Ignore` had no `open` guard and escaped `NoStartAfterShutdown`; leftover `StartOutcome`/`ChildStart` mismatches | **Accepted.** `Ignore` only while open; the ignore decision counts as a commit in the history; control `IgnoreAfterClose`. The non-goal line removed, the factory returns `S: Into>`, `FailedToStart { cause: ChildStartError, .. }` throughout, the rank 12 example matches `StartOutcome::Started`, `ChildInfo::key` | +| **agy 2**: stale `terminate` ids could not be replayed; `ExpectedChild::generation` vs failed replacements; tickets for directly consumed exits; an unlogged fan-out step | **Accepted.** A call names any generation the caller saw; `ExpectedChild` is the last published child (failed attempts publish nothing); an exit consumed by the waiting start or terminate takes no ticket (`DCleaned` ticket optional); the last signal ends the fan-out. `DClose` only for external or parent shutdown | +| **agy P2**: the loop must await finalization | **Accepted** (with Codex 1) | +| **Codex note**: use the canonical shared declarations | **Accepted**: `ChildInfo`/`ChildCounts`/`ChildKey` and `ChildStart` are #256's and #259's; the shapes here show only the fields this design depends on | +| **Unified start #259 rev. 3** (cross-design): `Ignored { pending }` and a stuck ignore keeping its slot until publication; a failed init never runs `stopped()` | **Adopted.** `start_child` returns `Ok(StartOutcome::Ignored { pending })`; a stuck ignored attempt answers at the deadline with `Some(handle)` and its slot counts (`Stopping`) until publication and finalization, which the model already does (`CleanupStuck` commits the ignore, the slot stays counted until `StuckDone` and `Finalize`). First-start failure and shutdown-during-construction text now say `stopped()` does not run; nothing in this design depended on it | diff --git a/docs/design/semantics.md b/docs/design/semantics.md index 624900a9..b170e7b1 100644 --- a/docs/design/semantics.md +++ b/docs/design/semantics.md @@ -607,6 +607,11 @@ ignored by non-trapping peers (X3), and the Permanent/Transient/Temporary table - Rank 11, deferred typed replies, forwarding and pipe-to-self: a reply may leave the handler's turn; adds exactly-one completion on panic and timeout. +- Rank 12a, dynamic supervisor (design in review, + [dynamic-supervisor.md](dynamic-supervisor.md)): adds V10-V13 (dynamic + admission, a cap that counts restarting children, terminated means + removed, concurrent shutdown of dynamic children) and V14 (a child stuck + while retiring fails only itself); touches V1, V3-V5, V8, V9, S1, S2. - Rank 13, bounded draining: an opt-in stop that handles queued work by policy instead of discarding it (D4 remains the default). - Rank 14, fair control path: lifecycle signals not stuck behind a backlog (X7). diff --git a/verification/tla/DynamicSupervisor.tla b/verification/tla/DynamicSupervisor.tla new file mode 100644 index 00000000..49d5f4cd --- /dev/null +++ b/verification/tla/DynamicSupervisor.tla @@ -0,0 +1,767 @@ +------------------------- MODULE DynamicSupervisor ------------------------- +(***************************************************************************) +(* Rank 12a design model (not implemented): a dynamic supervisor, OTP's *) +(* simple_one_for_one / Elixir's DynamicSupervisor. Design contract: *) +(* docs/design/dynamic-supervisor.md (revision 3). *) +(* *) +(* Slots 1..N are start_child calls made at any moment. TermCalls are *) +(* terminate_child calls, each aimed at one slot either by the actor id *) +(* the caller saw (the slot's last published generation at call time) or *) +(* by the slot (terminate_slot); several calls may target one slot. *) +(* *) +(* As in OTP, the supervisor is one control loop. Requests and child *) +(* exits arrive in one FIFO queue `q` (start requests, terminate calls, *) +(* exit notices, backoff retries). The loop takes the head, runs it to *) +(* completion (`op` holds a start, restart or terminate in progress), *) +(* then the next. The exit of the child an operation is waiting for is *) +(* consumed by that operation directly, as OTP's start_child and *) +(* shutdown/2 consume it. Children run, exit and clean up concurrently. *) +(* Shutdown and failure close admission at once (B, tree-wide closure). *) +(* *) +(* Backoff (opt-in) is a constant: without it the restart attempt runs in *) +(* the same loop turn as the exit decision (OTP restart/2); a failed *) +(* attempt re-queues its exit at the tail (OTP try_again_restart). *) +(* *) +(* Two fairness sets: CallerFairness has no progress for user cleanup *) +(* (CleanupDone, StuckDone, StopObserved, Ready); only deadlines fire. It *) +(* checks that callers are answered even if cleanup never ends. *) +(* Fairness adds cleanup progress, for shutdown completion and recovery. *) +(* *) +(* Instances are bounded: the per-PR ones use two slots; targeted *) +(* three-slot instances check admission order, the cap and the shared *) +(* budget with more children. These are bounded checks, not a cutoff. *) +(* *) +(* Event invariants read history variables that GhostUpdate computes *) +(* from each step's state change, separately from the actions. *) +(* Fault selects a negative control (DYNAMIC_CONTROLS, negative_checks). *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS + N, \* start_child calls (slots 1..N) + ModeSet, \* restart types a slot may have; chosen per slot in Init + MaxChildren, MaxRestarts, MaxExpire, + SelfExits, \* reasons a ready child may exit with on its own + StartFails, \* non-deadline outcomes of a failed construction + CleanupFails, \* {FALSE} or {FALSE, TRUE}: cleanup may record a failure + TermCalls, \* terminate_child calls + CallSlot, \* CallSlot[c]: slot the call is about + CallKind, \* CallKind[c] \in {"id", "slot", "expect"}: by actor id, by + \* slot, or by slot fenced on the expected id@generation + BackoffOn, \* backoff configured (opt-in) + FanoutSteps, \* shutdown fan-out as separate steps (refinement) + StartDeadlines, \* startup_timeout exists (TRUE in every configuration; + \* FALSE only for the NoAbort control, so that shutdown's + \* cancellation is the only thing that answers a start) + Fault + +Slots == 1..N +Modes == {"Permanent", "Transient", "Temporary"} +Reasons == {"none", "timeout", "Normal", "Shutdown", "Panic", "Kill", "Killed"} +Abnormal == {"none", "timeout", "Panic", "Kill", "Killed"} +Faults == {"None", + "IgnoreMax", "UncountedRestart", "RestartTemporary", "RestartTerminated", + "AcceptDuringShutdown", "RestartAfterClose", "NoEscalate", "EarlyDone", + "Sequential", "NoAbort", "StuckBackoff", "ConcurrentStart", "StuckFailsAll", + "PublishAfterClose", "OverlapGeneration", "PublishBeforeReady", "PrematureOk", + "UnchargedRetry", "ChargeFirstStart", "TransientNormalRestart", + "PermanentRetires", "RetryFirstStart", "EarlyFailedReply", "NoRefund", + "ExpireReserved", "TermReplyEarly", "LateFailedOverwrite", + \* revision 3 + "LaterOp", "MisclassifyStuck", "EarlyRemove", "OverReserve", "LostRestart", + "TermLost", "NoDeadline", "SkipSignal", "SlotLookup", "QueuedTermOk", + "PublishAfterExit", "StuckResultLost", "IgnoreExpect", + \* round 3 + "EarlyFree", "IgnoreFreesEarly", "IgnoreAfterClose"} + +ASSUME N \in Nat \ {0} /\ MaxChildren \in Nat /\ MaxRestarts \in Nat /\ MaxExpire \in Nat +ASSUME ModeSet \subseteq Modes /\ ModeSet # {} +ASSUME SelfExits \subseteq Reasons /\ StartFails \subseteq Reasons +ASSUME CleanupFails \subseteq BOOLEAN /\ FALSE \in CleanupFails +ASSUME \A c \in TermCalls : CallSlot[c] \in Slots /\ CallKind[c] \in {"id", "slot", "expect"} +ASSUME BackoffOn \in BOOLEAN /\ FanoutSteps \in BOOLEAN /\ StartDeadlines \in BOOLEAN +ASSUME Fault \in Faults + +States == {"idle", "queued", "starting", "running", "cleanup", "decide", + "backoff", "restarting", "stuck", "finalizing", "removed", "rejected"} +\* "finalizing": the loop decided to remove the slot; slot finalization +\* (dropping retained arguments) runs and the slot stays counted until it +\* ends (revision 3, Codex round 3). +Active == {"starting", "running", "cleanup", "decide", "backoff", "finalizing", + "restarting", "stuck"} +Terminal == {"idle", "removed", "rejected"} +Idle == [k |-> "idle", s |-> 0, c |-> 0] + +VARIABLES + open, failed, exhausted, sphase, + windowed, expired, reserved, stamped, + q, \* FIFO of [k, s, c, t]: "start", "exit", "retry", "term" + ticket, \* next arrival ticket + served, \* ticket of the last operation the loop took from the head + op, \* operation in progress [k, s, c] + mode, sl, tc, + \* history (GhostUpdate only) + lateCommit, latePub, lateGenClose, lateGenTerm, badRestart, badRetire, + restarts, outOfOrder, freedEarly, queuedAtClose, pendAtStuck + +sup == <> +ghost == <> +vars == <> + +SlotInit == [cs |-> "idle", gen |-> 0, alive |-> {}, pub |-> 0, lastPub |-> 0, + reason |-> "none", cfail |-> FALSE, readyGen |-> FALSE, + everReady |-> FALSE, result |-> "none", cause |-> "none", + term |-> FALSE, stopSig |-> FALSE, stuck |-> "none", + retryQ |-> FALSE, ign |-> FALSE, fstuck |-> FALSE] +\* terminate call: st \in none, queued, pending, ok, stuck, notfound, stopped; +\* g = the actor (generation) the caller named. +CallInit == [st |-> "none", g |-> 0] + +TypeOK == + /\ open \in BOOLEAN /\ failed \in BOOLEAN /\ exhausted \in BOOLEAN + /\ sphase \in {"running", "signal", "waiting", "done"} + /\ windowed \in Nat /\ expired \in 0..MaxExpire /\ reserved \subseteq Slots + /\ stamped \in Nat /\ ticket \in Nat /\ served \in Nat + /\ op.k \in {"idle", "start", "restart", "term", "final"} + /\ \A s \in Slots : sl[s].cs \in States /\ sl[s].alive \subseteq Nat + /\ \A c \in TermCalls : + tc[c].st \in {"none", "queued", "pending", "ok", "stuck", "notfound", "stopped", "stale"} + +Init == + /\ open = TRUE /\ failed = FALSE /\ exhausted = FALSE /\ sphase = "running" + /\ windowed = 0 /\ expired = 0 /\ reserved = {} /\ stamped = 0 + /\ q = <<>> /\ ticket = 1 /\ served = 0 /\ op = Idle + /\ mode \in [Slots -> ModeSet] + /\ sl = [s \in Slots |-> SlotInit] /\ tc = [c \in TermCalls |-> CallInit] + /\ lateCommit = [s \in Slots |-> FALSE] /\ latePub = [s \in Slots |-> FALSE] + /\ lateGenClose = [s \in Slots |-> FALSE] /\ lateGenTerm = [s \in Slots |-> FALSE] + /\ badRestart = [s \in Slots |-> FALSE] /\ badRetire = [s \in Slots |-> FALSE] + /\ restarts = 0 /\ outOfOrder = FALSE /\ freedEarly = [s \in Slots |-> FALSE] + /\ queuedAtClose = [c \in TermCalls |-> FALSE] + /\ pendAtStuck = [c \in TermCalls |-> FALSE] + +----------------------------------------------------------------------------- +(* Helpers *) + +Counted == + IF Fault = "UncountedRestart" + THEN {s \in Slots : sl[s].cs \in {"starting", "running"}} + ELSE {s \in Slots : sl[s].cs \in Active} +Budget == windowed + Cardinality(reserved) + +Enq(e) == q' = Append(q, [e EXCEPT !.t = ticket]) /\ ticket' = ticket + 1 +Rm(i) == [j \in 1..Len(q) - 1 |-> IF j < i THEN q[j] ELSE q[j + 1]] +IsHead(k, s, c) == Len(q) > 0 /\ q[1].k = k /\ q[1].s = s /\ q[1].c = c +\* Index of the exit notice of slot s, if queued. +ExitIdx(s) == {i \in 1..Len(q) : q[i].k = "exit" /\ q[i].s = s} +LoopIdle == op.k = "idle" \/ Fault = "ConcurrentStart" + +DesignAllowsRestart(m, r, cf) == + CASE m = "Temporary" -> FALSE + [] m = "Permanent" -> TRUE + [] m = "Transient" -> r \in {"Panic", "Kill", "Killed"} \/ cf +\* An attempt that ignored is dropped, never restarted (OTP: ignore on a +\* restart removes the child). +Allowed(s) == + /\ sl[s].everReady /\ ~sl[s].ign + /\ \/ DesignAllowsRestart(mode[s], sl[s].reason, sl[s].cfail) + \/ ~sl[s].readyGen /\ mode[s] # "Temporary" + +WouldRestart(s) == + /\ sl[s].everReady \/ Fault = "RetryFirstStart" + /\ \/ mode[s] = "Permanent" /\ Fault # "PermanentRetires" + \/ mode[s] = "Transient" + /\ (sl[s].reason \in Abnormal \/ sl[s].cfail \/ Fault = "TransientNormalRestart") + \/ mode[s] # "Temporary" /\ ~sl[s].readyGen + \/ mode[s] = "Temporary" /\ Fault = "RestartTemporary" + +Fail == failed' = TRUE /\ open' = FALSE + +\* The pending terminate call that holds the loop for slot s, if any. +HeldCall(s) == IF op.k = "term" /\ op.s = s THEN {op.c} ELSE {} + +----------------------------------------------------------------------------- +(* Callers *) + +\* start_child: queued, or rejected at once (arguments returned) if closed. +Request(s) == + /\ sl[s].cs = "idle" + /\ IF open + THEN /\ sl' = [sl EXCEPT ![s].cs = "queued", ![s].result = "pending"] + /\ Enq([k |-> "start", s |-> s, c |-> 0, t |-> 0]) + ELSE /\ sl' = [sl EXCEPT ![s].cs = "rejected", ![s].result = "stopped"] + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* The loop admits the start at the head (LaterOp: any queued start). +LoopAdmit(s) == + /\ sl[s].cs = "queued" /\ LoopIdle + /\ open \/ Fault = "AcceptDuringShutdown" + /\ \E i \in 1..Len(q) : + /\ q[i].k = "start" /\ q[i].s = s + /\ i = 1 \/ Fault = "LaterOp" + /\ q' = Rm(i) /\ served' = q[i].t + /\ IF Cardinality(Counted) >= MaxChildren /\ Fault # "IgnoreMax" + THEN /\ sl' = [sl EXCEPT ![s].cs = "rejected", ![s].result = "max"] + /\ UNCHANGED <> + ELSE /\ sl' = [sl EXCEPT ![s].cs = "starting", ![s].gen = 1, ![s].alive = {1}, + ![s].result = IF Fault = "PrematureOk" THEN "ok" ELSE "pending"] + /\ op' = IF Fault = "ConcurrentStart" THEN op ELSE [k |-> "start", s |-> s, c |-> 0] + /\ IF Fault = "ChargeFirstStart" + THEN stamped' = stamped + 1 /\ windowed' = windowed + 1 + ELSE UNCHANGED <> + /\ UNCHANGED <> + +\* Shutdown answers queued starts and terminate calls (Stopped, args back). +RejectQueued(s) == + /\ sl[s].cs = "queued" /\ ~open /\ Fault # "AcceptDuringShutdown" + /\ \E i \in 1..Len(q) : q[i].k = "start" /\ q[i].s = s /\ q' = Rm(i) + /\ sl' = [sl EXCEPT ![s].cs = "rejected", ![s].result = "stopped"] + /\ UNCHANGED <> + +\* terminate_child(id) or terminate_slot(slot, expect). The caller may name +\* any generation it ever saw published, the current one or a superseded +\* one (a stale id, an outdated expect), so stale calls replay (agy round 3). +TermCall(c) == + /\ tc[c].st = "none" /\ sl[CallSlot[c]].everReady + /\ IF open + THEN /\ \E g \in (IF CallKind[c] = "slot" THEN {0} ELSE 1..sl[CallSlot[c]].lastPub) : + tc' = [tc EXCEPT ![c] = [st |-> "queued", g |-> g]] + /\ Enq([k |-> "term", s |-> CallSlot[c], c |-> c, t |-> 0]) + ELSE /\ tc' = [tc EXCEPT ![c].st = "stopped"] /\ UNCHANGED <> + /\ UNCHANGED <> + +RejectQueuedTerm(c) == + /\ tc[c].st = "queued" /\ ~open + /\ \E i \in 1..Len(q) : q[i].k = "term" /\ q[i].c = c /\ q' = Rm(i) + /\ tc' = [tc EXCEPT ![c].st = IF Fault = "QueuedTermOk" THEN "ok" ELSE "stopped"] + /\ UNCHANGED <> + +\* The loop looks the target up when it handles the call (Elixir). +LoopTerm(c) == + /\ tc[c].st = "queued" /\ op.k = "idle" /\ open /\ IsHead("term", CallSlot[c], c) + /\ q' = Tail(q) /\ served' = q[1].t + /\ LET s == CallSlot[c] + named == CallKind[c] = "slot" \/ sl[s].lastPub = tc[c].g + live == sl[s].cs \in Active \ {"stuck"} + \* expect: the slot exists but its current published child moved on + stale == CallKind[c] = "expect" /\ sl[s].cs \in Active + /\ sl[s].lastPub # tc[c].g /\ Fault # "IgnoreExpect" + found == live /\ (named \/ Fault = "SlotLookup" + \/ (CallKind[c] = "expect" /\ Fault = "IgnoreExpect")) + IN IF stale + THEN /\ tc' = [tc EXCEPT ![c].st = "stale"] /\ UNCHANGED <> + ELSE IF sl[s].cs = "stuck" /\ named + THEN /\ tc' = [tc EXCEPT ![c].st = "stuck"] /\ UNCHANGED <> + ELSE IF ~found + THEN /\ tc' = [tc EXCEPT ![c].st = "notfound"] /\ UNCHANGED <> + ELSE /\ tc' = [tc EXCEPT ![c].st = "pending"] + /\ sl' = IF Fault = "TermLost" THEN sl + ELSE [sl EXCEPT ![s].term = TRUE, ![s].stopSig = TRUE] + /\ op' = [k |-> "term", s |-> s, c |-> c] + /\ UNCHANGED <> + +\* The terminated child was removed: Ok, and the loop moves on. +TermResolve(c) == + /\ tc[c].st = "pending" + /\ sl[CallSlot[c]].cs = "removed" \/ Fault = "TermReplyEarly" + /\ tc' = [tc EXCEPT ![c].st = "ok"] + /\ op' = IF op.k = "term" /\ op.c = c THEN Idle ELSE op + /\ UNCHANGED <> + +Close == + /\ open /\ open' = FALSE + /\ UNCHANGED <> + +WindowExpire == + /\ expired < MaxExpire + /\ IF windowed > 0 + THEN windowed' = windowed - 1 /\ UNCHANGED reserved + ELSE /\ Fault = "ExpireReserved" /\ reserved # {} + /\ \E r \in reserved : reserved' = reserved \ {r} + /\ UNCHANGED windowed + /\ expired' = expired + 1 + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Children *) + +Unchanged1 == UNCHANGED <> + +\* Readiness commits while open; a first start's Ok is committed now. +Ready(s) == + /\ sl[s].cs \in {"starting", "restarting"} + /\ \/ open + \/ Fault = "AcceptDuringShutdown" /\ sl[s].cs = "starting" + \/ Fault = "PublishAfterClose" /\ sl[s].cs = "restarting" + /\ sl' = [sl EXCEPT ![s].cs = "running", ![s].pub = sl[s].gen, + ![s].lastPub = sl[s].gen, + ![s].readyGen = TRUE, ![s].everReady = TRUE, + ![s].result = IF sl[s].cs = "starting" THEN "ok" ELSE sl[s].result] + /\ op' = IF op.s = s /\ op.k # "term" THEN Idle ELSE op + /\ UNCHANGED <> + +\* The factory returned ChildStart::Ignore or started() returned +\* Init::ignore(): nothing will be supervised (OTP {ok, undefined}), but the +\* attempt's state and owned work are cleaned up like any exit, and the slot +\* is finalized, before the answer and before the slot frees. The outcome is +\* decided now (cause "ignored"), answered after cleanup or at its deadline. +Ignore(s) == + /\ sl[s].cs \in {"starting", "restarting"} + \* an ignore decides the outcome: only while admission is open (agy round 3) + /\ \/ open + \/ Fault \in {"AcceptDuringShutdown", "IgnoreAfterClose"} /\ sl[s].cs = "starting" + /\ IF Fault = "IgnoreFreesEarly" + THEN sl' = [sl EXCEPT ![s].cs = "removed", ![s].alive = {}, ![s].pub = 0, + ![s].result = IF sl[s].cs = "starting" THEN "ignored" ELSE sl[s].result] + ELSE sl' = [sl EXCEPT ![s].cs = "cleanup", ![s].reason = "Normal", ![s].pub = 0, + ![s].ign = TRUE, + ![s].cause = IF sl[s].cs = "starting" THEN "ignored" ELSE sl[s].cause] + /\ op' = IF Fault = "IgnoreFreesEarly" /\ op.s = s THEN Idle ELSE op + /\ UNCHANGED <> + +FailStart(s, r) == + /\ sl' = [sl EXCEPT ![s].cs = IF Fault = "EarlyRemove" /\ sl[s].cs = "starting" + THEN "removed" ELSE "cleanup", + ![s].reason = r, ![s].pub = 0, + ![s].cause = IF sl[s].cs = "starting" THEN "failed" ELSE sl[s].cause, + ![s].result = IF Fault \in {"EarlyFailedReply", "EarlyRemove"} + /\ sl[s].cs = "starting" + THEN "failed" ELSE sl[s].result] + +\* Factory error or panic, panic or stop in started(). +StartFail(s, r) == + /\ sl[s].cs \in {"starting", "restarting"} /\ r \in StartFails + /\ FailStart(s, r) /\ Unchanged1 + +\* startup_timeout fired (a deadline: fair in both fairness sets). +StartTimeout(s) == + /\ StartDeadlines /\ sl[s].cs \in {"starting", "restarting"} + /\ FailStart(s, "timeout") /\ Unchanged1 + +AbortStart(s) == + /\ sl[s].cs \in {"starting", "restarting"} /\ ~open /\ Fault # "NoAbort" + /\ sl' = [sl EXCEPT ![s].cs = "cleanup", ![s].reason = "Shutdown", ![s].pub = 0, + ![s].cause = IF sl[s].cs = "starting" THEN "aborted" ELSE sl[s].cause] + /\ Unchanged1 + +SelfExit(s, r) == + /\ sl[s].cs = "running" /\ r \in SelfExits + /\ sl' = [sl EXCEPT ![s].cs = "cleanup", ![s].reason = r, + ![s].pub = IF Fault = "PublishAfterExit" THEN sl[s].pub ELSE 0] + /\ Unchanged1 + +StopObserved(s, r) == + /\ sl[s].cs = "running" /\ sl[s].stopSig /\ r \in {"Shutdown", "Killed"} + /\ sl' = [sl EXCEPT ![s].cs = "cleanup", ![s].reason = r, ![s].pub = 0] + /\ Unchanged1 + +\* Owned cleanup finished. The exit is queued for the loop (OTP 'EXIT'), +\* unless the operation in progress waits for this very child (a start or +\* a terminate), which consumes it directly: no queue entry, no ticket. A +\* failed restart attempt gives the loop back and re-queues +\* (try_again_restart). +CleanupDone(s, f) == + /\ sl[s].cs = "cleanup" /\ f \in CleanupFails + /\ sl' = [sl EXCEPT ![s].cs = "decide", ![s].cfail = f, + ![s].alive = sl[s].alive \ {sl[s].gen}] + /\ IF op.s = s /\ op.k \in {"start", "term"} + THEN UNCHANGED <> + ELSE Enq([k |-> "exit", s |-> s, c |-> 0, t |-> 0]) + /\ op' = IF op.k = "restart" /\ op.s = s THEN Idle ELSE op + /\ UNCHANGED <> + +\* A deadline was missed: signalled but still running after the kill and +\* the second interval, owned cleanup past its deadline, or slot +\* finalization past its deadline. The slot stays +\* counted. Results waiting on it are committed now and stay (historical). +\* Kind: "restart" only for a child the table would restart, judged from +\* the exit reason alone (a stall is not a recorded cleanup failure); +\* "closing" during shutdown; otherwise "retire" (fails only the child). +CleanupStuck(s) == + /\ Fault # "NoDeadline" + \* generation deadlines once per slot life; the finalization deadline has + \* its own flag, so a slot that was stuck before and then reached + \* finalization can still miss (and report) that deadline + /\ \/ sl[s].stuck = "none" /\ sl[s].cs = "cleanup" + \/ sl[s].stuck = "none" /\ sl[s].cs = "running" /\ sl[s].stopSig + \/ sl[s].cs = "finalizing" /\ ~sl[s].fstuck + /\ LET restartable == + /\ sl[s].everReady /\ ~sl[s].term /\ sl[s].cs = "cleanup" + /\ \/ DesignAllowsRestart(mode[s], sl[s].reason, FALSE) + \/ ~sl[s].readyGen /\ mode[s] # "Temporary" + kind == IF ~open THEN "closing" + ELSE IF restartable \/ (Fault = "MisclassifyStuck" /\ ~sl[s].term) + THEN "restart" ELSE "retire" + IN /\ sl' = [sl EXCEPT ![s].cs = "stuck", ![s].stuck = kind, ![s].pub = 0, + ![s].fstuck = (sl[s].fstuck \/ sl[s].cs = "finalizing"), + ![s].result = IF sl[s].result = "pending" + THEN sl[s].cause ELSE sl[s].result] + /\ IF kind # "retire" \/ Fault = "StuckFailsAll" + THEN Fail ELSE UNCHANGED <> + /\ tc' = [c \in TermCalls |-> + IF c \in HeldCall(s) /\ Fault # "StuckResultLost" + THEN [tc[c] EXCEPT !.st = "stuck"] ELSE tc[c]] + /\ op' = IF op.s = s /\ (op.k # "term" \/ Fault # "StuckResultLost") THEN Idle ELSE op + /\ UNCHANGED <> + +\* A stuck child finally ended: finalization follows. A stuck finalization +\* that ends is finalization done: the slot is removed. +StuckDone(s) == + /\ sl[s].cs = "stuck" + /\ sl' = [sl EXCEPT ![s].cs = IF sl[s].fstuck THEN "removed" ELSE "finalizing", + ![s].alive = {}] + /\ Unchanged1 + +\* Slot finalization ended: retained arguments dropped, then capacity and +\* the max_children slot released. A start's answer is given now. +Finalize(s) == + /\ sl[s].cs = "finalizing" + /\ sl' = [sl EXCEPT ![s].cs = "removed", + ![s].result = IF sl[s].result = "pending" + THEN IF Fault = "LateFailedOverwrite" /\ ~open + THEN "aborted" ELSE sl[s].cause + ELSE sl[s].result] + /\ op' = IF op = [k |-> "final", s |-> s, c |-> 0] THEN Idle ELSE op + /\ UNCHANGED <> + +\* The loop handles an exit: at the head of the queue, or directly when the +\* operation in progress waits for this child (start or terminate). +Decide(s) == + /\ \/ sl[s].cs = "decide" + \/ Fault = "OverlapGeneration" /\ sl[s].cs = "cleanup" + /\ \/ \E i \in ExitIdx(s) : + /\ \/ i = 1 /\ LoopIdle + \/ op.s = s /\ op.k \in {"start", "term"} + /\ q' = Rm(i) + /\ served' = IF i = 1 /\ LoopIdle THEN q[i].t ELSE served + \* consumed directly by the operation waiting for this child + \/ /\ op.s = s /\ op.k \in {"start", "term"} /\ ExitIdx(s) = {} + /\ sl[s].cs = "decide" + /\ UNCHANGED <> + \/ Fault = "OverlapGeneration" /\ sl[s].cs = "cleanup" /\ LoopIdle + /\ UNCHANGED <> + /\ LET ownStart == op.s = s /\ op.k = "start" + \* removal: finalize; the loop waits for it unless a terminate holds it + Remove == /\ sl' = [sl EXCEPT ![s].cs = IF Fault = "EarlyFree" THEN "removed" + ELSE "finalizing"] + /\ op' = IF op.k = "term" /\ op.s = s THEN op + ELSE IF Fault = "EarlyFree" THEN Idle + ELSE [k |-> "final", s |-> s, c |-> 0] + IN IF ~sl[s].everReady /\ Fault # "RetryFirstStart" + THEN \* first-start failure or ignore: answered after finalization + /\ Remove + /\ UNCHANGED <> + ELSE IF ~open \/ (sl[s].term /\ Fault # "RestartTerminated") \/ sl[s].ign + THEN /\ Remove + /\ UNCHANGED <> + ELSE IF WouldRestart(s) + THEN IF Budget < MaxRestarts \/ Fault = "OverReserve" + THEN IF BackoffOn \/ Fault = "LostRestart" + THEN \* reserve, wait off the loop + /\ sl' = [sl EXCEPT ![s].cs = "backoff"] + /\ reserved' = reserved \cup {s} + /\ op' = IF ownStart THEN Idle ELSE op + /\ UNCHANGED <> + ELSE \* reserve and stamp now; the attempt runs in this turn (OTP) + /\ LET g == sl[s].gen + 1 IN + sl' = [sl EXCEPT ![s].cs = "restarting", ![s].gen = g, + ![s].alive = sl[s].alive \cup {g}, + ![s].pub = IF Fault = "PublishBeforeReady" THEN g ELSE 0, + ![s].reason = "none", ![s].cfail = FALSE, ![s].readyGen = FALSE] + /\ IF Fault = "UnchargedRetry" /\ ~sl[s].readyGen + THEN UNCHANGED <> + ELSE stamped' = stamped + 1 /\ windowed' = windowed + 1 + /\ op' = [k |-> "restart", s |-> s, c |-> 0] + /\ UNCHANGED <> + ELSE /\ exhausted' = TRUE + /\ Remove + /\ IF Fault = "NoEscalate" THEN UNCHANGED <> ELSE Fail + /\ UNCHANGED <> + ELSE /\ Remove + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* The backoff timer fires: the retry joins the queue. +BackoffFire(s) == + /\ sl[s].cs = "backoff" /\ ~sl[s].retryQ /\ open /\ Fault # "LostRestart" + /\ sl' = [sl EXCEPT ![s].retryQ = TRUE] + /\ Enq([k |-> "retry", s |-> s, c |-> 0, t |-> 0]) + /\ UNCHANGED <> + +\* The loop takes the retry: stamp the reservation, construct. +BackoffDone(s) == + /\ sl[s].cs = "backoff" /\ sl[s].retryQ /\ LoopIdle + /\ IsHead("retry", s, 0) + /\ open \/ Fault = "RestartAfterClose" + /\ ~sl[s].term \/ Fault = "RestartTerminated" + /\ q' = Tail(q) /\ served' = q[1].t + /\ LET g == sl[s].gen + 1 IN + sl' = [sl EXCEPT ![s].cs = "restarting", ![s].gen = g, + ![s].alive = sl[s].alive \cup {g}, ![s].retryQ = FALSE, + ![s].pub = IF Fault = "PublishBeforeReady" THEN g ELSE 0, + ![s].reason = "none", ![s].cfail = FALSE, ![s].readyGen = FALSE] + /\ reserved' = reserved \ {s} + /\ IF Fault = "UnchargedRetry" /\ ~sl[s].readyGen + THEN UNCHANGED <> + ELSE stamped' = stamped + 1 /\ windowed' = windowed + 1 + /\ op' = IF Fault = "ConcurrentStart" THEN op ELSE [k |-> "restart", s |-> s, c |-> 0] + /\ UNCHANGED <> + +\* Shutdown or terminate cancels a pending restart and refunds it. +CancelBackoff(s) == + /\ sl[s].cs = "backoff" + /\ \/ ~open /\ Fault # "StuckBackoff" + \/ sl[s].term /\ Fault # "RestartTerminated" + /\ sl' = [sl EXCEPT ![s].cs = "finalizing", ![s].retryQ = FALSE] + /\ q' = SelectSeq(q, LAMBDA e : ~(e.k = "retry" /\ e.s = s)) + /\ reserved' = IF Fault = "NoRefund" THEN reserved ELSE reserved \ {s} + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Shutdown *) + +\* Atomic fan-out: every admitted child signalled in one step. +SupSignal == + /\ ~FanoutSteps /\ sphase = "running" /\ ~open + /\ sl' = [s \in Slots |-> + IF Fault = "SkipSignal" /\ s = 1 THEN sl[s] + ELSE [sl[s] EXCEPT !.stopSig = TRUE]] + /\ sphase' = "waiting" + /\ UNCHANGED <> + +\* Refinement: one signal per step, interleaved with the children. +\* Sequential waits for each signalled child to finish first. +SupSignalStep == + /\ FanoutSteps /\ sphase \in {"running", "signal"} /\ ~open + /\ Fault = "Sequential" => \A s \in Slots : sl[s].stopSig => sl[s].cs \notin Active + /\ LET todo == {s \in Slots : ~sl[s].stopSig /\ sl[s].cs \in Active} + IN IF todo = {} + THEN sphase' = "waiting" /\ UNCHANGED sl + ELSE \E s \in todo : + /\ sl' = [sl EXCEPT ![s].stopSig = TRUE] + \* the last signal ends the fan-out (no extra unlogged step) + /\ sphase' = IF todo = {s} THEN "waiting" ELSE "signal" + /\ UNCHANGED <> + +SupDone == + /\ sphase = "waiting" + /\ (\A s \in Slots : sl[s].cs \in Terminal) \/ Fault = "EarlyDone" + /\ sphase' = "done" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- + +Grew(s) == sl'[s].gen > sl[s].gen +\* A restart was decided (reservation, attempt or exhaustion) for slot s. +Decided(s) == + /\ sl[s].cs = "decide" + /\ \/ sl'[s].cs \in {"backoff", "restarting"} + \/ exhausted' /\ ~exhausted /\ sl'[s].cs \in {"finalizing", "removed"} + +GhostUpdate == + \* a start outcome committed after close: Ok, or the ignore decision + /\ lateCommit' = [s \in Slots |-> lateCommit[s] \/ + (((sl'[s].result = "ok" /\ sl[s].result # "ok") + \/ (sl'[s].cause = "ignored" /\ sl[s].cause # "ignored")) /\ ~open)] + /\ latePub' = [s \in Slots |-> latePub[s] \/ + (sl'[s].pub # sl[s].pub /\ sl'[s].pub # 0 /\ (~open \/ sl[s].term))] + /\ lateGenClose' = [s \in Slots |-> lateGenClose[s] \/ (Grew(s) /\ ~open)] + /\ lateGenTerm' = [s \in Slots |-> lateGenTerm[s] \/ (Grew(s) /\ sl[s].term)] + /\ badRestart' = [s \in Slots |-> badRestart[s] \/ + (((Grew(s) /\ sl[s].gen > 0) \/ Decided(s)) /\ ~Allowed(s))] + /\ badRetire' = [s \in Slots |-> badRetire[s] \/ + (sl[s].cs = "decide" /\ sl'[s].cs \in {"finalizing", "removed"} /\ open' + /\ ~sl[s].term /\ Allowed(s))] + /\ restarts' = restarts + Cardinality({s \in Slots : Grew(s) /\ sl[s].gen > 0}) + \* the loop selected an operation: it must be the head at selection + /\ outOfOrder' = (outOfOrder \/ ((served' # served) /\ ((Len(q) = 0) \/ (served' # q[1].t)))) + \* terminate calls still queued at the moment admission closed + /\ queuedAtClose' = [c \in TermCalls |-> queuedAtClose[c] \/ + (open /\ ~open' /\ tc[c].st = "queued")] + \* terminate calls in progress at the moment their child got stuck + /\ pendAtStuck' = [c \in TermCalls |-> pendAtStuck[c] \/ + (tc[c].st = "pending" /\ sl[CallSlot[c]].stuck = "none" + /\ sl'[CallSlot[c]].stuck # "none")] + /\ freedEarly' = [s \in Slots |-> freedEarly[s] \/ + (sl'[s].cs = "removed" /\ sl[s].cs \notin {"finalizing", "removed"} + /\ ~(sl[s].cs = "stuck" /\ sl[s].fstuck))] + /\ UNCHANGED mode + +SlotStep(s) == + \/ Request(s) \/ LoopAdmit(s) \/ RejectQueued(s) + \/ Ready(s) \/ Ignore(s) \/ \E r \in StartFails : StartFail(s, r) + \/ StartTimeout(s) \/ AbortStart(s) + \/ \E r \in SelfExits : SelfExit(s, r) + \/ \E r \in {"Shutdown", "Killed"} : StopObserved(s, r) + \/ \E f \in CleanupFails : CleanupDone(s, f) + \/ CleanupStuck(s) \/ StuckDone(s) \/ Finalize(s) + \/ Decide(s) \/ BackoffFire(s) \/ BackoffDone(s) \/ CancelBackoff(s) + +CallStep(c) == TermCall(c) \/ RejectQueuedTerm(c) \/ LoopTerm(c) \/ TermResolve(c) + +Act == + \/ Close \/ WindowExpire \/ SupSignal \/ SupSignalStep \/ SupDone + \/ \E s \in Slots : SlotStep(s) + \/ \E c \in TermCalls : CallStep(c) + +Next == Act /\ GhostUpdate + +\* Loop work and deadlines only: no user cleanup is assumed to finish. +CallerFairness == + /\ \A s \in Slots : + /\ WF_vars((LoopAdmit(s)) /\ GhostUpdate) /\ WF_vars((RejectQueued(s)) /\ GhostUpdate) /\ WF_vars((StartTimeout(s)) /\ GhostUpdate) + /\ WF_vars((AbortStart(s)) /\ GhostUpdate) /\ WF_vars((CleanupStuck(s)) /\ GhostUpdate) /\ WF_vars((Decide(s)) /\ GhostUpdate) + /\ WF_vars((BackoffFire(s)) /\ GhostUpdate) /\ WF_vars((BackoffDone(s)) /\ GhostUpdate) /\ WF_vars((CancelBackoff(s)) /\ GhostUpdate) + /\ \A c \in TermCalls : WF_vars((RejectQueuedTerm(c)) /\ GhostUpdate) /\ WF_vars((LoopTerm(c)) /\ GhostUpdate) /\ WF_vars((TermResolve(c)) /\ GhostUpdate) + /\ WF_vars((SupSignal) /\ GhostUpdate) /\ WF_vars((SupSignalStep) /\ GhostUpdate) /\ WF_vars((SupDone) /\ GhostUpdate) + +\* Plus progress of children and cleanup. +Fairness == + /\ CallerFairness + /\ \A s \in Slots : + /\ WF_vars((Ready(s)) /\ GhostUpdate) + /\ WF_vars((\E r \in {"Shutdown", "Killed"} : StopObserved(s, r)) /\ GhostUpdate) + /\ WF_vars((\E f \in CleanupFails : CleanupDone(s, f)) /\ GhostUpdate) + /\ WF_vars((StuckDone(s)) /\ GhostUpdate) + /\ WF_vars((Finalize(s)) /\ GhostUpdate) + +Spec == Init /\ [][Next]_vars /\ Fairness +CallerSpec == Init /\ [][Next]_vars /\ CallerFairness + +----------------------------------------------------------------------------- +(* Safety *) + +AtMostOneGeneration == \A s \in Slots : Cardinality(sl[s].alive) <= 1 + +PublishedIsLive == + \A s \in Slots : sl[s].pub # 0 => + /\ sl[s].cs = "running" /\ sl[s].pub = sl[s].gen + /\ sl[s].pub \in sl[s].alive /\ sl[s].readyGen + +NoChildOutlivesSupervisor == + sphase = "done" => \A s \in Slots : sl[s].alive = {} /\ sl[s].cs \in Terminal + +MaxChildrenBound == Cardinality({s \in Slots : sl[s].cs \in Active}) <= MaxChildren + +SerialConstruction == + Cardinality({s \in Slots : sl[s].cs \in {"starting", "restarting"}}) <= 1 + +\* The loop takes queued operations in arrival order. +FifoOrder == ~outOfOrder + +TemporaryNeverRestarted == \A s \in Slots : mode[s] = "Temporary" => sl[s].gen <= 1 +TerminatedNeverRestarted == \A s \in Slots : ~lateGenTerm[s] +NoGenerationAfterClose == \A s \in Slots : ~lateGenClose[s] +NoPublishAfterStop == \A s \in Slots : ~latePub[s] +NoStartAfterShutdown == \A s \in Slots : ~lateCommit[s] + +\* Restart decisions (reservation, attempt, exhaustion) only for exits the +\* table allows; no restartable exit is retired while open. +RestartFollowsPolicy == \A s \in Slots : ~badRestart[s] /\ ~badRetire[s] + +FirstStartNeverRetried == \A s \in Slots : sl[s].gen > 1 => sl[s].everReady + +\* FailedToStart/Aborted only once cleanup really finished, or with the +\* cleanup deadline failure recorded. +FailedAfterCleanup == + \A s \in Slots : sl[s].result \in {"failed", "aborted"} => + \/ sl[s].cs = "removed" /\ sl[s].alive = {} + \/ sl[s].stuck # "none" + +FailureCauseKept == + \A s \in Slots : sl[s].result \in {"failed", "aborted"} => sl[s].result = sl[s].cause + +ChargedRestarts == restarts = stamped +ReservationsMatch == reserved = {s \in Slots : sl[s].cs = "backoff"} +BudgetBounded == Budget <= MaxRestarts +ExhaustionCloses == exhausted => failed /\ ~open + +\* The supervisor fails only by exhaustion, a stuck child the table would +\* restart, or while closing; and a "restart" classification is checked +\* against the table, not trusted. +StuckIsolated == + /\ failed => exhausted \/ \E s \in Slots : sl[s].stuck \in {"restart", "closing"} + /\ \A s \in Slots : sl[s].stuck = "restart" => + /\ ~sl[s].term /\ sl[s].everReady + /\ \/ DesignAllowsRestart(mode[s], sl[s].reason, FALSE) + \/ ~sl[s].readyGen /\ mode[s] # "Temporary" + +\* A slot is freed (removed) only after slot finalization ran: the cap and +\* capacity cover retained arguments and an ignored attempt's cleanup. +RemovedAfterFinalize == \A s \in Slots : ~freedEarly[s] + +\* A terminate call still queued when shutdown began is answered Stopped +\* (and stays so), never Ok or NotFound. +QueuedTermStopped == + \A c \in TermCalls : queuedAtClose[c] => tc[c].st \in {"queued", "stopped"} + +ConcurrentShutdown == + sphase \in {"waiting", "done"} => \A s \in Slots : sl[s].cs = "running" => sl[s].stopSig + +OkMeansReady == \A s \in Slots : sl[s].result = "ok" => sl[s].everReady + +\* terminate results: Ok only after removal; a call whose child got stuck +\* while it waited is Stuck (and stays so); an id call or a fenced +\* (expect) slot call never reaches a generation other than the one named. +TermResultsSound == + \A c \in TermCalls : + LET s == CallSlot[c] IN + /\ tc[c].st = "ok" => sl[s].cs = "removed" /\ sl[s].alive = {} + \* a call in progress when its child got stuck reports CleanupStuck + /\ pendAtStuck[c] => tc[c].st = "stuck" + /\ tc[c].st = "pending" => op = [k |-> "term", s |-> s, c |-> c] + /\ tc[c].st = "pending" /\ CallKind[c] \in {"id", "expect"} => sl[s].lastPub = tc[c].g + +Safety == + /\ TypeOK /\ AtMostOneGeneration /\ PublishedIsLive /\ NoChildOutlivesSupervisor + /\ MaxChildrenBound /\ SerialConstruction /\ FifoOrder /\ TemporaryNeverRestarted + /\ TerminatedNeverRestarted /\ NoGenerationAfterClose /\ NoPublishAfterStop + /\ NoStartAfterShutdown /\ RestartFollowsPolicy /\ FirstStartNeverRetried + /\ FailedAfterCleanup /\ FailureCauseKept /\ ChargedRestarts /\ ReservationsMatch + /\ BudgetBounded /\ ExhaustionCloses /\ StuckIsolated /\ ConcurrentShutdown + /\ OkMeansReady /\ TermResultsSound /\ RemovedAfterFinalize /\ QueuedTermStopped + +NeverReopens == [][open' => open]_vars +\* A committed terminate result never changes. +TermResultStable == + [][\A c \in TermCalls : + tc[c].st \in {"ok", "stuck", "notfound", "stopped", "stale"} => tc'[c].st = tc[c].st]_vars + +(* Liveness *) +\* Under CallerSpec (cleanup may never end): +StartAnswered == \A s \in Slots : + (sl[s].result = "pending") ~> (sl[s].result # "pending") +TerminateAnswered == \A c \in TermCalls : + (tc[c].st \in {"queued", "pending"}) ~> (tc[c].st \notin {"queued", "pending"}) +\* Every admitted child is signalled even if siblings never finish. +FanoutCompletes == (~open) ~> (sphase \in {"waiting", "done"}) +\* Once shutdown began, every pending start is answered (by its abort and +\* cleanup deadline), even without startup deadlines (MCDynamicSupervisorAbort). +ShutdownAnswersStarts == \A s \in Slots : + (~open /\ sl[s].result = "pending") ~> (sl[s].result # "pending") +\* Under Spec (cleanup ends): +ClosedLeadsToDone == (~open) ~> (sphase = "done") +RecoveryProgress == \A s \in Slots : + (sl[s].cs \in {"decide", "backoff", "restarting"} /\ sl[s].everReady) + ~> (sl[s].cs \in {"running", "finalizing", "removed", "stuck"}) +============================================================================= diff --git a/verification/tla/MCDynamicSupervisor.cfg b/verification/tla/MCDynamicSupervisor.cfg new file mode 100644 index 00000000..afaf08ec --- /dev/null +++ b/verification/tla/MCDynamicSupervisor.cfg @@ -0,0 +1,50 @@ +\* Per PR, safety: two start_child calls (every pair of restart types), one +\* terminate_slot call fenced with expect (naming any generation seen), +\* max_children 1, budget 1, one window release, no backoff, exits Normal/Panic, +\* start failures factory/Normal/timeout, ignore, cleanup failures. +\* MCDynamicSupervisorWideDeep adds a terminate-by-id call. +SPECIFICATION Spec +CONSTANTS + N = 2 + ModeSet = {"Permanent", "Transient", "Temporary"} + MaxChildren = 1 + MaxRestarts = 1 + MaxExpire = 1 + SelfExits = {"Normal", "Panic"} + StartFails = {"none", "Normal"} + CleanupFails = {FALSE, TRUE} + TermCalls <- MCCalls1e + CallSlot <- MCCallSlot1e + CallKind <- MCCallKind1e + BackoffOn = FALSE + StartDeadlines = TRUE + FanoutSteps = FALSE + Fault = "None" +INVARIANT TypeOK +INVARIANT AtMostOneGeneration +INVARIANT PublishedIsLive +INVARIANT NoChildOutlivesSupervisor +INVARIANT MaxChildrenBound +INVARIANT SerialConstruction +INVARIANT FifoOrder +INVARIANT TemporaryNeverRestarted +INVARIANT TerminatedNeverRestarted +INVARIANT NoGenerationAfterClose +INVARIANT NoPublishAfterStop +INVARIANT NoStartAfterShutdown +INVARIANT RestartFollowsPolicy +INVARIANT FirstStartNeverRetried +INVARIANT FailedAfterCleanup +INVARIANT FailureCauseKept +INVARIANT ChargedRestarts +INVARIANT ReservationsMatch +INVARIANT BudgetBounded +INVARIANT ExhaustionCloses +INVARIANT StuckIsolated +INVARIANT ConcurrentShutdown +INVARIANT OkMeansReady +INVARIANT TermResultsSound +INVARIANT RemovedAfterFinalize +INVARIANT QueuedTermStopped +PROPERTY NeverReopens +PROPERTY TermResultStable diff --git a/verification/tla/MCDynamicSupervisor.tla b/verification/tla/MCDynamicSupervisor.tla new file mode 100644 index 00000000..399a110d --- /dev/null +++ b/verification/tla/MCDynamicSupervisor.tla @@ -0,0 +1,22 @@ +------------------------ MODULE MCDynamicSupervisor ------------------------ +(* Model-checking instances for DynamicSupervisor (rank 12a design). *) +EXTENDS DynamicSupervisor + +\* Two terminate calls on slot 1: by the id the caller saw, and by slot +\* fenced on the expected id@generation (introspection's console). +MCCalls2 == {1, 2} +MCCallSlot2 == [c \in MCCalls2 |-> 1] +MCCallKind2 == [c \in MCCalls2 |-> IF c = 1 THEN "id" ELSE "expect"] +\* One terminate call by slot (unfenced). +MCCalls1 == {1} +MCCallSlot1 == [c \in MCCalls1 |-> 1] +MCCallKind1 == [c \in MCCalls1 |-> "slot"] +\* One terminate_slot call fenced with expect. +MCCalls1e == {1} +MCCallSlot1e == [c \in MCCalls1e |-> 1] +MCCallKind1e == [c \in MCCalls1e |-> "expect"] +\* No terminate calls. +MCCalls0 == {} +MCCallSlot0 == [c \in MCCalls0 |-> 1] +MCCallKind0 == [c \in MCCalls0 |-> "id"] +============================================================================= diff --git a/verification/tla/MCDynamicSupervisorAbort.cfg b/verification/tla/MCDynamicSupervisorAbort.cfg new file mode 100644 index 00000000..a20381e9 --- /dev/null +++ b/verification/tla/MCDynamicSupervisorAbort.cfg @@ -0,0 +1,23 @@ +\* Per PR, liveness under CallerSpec without startup deadlines: once +\* shutdown begins every pending start is answered by its abort (and the +\* cleanup deadline), not by a startup timeout. Passes as is; the NoAbort +\* control must fail here. Small: one cap, no budget, no terminate calls. +SPECIFICATION CallerSpec +CONSTANTS + N = 2 + ModeSet = {"Permanent", "Transient", "Temporary"} + MaxChildren = 1 + MaxRestarts = 0 + MaxExpire = 0 + SelfExits = {"Normal", "Panic"} + StartFails = {"none"} + CleanupFails = {FALSE} + TermCalls <- MCCalls0 + CallSlot <- MCCallSlot0 + CallKind <- MCCallKind0 + BackoffOn = FALSE + StartDeadlines = FALSE + FanoutSteps = FALSE + Fault = "None" +INVARIANT TypeOK +PROPERTY ShutdownAnswersStarts diff --git a/verification/tla/MCDynamicSupervisorAbort.tla b/verification/tla/MCDynamicSupervisorAbort.tla new file mode 100644 index 00000000..fd8bb66b --- /dev/null +++ b/verification/tla/MCDynamicSupervisorAbort.tla @@ -0,0 +1,3 @@ +---- MODULE MCDynamicSupervisorAbort ---- +EXTENDS MCDynamicSupervisor +==== diff --git a/verification/tla/MCDynamicSupervisorBackoff.cfg b/verification/tla/MCDynamicSupervisorBackoff.cfg new file mode 100644 index 00000000..ae2a7096 --- /dev/null +++ b/verification/tla/MCDynamicSupervisorBackoff.cfg @@ -0,0 +1,47 @@ +\* Per PR, safety with backoff configured and one unfenced terminate_slot +\* call. MCDynamicSupervisorBackoffDeep has two calls. +SPECIFICATION Spec +CONSTANTS + N = 2 + ModeSet = {"Permanent", "Transient", "Temporary"} + MaxChildren = 1 + MaxRestarts = 1 + MaxExpire = 1 + SelfExits = {"Normal", "Panic"} + StartFails = {"none", "Normal"} + CleanupFails = {FALSE, TRUE} + TermCalls <- MCCalls1 + CallSlot <- MCCallSlot1 + CallKind <- MCCallKind1 + BackoffOn = TRUE + StartDeadlines = TRUE + FanoutSteps = FALSE + Fault = "None" +INVARIANT TypeOK +INVARIANT AtMostOneGeneration +INVARIANT PublishedIsLive +INVARIANT NoChildOutlivesSupervisor +INVARIANT MaxChildrenBound +INVARIANT SerialConstruction +INVARIANT FifoOrder +INVARIANT TemporaryNeverRestarted +INVARIANT TerminatedNeverRestarted +INVARIANT NoGenerationAfterClose +INVARIANT NoPublishAfterStop +INVARIANT NoStartAfterShutdown +INVARIANT RestartFollowsPolicy +INVARIANT FirstStartNeverRetried +INVARIANT FailedAfterCleanup +INVARIANT FailureCauseKept +INVARIANT ChargedRestarts +INVARIANT ReservationsMatch +INVARIANT BudgetBounded +INVARIANT ExhaustionCloses +INVARIANT StuckIsolated +INVARIANT ConcurrentShutdown +INVARIANT OkMeansReady +INVARIANT TermResultsSound +INVARIANT RemovedAfterFinalize +INVARIANT QueuedTermStopped +PROPERTY NeverReopens +PROPERTY TermResultStable diff --git a/verification/tla/MCDynamicSupervisorBackoff.tla b/verification/tla/MCDynamicSupervisorBackoff.tla new file mode 100644 index 00000000..f3c2683d --- /dev/null +++ b/verification/tla/MCDynamicSupervisorBackoff.tla @@ -0,0 +1,3 @@ +---- MODULE MCDynamicSupervisorBackoff ---- +EXTENDS MCDynamicSupervisor +==== diff --git a/verification/tla/MCDynamicSupervisorBackoffDeep.cfg b/verification/tla/MCDynamicSupervisorBackoffDeep.cfg new file mode 100644 index 00000000..e704e24c --- /dev/null +++ b/verification/tla/MCDynamicSupervisorBackoffDeep.cfg @@ -0,0 +1,48 @@ +\* Weekly (--deep): as WideDeep with backoff configured (reservation, timer, +\* retry through the queue, refund on cancel). 55M states, 13 min on fede. +\* The reservation controls run here. +SPECIFICATION Spec +CONSTANTS + N = 2 + ModeSet = {"Permanent", "Transient", "Temporary"} + MaxChildren = 1 + MaxRestarts = 1 + MaxExpire = 1 + SelfExits = {"Normal", "Panic"} + StartFails = {"none", "Normal"} + CleanupFails = {FALSE, TRUE} + TermCalls <- MCCalls2 + CallSlot <- MCCallSlot2 + CallKind <- MCCallKind2 + BackoffOn = TRUE + StartDeadlines = TRUE + FanoutSteps = FALSE + Fault = "None" +INVARIANT TypeOK +INVARIANT AtMostOneGeneration +INVARIANT PublishedIsLive +INVARIANT NoChildOutlivesSupervisor +INVARIANT MaxChildrenBound +INVARIANT SerialConstruction +INVARIANT FifoOrder +INVARIANT TemporaryNeverRestarted +INVARIANT TerminatedNeverRestarted +INVARIANT NoGenerationAfterClose +INVARIANT NoPublishAfterStop +INVARIANT NoStartAfterShutdown +INVARIANT RestartFollowsPolicy +INVARIANT FirstStartNeverRetried +INVARIANT FailedAfterCleanup +INVARIANT FailureCauseKept +INVARIANT ChargedRestarts +INVARIANT ReservationsMatch +INVARIANT BudgetBounded +INVARIANT ExhaustionCloses +INVARIANT StuckIsolated +INVARIANT ConcurrentShutdown +INVARIANT OkMeansReady +INVARIANT TermResultsSound +INVARIANT RemovedAfterFinalize +INVARIANT QueuedTermStopped +PROPERTY NeverReopens +PROPERTY TermResultStable diff --git a/verification/tla/MCDynamicSupervisorBackoffDeep.tla b/verification/tla/MCDynamicSupervisorBackoffDeep.tla new file mode 100644 index 00000000..a8e4c1ff --- /dev/null +++ b/verification/tla/MCDynamicSupervisorBackoffDeep.tla @@ -0,0 +1,3 @@ +---- MODULE MCDynamicSupervisorBackoffDeep ---- +EXTENDS MCDynamicSupervisor +==== diff --git a/verification/tla/MCDynamicSupervisorCallers.cfg b/verification/tla/MCDynamicSupervisorCallers.cfg new file mode 100644 index 00000000..3665eca7 --- /dev/null +++ b/verification/tla/MCDynamicSupervisorCallers.cfg @@ -0,0 +1,23 @@ +\* Per PR: as MCDynamicSupervisorCallersDeep with two restart types +\* (Permanent, Temporary) instead of three. +SPECIFICATION CallerSpec +CONSTANTS + N = 2 + ModeSet = {"Permanent", "Temporary"} + MaxChildren = 2 + MaxRestarts = 1 + MaxExpire = 1 + SelfExits = {"Normal", "Panic"} + StartFails = {"none"} + CleanupFails = {FALSE} + TermCalls <- MCCalls1 + CallSlot <- MCCallSlot1 + CallKind <- MCCallKind1 + BackoffOn = FALSE + StartDeadlines = TRUE + FanoutSteps = TRUE + Fault = "None" +INVARIANT TypeOK +PROPERTY StartAnswered +PROPERTY TerminateAnswered +PROPERTY FanoutCompletes diff --git a/verification/tla/MCDynamicSupervisorCallers.tla b/verification/tla/MCDynamicSupervisorCallers.tla new file mode 100644 index 00000000..731f643a --- /dev/null +++ b/verification/tla/MCDynamicSupervisorCallers.tla @@ -0,0 +1,3 @@ +---- MODULE MCDynamicSupervisorCallers ---- +EXTENDS MCDynamicSupervisor +==== diff --git a/verification/tla/MCDynamicSupervisorCallersDeep.cfg b/verification/tla/MCDynamicSupervisorCallersDeep.cfg new file mode 100644 index 00000000..df08b8fd --- /dev/null +++ b/verification/tla/MCDynamicSupervisorCallersDeep.cfg @@ -0,0 +1,26 @@ +\* Weekly (--deep): liveness under CallerSpec (no user cleanup ever assumed +\* to finish, only deadlines fire), every pair of restart types: every +\* start_child and terminate_child is answered, and the fan-out, as separate +\* steps, signals every admitted child even if siblings never finish. +\* 11.7M states, 47 min on a loaded fede. The liveness controls run here. +SPECIFICATION CallerSpec +CONSTANTS + N = 2 + ModeSet = {"Permanent", "Transient", "Temporary"} + MaxChildren = 2 + MaxRestarts = 1 + MaxExpire = 1 + SelfExits = {"Normal", "Panic"} + StartFails = {"none"} + CleanupFails = {FALSE} + TermCalls <- MCCalls1 + CallSlot <- MCCallSlot1 + CallKind <- MCCallKind1 + BackoffOn = FALSE + StartDeadlines = TRUE + FanoutSteps = TRUE + Fault = "None" +INVARIANT TypeOK +PROPERTY StartAnswered +PROPERTY TerminateAnswered +PROPERTY FanoutCompletes diff --git a/verification/tla/MCDynamicSupervisorCallersDeep.tla b/verification/tla/MCDynamicSupervisorCallersDeep.tla new file mode 100644 index 00000000..1d062954 --- /dev/null +++ b/verification/tla/MCDynamicSupervisorCallersDeep.tla @@ -0,0 +1,3 @@ +---- MODULE MCDynamicSupervisorCallersDeep ---- +EXTENDS MCDynamicSupervisor +==== diff --git a/verification/tla/MCDynamicSupervisorDeep.cfg b/verification/tla/MCDynamicSupervisorDeep.cfg new file mode 100644 index 00000000..e7b4db17 --- /dev/null +++ b/verification/tla/MCDynamicSupervisorDeep.cfg @@ -0,0 +1,49 @@ +\* Weekly (--deep): budget 2, two window releases, max_children 2, +\* backoff on, one terminate call, no recorded cleanup failures (with two +\* calls and cleanup failures it passed 4 GB of TLC state in 28 minutes). +\* Safety. +SPECIFICATION Spec +CONSTANTS + N = 2 + ModeSet = {"Permanent", "Transient", "Temporary"} + MaxChildren = 2 + MaxRestarts = 2 + MaxExpire = 2 + SelfExits = {"Normal", "Panic"} + StartFails = {"none", "Normal"} + CleanupFails = {FALSE} + TermCalls <- MCCalls1 + CallSlot <- MCCallSlot1 + CallKind <- MCCallKind1 + BackoffOn = TRUE + StartDeadlines = TRUE + FanoutSteps = FALSE + Fault = "None" +INVARIANT TypeOK +INVARIANT AtMostOneGeneration +INVARIANT PublishedIsLive +INVARIANT NoChildOutlivesSupervisor +INVARIANT MaxChildrenBound +INVARIANT SerialConstruction +INVARIANT FifoOrder +INVARIANT TemporaryNeverRestarted +INVARIANT TerminatedNeverRestarted +INVARIANT NoGenerationAfterClose +INVARIANT NoPublishAfterStop +INVARIANT NoStartAfterShutdown +INVARIANT RestartFollowsPolicy +INVARIANT FirstStartNeverRetried +INVARIANT FailedAfterCleanup +INVARIANT FailureCauseKept +INVARIANT ChargedRestarts +INVARIANT ReservationsMatch +INVARIANT BudgetBounded +INVARIANT ExhaustionCloses +INVARIANT StuckIsolated +INVARIANT ConcurrentShutdown +INVARIANT OkMeansReady +INVARIANT TermResultsSound +INVARIANT RemovedAfterFinalize +INVARIANT QueuedTermStopped +PROPERTY NeverReopens +PROPERTY TermResultStable diff --git a/verification/tla/MCDynamicSupervisorDeep.tla b/verification/tla/MCDynamicSupervisorDeep.tla new file mode 100644 index 00000000..2b821daf --- /dev/null +++ b/verification/tla/MCDynamicSupervisorDeep.tla @@ -0,0 +1,3 @@ +---- MODULE MCDynamicSupervisorDeep ---- +EXTENDS MCDynamicSupervisor +==== diff --git a/verification/tla/MCDynamicSupervisorLive.cfg b/verification/tla/MCDynamicSupervisorLive.cfg new file mode 100644 index 00000000..97f16aed --- /dev/null +++ b/verification/tla/MCDynamicSupervisorLive.cfg @@ -0,0 +1,22 @@ +\* Per PR, liveness under Spec (cleanup eventually ends): shutdown +\* completes, recovery progresses. Backoff on, one terminate call. +SPECIFICATION Spec +CONSTANTS + N = 2 + ModeSet = {"Permanent", "Transient", "Temporary"} + MaxChildren = 1 + MaxRestarts = 1 + MaxExpire = 1 + SelfExits = {"Normal", "Panic"} + StartFails = {"none"} + CleanupFails = {FALSE} + TermCalls <- MCCalls1 + CallSlot <- MCCallSlot1 + CallKind <- MCCallKind1 + BackoffOn = TRUE + StartDeadlines = TRUE + FanoutSteps = FALSE + Fault = "None" +INVARIANT TypeOK +PROPERTY ClosedLeadsToDone +PROPERTY RecoveryProgress diff --git a/verification/tla/MCDynamicSupervisorLive.tla b/verification/tla/MCDynamicSupervisorLive.tla new file mode 100644 index 00000000..ad366e00 --- /dev/null +++ b/verification/tla/MCDynamicSupervisorLive.tla @@ -0,0 +1,3 @@ +---- MODULE MCDynamicSupervisorLive ---- +EXTENDS MCDynamicSupervisor +==== diff --git a/verification/tla/MCDynamicSupervisorThree.cfg b/verification/tla/MCDynamicSupervisorThree.cfg new file mode 100644 index 00000000..e343a08d --- /dev/null +++ b/verification/tla/MCDynamicSupervisorThree.cfg @@ -0,0 +1,48 @@ +\* Targeted, three start_child calls (Permanent, crashing): FIFO +\* admission, max_children 2 with a restarting child holding its slot, +\* and two restartable children sharing a budget of 1. Safety. +SPECIFICATION Spec +CONSTANTS + N = 3 + ModeSet = {"Permanent"} + MaxChildren = 2 + MaxRestarts = 1 + MaxExpire = 1 + SelfExits = {"Panic"} + StartFails = {} + CleanupFails = {FALSE} + TermCalls <- MCCalls0 + CallSlot <- MCCallSlot0 + CallKind <- MCCallKind0 + BackoffOn = FALSE + StartDeadlines = TRUE + FanoutSteps = FALSE + Fault = "None" +INVARIANT TypeOK +INVARIANT AtMostOneGeneration +INVARIANT PublishedIsLive +INVARIANT NoChildOutlivesSupervisor +INVARIANT MaxChildrenBound +INVARIANT SerialConstruction +INVARIANT FifoOrder +INVARIANT TemporaryNeverRestarted +INVARIANT TerminatedNeverRestarted +INVARIANT NoGenerationAfterClose +INVARIANT NoPublishAfterStop +INVARIANT NoStartAfterShutdown +INVARIANT RestartFollowsPolicy +INVARIANT FirstStartNeverRetried +INVARIANT FailedAfterCleanup +INVARIANT FailureCauseKept +INVARIANT ChargedRestarts +INVARIANT ReservationsMatch +INVARIANT BudgetBounded +INVARIANT ExhaustionCloses +INVARIANT StuckIsolated +INVARIANT ConcurrentShutdown +INVARIANT OkMeansReady +INVARIANT TermResultsSound +INVARIANT RemovedAfterFinalize +INVARIANT QueuedTermStopped +PROPERTY NeverReopens +PROPERTY TermResultStable diff --git a/verification/tla/MCDynamicSupervisorThree.tla b/verification/tla/MCDynamicSupervisorThree.tla new file mode 100644 index 00000000..a4e39f7f --- /dev/null +++ b/verification/tla/MCDynamicSupervisorThree.tla @@ -0,0 +1,3 @@ +---- MODULE MCDynamicSupervisorThree ---- +EXTENDS MCDynamicSupervisor +==== diff --git a/verification/tla/MCDynamicSupervisorWideDeep.cfg b/verification/tla/MCDynamicSupervisorWideDeep.cfg new file mode 100644 index 00000000..8755422a --- /dev/null +++ b/verification/tla/MCDynamicSupervisorWideDeep.cfg @@ -0,0 +1,50 @@ +\* Weekly (--deep): the broad instance, two terminate calls (by id and by slot +\* fenced with expect, both naming any generation seen), budget 1, no backoff, +\* every outcome. 47M states, 10 min on fede: too slow per PR. The safety +\* negative controls run here (a counterexample is found in seconds whatever +\* the instance size). +SPECIFICATION Spec +CONSTANTS + N = 2 + ModeSet = {"Permanent", "Transient", "Temporary"} + MaxChildren = 1 + MaxRestarts = 1 + MaxExpire = 1 + SelfExits = {"Normal", "Panic"} + StartFails = {"none", "Normal"} + CleanupFails = {FALSE, TRUE} + TermCalls <- MCCalls2 + CallSlot <- MCCallSlot2 + CallKind <- MCCallKind2 + BackoffOn = FALSE + StartDeadlines = TRUE + FanoutSteps = FALSE + Fault = "None" +INVARIANT TypeOK +INVARIANT AtMostOneGeneration +INVARIANT PublishedIsLive +INVARIANT NoChildOutlivesSupervisor +INVARIANT MaxChildrenBound +INVARIANT SerialConstruction +INVARIANT FifoOrder +INVARIANT TemporaryNeverRestarted +INVARIANT TerminatedNeverRestarted +INVARIANT NoGenerationAfterClose +INVARIANT NoPublishAfterStop +INVARIANT NoStartAfterShutdown +INVARIANT RestartFollowsPolicy +INVARIANT FirstStartNeverRetried +INVARIANT FailedAfterCleanup +INVARIANT FailureCauseKept +INVARIANT ChargedRestarts +INVARIANT ReservationsMatch +INVARIANT BudgetBounded +INVARIANT ExhaustionCloses +INVARIANT StuckIsolated +INVARIANT ConcurrentShutdown +INVARIANT OkMeansReady +INVARIANT TermResultsSound +INVARIANT RemovedAfterFinalize +INVARIANT QueuedTermStopped +PROPERTY NeverReopens +PROPERTY TermResultStable diff --git a/verification/tla/MCDynamicSupervisorWideDeep.tla b/verification/tla/MCDynamicSupervisorWideDeep.tla new file mode 100644 index 00000000..2dfd17ba --- /dev/null +++ b/verification/tla/MCDynamicSupervisorWideDeep.tla @@ -0,0 +1,3 @@ +---- MODULE MCDynamicSupervisorWideDeep ---- +EXTENDS MCDynamicSupervisor +==== diff --git a/verification/tla/MCDynamicSupervisorZero.cfg b/verification/tla/MCDynamicSupervisorZero.cfg new file mode 100644 index 00000000..562510da --- /dev/null +++ b/verification/tla/MCDynamicSupervisorZero.cfg @@ -0,0 +1,47 @@ +\* Per PR, safety with max_restarts 0: the first restartable exit fails +\* the supervisor at once. +SPECIFICATION Spec +CONSTANTS + N = 2 + ModeSet = {"Permanent", "Transient", "Temporary"} + MaxChildren = 1 + MaxRestarts = 0 + MaxExpire = 0 + SelfExits = {"Normal", "Panic"} + StartFails = {"none", "Normal"} + CleanupFails = {FALSE, TRUE} + TermCalls <- MCCalls2 + CallSlot <- MCCallSlot2 + CallKind <- MCCallKind2 + BackoffOn = FALSE + StartDeadlines = TRUE + FanoutSteps = FALSE + Fault = "None" +INVARIANT TypeOK +INVARIANT AtMostOneGeneration +INVARIANT PublishedIsLive +INVARIANT NoChildOutlivesSupervisor +INVARIANT MaxChildrenBound +INVARIANT SerialConstruction +INVARIANT FifoOrder +INVARIANT TemporaryNeverRestarted +INVARIANT TerminatedNeverRestarted +INVARIANT NoGenerationAfterClose +INVARIANT NoPublishAfterStop +INVARIANT NoStartAfterShutdown +INVARIANT RestartFollowsPolicy +INVARIANT FirstStartNeverRetried +INVARIANT FailedAfterCleanup +INVARIANT FailureCauseKept +INVARIANT ChargedRestarts +INVARIANT ReservationsMatch +INVARIANT BudgetBounded +INVARIANT ExhaustionCloses +INVARIANT StuckIsolated +INVARIANT ConcurrentShutdown +INVARIANT OkMeansReady +INVARIANT TermResultsSound +INVARIANT RemovedAfterFinalize +INVARIANT QueuedTermStopped +PROPERTY NeverReopens +PROPERTY TermResultStable diff --git a/verification/tla/MCDynamicSupervisorZero.tla b/verification/tla/MCDynamicSupervisorZero.tla new file mode 100644 index 00000000..a603fe12 --- /dev/null +++ b/verification/tla/MCDynamicSupervisorZero.tla @@ -0,0 +1,3 @@ +---- MODULE MCDynamicSupervisorZero ---- +EXTENDS MCDynamicSupervisor +==== diff --git a/verification/tla/README.md b/verification/tla/README.md index e7e98223..99e4b4aa 100644 --- a/verification/tla/README.md +++ b/verification/tla/README.md @@ -18,6 +18,7 @@ this fits with Loom, Shuttle, Miri, ThreadSanitizer and mutation testing. | `DeferredReplies.tla`, `MCDeferredReplies*.tla/.cfg` | Rank 11 design model (not implemented), part 1: reply slots, send-time deadlines with shortening, deferral credits shared by a token and its first linked job, the exiting phase with unwind-local drops, a stuck phase (cleanup deadline passed while `stopped()` runs: nothing closed early, death later or never), death, and downstream request cleanup. Thirteen named negative controls. | | `DeferredJobs.tla`, `MCDeferredJobs*.tla/.cfg` | Rank 11 design model, part 2: pipe jobs with separate execution, cancellation and notification states; keyed replacement including notified jobs; optional job deadlines; a FIFO mailbox with emit credits and the terminal message last; `ActorId` fencing. `MCDeferredJobsEmits` is the fast configuration with emits. Nine named negative controls. | | `Lifecycle.tla`, `MCLifecycle{,Live,Fence,Deep,LiveDeep,WideDeep}.tla/.cfg` | Base actor lifecycle as proposed for v0.8 ([design](../../docs/design/otp-exit-signals.md)): links, monitors, `trap_exit`, exit signals (`Killed`, ignored `Normal`, `NoProc`, parent exits), administrative stops, requests around death, `Exit`/`Down` ordering. Seventeen negative-control faults (17 safety checks, 2 liveness checks): the v0.7 exit-signal behaviours (direct stops ignoring `trap_exit`, kills ending `Kill`, unfenced `unlink`/`demonitor`, real reasons for late registrations, `stopped()` after kills and untrapped signals, late signals ignored during exit), the PR #182/#185 bugs, early exit errors, kill and panic precedence, runtime-drop reasons, early notification, a split death point and a parent exit reaching `exit_received`. Per PR: `MCLifecycle` (7.5M states, fewer reasons, where the safety controls run), `MCLifecycleFence`, `MCLifecycleLive`; weekly: `MCLifecycleWideDeep` (the former 43M-state per-PR instance), `MCLifecycleDeep`, `MCLifecycleLiveDeep`. | +| `DynamicSupervisor.tla`, `MCDynamicSupervisor*.tla/.cfg` | Rank 12a design model (not implemented, [design](../../docs/design/dynamic-supervisor.md)): OTP's serialised control loop with one FIFO queue; `start_child` and `terminate_child` racing crashes, restarts, `max_children`, the budget reservation protocol, ignore, stuck children and shutdown. 44 named negative controls. Per PR: `MCDynamicSupervisor`, `Backoff`, `Zero`, `Three`, `Abort`, `Callers`, `Live`; weekly: `Deep`, `WideDeep`, `BackoffDeep`. | | `Start.tla`, `MCStart{,Names,Cap,Timeout,Continue,Scope,Live,Deep}.tla/.cfg` | Unified start API, 0.9 design (approved after three review rounds) ([design](../../docs/design/unified-start.md), not implemented; TLC-only in `model-map.toml` until trace validation lands with the implementation): `spawn`, `start`, `start_link`, `start_monitor`; placement inheritance; an atomic stage-1 commit with the owner gate; an immutable startup commitment and a waiter; death as D, release, then publication, for the child and the parent; the final reason fixed at D; fallible init with held-signal precedence; the continuation; S8 scope ownership with the polite Shutdown and the scope deadline. 40 negative controls (37 safety, 3 liveness); see [Unified start](#unified-start-09-design). Per PR: `MCStart`, `MCStartNames`, `MCStartCap`, `MCStartTimeout`, `MCStartContinue`, `MCStartScope`, `MCStartLive` (CI leg `start`); weekly: `MCStartDeep`. | | `TraceCohorts.tla`, `TraceNested.tla` | Policy and ownership projections of real cohort/nested Rust executions. | | `trace_check.py`, `negative_checks.py` | Replay recorded traces; deliberately wrong selections, premature resume/join and broken propagation must be rejected or produce counterexamples. | @@ -606,6 +607,41 @@ Measured 2026-11-10 (TLC 2.19, fede): All 22 named controls find their counterexample, each in a few seconds. +## Dynamic supervisor (rank 12a design) + +`DynamicSupervisor.tla` backs the [dynamic supervisor design](../../docs/design/dynamic-supervisor.md) +(revision 3), written before any implementation. `start_child` calls and +`terminate_child` calls (by the id the caller saw, or by slot) arrive at any +moment; one control loop takes starts, terminate calls, exit notices and +backoff retries from one FIFO queue, as OTP's supervisor process. Budget +reservations, stamping, refunds and window expiry are explicit; children can +ignore, fail, time out, exit, be stopped or killed, record a cleanup failure, +or get stuck. Event invariants read history variables computed by +`GhostUpdate`. `CallerSpec` assumes no user cleanup ever ends (only +deadlines fire) and checks that callers are answered; `Spec` adds cleanup +progress for shutdown completion and recovery. The design's +[model section](../../docs/design/dynamic-supervisor.md#what-the-model-establishes) +lists the 23 invariants, the properties and the 44 negative controls (37 +safety, 7 liveness), run one at a time from `negative_checks.py`; its +[test plan](../../docs/design/dynamic-supervisor.md#test-plan-relating-the-model-to-the-code) +lists the trace events the implementation must emit for trace validation. + +Measured 2026-11-11 (TLC 2.19, fede, 4 workers, `nice -n 19`). Bounded +checks; no cutoff argument is claimed. + +| Configuration | Distinct states | Depth | Time | +|---|---|---|---| +| `MCDynamicSupervisor` (per PR, safety) | 8,488,736 | 30 | 1m26s | +| `MCDynamicSupervisorBackoff` (per PR, safety) | 9,878,333 | 36 | 1m48s | +| `MCDynamicSupervisorZero` (per PR, safety) | 1,170,745 | 21 | 12 s | +| `MCDynamicSupervisorThree` (per PR, safety, three slots) | 442,239 | 30 | 7 s | +| `MCDynamicSupervisorCallers` (per PR, liveness under `CallerSpec`) | 3,380,536 | 29 | 6m33s | +| `MCDynamicSupervisorLive` (per PR, liveness under `Spec`) | 581,563 | 34 | 55 s | +| `MCDynamicSupervisorDeep` (weekly, safety) | 9,992,213 | 45 | 1m35s | + +Not yet: Apalache inductive invariants, and trace validation, which comes +with the implementation. + ## Unified start (0.9 design) `Start.tla` backs the [unified start design](../../docs/design/unified-start.md) diff --git a/verification/tla/negative_checks.py b/verification/tla/negative_checks.py index 289f4f95..df60ccb6 100644 --- a/verification/tla/negative_checks.py +++ b/verification/tla/negative_checks.py @@ -96,10 +96,13 @@ def model_fault(module, fault, tlc, temporal=False, invariant="Safety", drop=()) print(f"COUNTEREXAMPLE model: {module}/{fault}" + ("" if temporal else f" ({invariant})")) -def named_fault(module, fault, invariant, tlc): +def named_fault(module, fault, invariant, tlc, constants=None): """Run MODULE (safety only) with Fault = FAULT, checking TypeOK and the single named INVARIANT, and require that invariant to be violated. This - shows the mutation breaks the property it targets, not just Safety.""" + shows the mutation breaks the property it targets, not just Safety. + CONSTANTS overrides constant values (an instance where the fault can + show).""" + constants = constants or {} with tempfile.TemporaryDirectory(prefix="bad-model-") as directory: work = Path(directory) for source in HERE.glob("*.tla"): @@ -112,6 +115,9 @@ def named_fault(module, fault, invariant, tlc): line = "SPECIFICATION Spec" if line.startswith("INVARIANT"): line = f"INVARIANT TypeOK\nINVARIANT {invariant}" + name = line.strip().split(" ")[0] + if name in constants: + line = f" {name} = {constants[name]}" lines.append(line.replace('Fault = "None"', f'Fault = "{fault}"')) (work / f"{module}.cfg").write_text("\n".join(lines) + "\n") result = subprocess.run(shlex.split(tlc) + ["-workers", "1", "-deadlock", "-cleanup", module], @@ -216,6 +222,60 @@ def named_temporal(module, fault, prop, tlc, constants=None): ] LIFECYCLE_SMALL = {"Reqs": "{}", "MaxSignals": "0", "DropEnabled": "FALSE"} +# Rank 12a design model (docs/design/dynamic-supervisor.md, revision 3): +# each mutation against the property it must break. Every invariant and +# liveness property of DynamicSupervisor.tla has at least one. Run one at a +# time (parallel TLC runs race on the standard modules TLC extracts to /tmp). +DYNAMIC_CONTROLS = [ + ("MCDynamicSupervisorWideDeep", "IgnoreMax", "MaxChildrenBound"), + ("MCDynamicSupervisorWideDeep", "UncountedRestart", "MaxChildrenBound"), + ("MCDynamicSupervisorWideDeep", "RestartTemporary", "TemporaryNeverRestarted"), + ("MCDynamicSupervisorWideDeep", "RestartTerminated", "TerminatedNeverRestarted"), + ("MCDynamicSupervisorWideDeep", "AcceptDuringShutdown", "NoStartAfterShutdown"), + ("MCDynamicSupervisorBackoffDeep", "RestartAfterClose", "NoGenerationAfterClose"), + ("MCDynamicSupervisorWideDeep", "NoEscalate", "ExhaustionCloses"), + ("MCDynamicSupervisorWideDeep", "EarlyDone", "NoChildOutlivesSupervisor"), + ("MCDynamicSupervisorWideDeep", "SkipSignal", "ConcurrentShutdown"), + ("MCDynamicSupervisorWideDeep", "ConcurrentStart", "SerialConstruction", {"MaxChildren": "2"}), + ("MCDynamicSupervisorWideDeep", "LaterOp", "FifoOrder"), + ("MCDynamicSupervisorWideDeep", "StuckFailsAll", "StuckIsolated"), + ("MCDynamicSupervisorWideDeep", "MisclassifyStuck", "StuckIsolated"), + ("MCDynamicSupervisorWideDeep", "PublishAfterClose", "NoPublishAfterStop"), + ("MCDynamicSupervisorWideDeep", "PublishAfterExit", "PublishedIsLive"), + ("MCDynamicSupervisorWideDeep", "OverlapGeneration", "AtMostOneGeneration"), + ("MCDynamicSupervisorWideDeep", "PublishBeforeReady", "PublishedIsLive"), + ("MCDynamicSupervisorWideDeep", "PrematureOk", "OkMeansReady"), + ("MCDynamicSupervisorWideDeep", "UnchargedRetry", "ChargedRestarts"), + ("MCDynamicSupervisorWideDeep", "ChargeFirstStart", "ChargedRestarts"), + ("MCDynamicSupervisorWideDeep", "TransientNormalRestart", "RestartFollowsPolicy"), + ("MCDynamicSupervisorWideDeep", "TransientNormalRestart", "RestartFollowsPolicy", {"MaxRestarts": "0", "MaxExpire": "0"}), + ("MCDynamicSupervisorWideDeep", "PermanentRetires", "RestartFollowsPolicy"), + ("MCDynamicSupervisorWideDeep", "RetryFirstStart", "FirstStartNeverRetried"), + ("MCDynamicSupervisorWideDeep", "EarlyFailedReply", "FailedAfterCleanup"), + ("MCDynamicSupervisorWideDeep", "EarlyRemove", "FailedAfterCleanup"), + ("MCDynamicSupervisorWideDeep", "LateFailedOverwrite", "FailureCauseKept"), + ("MCDynamicSupervisorBackoffDeep", "NoRefund", "ReservationsMatch"), + ("MCDynamicSupervisorBackoffDeep", "ExpireReserved", "ReservationsMatch"), + ("MCDynamicSupervisorWideDeep", "OverReserve", "BudgetBounded"), + ("MCDynamicSupervisorWideDeep", "TermReplyEarly", "TermResultsSound"), + ("MCDynamicSupervisorWideDeep", "SlotLookup", "TermResultsSound"), + ("MCDynamicSupervisorWideDeep", "QueuedTermOk", "QueuedTermStopped"), + ("MCDynamicSupervisorWideDeep", "StuckResultLost", "TermResultsSound"), + ("MCDynamicSupervisorWideDeep", "IgnoreExpect", "TermResultsSound"), + ("MCDynamicSupervisorWideDeep", "EarlyFree", "RemovedAfterFinalize"), + ("MCDynamicSupervisorWideDeep", "IgnoreFreesEarly", "RemovedAfterFinalize"), + ("MCDynamicSupervisorWideDeep", "IgnoreAfterClose", "NoStartAfterShutdown"), +] +DYNAMIC_TEMPORAL_CONTROLS = [ + # MCDynamicSupervisorAbort has no startup deadlines and passes unmutated. + ("MCDynamicSupervisorAbort", "NoAbort", "ShutdownAnswersStarts"), + ("MCDynamicSupervisorCallersDeep", "NoDeadline", "StartAnswered"), + ("MCDynamicSupervisorCallersDeep", "TermLost", "TerminateAnswered"), + ("MCDynamicSupervisorCallersDeep", "Sequential", "FanoutCompletes"), + ("MCDynamicSupervisorLive", "StuckBackoff", "ClosedLeadsToDone"), + ("MCDynamicSupervisorLive", "LostRestart", "RecoveryProgress"), +] + DEFERRED_CONTROLS = [ ("MCDeferredReplies", "NoAutoReply", "NoOrphan"), ("MCDeferredReplies", "NoAtomicExpiry", "AtMostOneDischarge"), @@ -386,6 +446,10 @@ def fail_instead_of_retry(events): named_fault(module, fault, invariant, args.tlc) for fault, prop in LIFECYCLE_TEMPORAL_CONTROLS: named_temporal("MCLifecycleLive", fault, prop, args.tlc, LIFECYCLE_SMALL) + for module, fault, invariant, *constants in DYNAMIC_CONTROLS: + named_fault(module, fault, invariant, args.tlc, *constants) + for module, fault, prop, *constants in DYNAMIC_TEMPORAL_CONTROLS: + named_temporal(module, fault, prop, args.tlc, *constants) start_controls(args.tlc)