design: introspection v1 (0.9, priority tier 2)

CHANGELOG.md

@@ -33,6 +33,31 @@
   action; every model must be trace-validated or allowlisted as TLC-only with
   a tracking item (Coordinator, Lifecycle, DeferredReplies, DeferredJobs);
   per-model trace coverage has a floor that may only go up.
+- Design: introspection v1 for 0.9 (priority tier 2), in review:
+  [`docs/design/introspection.md`](docs/design/introspection.md). Per-actor
+  `process_info`, `sys:get_state`/`get_status` answered between turns,
+  supervision-tree and system snapshots, an opt-in stall watchdog (rank 8) and
+  the data model for `spawned-top` (rank 30), an attachable remote console on
+  a local Unix socket (`spawned-ctl`, on by default, read-only by default, no
+  TCP, no eval), with a cost table per field, consistency guarantees and a
+  test plan. TLA+ model `Introspection.tla` (fenced watchdog kill, status
+  between turns and at death) with six negative controls. Design only; no
+  library code change.
+
+- Design: introspection v1 for 0.9 (priority tier 2), revision 2 after two
+  reviews: [`docs/design/introspection.md`](docs/design/introspection.md).
+- Design: introspection v1 for 0.9 (priority tier 2), revision 3 after two
+  review rounds: [`docs/design/introspection.md`](docs/design/introspection.md).
+  `process_info`-style `info()` readable while a handler is wedged (strictly
+  free tier 0, richer with the `introspection` feature), `sys:get_state`/
+  `get_status` as a turn of their own, supervision-tree and system
+  snapshots, structured reports, an opt-in stall watchdog (rank 8) with a
+  fenced kill, and an attachable remote console on a local Unix socket
+  (`spawned-ctl`; on with `ActorSystem::new`, read-only by default, no TCP,
+  no eval). TLA+ model `Introspection.tla` (every activity end, including
+  panics in `started()` and `stopped()`, consumes the kill bit; status between
+  turns and at D; runtime drop; one action per linearization point, status admission included) with 20
+  negative controls; a fork-safe, lock-first socket publication protocol. Design only; no library code change.
 - Tests: coverage follow-ups. `restart_modes_distinguish_normal_shutdown_and_panic`
   now sends a real `Normal` exit; a per-PR `MCSupervisionTemporary` TLC
   configuration makes `TemporaryStartsOnce` non-vacuous, with a negative

ROADMAP.md

@@ -40,6 +40,13 @@ 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).
+- **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`
+  between turns, supervision-tree and system snapshots, structured crash and
+  supervisor reports, the stall watchdog (rank 8) and an attachable remote
+  console on a local Unix socket (`spawned-ctl`, gap G23; starts with
+  `ActorSystem::new`, read-only by default). Revision 3 answers two review rounds. Flight recorder (rank 9) deferred to 0.10.
 - **Process:** every PR merges through GitHub's merge queue with 19 required
   checks, including the simulated suites (`sim`). Robustness features must add
   no cost on the default path (see [Non-goals](#non-goals)).
@@ -704,11 +711,11 @@ the first start (semantics §11; found reviewing #233). Behaviour change: extend
 | 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. |
-| 8 | Stall watchdog | **Client evidence:** wedged and runtime-starving handlers in both clients (see sweep). Upgrade the debug-only `WarnOnBlocking` (whole-loop type name, 10 ms per poll, Async backend only): name the actor and message type, separate "one poll blocked a worker" from "handler stuck across awaits", optional in release builds. Long handler time alone does not establish deadlock. **Research ([deadlock and stall detection](docs/research/deadlock-and-stall-detection.md)):** three detectors: per-poll timing inside dispatch with actor id and message type (a poll blocking a worker), turn age (a handler stuck across awaits), and an Akka-style scheduling-delay probe per execution group (starvation). Tokio's `tokio_unstable` task hooks are optional behind a feature, not required. |
+| 8 | Stall watchdog | **0.9 design in review ([introspection](docs/design/introspection.md), PR #256):** four detectors on an OS-thread watchdog, report by default, fenced `Killed` opt-in. **Client evidence:** wedged and runtime-starving handlers in both clients (see sweep). Upgrade the debug-only `WarnOnBlocking` (whole-loop type name, 10 ms per poll, Async backend only): name the actor and message type, separate "one poll blocked a worker" from "handler stuck across awaits", optional in release builds. Long handler time alone does not establish deadlock. **Research ([deadlock and stall detection](docs/research/deadlock-and-stall-detection.md)):** three detectors: per-poll timing inside dispatch with actor id and message type (a poll blocking a worker), turn age (a handler stuck across awaits), and an Akka-style scheduling-delay probe per execution group (starvation). Tokio's `tokio_unstable` task hooks are optional behind a feature, not required. |
 | 8a | Cooperative budgets and per-turn work measurement | **Client evidence:** the same incidents as rank 8 (ethrex d958dcba4 filled every runtime worker; ethlambda moved its chain actor to `Backend::Thread`). Spawned cannot preempt Rust code; do what the BEAM does for native code instead. (A) Fairness between messages: an opt-in dispatch policy that yields after N messages or T µs per poll (today's private `MessageTurn` experiment), framework operations that consume Tokio's coop budget, and per-actor work metrics (poll time per message, polls per turn, long polls) feeding ranks 8, 29 and 39. (B) Opt-in `ctx.checkpoint().await` and a budgeted iterator that yield only when the turn is over budget. (C) Synchronous code is detected (rank 8) and isolated (placement, rank 11b), never preempted. Rejected: auto-instrumentation by macro, signal-based preemption. Acceptance: single-CPU starvation bound; watchdog fires on a blocking handler. See [preemption and budgets](docs/research/concurrency-models.md#3-preemption-reduction-counting-and-cooperative-budgets). Per-turn work measurement uses the same instrumentation point as rank 8. |
 | 8b | Simulator check for handlers that never yield | **Implemented** (see [Implemented](#implemented-no-longer-ranked)). Simulator only (`cfg(spawned_sim)`), no production cost: a run fails when one actor turn runs longer than `SPAWNED_SIM_TURN_BUDGET` (default 250 ms of wall-clock time) inside a single poll, naming the actor and message type, so a blocking or spinning handler is caught in tests before production. Wall-clock, not a poll count: a poll cannot be preempted or its work counted, and a self-waking turn already yields ([testing](docs/TESTING.md#seeds-and-decision-tapes-under---cfg-spawned_sim)). Erlang gap: preemption. |
 | 8c | Per-group stack size | Configuration only. A stack size for native and threaded execution groups, so actors with deep recursion get a bigger stack instead of overflowing, which Rust cannot catch. Erlang gap: crash containment. |
-| 9 | Per-actor flight recorder | Last N handled message types and timestamps per actor, dumped on panic, stall or timeout. Bounded and opt-in; a building block for rank 22. **Research ([observability](docs/research/observability.md)):** the minimal record per message is type, enqueue time, start time and outcome, bounded per actor and readable by `spawned-top` (rank 30). |
+| 9 | Per-actor flight recorder | **Deferred to 0.10** by the introspection design (PR #256), to share the event sink and per-turn ring with full `sys:trace` (G9) and rank 5c. Last N handled message types and timestamps per actor, dumped on panic, stall or timeout. Bounded and opt-in; a building block for rank 22. **Research ([observability](docs/research/observability.md)):** the minimal record per message is type, enqueue time, start time and outcome, bounded per actor and readable by `spawned-top` (rank 30). |
 | 10 | Published state snapshots (`Projected<S>`) | **Client evidence:** ethrex actors await read requests to `PeerTableServer` (see results above); its read-only queries are the first use.  Single-writer, many-reader snapshot slot so readers do not wait behind a long handler; replaces the `Arc<RwLock<_>>` escape hatch. Document that a snapshot can lag messages already sent (no read-your-writes). |
 
 ### Step 4: request semantics
@@ -755,7 +762,7 @@ the first start (semantics §11; found reviewing #233). Behaviour change: extend
 | 27 | Process groups, typed topics and routers | After rank 12. Membership cleanup, per-recipient backpressure and partial-failure semantics matter more than a broadcast convenience method. Pools with round-robin, least-busy or key-hash routing (key hash preserves per-key order) belong here. Broadcast can share one payload behind an `Arc` instead of cloning it per member; each mailbox still needs its own queue entry, so this saves payload copies, not per-recipient allocation. Elixir's `PartitionSupervisor` is prior art for key-hash pools ([supervision models](docs/research/supervision-models.md)). |
 | 28 | Causal tracing and ingress context | Preserve span context across awaits/fan-out and bound retention/sampling cost. **Research ([observability](docs/research/observability.md)):** follow the OpenTelemetry messaging conventions: capture the sender's context when a message is queued and carry it in the envelope; link the handler's span to it, and use parent-child only for `request`; sample at ingress. `tracing` spans do not cross a mailbox unless the envelope carries them. |
 | 29 | Bounded role/cohort metrics, oldest age, active monitor counts | Bound cohort/role cardinality and define gauge lifetime; avoid actor-ID label growth. Exact queue age needs a transport contract independent of sampled timing. The Prometheus `_max` exposition bug found by the Ethlambda canary is fixed (maxima are separate gauge families, checked by `scripts/check-metrics-exposition.py` in CI). Next, add what Orleans exposes and Spawned lacks: a long-running-turn counter (fed by rank 8), started/stopped/failed counts per role and oldest-message age ([observability](docs/research/observability.md)). |
-| 30 | Read-only runtime inspection | Safe status/last-known snapshots: id, type, parent/links, mailbox depth, idle/polling/suspended status, current message type, turn age, wait-for edges. Actor state `Debug` only between turns, because the handler future holds `&mut A` across awaits. A concrete first tool: `spawned-top`, an Erlang-observer-style live view that attaches to a running node and lists actors with mailbox depth, state, links and current message. **Research ([observability](docs/research/observability.md)):** take observer's columns and recon's safety rules: never copy a mailbox to inspect it, rank actors over a sliding window rather than totals, rate-limit any tracing, read state only between turns; show rank 7's wait-for edges as `jstack` prints lock cycles. kameo's console TUI is the nearest Rust design to compare against. Optional tokio-console integration (task names and a span per turn via `console-subscriber`, behind `tokio_unstable`) complements `spawned-top` but cannot see Thread or Blocking actors or mailboxes. |
+| 30 | Read-only runtime inspection | **0.9 design in review ([introspection](docs/design/introspection.md), PR #256):** `info()`, snapshots, the `spawned-top` data model and the `spawned-ctl` console over one versioned JSON protocol. Safe status/last-known snapshots: id, type, parent/links, mailbox depth, idle/polling/suspended status, current message type, turn age, wait-for edges. Actor state `Debug` only between turns, because the handler future holds `&mut A` across awaits. A concrete first tool: `spawned-top`, an Erlang-observer-style live view that attaches to a running node and lists actors with mailbox depth, state, links and current message. **Research ([observability](docs/research/observability.md)):** take observer's columns and recon's safety rules: never copy a mailbox to inspect it, rank actors over a sliding window rather than totals, rate-limit any tracing, read state only between turns; show rank 7's wait-for edges as `jstack` prints lock cycles. kameo's console TUI is the nearest Rust design to compare against. Optional tokio-console integration (task names and a span per turn via `console-subscriber`, behind `tokio_unstable`) complements `spawned-top` but cannot see Thread or Blocking actors or mailboxes. |
 | 31 | Handler middleware (Tower-style) | Tracing, rate limits, timeouts, retries and dedup without handler edits; deadlines and tracing could be middleware rather than core special cases. |
 | 32 | State-machine behavior | `gen_statem`-style per-state handlers and timeouts, built on bounded stashing (rank 16). |
 | 33 | Typed streams and demand-driven pipelines | **Client evidence:** unbounded and lag-dropping `spawn_listener` inputs in both clients; promote with credits. After credits. Specify subscription ownership, slow consumers, failure, credit release and bounded completion-watermark windows. Ownership release differs from explicit acknowledgement. Start with one concrete producer/consumer. Reactive Streams' `request(n)` demand is rank 18's credits; build on them rather than a second mechanism ([streams note](docs/research/concurrency-models.md#4-streams-with-backpressure)). |

docs/design/README.md

@@ -19,6 +19,11 @@ 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`.
+- **[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,
+  structured reports, the stall watchdog and the attachable remote console
+  (`spawned-ctl`). Model: `verification/tla/Introspection.tla`.
 
 Earlier designs (the v0.5 API redesign alternatives, the framework comparison
 and superseded roadmap plans) are archived in