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.

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 determines release eligibility. Timing and evidence defines how a claim becomes substantiated. Port pages explain implementation details and historical measurements.

Implemented subset

Area	Current implementation	Evidence and limits
Execution and scheduling	UP fixed priority, base bitmap/FIFO scheduler, tiny thread table, scheduler lock, thread lifecycle	Common conformance cases; tiny has unique base priorities and restricted scheduling semantics
Waiting and time	Shared wait protocol, sleep, deadlines, cancellation, suspend overlay, ordered timeouts	Native virtual time exercises periodic and tickless modes; embedded ports currently reject tickless
Synchronization	Semaphores, mutexes with inheritance, ceiling, recursion and owner-death policy	Conformance and native differential bridge; inheritance and deadlock detection have a configured depth limit
Notifications	Per-thread bits and one semaphore-to-thread binding	Binding takes a one-bit mask; no unbind implementation; pointer lifetime remains caller responsibility
Objects	Caller-owned generated storage and POINTER handles	No INDEXED or TABLE handles, capability rights, partition restart or system freeze implementation
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 machine mode; boards Arduino Uno, NUCLEO-F446RE, QEMU’s MPS2 and RV32 virt	QEMU jobs and EmbSIM jobs (Uno, NUCLEO-F446RE) 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
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, 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

Event flags, condition variables, barriers, software timers, work queues, message queues, 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; executed-case requirement traceability/coverage reports and support matrix; 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.

Validation recorded in this workspace

The onboarding runs on the baseline used GCC 14.2.0, Python 3.12.14, CMake 3.31.10 and Ninja 1.13.0 on Linux. native-gcc, native-release, and native-tiny each passed ten CTest targets, including nine conformance executables and the differential bridge. Those are runner targets, not ten individual assertions. The base checked run reported 82 internal conformance cases with zero skips, and 210/210 bridge runs agreed with the model with one scenario excluded for that configuration. Counts for other configurations must be read from their own logs.

The reference model passed 44 pytest tests with Hypothesis installed. The banned-construct check reported zero findings. Configuration generation for native/base passed. A repeat setup run reused build outputs and passed. These are current-workspace observations, not archived release artifacts or evidence of a new machine, compiler matrix, physical board, or published environment.

The M2-01 timer correction, source ca0ed3f, subsequently passed 53 model tests, eleven CTest targets on each of native checked/release/tiny/periodic, sixteen exact live regression inputs and 11,200 unfiltered deep-campaign runs with zero divergences. Its source/build/configuration identities and outputs are archived separately from the original failing captures. The corrected model accepts all seven original archived traces; production kernel and architecture sources are unchanged.

The differential evidence workflow, source 8d7bca4, adds automatic failure/probe bundles, offline/live replay and bounded confirmed schedule reduction, including full resolved-configuration checks independent of checkout paths. It passed 67 model/tooling tests, twelve CTest targets per checked/release/tiny/periodic native configuration and another 11,200 deep-campaign runs with zero divergences. Its workflow checks deliberately create search-budget failures to validate capture/replay, and keep those separate from actual kernel evidence. Native CI is configured to retain default failure bundles on failed jobs.

The bounded seed-5 triage, current source 37887c9, subsequently passed 56,000 unfiltered executions across seeds 1–10 on those four presets, with the existing applicability exclusions. Rebuilding the source that first recorded the report reproduced the expected old seed-3 mismatch (1399/1400 agree) and passed 4,200 seed-5 runs on checked/release/tiny. This retains the historical cancellation finding as unconfirmed with unknown cause, not fixed. Commands, bounds, source/build/configuration identities, logs and exact current cancellation schedules are archived separately.

The EmbCC review, compiler source a3c3ef4 and RTOS source 2e59c2a, confirms upstream implementation of the ten former compiler gaps within their stated restrictions. Ten focused local checks passed; AVR linking/program-memory fixtures and small RV32/AVR atomic values executed under EmbSim. No local QEMU, board, live-debug, CMSE-crossing or complete EmbCC RTOS conformance run is claimed. The host compiler bootstrap required local flags and was not warning-clean. Linux executable configure lacked a built target runtime; compile-only configure succeeded but the RTOS storage probe failed on the missing EmbCC EMB_LAYOUT_MARKER. Upstream PR #119 reports RTOS experiments with an injected marker, recorded separately from current CI qualification.

CI definitions versus outcomes

.github/workflows/ci.yml defines native GCC/Clang, release/tiny/periodic, ASan/UBSan and TSan jobs; Cortex-M, RV32 and AVR cross-GCC/QEMU jobs; the AVR and Cortex-M conformance suites on EmbSIM’s Uno and NUCLEO-F446RE; formatting, banned-construct and configuration checks; model tests; and AVR footprint gates. A job definition is not a successful run. Link immutable run results and artifacts before advertising a target/version as supported or validated.

On 2026-10-14, GitHub reported the complete pre-workflow-preparation matrix successful for merged source efff40cc2dbf803a56bab5c3fc844b78a4837f9f: CI run, docs build and Pages deployment. The configured site URL is https://emblinkos.github.io/EmbLinkRTOS/. These are observed workflow/job outcomes, not individual requirement coverage or physical hardware qualification; the new stable checks need their own PR results.

On the same date, the manual Documentation build and Pages deployment succeeded for reviewed main source 37887c9e92e2242ff4d11cfa58c6972fce4b0e0e. An HTTP 200 request to the served evidence-workflow page confirmed that snapshot’s content. This later publication includes the correction/capture tooling, not this subsequent unmerged triage/contract-review documentation. GitHub’s effective branch-rules API also reported the three strict required checks (CI merge gate, Documentation build, Repository policy), PRs with zero required approvals, resolved review conversations, and blocked deletion/non-fast-forward updates on main. Observing settings is distinct from testing a rejected push.

The later main publication succeeded for 2e59c2a37b36c90e5f15892fb258c8a2e21be306, and the served M2-02 contract-review page returned HTTP 200 with its expected content. This publishes the merged seed-5 triage/contract proposals, before the present EmbCC review update.

The repository preparation adds a stable CI merge gate depending on all of those matrix/lint jobs, rejects empty CTest runs, and selects Bash with pipeline failure propagation for footprint commands. Documentation build names the strict docs check and Repository policy checks matching author DCO trailers on non-merge commits. The repository workflow describes the exact scope, limitations and additive main ruleset policy; GitHub settings must be activated and verified separately. Local validation used actionlint 1.7.7, parsed the issue forms/policy, exercised success/failure/skip/cancellation/empty dependency outcomes, and checked DCO rejection/acceptance with an actual temporary Git range. These checks do not establish remote CI or live branch enforcement.

Generated requirement coverage, coverage percentages, clang-tidy/cppcheck gates, include-boundary checks, double-build reproducibility, fuzzing and HIL are not currently CI gates. The roadmap must deliver them for the released scope rather than assume the engineering-system target description is already enforced.

The separate documentation toolchain is installed in .venv-docs with a checksummed Doxygen 1.15.0 binary under build/tools/. Its local HTML build extracts 361 design requirements and 82 current API functions. All extracted functions have eight contract tags and parameter descriptions; their declared requirement IDs resolve in the normative catalog. The strict build rejects omissions and unresolved IDs. This is extraction/documentation evidence, not API semantic compliance or test coverage. A related requirement can describe more than the implemented subset. The documentation integrity suite checks malformed/duplicate/empty catalogs, annotation omissions and wrapped contract fields, and keeps design acceptance separate from execution evidence.

The user-guide pass also configured native/base with stack statistics and two TLS slots in a separate native-inspect build; all ten CTest targets passed. Both complete tutorial programs were compiled with strict C11 warnings and run with the documented expected output and zero exit status against checked base, release, tiny and this diagnostic configuration. The diagnostic callback fragment compiled as C11, and all three fragments compiled as C++17 against native/base headers. These are local tutorial/configuration checks; they add no physical-board or universal API-coverage claim.

Known limits and unresolved evidence

The EmbCC layout-marker correction, source 3578006, supplies the portability macro; storage/assertion/kernel-archive compilation passed on eight configurations. The subsequent Linux native integration, source df32ec2, adds explicit experimental EmbCC-kernel/GCC-host presets and a build-time layout guard. Actual checked/release/tiny/periodic mixed builds passed all twelve CTest targets each and 11,200 seeded model comparisons in total, with zero divergences. GCC compiles the POSIX port, board, applications and harness and links the real Linux runtime; this is not an all-EmbCC host build. The latter still fails on glibc header compatibility after an explicit system-header/link experiment. Compiler CI currently checks the marker/launcher contracts and the existing matrix; the EmbCC executions are scoped local evidence.

• Hardware timing and total memory use remain to be demonstrated on the primary Cortex-M board. Map-derived kernel subtotals exclude port, board, runtime and stack costs.

• The Cortex-M base TCB figures in the port page exceed R-003 T4’s target; that is a disclosed target miss, not a failed native setup.

• The M2-01 timer correction addresses the reproduced seed-3 model timing gap, and the evidence workflow provides automatic bundles, exact replay and bounded schedule reduction. The bounded triage leaves the historical seed-5 cancellation finding unconfirmed without its original schedule/build. Passing current campaigns does not establish the historical cause or close all of M2-01.

• AVR launch/restore uses out SREG; pop r0; ret; pending IRQ coherence during that tail remains a physical validation obligation (A27), not a verified atomic out/ret pair.

• Embedded fault-expectation cases that require host fork are skipped. A passing emulator job does not establish those misuse paths on hardware.

• emb_irq_set_level() does not yet implement KRN-IRQ-028’s generic priority convention consistently: Cortex-M maps zero to the most urgent kernel-aware level and larger values toward lower urgency; native, AVR and current RV32 ignore the requested level. Header comments and the debugging guide disclose this implementation gap; no priority-programming code was changed during documentation work.

• Tiny uses its current base-priority table slot as emb_thread_index(), so reprioritization changes that diagnostic index. KRN-THR-025’s stable-index target is not met across that operation. Generic fault records also leave api_id at zero; retained crash records and full API attribution remain incomplete.

• Base diagnostic-index allocation saturates at 0xFD, so uniqueness is not established across repeated initialization; current init paths also lack general active-storage double-init detection. The M2-02 review records these source-analysis findings and proposals, without changing accepted contracts or claiming new runtime tests.

• The former ten-item EmbCC compiler backlog is implemented upstream and the RTOS layout marker is supplied. An explicit mixed Linux native strategy now executes the kernel; all-EmbCC POSIX host compatibility, AVR flash/registration macros and compiler-matrix CI/qualification remain open. Available CMSE, atomics, DWARF and embedded C++ retain their documented scope and restrictions; see the capability review and marker correction.

• Planned isolation must meet SPEC-010’s DMA, pointer lifetime, generation and restart obligations before fault containment is claimed. CPU protection alone is insufficient.

Updating this page

Record source revision, configuration, tool versions, runner results, individual cases, skips and artifacts together. Move a feature from specified to implemented after inspecting the code; call a requirement verified only after its named evidence passes for the applicable profile. Do not infer universal coverage from one representative configuration. Preserve historical port measurements with their original toolchain and feature set.