docs: unified start API design (0.9)

.github/workflows/verification.yml

@@ -36,8 +36,10 @@ jobs:
             select: --only 'MCLifecycle*'
           - leg: deferred
             select: --only 'MCDeferred*'
+          - leg: start
+            select: --only 'MCStart*'
           - leg: other
-            select: --exclude 'MCSupervision,MCLifecycle*,MCDeferred*'
+            select: --exclude 'MCSupervision,MCLifecycle*,MCDeferred*,MCStart*'
     steps:
       - uses: actions/checkout@v4
       - uses: DeterminateSystems/nix-installer-action@v16
@@ -112,6 +114,7 @@ jobs:
           - MCLifecycleWideDeep
           - MCLifecycleLiveDeep
           - MCLifecycleDeep
+          - MCStartDeep
     steps:
       - uses: actions/checkout@v4
       - uses: DeterminateSystems/nix-installer-action@v16

CHANGELOG.md

@@ -2,6 +2,20 @@
 
 ## Unreleased
 
+- Design (0.9, approved for implementation after round 3): a unified start API
+  (`docs/design/unified-start.md`, rank 5h). OTP's `start`, `start_link` and
+  `start_monitor` wait for `started()`, and `spawn` does not. All four take one
+  typed `StartOptions`. `started()` may fail, ignore or continue (`Init`), and a
+  failed init never runs `stopped()`, as OTP. Every instance has an immutable
+  startup commitment, and readiness is committed by the child, independently
+  of the waiter. Errors are answered after publication with the final exit
+  reason. One global lock order covers the commit, readiness and scope
+  admission. Linked children in the parent's system are owned by its scope,
+  with a polite Shutdown at the parent's publication and absolute,
+  composing deadlines. It replaces `start_on`, `start_with_backend`,
+  `ExecutionGroup::start` and `start_linked`. A new TLA+ model, `Start.tla`,
+  has eight configurations and 40 negative controls, and a client mapping
+  covers 51 sites.
 - TESTING.md: how databases test (FoundationDB, TigerBeetle, SQLite, AWS,
   Jepsen and others), how each technique maps to spawned, and the gaps.
 - Tests: planted-bug follow-ups. New scenario-fuzzer oracles for restart

ROADMAP.md

@@ -40,6 +40,8 @@ handlers and the existing default behavior. New policies are explicit and opt-in
   release. Client ports are ready on the clients' `spawned-v0.8` branches.
 - **Next feature:** dynamic supervisor (rank 12a), design and TLA+ model in
   review (PR #245).
+- **v0.9 design in review:** unified start API (rank 5h, PR #259,
+  [design](docs/design/unified-start.md)).
 - **0.9 introspection (priority tier 2):** design and TLA+ model in review
   (PR #256, [design](docs/design/introspection.md)): `process_info`-style
   `info()` readable while a handler is wedged, `sys:get_state`/`get_status`
@@ -708,6 +710,7 @@ startup: OTP aborts `start_link` on any child start error, while Spawned retries
 a Permanent or Transient child's failed factory, panic or startup timeout during
 the first start (semantics §11; found reviewing #233). Behaviour change: extend the `Supervision`/`Cohorts` TLA+ models and their Apalache inductive checks (`BudgetBounded`) to the new rule, with a negative control for counting per child, and update the Kani restart-window proofs and the guide. |
 | 5g | One exit reason when the runtime drops an actor (v0.8) | Tasks mode reports `Kill` when the runtime drops an actor; threads mode falls back to `Panic("unexpected framework panic")` for an actor that never finishes cleanup. Pick one documented reason for both modes and test it in both. |
+| 5h | Unified start API (v0.9, design approved for implementation after three review rounds, PR #259) | [Design](docs/design/unified-start.md) with the `Start.tla` model (8 configurations, 40 negative controls; TLC-only until implemented) and a [client mapping](docs/design/unified-start-client-mapping.md). OTP's `start`, `start_link` and `start_monitor` wait for `started()` and answer `Started`, `Ignored` or an error after the child's publication (with the final exit reason); `spawn` does not wait. One typed `StartOptions`. `started()` may fail, ignore or continue (`Init`); a failed init never runs `stopped()`. An immutable startup commitment per instance; readiness committed by the child under the global lock order; the init timer and abandonment arbitrate through the commitment. Linked and monitored children inherit the parent's group or backend (API-review footgun 5.11); linked children in the parent's system are owned by its scope (polite Shutdown at the parent's publication, absolute composing deadlines). Supervisors keep the whole-attempt `startup_timeout`, and `ignore` keeps the spec as OTP. Shared result types with #245 and #256. Client impact: 51 mechanical sites, no behaviour change. |
 | 6 | Test kit with `ActorRef::mock()` | **Phase A implemented** in [`spawned-test`](#testing-crate-spawned-test) (unreleased): closure-backed `Mock` actors that implement `Handler<M>` for every message, so `ActorRef<Mock>` satisfies any `#[protocol]` and replaces hand-stubbed protocol refs with no production change; recording `Probe<M>` recipients (`expect`, `expect_no_message`); bounded harness waits; fault injection (`faults::exit`, `restart_child`, mock delay/discard/crash). Unmocked messages fail loudly. **Remaining:** mocking a field typed as a concrete `ActorRef<B>` needs an `Envelope` hook that downcasts to the concrete message and yields message and reply sender (a core change, deferred); controllable time for timers; a generic idle check; core `ChildHandle::exit(reason)` would make injected exits exact (today `Panic` and `Kill` go through a linked helper, so a panic surfaces as `Panic("panic in handler: ...")`). **Client evidence:** hand-stubbed protocols in ethlambda tests (`RecordingChain` in `column_checks.rs`, also `envelope_checks.rs`, `verdict.rs`). **Research ([actor testing](docs/research/actor-testing.md)):** three gaps against Akka/Erlang kits. (1) A synchronous behavior test kit (Akka `BehaviorTestKit`): run one handler with a test `Context` and record its effects (sends, spawns, timers, stop) without a runtime; needs a core change. (2) Manual time (Akka `ManualTime`): document Tokio's `start_paused` for async actors; thread actors need the framework-owned clock, the same seam as the [simulation backend spike](#simulation-backend-spike) and `ctx.now()`, so build one clock, not two. (3) Concrete `ActorRef<B>` mocking stays deferred (actix's `Mocker` is the precedent); until then users hold protocol refs or `Recipient`s. Also: the idle check should report total deadlock Go-`checkdead` style (every actor idle, a request outstanding, no timer pending), and a replay-equivalence check for event-sourced actors ([event sourcing](docs/research/event-sourcing.md)). |
 | 6b | Shared-state and abort lints in `#[actor]` | Zero runtime cost. The macro warns when an actor's fields hold shared mutable state (`Arc<Mutex<_>>`, `Arc<RwLock<_>>`, atomics behind `Arc`, `static mut`), with an opt-out attribute for deliberate cases, and a build script check warns when the profile uses `panic = "abort"`, under which a handler panic kills the process instead of one actor. Syntactic only (it cannot see sharing behind a type alias), but it catches the common pattern, including the one LLM-written code reaches for first. Erlang gap: memory isolation. |
 | 7 | Request deadlock detection | **Client evidence:** requests awaited inside handlers exist (ethrex peer table), no cycle found; keep as a cheap safety net.  `ActorError::WouldDeadlock` naming the cycle instead of a timeout. `ActorRef::request` takes only `&self`, so set a thread-local `CURRENT_ACTOR` only while the actor's own handler future is polled (and around the synchronous handler in thread mode); detached helpers create no edges. Keep a small wait set per actor for `join!`. Measure cost before enabling outside debug builds. **Approach chosen ([deadlock and stall detection](docs/research/deadlock-and-stall-detection.md)):** eager detection. Add a wait-for edge when a handler sends a request, walk the per-actor wait sets for a cycle, fail the request that would close it with `WouldDeadlock` naming the cycle, remove the edge on reply or timeout; a request to self fails at once (Erlang's `calling_self`). Waits on raw channels, locks or `spawn_blocking` create no edges, so it is a safety net, not a proof. Edges are exported to rank 30. |

docs/design/README.md

@@ -25,6 +25,13 @@ Active design contracts. Usage is documented in the [guide](../GUIDE.md).
   structured reports, the stall watchdog and the attachable remote console
   (`spawned-ctl`). Model: `verification/tla/Introspection.tla`.
 
+- **[unified-start.md](unified-start.md)** (rank 5h, 0.9, design in review,
+  not implemented): one start API as OTP's `start`, `start_link` and
+  `start_monitor` plus `spawn`, with `StartOptions`, placement inheritance,
+  fallible init, continuations and atomic names. Model:
+  `verification/tla/Start.tla`. Client rewrites:
+  [unified-start-client-mapping.md](unified-start-client-mapping.md).
+
 Earlier designs (the v0.5 API redesign alternatives, the framework comparison
 and superseded roadmap plans) are archived in
 [`legacy/docs/design`](https://github.com/lambdaclass/spawned/tree/efba24340a01df82f872ec422b9dbaf48f897b04/legacy/docs/design).