Make FreeUnit's state machines bulletproof: FSM contracts + systematic flow/resource audits

[andypost]

Why

Most of this codebase's control flow runs on implicit state machines — state encoded in which handler pointer is installed (nxt_conn_state_t, 25+ instances), in flag combinations (timer enabled/queued/change, h1p bits), or in counter invariants (router nxt_app_t). A code survey found 20 distinct FSMs; only 4 are explicit enums. History shows this is where the bugs live: the chunked-relay proxy fix (nginx#72), the port-IPC reply-path leaks (71fcd89), the CI-only vanishing-headers flake (uninitialized field flags in the resumable parser), and the io_uring engine work's edge-delivery wedges — every one was a missing/undocumented state transition or an ownership gap on an error exit.

The one documentation format with a local track record is docs/io_uring/engine-contract.md (currently on the #31 branch): a code-verified prose contract with per-operation semantics, invariants, and a mismatch inventory — it predicted two real bugs (oneshot accept re-arm, consumed-wakeup readiness loss) before the engine existed. This issue proposes extending that bar to the whole codebase.

Proposal (full plan in the gist)

Plan: https://gist.github.com/andypost/6d47c38db20a977dc5edc62589010b63

Highlights:

• Inventory: 20 FSMs ranked by risk (state storage file:line, explicit vs implicit, transition-site dispersion, resources keyed to each state). High-risk: conn lifecycle + 3-phase teardown, port send/recv + shm chunk bitmaps, h1proto client/peer pairs, process/app lifecycle, timers (deferred-change queue).
• Format: layered — engine-contract-style prose contracts under docs/fsm/ as the normative spine; a machine-readable YAML transition block per doc; Mermaid diagrams generated from the YAML (never hand-drawn); NXT_DEBUG-gated assertions citing invariant IDs as living documentation (later, small PRs); TLA+/spin for exactly two machines — port messaging and conn close/free — where concurrency meets refcounting.
• Audit techniques, ranked by expected bugs-per-effort: transition-completeness audits (every state × event cell gets a verdict — the io_uring wedges were exactly undefined cells); resource-ownership tracing per exit path (the 71fcd89 class); a trace-replay checker that replays debug-build pytest logs against the documented FSM and flags illegal transitions — the only technique that would have caught the CI-only parser flake; targeted fault injection extending the PR SIGSEGV in unit controller process on CentOS 6.9 nginx/unit#57 scaffolding.
• Review gate: every doc independently re-derived from code by a second reviewer and diffed; every claim carries file:line. A doc failing verification is itself a finding.
• Pilots: (A) unified conn lifecycle + fd-event + timer + accept contract; (B) router↔app port messaging incl. shm chunks and the RPC cancel matrix. Acceptance includes retro-predicting the known historical bugs in each area and a zero-illegal-transition replay of a full debug pytest run.

Relationship to other work

• Resource-leak detection at test time (fd/process accounting, orphaned-daemon prevention — the armv7/armhf builder pkill workaround in Alpine's freeunit APKBUILD) is a separate effort planned on PR tools: event-engine A/B benchmark harness (oha + ab) #32; the FSM docs feed it the per-object definition of "leaked" (object exiting in a non-terminal state).
• docs/io_uring/engine-contract.md + design.md (PR io_uring event engine — Stage 2: completion-mode accept, tiers, hardening #31) become the fd-event section's substrate and get cross-linked, not duplicated.

First steps

1. Historical bug corpus: tag past control-flow/resource fixes with their FSM (grounds the risk ranking).
2. Pilot A (docs/fsm/conn.md) + the trace checker.
3. Pilot B (docs/fsm/port-messaging.md), then the TLA+ model transcribed from its verified YAML.

Findings are expected from the first doc onward — writing the transition table is the audit.

[andypost]

Pilot A (connection lifecycle) is done: branch docs/fsm-conn-pilot in this fork, from master eb1767c. src/ is not changed.

• docs/fsm/conn.md (700 lines):
  • 9 states and 20 events;
  • a full 180-cell transition table, generated from the YAML;
  • sub-machines for idle tracking, read, write, timers and accept;
  • 17 invariants (CONN-INV-1…17);
  • resource ownership by resource and for 12 exit paths;
  • a mismatch inventory. Every claim cites file:line.
• docs/fsm/conn.yaml is the machine-readable model. tools/fsm/render.py generates the table and the Mermaid diagram from it.
• tools/fsm/trace_check.py replays debug-build logs against the YAML.
  • A replay of a debug pytest run (header/static/proxy/asgi-websocket, about 2M log lines): 13,027 connections, 0 illegal transitions.
  • A synthetic log with 9 planted violations: all 9 are reported.

Mismatch inventory (candidate bugs, found statically):

• M-1 HIGH. nxt_conn_io_write() (nxt_conn_write.c:30-36) checks block_write before c->write == NULL, then queues write_state->error_handler. nxt_h1p_peer_close_state (nxt_h1proto.c:3374) has no error_handler, and the engine calls the handler without a NULL check (nxt_event_engine.c:545). A write already queued when the peer is closed with block_write would call NULL. The same code is in upstream NGINX Unit. Needs a reproduction.
• M-2 MEDIUM: nxt_conn_close() blocks only the write side; a read that is already queued can run on a closing connection.
• M-3 MEDIUM: nxt_conn_close() is not idempotent, so a second call releases the connection twice. Only a debug assert catches it.
• M-4…M-6 LOW, in accept and listen:
  • a non-accept4 path falls through after a failure;
  • a repeated EPOLL_CTL_DEL on an inactive listener logs an alert every 100 ms;
  • nxt_listen_event() reports success when the spare allocation fails.
• M-9, M-11 LOW: nxt_conn_free() does not assert that the fd is closed; nxt_runtime_close_idle_connections() does not install a release state.
• M-7, M-8, M-10, M-12 INFO: SO_LINGER is never used for HTTP/1, an extra engine cycle per close with epoll, timer bias, and a shared log ident.

Proposed debug-only log lines (P-1…P-6: accept, free, timer identity, tracking, a unique ident, an extended close line). With them the checker could verify what it can only infer today.

Next steps:

• a reproduction test and a fix PR for M-1;
• then M-2/M-3;
• then Pilot B (port messaging).

---

Generated by Claude Code