diff --git a/CHANGELOG.md b/CHANGELOG.md index f08e87f..07ff362 100644 --- a/CHANGELOG.md +++ b/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. diff --git a/docs/STATUS.md b/docs/STATUS.md index 745060a..8f788c5 100644 --- a/docs/STATUS.md +++ b/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. diff --git a/docs/architecture/07-roadmap.md b/docs/architecture/07-roadmap.md index b1da65f..e6c9565 100644 --- a/docs/architecture/07-roadmap.md +++ b/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. diff --git a/docs/engineering/index.md b/docs/engineering/index.md index ed43fb8..7c079cf 100644 --- a/docs/engineering/index.md +++ b/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 diff --git a/docs/engineering/m2-checklist.md b/docs/engineering/m2-checklist.md index 3c72d67..3a8a1ff 100644 --- a/docs/engineering/m2-checklist.md +++ b/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. diff --git a/docs/engineering/m2-exit-review.md b/docs/engineering/m2-exit-review.md new file mode 100644 index 0000000..920f768 --- /dev/null +++ b/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 `` 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 `` | 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. diff --git a/docs/user/configuration.md b/docs/user/configuration.md index 500d830..8dc046b 100644 --- a/docs/user/configuration.md +++ b/docs/user/configuration.md @@ -12,6 +12,7 @@ The configuration pipeline resolves Kconfig defaults seeded by a port manifest, | `native-periodic` | GCC, checked base with a periodic clock for timer/wait validation | | `native-clang` | Clang compiler coverage; requires Clang | | `native-asan` / `native-tsan` | Sanitizer configurations; require supported compiler runtimes | +| `native-coverage` | GCC `--coverage` build; after CTest, `tools/coverage/report.py` prints kernel statement and branch coverage | Use the same preset name for configure, build and CTest. A tiny result does not verify base-only features; a release result does not exercise checked-build faults. Embedded presets additionally require their cross-compiler, libc and emulator; do not interpret a build with no registered tests as conformance. @@ -19,6 +20,21 @@ Onboarding validated the first three GCC presets in this cloud machine. Clang/sa The later [timer-delivery validation](../engineering/m2-01-timer-correction.md) also exercised `native-periodic` and added exact timer-boundary regressions to every applicable native CTest build. Its recorded outcomes distinguish periodic and tickless runs. +## Kernel object options + +| Option | Default | Notes | +|---|---|---| +| `CONFIG_EMB_EVENT`, `CONFIG_EMB_EVENT_BITS` | y; 32 bits (8 on tiny) | event flags | +| `CONFIG_EMB_COND` | y (n on tiny) | condition variables; needs `CONFIG_EMB_MUTEX` | +| `CONFIG_EMB_MSGQ`, `CONFIG_EMB_MSGQ_MAX_ITEM` | y; 64 bytes (16 on tiny) | message queues; the item bound limits the copy made with interrupts masked | +| `CONFIG_EMB_IPC_SMALL` | n (y on tiny) | 8-bit queue counts, at most 255 items | +| `CONFIG_EMB_WORKQ` | y | work queues and, with timers, delayed work; not available with the tiny profile's table scheduler | +| `CONFIG_EMB_SYSTEM_WORKQ`, `_PRIO`, `_STACK` | y; 0 (second-highest priority); 2048 bytes | the system work queue, linked only when `emb_workq_system()` is referenced | +| `CONFIG_EMB_TIMER` | y | software timers; not available with the table scheduler | +| `CONFIG_EMB_OBJ_LIST` | y (n on tiny) | exact refusal of init on live storage | + +The tiny `footprint_t1` reference configuration turns event flags and message queues off. + ## Add diagnostic options without changing the reference preset Activate native tools, then configure a separate ignored build directory. `EMB_SET` uses Kconfig names without the generated `CONFIG_` prefix; quote the semicolon-separated list so the shell passes one argument: