Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 12 additions & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ jobs:
strategy:
fail-fast: false
matrix:
preset: [native-gcc, native-clang, native-release, native-tiny, native-periodic, native-asan, native-tsan]
preset: [native-gcc, native-clang, native-release, native-tiny, native-periodic, native-asan, native-tsan, native-coverage]
steps:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
- name: Install tools
Expand All @@ -39,6 +39,15 @@ jobs:
run: cmake --build --preset ${{ matrix.preset }}
- name: Test
run: ctest --preset ${{ matrix.preset }} --output-on-failure --no-tests=error
- name: Coverage report
if: matrix.preset == 'native-coverage'
run: python3 -I tools/coverage/report.py --json coverage.json --markdown coverage.md && cat coverage.md >> "$GITHUB_STEP_SUMMARY"
- name: Upload coverage
if: matrix.preset == 'native-coverage'
uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2
with:
name: coverage
path: coverage.*
- name: Collect case evidence
if: always()
run: python3 -I tools/evidence/collect.py --build build/${{ matrix.preset }} --preset ${{ matrix.preset }} --out case-evidence-${{ matrix.preset }}.json
Expand Down Expand Up @@ -228,6 +237,8 @@ jobs:
run: python3 -I -m unittest discover -s tools/footprint -p 'test_*.py' -v
- name: Case evidence tools
run: python3 -I -m unittest discover -s tools/evidence -p 'test_*.py' -v
- name: Coverage report tool tests
run: python3 -I -m unittest discover -s tools/coverage -p 'test_*.py' -v
- name: Resource-bound inventory covers every non-constant cost
run: python3 -I tools/evidence/check_bounds.py
- name: Configuration tool self-check
Expand Down
6 changes: 6 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ User-visible changes are recorded here. There are no released versions or releas

### Added

- 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.

- Software timers (`CONFIG_EMB_TIMER`, `include/emb/timer.h`, M2-09): one-shot and periodic timers whose callbacks run on a named work queue or, with `EMB_TIMER_ISR_CONTEXT`, in the expiry interrupt. Periodic timers re-arm from the previous deadline, skip missed periods in closed form and count them with coalesced callbacks as overruns; `stop` reports the callback's state and `stop_sync` waits for it. Timers have their own deadline list, merged with thread timeouts at expiry (ADR-047). The reference model, the differential bridge and a conformance suite cover them; they require the list scheduler, so the tiny profile has none in this milestone.
Expand Down Expand Up @@ -73,6 +75,10 @@ User-visible changes are recorded here. There are no released versions or releas

### Fixed

- Raising a ready thread's priority above the running thread with `emb_thread_set_priority()` now preempts at once; before, the caller ran on until its next block or yield (found by the M2-10 campaign).

- The conformance suites run under AddressSanitizer on macOS: registration-table entries no longer get Mach-O redzones that the table walk read as entries.

- Thread diagnostic IDs remain stable across priority changes on tiny and unique among live objects on every profile. IDs are released only by successful destroy; exhaustion returns `EMB_ENOMEM` without partial construction.

- Generic IRQ priorities now increase with urgency on Cortex-M, with board-derived bounds and validation before register writes; fixed-level native/AVR/RV32 reject nonzero levels. SysTick defaults to highest kernel-aware urgency. Raw kernel-independent vectors remain unsupported.
Expand Down
22 changes: 22 additions & 0 deletions CMakePresets.json
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,17 @@
"EMB_PROFILE": "base"
}
},
{
"name": "native-coverage",
"displayName": "native, GCC, gcov coverage, checked",
"generator": "Ninja",
"binaryDir": "${sourceDir}/build/native-coverage",
"toolchainFile": "${sourceDir}/cmake/toolchains/native-coverage.cmake",
"cacheVariables": {
"EMB_BOARD": "native",
"EMB_PROFILE": "base"
}
},
{
"name": "avr-uno",
"displayName": "Arduino Uno, avr-gcc, tiny profile, checked",
Expand Down Expand Up @@ -283,6 +294,10 @@
"name": "native-tsan",
"configurePreset": "native-tsan"
},
{
"name": "native-coverage",
"configurePreset": "native-coverage"
},
{
"name": "avr-uno",
"configurePreset": "avr-uno"
Expand Down Expand Up @@ -402,6 +417,13 @@
"outputOnFailure": true
}
},
{
"name": "native-coverage",
"configurePreset": "native-coverage",
"output": {
"outputOnFailure": true
}
},
{
"name": "avr-uno",
"configurePreset": "avr-uno",
Expand Down
7 changes: 7 additions & 0 deletions arch/native/native_port.c
Original file line number Diff line number Diff line change
Expand Up @@ -565,8 +565,15 @@ void emb_arch_breakpoint(void)
{
}

#ifdef EMB_NATIVE_COVERAGE
void __gcov_dump(void); /* the gcov runtime: _exit() skips its exit-time flush */
#endif

void emb_native_exit(int code)
{
(void)fflush(NULL);
#ifdef EMB_NATIVE_COVERAGE
__gcov_dump();
#endif
_exit(code);
}
12 changes: 12 additions & 0 deletions cmake/toolchains/native-coverage.cmake
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
# SPDX-License-Identifier: Apache-2.0
# Copyright 2026 Junior Deogracias
# Host build with gcov instrumentation for statement and branch coverage (M2-10);
# tools/coverage/report.py turns the counters into the report.
set(CMAKE_C_COMPILER gcc)
set(EMB_TOOLCHAIN_C_FLAGS -pthread -g -O0 --coverage)
set(EMB_TOOLCHAIN_LINK_FLAGS -pthread --coverage)
set(EMB_TOOLCHAIN_DEFINES _POSIX_C_SOURCE=200809L _DEFAULT_SOURCE EMB_NATIVE_COVERAGE=1)

if(APPLE)
list(APPEND EMB_TOOLCHAIN_LINK_FLAGS -Wl,-no_warn_duplicate_libraries)
endif()
2 changes: 2 additions & 0 deletions docs/STATUS.md
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,8 @@ An API or path named in a design or a requirement's verification field may be a

## Validation recorded in this workspace

The [M2-10 integrated campaign](engineering/m2-10-campaign.md), source `f563ef5`, passed 158,800 differential runs across seeds 1–10 on native checked/clang/periodic/release/tiny with no divergence; all 21 local configurations (native, sanitizers, coverage, QEMU, AVR, EmbSIM) passed; kernel coverage was 91.4% of lines and 72.5% of branches. Hardware-in-the-loop and physical timing remain unrun.

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.
Expand Down
1 change: 1 addition & 0 deletions docs/engineering/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ m2-02-irq-priority
m2-02-thread-identity
m2-02-fault-api-ids
m2-02-object-lifecycle
m2-10-campaign
case-evidence
resource-bounds
embcc-capability-review
Expand Down
76 changes: 76 additions & 0 deletions docs/engineering/m2-10-campaign.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
# M2-10 integrated campaign

**Date:** 2026-10-30. **Kernel at:** `f563ef5` (campaign) and `f563ef5` plus this report (coverage, matrix). **Scope:** every M2 primitive on every native configuration, the emulated targets, sanitizers and coverage. Hardware-in-the-loop and physical timing remain unrun: no NUCLEO-F446RE board was available.

## Combined scenarios

The `COMBINED` group of the reference model (`tools/model/tests/scenarios.py`) meets several mechanisms at section boundaries. The model explores every ISR and tick placement; the differential bridge replays seeded placements on the kernel:

| Scenario | What meets |
|---|---|
| `combined_suspend_cancel_msgq_receiver` | a suspended, canceled and resumed message queue receiver against an ISR send (capacity 1) |
| `combined_inheritance_priority_change_event_timeout` | an inheriting owner's base-priority change against another thread's event wait, its timeout and an ISR set |
| `combined_destroy_timeout_and_isr_give` | a timed take against a give and the semaphore's destroy at the same ticks |
| `combined_bindings_two_sources` | one thread bound to a message queue and to event flags |
| `combined_timer_feeds_handler_queue` | an ISR-context timer feeding a queue that a work handler reads, while the thread flushes the work queue and stops the timer |
| `combined_dwork_cancel_races_expiry` | an ISR cancel racing a delayed item's expiry |

Every invariant of every group holds in every explored state (122 model tests, `cd tools/model && python3 -m pytest`).

## Differential campaign

`tools/model/campaign.py` ran the whole catalogue with `--runs 40` for seeds 1 to 10, plus the exact timer regressions, on five native runners (summaries in `tools/model/evidence/m2-10/campaign-*.json`, clean tree at `f563ef5`):

| Runner | Configuration | Runs | Agree | Regressions |
|---|---|---:|---:|---:|
| native-gcc | base, checked, tickless | 33,600 | 33,600 | 5/5 |
| native-clang | base, checked, tickless | 33,600 | 33,600 | 5/5 |
| native-periodic | base, checked, periodic | 33,600 | 33,600 | 5/5 |
| native-release | base, release, owner death releases | 33,600 | 33,600 | 5/5 |
| native-tiny | tiny, checked (no work queues, timers or condition variables) | 24,400 | 24,400 | 4/4 |

158,800 runs, no divergence. Mutation checks during M2-07 to M2-09 confirmed that the bridge catches deliberately broken message queues, work queues, timers and delayed work.

## Defects the campaign found

- **A raised ready thread did not preempt.** `emb_thread_set_priority()` raising a ready thread above the caller left the caller running until its next block or yield: the scheduler hook marked a reschedule only when the running thread's own priority fell. The combined inheritance scenario diverged in release builds, where its owner-death policy lets the run continue. Fixed in the hook and, for builds without mutexes, in `emb_thread_set_priority()`; `sched_raising_a_ready_thread_above_the_caller_preempts` fails on the old kernel and passes on every target now.
- **AddressSanitizer could not run the suites on macOS.** Clang pads Mach-O section globals with redzones, so the test and init table walks read padding as entries. Table entries now opt out (`EMB_TABLE_ENTRY_ATTR`); `native-asan` passes 20/20 locally, as it already did on CI's Linux runners.

Earlier M2 campaigns found the work queue flush deadline (M2-08, now a timer regression) and the RISC-V reset-section collision (M2-09).

## Sanitizers

| Build | Result |
|---|---|
| native-asan (AddressSanitizer + UBSan) | 20/20 |
| native-tsan (ThreadSanitizer) | 20/20 |
| tiny AddressSanitizer build | 17/17 |

## Coverage

`native-coverage` (GCC `--coverage`, `-O0`, checked) after its full CTest run, which includes the differential bridge, measured with `tools/coverage/report.py` (CI runs the same; `tools/model/evidence/m2-10/coverage.json`): **91.4%** of 2,900 kernel lines and **72.5%** of 1,472 branches taken, over all 18 kernel files of the base build; nothing is excluded. Header inline functions are counted in the files that include them. The lowest files and why:

| File | Lines | Branches | Not reached |
|---|---:|---:|---|
| `kernel/irq/irq.c` | 21/32 | 13/16 | connect and priority paths the native port does not use |
| `kernel/exec/exec.c` | 87/108 | 32/50 | early-start failure and port-specific paths |
| `kernel/work/dwork.c` | 79/89 | 29/48 | misuse arguments and the cancel-between-expiry-and-submit window |
| `kernel/sync/mutex.c` | 242/278 | 113/152 | depth-limit and rare ceiling/recursion branches |

Misuse faults are covered where checked builds fork to observe them; release-build misuse returns are covered by the release presets' suites, which this coverage build does not measure.

## Case evidence and gaps

The requirement matrix (`tools/evidence/matrix.py` over the case evidence of all 21 configurations, `tools/model/evidence/m2-10/matrix-summary.json`) has no failed case. Of 377 catalogued requirements, 127 have a passing executed case; 39 are marked implemented in their cards. The implemented ones without an executed case are verified by analysis or by the model, as their cards say:

- KRN-IPC-022 (model coverage before the queue implementation): analysis.
- KRN-WQ-011 (work queue trace and statistics): trace records exist, statistics do not; no trace decoder test.

KRN-IPC-021 gained `msgq_small_counts_refuse_a_capacity_above_255` in this campaign. Fourteen cited KRN-SCH and KRN-MEM IDs still belong to requirement groups pending migration into the catalogue.

## Not covered

- Hardware-in-the-loop, physical timing, masked-time and jitter measurements (no board).
- Work queues, software timers, delayed work and condition variables on the tiny profile, which has none in M2.
- The EmbCC native flow, which CI does not build.
- Seed-5 of M2-01 stays closed as not reproducible.
4 changes: 2 additions & 2 deletions docs/engineering/m2-checklist.md
Original file line number Diff line number Diff line change
Expand Up @@ -85,8 +85,8 @@ For each new public API: complete annotations and parameter/lifetime docs, gener

## M2-10 and M2-11: Integrated exit

- [ ] Combine timeout, cancel, suspend, destroy, hand-off, priority change and callback delivery at section boundaries, with boundary resource counts and adversarial IRQ/tick placement.
- [ ] Execute applicable misuse/property/sanitizer campaigns and report statement/branch coverage with exclusions and actual case identity.
- [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.
Expand Down
4 changes: 4 additions & 0 deletions include/emb/compiler.h
Original file line number Diff line number Diff line change
Expand Up @@ -144,6 +144,10 @@ extern "C" {
/* A registration-table entry: placed by its section name alone, never by a
* program-memory attribute (which overrides the section on GCC for AVR). */
#define EMB_TABLE_CONST const
/* What a table entry needs so that its section stays a dense array (sanitizers). */
#ifndef EMB_TABLE_ENTRY_ATTR
#define EMB_TABLE_ENTRY_ATTR
#endif

/* The bounds of a bracketed registration table (09 §7): declare once per file with
* EMB_TABLE_BOUNDS, read with EMB_TABLE_START and EMB_TABLE_STOP. The fallback is the
Expand Down
25 changes: 16 additions & 9 deletions include/emb/compiler/clang.h
Original file line number Diff line number Diff line change
Expand Up @@ -13,15 +13,22 @@
((__clang_major__ * 10000) + (__clang_minor__ * 100) + __clang_patchlevel__)

/* NOLINTBEGIN(portability-no-assembler,hicpp-no-assembler): CS-1.5, the compiler layer */
#define EMB_INLINE inline
#define EMB_ALWAYS_INLINE inline __attribute__((always_inline))
#define EMB_NOINLINE __attribute__((noinline))
#define EMB_NORETURN __attribute__((noreturn))
#define EMB_UNUSED __attribute__((unused))
#define EMB_USED __attribute__((used))
#define EMB_WEAK __attribute__((weak))
#define EMB_ALIAS(sym) __attribute__((alias(#sym)))
#define EMB_SECTION(name) __attribute__((section(name)))
#define EMB_INLINE inline
#define EMB_ALWAYS_INLINE inline __attribute__((always_inline))
#define EMB_NOINLINE __attribute__((noinline))
#define EMB_NORETURN __attribute__((noreturn))
#define EMB_UNUSED __attribute__((unused))
#define EMB_USED __attribute__((used))
#define EMB_WEAK __attribute__((weak))
#define EMB_ALIAS(sym) __attribute__((alias(#sym)))
#define EMB_SECTION(name) __attribute__((section(name)))
#if defined(__has_feature)
#if __has_feature(address_sanitizer)
/* Mach-O AddressSanitizer pads section globals with redzones, which a table walk would
* read as entries; ELF builds leave section globals alone. */
#define EMB_TABLE_ENTRY_ATTR __attribute__((no_sanitize("address")))
#endif
#endif
#define EMB_ALIGNED(n) __attribute__((aligned(n)))
#define EMB_PACKED __attribute__((packed))
#define EMB_NAKED __attribute__((naked))
Expand Down
6 changes: 3 additions & 3 deletions include/emb/kernel.h
Original file line number Diff line number Diff line change
Expand Up @@ -62,9 +62,9 @@ typedef struct EMB_ALIGNED(sizeof(void *)) emb_init_entry {
/* Registers @fn to run from emb_kernel_init(). The table is the bracketed section
* emb_init_table that embld and GNU ld both provide (09 §7). MISRA Dev CS-12: rule
* 20.7, `fn` is a token. */
#define EMB_INIT_TABLE_ENTRY(fn) \
static EMB_TABLE_CONST emb_init_entry_t fn##_init_entry_ EMB_USED EMB_SECTION( \
EMB_TABLE_SECTION("emb_init_table")) = {fn}
#define EMB_INIT_TABLE_ENTRY(fn) \
static EMB_TABLE_CONST emb_init_entry_t fn##_init_entry_ EMB_USED EMB_TABLE_ENTRY_ATTR \
EMB_SECTION(EMB_TABLE_SECTION("emb_init_table")) = {fn}

/* ---- EMB_CHECK --------------------------------------------------------------- */

Expand Down
3 changes: 3 additions & 0 deletions kernel/sched/sched.c
Original file line number Diff line number Diff line change
Expand Up @@ -343,5 +343,8 @@ void embk_sched_prio_changed(embk_thread_t *t, uint8_t old_eff)
if (top != NULL && top->eff_prio > t->eff_prio) {
embk_cpu.reschedule_pending = 1u;
}
} else if (embk_cpu.current != NULL && t->eff_prio > embk_cpu.current->eff_prio &&
embk_sched_is_ready(t)) {
embk_cpu.reschedule_pending = 1u; /* a ready thread raised above the running one */
}
}
4 changes: 4 additions & 0 deletions kernel/thread/thread.c
Original file line number Diff line number Diff line change
Expand Up @@ -625,6 +625,10 @@ emb_status_t emb_thread_set_priority(emb_thread_t thread, uint8_t priority)
t->base_prio = priority;
#endif
embk_prio_propagate(t);
if (t != embk_cpu.current && embk_sched_is_ready(t) &&
t->eff_prio > embk_cpu.current->eff_prio) {
embk_cpu.reschedule_pending = 1u; /* also where no recomputation runs (tiny, no mutexes) */
}
EMBK_TRACE(EMB_TRACE_PRIORITY, embk_thread_index(t), t->base_prio, t->eff_prio);
embk_sched_reschedule_if_needed();
embk_unlock_sched(key);
Expand Down
16 changes: 16 additions & 0 deletions tests/conformance/test_msgq.c
Original file line number Diff line number Diff line change
Expand Up @@ -294,3 +294,19 @@ EMB_TEST(msgq_storage_reuse_requires_destroy)
EMB_ASSERT_OK(emb_msgq_destroy(mq));
}
#endif

#if CONFIG_EMB_IPC_SMALL
EMB_TEST(msgq_small_counts_refuse_a_capacity_above_255)
{
static EMB_MSGQ_RING(big_ring, 1u, 1u);
emb_msgq_attr_t attr;
emb_msgq_t q;
EMB_TEST_REQ("KRN-IPC-021");
emb_msgq_attr_default(&attr);
attr.ring = big_ring;
attr.ring_size = 256u; /* claimed: the capacity check comes first */
attr.item_size = 1u;
attr.capacity = 256u;
EMB_ASSERT_MISUSE(emb_msgq_init(&storage, &attr, &q), EMB_EINVAL); /* 8-bit counts (A45) */
}
#endif
Loading