design: dynamic supervisor (rank 12a)

.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

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<Started<A>>`, `ChildStartError`, `Init::continue_with`,
+  `StartOptions<A>`), 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

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. |

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

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,