docs(m2-11): M2 exit review

CHANGELOG.md

@@ -16,6 +16,8 @@ User-visible changes are recorded here. There are no released versions or releas
 
 ### Added
 
+- The M2 exit review (`docs/engineering/m2-exit-review.md`): every checklist item with its pull requests and evidence, the reconciliation of APIs, configuration, model and requirements, the defects found, and the remaining M3a hardware work.
+
 - The M2-10 integrated campaign: combined model scenarios across primitives, a `native-coverage` preset with `tools/coverage/report.py` (statement and branch coverage, run in CI), and `tools/model/campaign.py`, whose 158,800-run summaries are archived under `tools/model/evidence/m2-10/` (see `docs/engineering/m2-10-campaign.md`).
 
 - Delayed work (`emb_dwork_t`, M2-09, KRN-WQ-003/007): an item that an internal interrupt-context timer submits to a work queue after a delay or at an instant, with idempotent schedule, reschedule, cancel reporting a stopped delay or removed item as pending, and `cancel_sync`. The queue cannot be destroyed while a delay names it. The reference model, the differential bridge and the work queue conformance suite cover it.

docs/STATUS.md

@@ -1,6 +1,6 @@
 # Project status and evidence
 
-**Reviewed:** 2026-10-14 against implementation baseline `f0f3afb473a61ebf02a47a9106cf9690f98ece2e`, the documentation foundation merged in `eea5b5d`, and the subsequent user-guide/API-comment review. This inventory is maintained manually until evidence tooling exists. It is not a generated support matrix.
+**Reviewed:** 2026-10-30 at the [M2 exit review](engineering/m2-exit-review.md), against the M2 branch stack ending in `docs/m2-11-exit`; previously 2026-10-14 against baseline `f0f3afb473a61ebf02a47a9106cf9690f98ece2e`. This inventory is maintained manually; the [requirement matrix](engineering/case-evidence.md) generated from executed cases complements it and is not a published support matrix.
 
 This page is the authoritative inventory of implementation and available evidence. Specifications define target contracts; their acceptance dates do not mean that all described APIs exist. The [roadmap](architecture/07-roadmap.md) determines release eligibility. [Timing and evidence](engineering/timing-and-evidence.md) defines how a claim becomes substantiated. Port pages explain implementation details and historical measurements.
 
@@ -14,19 +14,19 @@ This page is the authoritative inventory of implementation and available evidenc
 | Communication | Copy-by-value message queues: direct hand-off to a waiting receiver, slot hand-off from a waiting sender, send to front, peek, `EMB_NO_WAIT` calls from ISRs and a receive-side binding (M2-07) | Conformance and native differential bridge; no pipes, buffer pools or zero-copy ownership queues; the masked copy time is bounded by configuration, not measured on hardware |
 | Software timers | One-shot and drift-free periodic timers in their own deadline list (ADR-047), with callbacks on a work queue or in interrupt context, closed-form catch-up and overrun counts, stop states and `stop_sync` (M2-09) | Conformance and native differential bridge; list scheduler only (not tiny); arming overhead and jitter not measured on hardware |
 | Deferred work | Work queues on a kernel thread with FIFO execution, idempotent and ISR-safe submit, resubmission while running, cancel and synchronous cancel, flush, destroy joining the thread, a system queue linked only when referenced (M2-08, ADR-048), and delayed work items over internal timers (M2-09) | Conformance and native differential bridge; list scheduler only (not tiny); no statistics |
-| Notifications | Per-thread bits and one semaphore-to-thread binding, with unbind; a bound thread cannot be destroyed (ADR-046) | Binding takes a one-bit mask; other objects' bindings arrive with those objects; restart generations need the isolated profile |
-| Objects | Caller-owned generated storage and POINTER handles; per-type active-object lists for semaphores and mutexes (`CONFIG_EMB_OBJ_LIST`) used by init | No INDEXED or TABLE handles, capability rights, partition restart, system freeze, `emb_obj_foreach()` or debug-descriptor export |
+| Notifications | Per-thread bits; bindings from semaphores, event flags and message queues to a thread, with unbind; a bound thread cannot be destroyed (ADR-046) | Binding takes a one-bit mask; pipes and pools do not exist to bind; restart generations need the isolated profile |
+| Objects | Caller-owned generated storage and POINTER handles; per-type active-object lists for every handle object type (`CONFIG_EMB_OBJ_LIST`) used by init to refuse live storage (ADR-045) | No INDEXED or TABLE handles, capability rights, partition restart, system freeze, `emb_obj_foreach()` or debug-descriptor export |
 | Native port | POSIX host-thread gate, deterministic IRQ injection, virtual time | Base/tiny development workflow; no current wall-clock, asynchronous signal stress, simulated isolated profile or Win32 backend |
 | Embedded ports | ATmega328P; Cortex-M3/M4F; RV32IMAC and RV32IMC machine mode; boards Arduino Uno, NUCLEO-F446RE, ESP32-C3-DevKitM-1, QEMU's MPS2 and RV32 virt | QEMU jobs and EmbSIM jobs (Uno, NUCLEO-F446RE, ESP32-C3-DevKitM-1) defined in CI; no real-board timing or peripheral/HIL validation recorded here |
 | Configuration/build | Kconfig subset, port manifests, CMake/Ninja, layout probe, footprint tool | GCC/Clang native CI and cross-GCC QEMU jobs; ten legacy EmbCC capabilities reviewed with scoped local checks, but current RTOS compiler CI/qualification remains incomplete |
-| Observability | M1 trace sink and fault reporting | CTF rings/metadata, deferred log decoder, retained crash records, debug descriptor and worst-case monitors remain planned |
+| Observability | M1 trace sink and fault reporting; trace records for every outcome of the M2 waits and for queue, work and timer events (IDs 31 to 44) | CTF rings/metadata, deferred log decoder, retained crash records, debug descriptor and worst-case monitors remain planned |
 | Documentation | Sphinx/MyST manuals and native tutorials, Doxygen/Breathe C API, Sphinx Needs design catalog, JSON/CSV downloads and annotation audit | Strict local HTML build, complete extracted function annotations, source-preservation and catalog-integrity checks; merged `37887c9` Pages deployment and served evidence-workflow page independently observed successful |
 | Repository process | Issue forms, PR checklist, changelog, release/M2 work checklists, stable CI merge checks, authored-commit DCO checker and a main ruleset policy | Local syntax and DCO/gate failure checks; GitHub's effective main rules report PRs, resolved conversations, the three strict CI checks and deletion/non-fast-forward protection; no remote rejection experiment claimed |
-| Semantic model | UP scheduler/wait/mutex/notification/lifecycle scenarios; message queues, modeled before their implementation (KRN-IPC-022), work queues and software timers; exhaustive section-level exploration and randomized walks | Scenario-scoped exploration, not a proof of all C execution, arbitrary programs, SMP or hardware protection |
+| Semantic model | UP scheduler/wait/mutex/notification/lifecycle scenarios; binding lifetime, event flags, condition variables, message queues (modeled before their implementation, KRN-IPC-022), work queues, software timers, delayed work and combined scenarios; exhaustive section-level exploration and randomized walks | Scenario-scoped exploration, not a proof of all C execution, arbitrary programs, SMP or hardware protection |
 
 ## Specified but unimplemented
 
-Barriers, pipes and buffer pools; indexed handles and capability tables; static partitions, syscall marshallers and supervisor restart; execution budgets and partition shares; full SoC/board/system schema validation and generation; reusable driver classes; power management; boot/update services; full observability formats; statement/branch coverage reports and the support matrix (executed-case requirement traceability exists, see [case evidence](engineering/case-evidence.md)); fuzz/HIL campaigns; SMP/AMP ports and transports.
+Barriers, pipes and buffer pools; indexed handles and capability tables; static partitions, syscall marshallers and supervisor restart; execution budgets and partition shares; full SoC/board/system schema validation and generation; reusable driver classes; power management; boot/update services; full observability formats; a published support matrix (executed-case requirement traceability and kernel statement/branch coverage exist, see [case evidence](engineering/case-evidence.md) and the [M2-10 campaign](engineering/m2-10-campaign.md)); fuzz/HIL campaigns; SMP/AMP ports and transports.
 
 An API or path named in a design or a requirement's verification field may be a planned deliverable. Check this inventory and the filesystem before treating it as available.
 

docs/architecture/07-roadmap.md

@@ -33,7 +33,7 @@ Continue native and emulator regression testing. Preserve AVR as the tiny-profil
 
 The [ordered M2 checklist](../engineering/m2-checklist.md) sequences the known-failure investigations, contract/lifecycle decisions, primitives and evidence review into scoped implementation work. Checklist items are plans, not executed requirement evidence.
 
-Open work: event flags, condition variables, work queues, software timers, message queues; defined binding teardown/lifetime; applicable object lifecycle/freeze behavior; misuse/property campaigns; generated traceability for the implemented core. Pipes, pools, barriers and INDEXED handles have separate feature gates if not needed by the reference application. TABLE handles belong to M3b.
+Delivered for review (2026-10-30, [M2 exit review](../engineering/m2-exit-review.md)): event flags, condition variables, copy-by-value message queues, work queues, software timers and delayed work; binding teardown and lifetime; object storage-reuse refusal; the integrated misuse/property/sanitizer/coverage campaign and executed-case traceability. Not in M2: system freeze, pipes, pools, barriers and INDEXED handles (separate feature gates if not needed by the reference application); work queues, timers and condition variables on the tiny profile. TABLE handles belong to M3b.
 
 Extend model scenarios and conformance with each primitive, including timeout/cancel/destroy races, ownership conservation and boundary resource counts. Diagnose/minimize the deep replay cases before declaring a campaign clean. Reconcile public annotations with actual complexity and implement the complete resource-bound inventory.
 

docs/engineering/index.md

@@ -19,6 +19,7 @@ m2-02-thread-identity
 m2-02-fault-api-ids
 m2-02-object-lifecycle
 m2-10-campaign
+m2-exit-review
 case-evidence
 resource-bounds
 embcc-capability-review

docs/engineering/m2-checklist.md

@@ -87,8 +87,8 @@ For each new public API: complete annotations and parameter/lifetime docs, gener
 
 - [x] Combine timeout, cancel, suspend, destroy, hand-off, priority change and callback delivery at section boundaries, with boundary resource counts and adversarial IRQ/tick placement.
 - [x] Execute applicable misuse/property/sanitizer campaigns and report statement/branch coverage with exclusions and actual case identity. See the [M2-10 campaign report](m2-10-campaign.md).
-- [ ] Reconcile every delivered API's docs, configuration, model, current complexity and implemented requirement scope.
-- [ ] Require green current CI plus the scoped individual evidence; no unexplained required failure and no unsupported feature advertised as working.
-- [ ] Update STATUS, Unreleased changelog and tutorials, then record the M2 exit review and remaining M3a hardware/release work.
+- [x] Reconcile every delivered API's docs, configuration, model, current complexity and implemented requirement scope. See the [M2 exit review](m2-exit-review.md).
+- [x] Require green current CI plus the scoped individual evidence; no unexplained required failure and no unsupported feature advertised as working. CI state is recorded in the [exit review](m2-exit-review.md).
+- [x] Update STATUS, Unreleased changelog and tutorials, then record the M2 exit review and remaining M3a hardware/release work.
 
 Barriers, pipes, buffer pools and INDEXED handles have separate feature gates unless the reference application's agreed scope requires them. TABLE capabilities, partitions/restart, budgets, SMP/AMP and a full driver platform remain later gates. Completing M2 is not a 1.0 release or hardware-support qualification; use the [release checklist](releases.md) when that stage is reached.

docs/engineering/m2-exit-review.md

@@ -0,0 +1,57 @@
+# M2 exit review
+
+**Date:** 2026-10-30. **Delivered as:** the stacked pull requests #21 to #39 (one logical change each, every one with its own validation), awaiting the project owner's review and merge. **Not done:** anything that needs the NUCLEO-F446RE board.
+
+## Checklist items
+
+| Item | Delivered | Pull requests | Evidence |
+|---|---|---|---|
+| M2-01 known failures | Seed 5 closed as not reproducible (maintainer decision 2026-10-27), with reopen triggers | #23 | [seed-5 triage](m2-01-seed5-triage.md), [timing and evidence](timing-and-evidence.md) |
+| M2-02 contracts and lifecycle | Live-storage refusal for every object type (ADR-045), contract corrections A29 to A33, tiny RAM headroom (slim idle ADR-050, thread table and fault-hook savings), clean IDE diagnostics | #21, #22, #24, #25, #26, #27 | [object lifecycle](m2-02-object-lifecycle.md); T1 39 bytes of RAM, TCB 32 |
+| M2-03 binding lifetime | Unbind, a bound thread outlives its bindings (ADR-046) | #28 | KRN-NOTIF-013, -014; BINDING model group |
+| M2-04 evidence | Individual case evidence and the requirement matrix; the resource-bound inventory and its check | #29, #30 | [case evidence](case-evidence.md), [resource bounds](resource-bounds.md) (16 bounds, 59 functions) |
+| M2-05 event flags | ANY/ALL/CLEAR, deterministic consumption, binding | #31 | `test_event`, EVENT group |
+| M2-06 condition variables | Atomic release, mandatory non-cancelable relock | #32 | `test_cond`, COND group |
+| M2-07 message queues | Model first (#33), then copy-by-value queues with hand-off both ways | #33, #34 | `test_msgq`, MSGQ group |
+| M2-08 work queues | Kernel-thread queues, system queue linked only when used (ADR-048) | #35 | `test_workq`, WORKQ group |
+| M2-09 software timers | Own deadline list (ADR-047), drift-free periodic, closed-form catch-up, delayed work | #36, #37 | `test_timer`, TIMER and DWORK groups |
+| M2-10 integrated campaign | Combined scenarios, 158,800-run campaign, sanitizers, coverage | #38 | [M2-10 campaign](m2-10-campaign.md) |
+| M2-11 exit review | This review, STATUS, roadmap, configuration guide | #39 | this page |
+
+## Reconciliation
+
+- **Public API.** Every function in `include/emb/` has the complete annotation set (the docs annotation audit passes) and a registered API ID (142 IDs; `tools/fault/generate.py --check`). Each new header is reachable from `<emb/emb.h>` under its `CONFIG_` symbol.
+- **Complexity.** Every non-constant `@time` annotation maps to the resource-bound inventory (`tools/evidence/check_bounds.py`: 16 bounds cover 59 functions).
+- **Configuration.** Each primitive has a Kconfig symbol, a documented default per profile ([configuration](../user/configuration.md)) and, where it is off on tiny, a dependency or a `footprint-t1.conf` line. The T1 reference image stays at 4,056 bytes of kernel text, 39 bytes of kernel RAM and a 32-byte control block on AVR.
+- **Model.** Every delivered primitive has a model group and is followed by the differential bridge: 122 model tests, the catalogue on five native runners.
+- **Requirements.** The cards of the delivered requirements say "implemented" with their executed cases; the two implemented ones without a case (KRN-IPC-022, KRN-WQ-011) say what verifies them instead.
+- **Contract changes.** Amendments A29 to A61 ([M2 amendments](../specs/AMENDMENTS-M2.md)) and ADR-045 to ADR-048 and ADR-050 record every deviation from the accepted specifications. They are implemented for review: the project owner may still revise them.
+
+## Defects found during M2
+
+| Defect | Found by | Fixed in |
+|---|---|---|
+| A work queue flush computed its deadline after a tick could advance the clock in its first section | seeded bridge campaign | #35, plus a timer regression |
+| The EmbCC native ABI probe lacked `<embk/ipc.h>` | inspection while adding work queues | #34 |
+| A C function named `reset` could take the RISC-V reset vector's place | a conformance hang on rv32-virt | #36 |
+| Raising a ready thread above the caller did not preempt | the M2-10 combined campaign | #38 |
+| AddressSanitizer suites could not run on macOS | the M2-10 sanitizer leg | #38 |
+
+## CI
+
+At this review, #21 to #39 pass every required check, including the new `native-coverage` job. Three jobs that had hung in their tool installation until GitHub's six-hour limit (on #32, #34 and #35) were re-run and passed. No required check fails unexplained.
+
+## Limits carried out of M2
+
+- **Hardware.** No physical-board run, HIL, masked-time, jitter or latency measurement; arming-overhead compensation is unmeasured.
+- **Tiny profile.** No work queues, timers, delayed work or condition variables (maintainer decision for timers, 2026-10-27).
+- **Not built.** No pipes, buffer pools, ownership queues, barriers, statistics, system freeze, or INDEXED or TABLE handles.
+- **Toolchains.** The EmbCC native flow is not built in CI. The local docs build uses a Doxygen version shim: CI's pinned Doxygen is authoritative.
+
+## Remaining M3a work
+
+1. Bring up the NUCLEO-F446RE: run the existing suites on the board, enable kernel-aware IRQ and timer behavior on real hardware, and record the first HIL runner.
+2. Measure the masked copy time of a maximum-size message, timer arming overhead and jitter, and work queue latency (KRN-IPC-011, KRN-TIM-006, KRN-WQ-011).
+3. Retained crash records and their decoder, trace and debug metadata (SPEC-015).
+4. The hardware description generator with one SoC and two boards.
+5. Decide, with the project owner, on the amendments and ADRs of M2 before any API is marked stable.