From bb60e2ff17d652114e6ff52f4c319aa17859c945 Mon Sep 17 00:00:00 2001
From: teo1747 <motsoujunior17@gmail.com>
Date: Fri, 30 Oct 2026 22:42:47 +0100
Subject: [PATCH 1/6] test(m2-10): combined scenarios, a coverage preset and
 the campaign runner

- The COMBINED scenario group meets several mechanisms at section
  boundaries, with ISR and tick placement left to the explorer and the
  bridge:
  - a suspended, canceled and resumed message queue receiver against an
    ISR send;
  - an inheriting owner's priority change against an event wait's timeout
    and an ISR set;
  - a timed take against a give and destroy at the same ticks;
  - one thread bound to a message queue and to event flags;
  - an ISR-context timer feeding a queue a work handler reads while the
    thread flushes and stops it;
  - an ISR cancel racing a delayed item's expiry.
- native-coverage preset: GCC with --coverage at -O0. The native port
  dumps the gcov counters before _exit(), which skips the exit-time
  flush.
- tools/coverage/report.py: kernel statement and branch coverage from
  gcov or llvm-cov gcov, with file exclusions and their reasons.
- tools/model/campaign.py: runs the bridge over runners and seeds plus
  the timer regressions and writes a JSON summary with the build
  identities.

Signed-off-by: teo1747 <motsoujunior17@gmail.com>
---
 CMakePresets.json                      |  22 ++++++
 arch/native/native_port.c              |   7 ++
 cmake/toolchains/native-coverage.cmake |  12 +++
 tools/coverage/exclusions.json         |   1 +
 tools/coverage/report.py               | 105 +++++++++++++++++++++++++
 tools/model/campaign.py                |  75 ++++++++++++++++++
 tools/model/tests/scenarios.py         |  70 +++++++++++++++++
 tools/model/tests/test_explore.py      |  37 +++++++++
 8 files changed, 329 insertions(+)
 create mode 100644 cmake/toolchains/native-coverage.cmake
 create mode 100644 tools/coverage/exclusions.json
 create mode 100644 tools/coverage/report.py
 create mode 100644 tools/model/campaign.py

diff --git a/CMakePresets.json b/CMakePresets.json
index 1669535..412cab4 100644
--- a/CMakePresets.json
+++ b/CMakePresets.json
@@ -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",
@@ -283,6 +294,10 @@
       "name": "native-tsan",
       "configurePreset": "native-tsan"
     },
+    {
+      "name": "native-coverage",
+      "configurePreset": "native-coverage"
+    },
     {
       "name": "avr-uno",
       "configurePreset": "avr-uno"
@@ -402,6 +417,13 @@
         "outputOnFailure": true
       }
     },
+    {
+      "name": "native-coverage",
+      "configurePreset": "native-coverage",
+      "output": {
+        "outputOnFailure": true
+      }
+    },
     {
       "name": "avr-uno",
       "configurePreset": "avr-uno",
diff --git a/arch/native/native_port.c b/arch/native/native_port.c
index e0c0169..92f87e0 100644
--- a/arch/native/native_port.c
+++ b/arch/native/native_port.c
@@ -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);
 }
diff --git a/cmake/toolchains/native-coverage.cmake b/cmake/toolchains/native-coverage.cmake
new file mode 100644
index 0000000..fef142d
--- /dev/null
+++ b/cmake/toolchains/native-coverage.cmake
@@ -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()
diff --git a/tools/coverage/exclusions.json b/tools/coverage/exclusions.json
new file mode 100644
index 0000000..69b685d
--- /dev/null
+++ b/tools/coverage/exclusions.json
@@ -0,0 +1 @@
+{"files": {}}
diff --git a/tools/coverage/report.py b/tools/coverage/report.py
new file mode 100644
index 0000000..daf635f
--- /dev/null
+++ b/tools/coverage/report.py
@@ -0,0 +1,105 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+# Copyright 2026 Junior Deogracias
+"""Statement and branch coverage of the kernel from a gcov-instrumented build (M2-10).
+
+Runs gcov (or `llvm-cov gcov`) on every kernel translation unit of a build made with the
+native-coverage preset after its tests ran, and reports per-file and total line and
+branch coverage. Only kernel .c files count: header inline functions are reported per
+translation unit by gcov and cannot be merged from its summaries. Files listed in the
+exclusions file are reported with their reason and left out of the totals.
+"""
+import argparse
+import json
+from pathlib import Path
+import re
+import shlex
+import subprocess
+import sys
+
+ROOT = Path(__file__).resolve().parents[2]
+BLOCK = re.compile(r"File '([^']+)'\n(?:Lines executed:([\d.]+)% of (\d+)\n)?"
+                   r"(?:Branches executed:[\d.]+% of \d+\nTaken at least once:([\d.]+)% of (\d+)\n)?")
+
+
+def gcov_summary(gcov, gcno):
+    """{source: (lines, lines_hit, branches, branches_taken)} for one translation unit."""
+    out = subprocess.run(gcov + ["-b", "-c", "-n", gcno.name], cwd=gcno.parent, capture_output=True,
+                         text=True)
+    result = {}
+    for m in BLOCK.finditer(out.stdout):
+        src, lpct, lines, bpct, branches = m.groups()
+        lines, branches = int(lines or 0), int(branches or 0)
+        hit = round(float(lpct or 0) * lines / 100)
+        taken = round(float(bpct or 0) * branches / 100)
+        result[str(Path(src).resolve())] = (lines, hit, branches, taken)
+    return result
+
+
+def collect(build, gcov):
+    files = {}
+    for gcno in sorted((build / "kernel").rglob("*.gcno")):
+        for src, counts in gcov_summary(gcov, gcno).items():
+            path = Path(src)
+            if path.suffix != ".c" or not path.is_relative_to(ROOT / "kernel"):
+                continue
+            rel = str(path.relative_to(ROOT))
+            files[rel] = dict(lines=counts[0], lines_hit=counts[1], branches=counts[2],
+                              branches_taken=counts[3], executed=gcno.with_suffix(".gcda").exists())
+    return files
+
+
+def pct(n, d):
+    return 100.0 * n / d if d else 100.0
+
+
+def render(files, exclusions, title):
+    rows = ["| file | lines | branches | note |", "|---|---:|---:|---|"]
+    tl = th = tb = tt = 0
+    for rel, f in sorted(files.items()):
+        note = exclusions.get(rel, "")
+        if not note:
+            tl += f["lines"]
+            th += f["lines_hit"]
+            tb += f["branches"]
+            tt += f["branches_taken"]
+        elif not f["executed"]:
+            note = note or "not executed"
+        rows.append(f"| `{rel}` | {pct(f['lines_hit'], f['lines']):.1f}% of {f['lines']} | "
+                    f"{pct(f['branches_taken'], f['branches']):.1f}% of {f['branches']} | "
+                    f"{'excluded: ' + note if note else ''} |")
+    total = dict(lines=tl, lines_hit=th, branches=tb, branches_taken=tt,
+                 line_pct=round(pct(th, tl), 1), branch_pct=round(pct(tt, tb), 1))
+    md = [f"# {title}", "", f"Kernel statement (line) coverage **{total['line_pct']}%** of {tl} lines; "
+          f"branch coverage (taken at least once) **{total['branch_pct']}%** of {tb} branches, "
+          "over the files not excluded.", ""] + rows + [""]
+    return "\n".join(md), total
+
+
+def main(argv=None):
+    ap = argparse.ArgumentParser(description=__doc__.split("\n\n")[0])
+    ap.add_argument("--build", type=Path, default=ROOT / "build/native-coverage")
+    ap.add_argument("--gcov", default="gcov", help='the gcov command, e.g. "xcrun llvm-cov gcov"')
+    ap.add_argument("--exclusions", type=Path, default=ROOT / "tools/coverage/exclusions.json")
+    ap.add_argument("--json", type=Path)
+    ap.add_argument("--markdown", type=Path)
+    ap.add_argument("--title", default="Kernel coverage")
+    args = ap.parse_args(argv)
+    exclusions = json.loads(args.exclusions.read_text())["files"] if args.exclusions.is_file() else {}
+    files = collect(args.build.resolve(), shlex.split(args.gcov))
+    if not files:
+        print("coverage: no kernel coverage data; build and test the native-coverage preset first",
+              file=sys.stderr)
+        return 2
+    md, total = render(files, exclusions, args.title)
+    if args.json:
+        args.json.write_text(json.dumps(dict(total=total, files=files, exclusions=exclusions), indent=2) + "\n")
+    if args.markdown:
+        args.markdown.write_text(md)
+    print(f"coverage: lines {total['line_pct']}% of {total['lines']}, branches {total['branch_pct']}% "
+          f"of {total['branches']} ({len(files)} kernel files, {len(exclusions)} excluded)")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/tools/model/campaign.py b/tools/model/campaign.py
new file mode 100644
index 0000000..ff4726d
--- /dev/null
+++ b/tools/model/campaign.py
@@ -0,0 +1,75 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+# Copyright 2026 Junior Deogracias
+"""The M2-10 differential campaign: every catalogue scenario on each runner, for a range of
+seeds, plus the exact timer regressions, summarized as JSON.
+
+Each (runner, seed) pair runs `bridge.py --runs N --seed S` as a separate process, so the
+per-seed schedules are the same as a manual run. Failures are captured by the bridge as
+usual (build/differential-failures/); the summary records counts and identities only.
+"""
+import argparse
+from datetime import datetime, timezone
+import hashlib
+import json
+from pathlib import Path
+import re
+import subprocess
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+LINE = re.compile(r"bridge: (\d+)/(\d+) runs agree with the model, (\d+) scenarios skipped on this build, "
+                  r"(\d+) divergences")
+CONFIG = re.compile(r"bridge: runner (profile=\S+ owner_death=\S+ checked=\S+ tickless=\S+)")
+
+
+def bridge(runner, *args, timeout):
+    cmd = [sys.executable, "-I", str(HERE / "bridge.py"), "--runner", str(runner), *map(str, args)]
+    out = subprocess.run(cmd, capture_output=True, text=True, timeout=timeout)
+    m = LINE.search(out.stdout)
+    if m is None:
+        raise RuntimeError(f"no bridge summary from {cmd}: {out.stdout[-500:]} {out.stderr[-500:]}")
+    agree, total, skipped, diverged = map(int, m.groups())
+    c = CONFIG.search(out.stdout)
+    return dict(agree=agree, runs=total, skipped=skipped, divergences=diverged,
+                config=c.group(1) if c else None, exit=out.returncode)
+
+
+def main(argv=None):
+    ap = argparse.ArgumentParser(description=__doc__.split("\n\n")[0])
+    ap.add_argument("--runner", action="append", required=True, type=Path, help="a diff_runner; repeatable")
+    ap.add_argument("--seeds", default="1-10", help="first-last (default 1-10)")
+    ap.add_argument("--runs", type=int, default=40)
+    ap.add_argument("--timeout", type=float, default=7200, help="per bridge process, seconds")
+    ap.add_argument("--out", type=Path, required=True, help="the summary JSON to write")
+    args = ap.parse_args(argv)
+    first, last = (int(x) for x in args.seeds.split("-"))
+    git = subprocess.run(["git", "-C", str(ROOT), "rev-parse", "HEAD"], capture_output=True, text=True).stdout.strip()
+    dirty = bool(subprocess.run(["git", "-C", str(ROOT), "status", "--porcelain", "--untracked-files=no"],
+                                capture_output=True, text=True).stdout.strip())
+    result = dict(schema="emblink-campaign", version=1, started=datetime.now(timezone.utc).isoformat(timespec="seconds"),
+                  git_sha=git, tracked_dirty=dirty, runs_per_scenario=args.runs, seeds=[first, last], runners=[])
+    for runner in args.runner:
+        entry = dict(runner=str(runner.relative_to(ROOT)) if runner.resolve().is_relative_to(ROOT) else str(runner),
+                     runner_sha256=hashlib.sha256(runner.read_bytes()).hexdigest(), seeds={})
+        for seed in range(first, last + 1):
+            entry["seeds"][seed] = bridge(runner, "--runs", args.runs, "--seed", seed, timeout=args.timeout)
+            print(f"campaign: {entry['runner']} seed {seed}: {entry['seeds'][seed]['agree']}/"
+                  f"{entry['seeds'][seed]['runs']}", flush=True)
+        entry["regressions"] = bridge(runner, "--regressions", timeout=args.timeout)
+        entry["config"] = entry["regressions"]["config"]
+        entry["total"] = dict(runs=sum(s["runs"] for s in entry["seeds"].values()),
+                              agree=sum(s["agree"] for s in entry["seeds"].values()),
+                              divergences=sum(s["divergences"] for s in entry["seeds"].values()))
+        result["runners"].append(entry)
+    result["finished"] = datetime.now(timezone.utc).isoformat(timespec="seconds")
+    result["divergences"] = sum(r["total"]["divergences"] + r["regressions"]["divergences"] for r in result["runners"])
+    args.out.parent.mkdir(parents=True, exist_ok=True)
+    args.out.write_text(json.dumps(result, indent=2) + "\n")
+    print(f"campaign: {result['divergences']} divergences in all; summary {args.out}")
+    return 0 if result["divergences"] == 0 else 1
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/tools/model/tests/scenarios.py b/tools/model/tests/scenarios.py
index b09d51d..81b08da 100644
--- a/tools/model/tests/scenarios.py
+++ b/tools/model/tests/scenarios.py
@@ -779,3 +779,73 @@ def dwork_isr_schedule():
 
 DWORK = [dwork_runs_after_its_delay, dwork_reschedule_and_cancel, dwork_isr_schedule]
 ALL = ALL + DWORK
+
+
+# ---------------------------------------------------------------------------------------
+# M2-10: combined scenarios: several mechanisms meeting at section boundaries, with the ISR
+# and tick placement left to the explorer and the bridge
+# ---------------------------------------------------------------------------------------
+
+
+def combined_suspend_cancel_msgq_receiver():
+    """A receiver suspended, canceled and resumed while an ISR's send may hand it the item:
+    it receives the item, or is canceled and the item stays stored, never both or neither."""
+    return Scenario(name="combined_suspend_cancel_msgq_receiver",
+                    threads={1: (3, (MsgRecv(0, 6),)), 2: (2, (Suspend(1), Cancel(1), Resume(1)))},
+                    msgqs={0: dict(capacity=1)},
+                    isrs=((MsgSend(0, 5, NO_WAIT),),))
+
+
+def combined_inheritance_priority_change_event_timeout():
+    """An inheriting owner whose base priority changes while a third thread's event wait races
+    an ISR set and its own timeout."""
+    return Scenario(name="combined_inheritance_priority_change_event_timeout",
+                    threads={1: (1, (Lock(0), Sleep(2), Unlock(0))), 2: (4, (Sleep(1), Lock(0, 3))),
+                             3: (2, (Sleep(1), SetPrio(1, 3), EventWait(0, 0x1, timeout=2)))},
+                    mutexes={0: {}}, events={0: dict(bits=0)},
+                    isrs=((EventSet(0, 0x1),),))
+
+
+def combined_destroy_timeout_and_isr_give():
+    """A timed take whose timeout, another thread's give and the semaphore's destroy meet at the
+    same ticks. (A give after destroy is a stale handle: checked builds fault, so no ISR gives.)"""
+    return Scenario(name="combined_destroy_timeout_and_isr_give",
+                    threads={1: (3, (Take(0, 2),)), 2: (1, (Sleep(2), Destroy(0))), 3: (2, (Sleep(1), Give(0)))},
+                    sems={0: dict(count=0)})
+
+
+def combined_bindings_two_sources():
+    """One thread bound to a message queue and to event flags waits for either; the queue's
+    binding fires on empty to nonempty only, the event's for bits left set."""
+    return Scenario(name="combined_bindings_two_sources",
+                    threads={1: (3, (NotifyWait(0x3, timeout=5), MsgRecv(0, NO_WAIT), NotifyWait(0x3, timeout=3))),
+                             2: (1, (MsgSend(0, 1), EventSet(0, 0x1)))},
+                    msgqs={0: dict(capacity=2, binding=(1, 0))},
+                    events={0: dict(bits=0, binding=(1, 1))})
+
+
+def combined_timer_feeds_handler_queue():
+    """An ISR-context timer sends into a message queue a work handler receives from, while the
+    thread flushes the work queue and stops the timer."""
+    return Scenario(name="combined_timer_feeds_handler_queue",
+                    threads={1: (1, (TimerStart(0, 1), Submit(0, 0), WorkFlush(0), TimerStop(0)))},
+                    msgqs={0: dict(capacity=1)},
+                    workqs={0: dict(tid=9, prio=2)},
+                    works={0: dict(body=(MsgRecv(0, 3),))},
+                    timers={0: dict(isr=True, body=(MsgSend(0, 7, NO_WAIT),))})
+
+
+def combined_dwork_cancel_races_expiry():
+    """An ISR cancels a delayed item at any point around its expiry: it ran once or not at all."""
+    return Scenario(name="combined_dwork_cancel_races_expiry",
+                    threads={1: (1, (DworkSchedule(0, 0, 2), Take(0, 4)))},
+                    sems={0: dict(count=0)},
+                    workqs={0: dict(tid=9, prio=2)},
+                    works={0: dict(body=(Give(0),), delayed=True)},
+                    isrs=((DworkCancel(0),),))
+
+
+COMBINED = [combined_suspend_cancel_msgq_receiver, combined_inheritance_priority_change_event_timeout,
+            combined_destroy_timeout_and_isr_give, combined_bindings_two_sources,
+            combined_timer_feeds_handler_queue, combined_dwork_cancel_races_expiry]
+ALL = ALL + COMBINED
diff --git a/tools/model/tests/test_explore.py b/tools/model/tests/test_explore.py
index 0074466..815eff0 100644
--- a/tools/model/tests/test_explore.py
+++ b/tools/model/tests/test_explore.py
@@ -610,3 +610,40 @@ def test_isr_schedule(self):
         for d, w in self.outcomes(S.dwork_isr_schedule):
             seen.add(d[1][0][1])
         self.assertIn(Result.SATISFIED, seen)
+
+
+class Combined(unittest.TestCase):
+    """M2-10: mechanisms combined at section boundaries. Every invariant of every group holds in
+    every explored state; these tests pin the end results that matter."""
+
+    def test_every_combined_scenario_holds_invariants(self):
+        for make in S.COMBINED:
+            sc = make()
+            with self.subTest(scenario=sc.name):
+                self.assertGreater(explore(sc).terminals, 0)
+
+    def test_suspended_canceled_receiver_gets_the_item_or_leaves_it(self):
+        seen = set()
+        for o in explore(S.combined_suspend_cancel_msgq_receiver()).outcomes:
+            d, q = dict(dict(o)["threads"]), dict(dict(o)["msgqs"])
+            r = d[1][0]
+            seen.add(r[1])
+            if r[1] == Result.SATISFIED:
+                self.assertEqual((r[2], q[0]), (5, ()))
+            else:
+                self.assertIn(r[1], (Result.CANCELED, Result.TIMEOUT))     # the item, if sent, is stored
+        self.assertTrue({Result.SATISFIED, Result.CANCELED} <= seen)
+
+    def test_destroy_timeout_and_give(self):
+        seen = {dict(dict(o)["threads"])[1][0][1] for o in explore(S.combined_destroy_timeout_and_isr_give()).outcomes}
+        self.assertTrue(seen <= {Result.SATISFIED, Result.TIMEOUT, Result.DESTROYED})
+        self.assertIn(Result.SATISFIED, seen)
+
+    def test_dwork_cancel_racing_expiry_runs_at_most_once(self):
+        seen = set()
+        for o in explore(S.combined_dwork_cancel_races_expiry()).outcomes:
+            d, w = dict(dict(o)["threads"]), {wid: n for wid, _, n in dict(o)["works"]}
+            seen.add(w[0])
+            if w[0] == 0:
+                self.assertNotEqual(d[1][1][1], Result.SATISFIED)          # canceled: nothing gave
+        self.assertEqual(seen, {0, 1})

From 77768fb7e3cadcd8a28dea060677b1dd59c16bf2 Mon Sep 17 00:00:00 2001
From: teo1747 <motsoujunior17@gmail.com>
Date: Fri, 30 Oct 2026 22:57:58 +0100
Subject: [PATCH 2/6] fix(sched): raising a ready thread above the running one
 preempts at once

embk_sched_prio_changed() set reschedule_pending only when the running
thread's own effective priority fell below a ready thread. When another
thread raised a ready thread above the caller with
emb_thread_set_priority(), nothing marked the reschedule, and the caller
kept running past its preemption point until its next block or yield.

The M2-10 combined campaign found it: in release builds, where the
scenario's owner-death policy lets the run continue, a raised owner did
not run before the raising thread's next wait. The hook now marks the
reschedule when a ready thread other than the running one rises above
it. The new case sched_raising_a_ready_thread_above_the_caller_preempts
fails on the old kernel (marks 1, 3, 2) and passes now.

Signed-off-by: teo1747 <motsoujunior17@gmail.com>
---
 kernel/sched/sched.c           |  3 +++
 tests/conformance/test_sched.c | 24 ++++++++++++++++++++++++
 2 files changed, 27 insertions(+)

diff --git a/kernel/sched/sched.c b/kernel/sched/sched.c
index 6972922..2d366c0 100644
--- a/kernel/sched/sched.c
+++ b/kernel/sched/sched.c
@@ -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 */
     }
 }
diff --git a/tests/conformance/test_sched.c b/tests/conformance/test_sched.c
index e2d731a..7733db7 100644
--- a/tests/conformance/test_sched.c
+++ b/tests/conformance/test_sched.c
@@ -126,3 +126,27 @@ EMB_TEST(sched_thread_self_and_priorities)
     EMB_ASSERT_EQ(emb_thread_get_effective_priority(me), EMB_TEST_RUNNER_PRIORITY);
     EMB_ASSERT_EQ(emb_context(), EMB_CONTEXT_THREAD);
 }
+
+static emb_thread_t raised;
+
+static void raised_body(void *arg)
+{
+    (void)arg;
+    emb_test_mark(2);
+}
+
+static void raiser(void *arg)
+{
+    (void)arg;
+    raised = emb_test_thread(EMB_TEST_NAME("lo"), 2u, 0u, raised_body, NULL); /* ready, below us */
+    emb_test_mark(1);
+    EMB_ASSERT_OK(emb_thread_set_priority(raised, 4u)); /* now above us: it runs at once */
+    emb_test_mark(3);
+}
+
+EMB_TEST(sched_raising_a_ready_thread_above_the_caller_preempts)
+{
+    EMB_TEST_REQ("KRN-THR-022", "KRN-SYNC-032");
+    (void)emb_test_thread(EMB_TEST_NAME("hi"), 3u, 0u, raiser, NULL);
+    EMB_ASSERT_MARKS(1, 2, 3);
+}

From 617e1dbce89f77d78b6b09714063a3302e94d09c Mon Sep 17 00:00:00 2001
From: teo1747 <motsoujunior17@gmail.com>
Date: Fri, 30 Oct 2026 22:57:58 +0100
Subject: [PATCH 3/6] fix(native): keep registration tables dense under Mach-O
 AddressSanitizer

Clang's AddressSanitizer on Mach-O pads globals in custom sections with
redzones, so walking the test or init table read the padding as
entries. Every conformance suite aborted with a global-buffer-overflow
in the runner, and native-asan could not run on macOS. ELF builds leave
section globals alone, which is why CI passed.

Table entries now carry EMB_TABLE_ENTRY_ATTR: no_sanitize("address")
under Clang with AddressSanitizer, empty everywhere else. native-asan
passes 20/20 locally and the tiny ASan build 17/17.

Signed-off-by: teo1747 <motsoujunior17@gmail.com>
---
 include/emb/compiler.h       |  4 ++++
 include/emb/compiler/clang.h | 25 ++++++++++++++++---------
 include/emb/kernel.h         |  6 +++---
 tests/framework/emb_test.h   | 10 +++++-----
 4 files changed, 28 insertions(+), 17 deletions(-)

diff --git a/include/emb/compiler.h b/include/emb/compiler.h
index 1573066..6effd2f 100644
--- a/include/emb/compiler.h
+++ b/include/emb/compiler.h
@@ -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
diff --git a/include/emb/compiler/clang.h b/include/emb/compiler/clang.h
index ae6aabd..d8dc5ff 100644
--- a/include/emb/compiler/clang.h
+++ b/include/emb/compiler/clang.h
@@ -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))
diff --git a/include/emb/kernel.h b/include/emb/kernel.h
index 0a1442a..c110706 100644
--- a/include/emb/kernel.h
+++ b/include/emb/kernel.h
@@ -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 --------------------------------------------------------------- */
 
diff --git a/tests/framework/emb_test.h b/tests/framework/emb_test.h
index 90a272f..7558856 100644
--- a/tests/framework/emb_test.h
+++ b/tests/framework/emb_test.h
@@ -31,11 +31,11 @@ typedef struct EMB_ALIGNED(sizeof(void *) * 4) emb_test_case {
 } emb_test_case_t;
 
 /* Defines a test and registers it. MISRA Dev CS-12: rule 20.7, `name` is a token. */
-#define EMB_TEST(name)                                                                        \
-    static void name(void);                                                                   \
-    static EMB_FLASH_CONST char name##_name_[] = #name;                                       \
-    static EMB_TABLE_CONST emb_test_case_t name##_case_                                       \
-        EMB_USED EMB_SECTION(EMB_TABLE_SECTION("emb_test_table")) = {name##_name_, name, ""}; \
+#define EMB_TEST(name)                                                                             \
+    static void name(void);                                                                        \
+    static EMB_FLASH_CONST char name##_name_[] = #name;                                            \
+    static EMB_TABLE_CONST emb_test_case_t name##_case_ EMB_USED EMB_TABLE_ENTRY_ATTR EMB_SECTION( \
+        EMB_TABLE_SECTION("emb_test_table")) = {name##_name_, name, ""};                           \
     static void name(void)
 
 /* Requirement citation inside a test body: printed as the case's "req" line. */

From b04cf96f16aad314a429c3637a4cd8ad1f8f5e66 Mon Sep 17 00:00:00 2001
From: teo1747 <motsoujunior17@gmail.com>
Date: Fri, 30 Oct 2026 22:57:58 +0100
Subject: [PATCH 4/6] fix(model): resolve campaign runner paths before naming
 them

Signed-off-by: teo1747 <motsoujunior17@gmail.com>
---
 tools/model/campaign.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tools/model/campaign.py b/tools/model/campaign.py
index ff4726d..3731e8a 100644
--- a/tools/model/campaign.py
+++ b/tools/model/campaign.py
@@ -50,8 +50,8 @@ def main(argv=None):
                                 capture_output=True, text=True).stdout.strip())
     result = dict(schema="emblink-campaign", version=1, started=datetime.now(timezone.utc).isoformat(timespec="seconds"),
                   git_sha=git, tracked_dirty=dirty, runs_per_scenario=args.runs, seeds=[first, last], runners=[])
-    for runner in args.runner:
-        entry = dict(runner=str(runner.relative_to(ROOT)) if runner.resolve().is_relative_to(ROOT) else str(runner),
+    for runner in (r.resolve() for r in args.runner):
+        entry = dict(runner=str(runner.relative_to(ROOT)) if runner.is_relative_to(ROOT) else str(runner),
                      runner_sha256=hashlib.sha256(runner.read_bytes()).hexdigest(), seeds={})
         for seed in range(first, last + 1):
             entry["seeds"][seed] = bridge(runner, "--runs", args.runs, "--seed", seed, timeout=args.timeout)

From f563ef5ca99cda5898bfcfb328d5e84afc8df257 Mon Sep 17 00:00:00 2001
From: teo1747 <motsoujunior17@gmail.com>
Date: Fri, 30 Oct 2026 23:07:47 +0100
Subject: [PATCH 5/6] fix(thread): preempt after a priority raise without
 mutexes too

The previous fix marked the reschedule in the scheduler's priority hook,
which the inheritance recomputation calls. A build without mutexes,
such as the tiny footprint configuration, sets the effective priority
directly and never reaches that hook, so
sched_raising_a_ready_thread_above_the_caller_preempts still failed on
avr-uno-t1. emb_thread_set_priority() now checks the raised thread
against the running one itself.

Signed-off-by: teo1747 <motsoujunior17@gmail.com>
---
 kernel/thread/thread.c | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/kernel/thread/thread.c b/kernel/thread/thread.c
index a21be9e..174a913 100644
--- a/kernel/thread/thread.c
+++ b/kernel/thread/thread.c
@@ -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);

From 2a29b1b120d652a772469428194a935e9e71a376 Mon Sep 17 00:00:00 2001
From: teo1747 <motsoujunior17@gmail.com>
Date: Fri, 30 Oct 2026 23:18:12 +0100
Subject: [PATCH 6/6] docs(m2-10): integrated campaign evidence and report

- tools/model/evidence/m2-10/: the campaign summaries for native gcc,
  clang, periodic, release and tiny (seeds 1-10, --runs 40, plus the
  timer regressions): 158,800 runs, no divergence, clean tree at
  f563ef5. Also the kernel coverage (91.4% of lines, 72.5% of branches,
  nothing excluded) and the requirement-matrix summary over all 21
  configurations.
- docs/engineering/m2-10-campaign.md reports the combined scenarios,
  the two defects the campaign found (the missing preemption on a
  priority raise and the macOS AddressSanitizer table padding), the
  sanitizer results, the lowest-covered files, and the implemented
  requirements verified by analysis rather than by a case.
- CI builds native-coverage, publishes the report and runs the report
  tool's tests. The sanitizer and coverage configurations join the
  evidence catalogue.
- msgq_small_counts_refuse_a_capacity_above_255 gives KRN-IPC-021 an
  executed case.
- The checklist's two campaign items, STATUS and the changelog are
  updated.

Signed-off-by: teo1747 <motsoujunior17@gmail.com>
---
 .github/workflows/ci.yml                      |  13 +-
 CHANGELOG.md                                  |   6 +
 docs/STATUS.md                                |   2 +
 docs/engineering/index.md                     |   1 +
 docs/engineering/m2-10-campaign.md            |  76 +++++++
 docs/engineering/m2-checklist.md              |   4 +-
 tests/conformance/test_msgq.c                 |  16 ++
 tools/coverage/exclusions.json                |   5 +-
 tools/coverage/test_report.py                 |  39 ++++
 tools/evidence/configurations.json            |   3 +
 tools/model/evidence/m2-10/README.md          |   7 +
 .../evidence/m2-10/campaign-native-clang.json | 116 ++++++++++
 .../evidence/m2-10/campaign-native-gcc.json   | 116 ++++++++++
 .../m2-10/campaign-native-periodic.json       | 116 ++++++++++
 .../m2-10/campaign-native-release.json        | 116 ++++++++++
 .../evidence/m2-10/campaign-native-tiny.json  | 116 ++++++++++
 tools/model/evidence/m2-10/coverage.json      | 139 ++++++++++++
 .../model/evidence/m2-10/matrix-summary.json  | 211 ++++++++++++++++++
 18 files changed, 1098 insertions(+), 4 deletions(-)
 create mode 100644 docs/engineering/m2-10-campaign.md
 create mode 100644 tools/coverage/test_report.py
 create mode 100644 tools/model/evidence/m2-10/README.md
 create mode 100644 tools/model/evidence/m2-10/campaign-native-clang.json
 create mode 100644 tools/model/evidence/m2-10/campaign-native-gcc.json
 create mode 100644 tools/model/evidence/m2-10/campaign-native-periodic.json
 create mode 100644 tools/model/evidence/m2-10/campaign-native-release.json
 create mode 100644 tools/model/evidence/m2-10/campaign-native-tiny.json
 create mode 100644 tools/model/evidence/m2-10/coverage.json
 create mode 100644 tools/model/evidence/m2-10/matrix-summary.json

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 38c2c1c..8ee2b9b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -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
@@ -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
@@ -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
diff --git a/CHANGELOG.md b/CHANGELOG.md
index b65cee1..f08e87f 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-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.
@@ -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.
diff --git a/docs/STATUS.md b/docs/STATUS.md
index 8260224..745060a 100644
--- a/docs/STATUS.md
+++ b/docs/STATUS.md
@@ -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.
diff --git a/docs/engineering/index.md b/docs/engineering/index.md
index 78f32ce..ed43fb8 100644
--- a/docs/engineering/index.md
+++ b/docs/engineering/index.md
@@ -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
diff --git a/docs/engineering/m2-10-campaign.md b/docs/engineering/m2-10-campaign.md
new file mode 100644
index 0000000..3217dcc
--- /dev/null
+++ b/docs/engineering/m2-10-campaign.md
@@ -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.
diff --git a/docs/engineering/m2-checklist.md b/docs/engineering/m2-checklist.md
index 5c12bf3..3c72d67 100644
--- a/docs/engineering/m2-checklist.md
+++ b/docs/engineering/m2-checklist.md
@@ -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.
diff --git a/tests/conformance/test_msgq.c b/tests/conformance/test_msgq.c
index d0b765b..3de770a 100644
--- a/tests/conformance/test_msgq.c
+++ b/tests/conformance/test_msgq.c
@@ -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
diff --git a/tools/coverage/exclusions.json b/tools/coverage/exclusions.json
index 69b685d..6af1ca1 100644
--- a/tools/coverage/exclusions.json
+++ b/tools/coverage/exclusions.json
@@ -1 +1,4 @@
-{"files": {}}
+{
+  "_comment": "Kernel files left out of the coverage totals, with the reason (M2-10). Only kernel .c files of the native-coverage build count; files of other profiles (the tiny slim idle context) are not built there. Nothing is excluded: every built kernel file counts.",
+  "files": {}
+}
diff --git a/tools/coverage/test_report.py b/tools/coverage/test_report.py
new file mode 100644
index 0000000..ff29731
--- /dev/null
+++ b/tools/coverage/test_report.py
@@ -0,0 +1,39 @@
+# SPDX-License-Identifier: Apache-2.0
+# Copyright 2026 Junior Deogracias
+"""Unit tests for the coverage report's gcov parsing and totals."""
+import sys
+import unittest
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+import report  # noqa: E402
+
+SAMPLE = """File '/x/kernel/sched/sched.c'
+Lines executed:50.00% of 10
+Branches executed:100.00% of 4
+Taken at least once:75.00% of 4
+No calls
+
+File '/x/kernel/include/embk/list.h'
+Lines executed:100.00% of 3
+No branches
+No calls
+"""
+
+
+class Report(unittest.TestCase):
+    def test_gcov_blocks_parse_lines_and_branches(self):
+        blocks = {m.group(1): m.groups()[1:] for m in report.BLOCK.finditer(SAMPLE)}
+        self.assertEqual(blocks["/x/kernel/sched/sched.c"], ("50.00", "10", "75.00", "4"))
+        self.assertEqual(blocks["/x/kernel/include/embk/list.h"][:2], ("100.00", "3"))
+
+    def test_exclusions_leave_the_totals(self):
+        files = {"kernel/a.c": dict(lines=10, lines_hit=5, branches=4, branches_taken=3, executed=True),
+                 "kernel/b.c": dict(lines=10, lines_hit=0, branches=0, branches_taken=0, executed=False)}
+        md, total = report.render(files, {"kernel/b.c": "tiny profile only"}, "t")
+        self.assertEqual((total["lines"], total["line_pct"], total["branch_pct"]), (10, 50.0, 75.0))
+        self.assertIn("excluded: tiny profile only", md)
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/tools/evidence/configurations.json b/tools/evidence/configurations.json
index 31f881c..9492e4e 100644
--- a/tools/evidence/configurations.json
+++ b/tools/evidence/configurations.json
@@ -6,6 +6,9 @@
     "native-release": {"target": "native", "scope": "host", "profile": "base", "checked": false},
     "native-tiny": {"target": "native", "scope": "host", "profile": "tiny", "checked": true},
     "native-periodic": {"target": "native", "scope": "host", "profile": "base", "checked": true},
+    "native-asan": {"target": "native", "scope": "host", "profile": "base", "checked": true},
+    "native-tsan": {"target": "native", "scope": "host", "profile": "base", "checked": true},
+    "native-coverage": {"target": "native", "scope": "host", "profile": "base", "checked": true},
     "cm3-an385": {"target": "qemu mps2-an385", "scope": "emulated", "profile": "base", "checked": true},
     "cm4-an386": {"target": "qemu mps2-an386", "scope": "emulated", "profile": "base", "checked": true},
     "cm4-an386-release": {"target": "qemu mps2-an386", "scope": "emulated", "profile": "base", "checked": false},
diff --git a/tools/model/evidence/m2-10/README.md b/tools/model/evidence/m2-10/README.md
new file mode 100644
index 0000000..32d4e8c
--- /dev/null
+++ b/tools/model/evidence/m2-10/README.md
@@ -0,0 +1,7 @@
+# M2-10 campaign evidence
+
+- `campaign-<runner>.json`: `tools/model/campaign.py` summaries (seeds 1 to 10, `--runs 40`, plus the timer regressions) with the commit, the tree's cleanliness and each runner's SHA-256.
+- `coverage.json`: `tools/coverage/report.py` over the `native-coverage` build after its CTest run.
+- `matrix-summary.json`: the per-configuration summary of `tools/evidence/matrix.py` over all 21 configurations' case evidence, with the implemented requirements that have no executed case.
+
+The report is `docs/engineering/m2-10-campaign.md`.
diff --git a/tools/model/evidence/m2-10/campaign-native-clang.json b/tools/model/evidence/m2-10/campaign-native-clang.json
new file mode 100644
index 0000000..b35c83a
--- /dev/null
+++ b/tools/model/evidence/m2-10/campaign-native-clang.json
@@ -0,0 +1,116 @@
+{
+  "schema": "emblink-campaign",
+  "version": 1,
+  "started": "2026-10-30T22:14:22+00:00",
+  "git_sha": "f563ef5ca99cda5898bfcfb328d5e84afc8df257",
+  "tracked_dirty": false,
+  "runs_per_scenario": 40,
+  "seeds": [
+    1,
+    10
+  ],
+  "runners": [
+    {
+      "runner": "build/native-clang/tests/differential/diff_runner",
+      "runner_sha256": "ee53d5980b9ba4af4f00ff013d0030f96b59ee7e4a355283fcde950d70dbd66a",
+      "seeds": {
+        "1": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "2": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "3": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "4": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "5": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "6": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "7": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "8": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "9": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "10": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        }
+      },
+      "regressions": {
+        "agree": 5,
+        "runs": 5,
+        "skipped": 0,
+        "divergences": 0,
+        "config": "profile=base owner_death=fault checked=1 tickless=1;",
+        "exit": 0
+      },
+      "config": "profile=base owner_death=fault checked=1 tickless=1;",
+      "total": {
+        "runs": 33600,
+        "agree": 33600,
+        "divergences": 0
+      }
+    }
+  ],
+  "finished": "2026-10-30T22:16:02+00:00",
+  "divergences": 0
+}
diff --git a/tools/model/evidence/m2-10/campaign-native-gcc.json b/tools/model/evidence/m2-10/campaign-native-gcc.json
new file mode 100644
index 0000000..ef71ed7
--- /dev/null
+++ b/tools/model/evidence/m2-10/campaign-native-gcc.json
@@ -0,0 +1,116 @@
+{
+  "schema": "emblink-campaign",
+  "version": 1,
+  "started": "2026-10-30T22:14:22+00:00",
+  "git_sha": "f563ef5ca99cda5898bfcfb328d5e84afc8df257",
+  "tracked_dirty": false,
+  "runs_per_scenario": 40,
+  "seeds": [
+    1,
+    10
+  ],
+  "runners": [
+    {
+      "runner": "build/native-gcc/tests/differential/diff_runner",
+      "runner_sha256": "77dc9f79dce2b6d18a7be3a4bc9c3e2d14e649adf3ebb21d49da37a2ff8039d3",
+      "seeds": {
+        "1": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "2": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "3": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "4": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "5": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "6": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "7": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "8": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "9": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "10": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        }
+      },
+      "regressions": {
+        "agree": 5,
+        "runs": 5,
+        "skipped": 0,
+        "divergences": 0,
+        "config": "profile=base owner_death=fault checked=1 tickless=1;",
+        "exit": 0
+      },
+      "config": "profile=base owner_death=fault checked=1 tickless=1;",
+      "total": {
+        "runs": 33600,
+        "agree": 33600,
+        "divergences": 0
+      }
+    }
+  ],
+  "finished": "2026-10-30T22:16:02+00:00",
+  "divergences": 0
+}
diff --git a/tools/model/evidence/m2-10/campaign-native-periodic.json b/tools/model/evidence/m2-10/campaign-native-periodic.json
new file mode 100644
index 0000000..f27b646
--- /dev/null
+++ b/tools/model/evidence/m2-10/campaign-native-periodic.json
@@ -0,0 +1,116 @@
+{
+  "schema": "emblink-campaign",
+  "version": 1,
+  "started": "2026-10-30T22:14:22+00:00",
+  "git_sha": "f563ef5ca99cda5898bfcfb328d5e84afc8df257",
+  "tracked_dirty": false,
+  "runs_per_scenario": 40,
+  "seeds": [
+    1,
+    10
+  ],
+  "runners": [
+    {
+      "runner": "build/native-periodic/tests/differential/diff_runner",
+      "runner_sha256": "38ea41d27a795fb389e6d72c6c9185e80204c8a196f6a6d92b11991b53a8e09f",
+      "seeds": {
+        "1": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=0;",
+          "exit": 0
+        },
+        "2": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=0;",
+          "exit": 0
+        },
+        "3": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=0;",
+          "exit": 0
+        },
+        "4": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=0;",
+          "exit": 0
+        },
+        "5": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=0;",
+          "exit": 0
+        },
+        "6": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=0;",
+          "exit": 0
+        },
+        "7": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=0;",
+          "exit": 0
+        },
+        "8": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=0;",
+          "exit": 0
+        },
+        "9": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=0;",
+          "exit": 0
+        },
+        "10": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=fault checked=1 tickless=0;",
+          "exit": 0
+        }
+      },
+      "regressions": {
+        "agree": 5,
+        "runs": 5,
+        "skipped": 0,
+        "divergences": 0,
+        "config": "profile=base owner_death=fault checked=1 tickless=0;",
+        "exit": 0
+      },
+      "config": "profile=base owner_death=fault checked=1 tickless=0;",
+      "total": {
+        "runs": 33600,
+        "agree": 33600,
+        "divergences": 0
+      }
+    }
+  ],
+  "finished": "2026-10-30T22:16:02+00:00",
+  "divergences": 0
+}
diff --git a/tools/model/evidence/m2-10/campaign-native-release.json b/tools/model/evidence/m2-10/campaign-native-release.json
new file mode 100644
index 0000000..b1e875a
--- /dev/null
+++ b/tools/model/evidence/m2-10/campaign-native-release.json
@@ -0,0 +1,116 @@
+{
+  "schema": "emblink-campaign",
+  "version": 1,
+  "started": "2026-10-30T22:14:22+00:00",
+  "git_sha": "f563ef5ca99cda5898bfcfb328d5e84afc8df257",
+  "tracked_dirty": false,
+  "runs_per_scenario": 40,
+  "seeds": [
+    1,
+    10
+  ],
+  "runners": [
+    {
+      "runner": "build/native-release/tests/differential/diff_runner",
+      "runner_sha256": "7bb008ceccb4c3d81b41499222cd065755ee103142830156c533117360a3fd60",
+      "seeds": {
+        "1": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=release checked=0 tickless=1;",
+          "exit": 0
+        },
+        "2": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=release checked=0 tickless=1;",
+          "exit": 0
+        },
+        "3": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=release checked=0 tickless=1;",
+          "exit": 0
+        },
+        "4": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=release checked=0 tickless=1;",
+          "exit": 0
+        },
+        "5": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=release checked=0 tickless=1;",
+          "exit": 0
+        },
+        "6": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=release checked=0 tickless=1;",
+          "exit": 0
+        },
+        "7": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=release checked=0 tickless=1;",
+          "exit": 0
+        },
+        "8": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=release checked=0 tickless=1;",
+          "exit": 0
+        },
+        "9": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=release checked=0 tickless=1;",
+          "exit": 0
+        },
+        "10": {
+          "agree": 3360,
+          "runs": 3360,
+          "skipped": 1,
+          "divergences": 0,
+          "config": "profile=base owner_death=release checked=0 tickless=1;",
+          "exit": 0
+        }
+      },
+      "regressions": {
+        "agree": 5,
+        "runs": 5,
+        "skipped": 0,
+        "divergences": 0,
+        "config": "profile=base owner_death=release checked=0 tickless=1;",
+        "exit": 0
+      },
+      "config": "profile=base owner_death=release checked=0 tickless=1;",
+      "total": {
+        "runs": 33600,
+        "agree": 33600,
+        "divergences": 0
+      }
+    }
+  ],
+  "finished": "2026-10-30T22:16:03+00:00",
+  "divergences": 0
+}
diff --git a/tools/model/evidence/m2-10/campaign-native-tiny.json b/tools/model/evidence/m2-10/campaign-native-tiny.json
new file mode 100644
index 0000000..c6a2e5b
--- /dev/null
+++ b/tools/model/evidence/m2-10/campaign-native-tiny.json
@@ -0,0 +1,116 @@
+{
+  "schema": "emblink-campaign",
+  "version": 1,
+  "started": "2026-10-30T22:14:22+00:00",
+  "git_sha": "f563ef5ca99cda5898bfcfb328d5e84afc8df257",
+  "tracked_dirty": false,
+  "runs_per_scenario": 40,
+  "seeds": [
+    1,
+    10
+  ],
+  "runners": [
+    {
+      "runner": "build/native-tiny/tests/differential/diff_runner",
+      "runner_sha256": "eabefa0a305663b524f837add5beafdab83a8dc9a7fb8bb7f08c846c4817e7a7",
+      "seeds": {
+        "1": {
+          "agree": 2440,
+          "runs": 2440,
+          "skipped": 24,
+          "divergences": 0,
+          "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "2": {
+          "agree": 2440,
+          "runs": 2440,
+          "skipped": 24,
+          "divergences": 0,
+          "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "3": {
+          "agree": 2440,
+          "runs": 2440,
+          "skipped": 24,
+          "divergences": 0,
+          "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "4": {
+          "agree": 2440,
+          "runs": 2440,
+          "skipped": 24,
+          "divergences": 0,
+          "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "5": {
+          "agree": 2440,
+          "runs": 2440,
+          "skipped": 24,
+          "divergences": 0,
+          "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "6": {
+          "agree": 2440,
+          "runs": 2440,
+          "skipped": 24,
+          "divergences": 0,
+          "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "7": {
+          "agree": 2440,
+          "runs": 2440,
+          "skipped": 24,
+          "divergences": 0,
+          "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "8": {
+          "agree": 2440,
+          "runs": 2440,
+          "skipped": 24,
+          "divergences": 0,
+          "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "9": {
+          "agree": 2440,
+          "runs": 2440,
+          "skipped": 24,
+          "divergences": 0,
+          "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        },
+        "10": {
+          "agree": 2440,
+          "runs": 2440,
+          "skipped": 24,
+          "divergences": 0,
+          "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+          "exit": 0
+        }
+      },
+      "regressions": {
+        "agree": 4,
+        "runs": 4,
+        "skipped": 1,
+        "divergences": 0,
+        "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+        "exit": 0
+      },
+      "config": "profile=tiny owner_death=fault checked=1 tickless=1;",
+      "total": {
+        "runs": 24400,
+        "agree": 24400,
+        "divergences": 0
+      }
+    }
+  ],
+  "finished": "2026-10-30T22:15:36+00:00",
+  "divergences": 0
+}
diff --git a/tools/model/evidence/m2-10/coverage.json b/tools/model/evidence/m2-10/coverage.json
new file mode 100644
index 0000000..b26f4f4
--- /dev/null
+++ b/tools/model/evidence/m2-10/coverage.json
@@ -0,0 +1,139 @@
+{
+  "total": {
+    "lines": 2900,
+    "lines_hit": 2652,
+    "branches": 1472,
+    "branches_taken": 1067,
+    "line_pct": 91.4,
+    "branch_pct": 72.5
+  },
+  "files": {
+    "kernel/exec/exec.c": {
+      "lines": 108,
+      "lines_hit": 87,
+      "branches": 50,
+      "branches_taken": 32,
+      "executed": true
+    },
+    "kernel/fault/fault.c": {
+      "lines": 38,
+      "lines_hit": 38,
+      "branches": 10,
+      "branches_taken": 9,
+      "executed": true
+    },
+    "kernel/ipc/msgq.c": {
+      "lines": 238,
+      "lines_hit": 220,
+      "branches": 144,
+      "branches_taken": 100,
+      "executed": true
+    },
+    "kernel/irq/irq.c": {
+      "lines": 32,
+      "lines_hit": 21,
+      "branches": 16,
+      "branches_taken": 13,
+      "executed": true
+    },
+    "kernel/notify/notify.c": {
+      "lines": 117,
+      "lines_hit": 111,
+      "branches": 66,
+      "branches_taken": 54,
+      "executed": true
+    },
+    "kernel/sched/sched.c": {
+      "lines": 143,
+      "lines_hit": 135,
+      "branches": 92,
+      "branches_taken": 73,
+      "executed": true
+    },
+    "kernel/sync/cond.c": {
+      "lines": 124,
+      "lines_hit": 113,
+      "branches": 62,
+      "branches_taken": 40,
+      "executed": true
+    },
+    "kernel/sync/event.c": {
+      "lines": 165,
+      "lines_hit": 152,
+      "branches": 92,
+      "branches_taken": 65,
+      "executed": true
+    },
+    "kernel/sync/mutex.c": {
+      "lines": 278,
+      "lines_hit": 242,
+      "branches": 152,
+      "branches_taken": 113,
+      "executed": true
+    },
+    "kernel/sync/sem.c": {
+      "lines": 144,
+      "lines_hit": 139,
+      "branches": 76,
+      "branches_taken": 54,
+      "executed": true
+    },
+    "kernel/thread/thread.c": {
+      "lines": 479,
+      "lines_hit": 442,
+      "branches": 266,
+      "branches_taken": 193,
+      "executed": true
+    },
+    "kernel/time/time.c": {
+      "lines": 197,
+      "lines_hit": 182,
+      "branches": 76,
+      "branches_taken": 64,
+      "executed": true
+    },
+    "kernel/time/timer.c": {
+      "lines": 257,
+      "lines_hit": 241,
+      "branches": 118,
+      "branches_taken": 83,
+      "executed": true
+    },
+    "kernel/trace/trace.c": {
+      "lines": 19,
+      "lines_hit": 19,
+      "branches": 2,
+      "branches_taken": 2,
+      "executed": true
+    },
+    "kernel/wait/wait.c": {
+      "lines": 157,
+      "lines_hit": 147,
+      "branches": 70,
+      "branches_taken": 54,
+      "executed": true
+    },
+    "kernel/work/dwork.c": {
+      "lines": 89,
+      "lines_hit": 79,
+      "branches": 48,
+      "branches_taken": 29,
+      "executed": true
+    },
+    "kernel/work/system_workq.c": {
+      "lines": 10,
+      "lines_hit": 10,
+      "branches": 0,
+      "branches_taken": 0,
+      "executed": true
+    },
+    "kernel/work/workq.c": {
+      "lines": 305,
+      "lines_hit": 274,
+      "branches": 132,
+      "branches_taken": 89,
+      "executed": true
+    }
+  },
+  "exclusions": {}
+}
diff --git a/tools/model/evidence/m2-10/matrix-summary.json b/tools/model/evidence/m2-10/matrix-summary.json
new file mode 100644
index 0000000..3850be8
--- /dev/null
+++ b/tools/model/evidence/m2-10/matrix-summary.json
@@ -0,0 +1,211 @@
+{
+ "summary": {
+  "avr-uno": {
+   "passed": 98,
+   "failed": 0,
+   "skipped": 1,
+   "no assertion": 0,
+   "no case": 278,
+   "not run": 0
+  },
+  "avr-uno-embsim": {
+   "passed": 98,
+   "failed": 0,
+   "skipped": 1,
+   "no assertion": 0,
+   "no case": 278,
+   "not run": 0
+  },
+  "avr-uno-release": {
+   "passed": 99,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 278,
+   "not run": 0
+  },
+  "avr-uno-t1": {
+   "passed": 77,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 300,
+   "not run": 0
+  },
+  "cm3-an385": {
+   "passed": 124,
+   "failed": 0,
+   "skipped": 2,
+   "no assertion": 0,
+   "no case": 251,
+   "not run": 0
+  },
+  "cm4-an386": {
+   "passed": 124,
+   "failed": 0,
+   "skipped": 2,
+   "no assertion": 0,
+   "no case": 251,
+   "not run": 0
+  },
+  "cm4-an386-release": {
+   "passed": 126,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 251,
+   "not run": 0
+  },
+  "cm4-an386-tiny": {
+   "passed": 100,
+   "failed": 0,
+   "skipped": 2,
+   "no assertion": 0,
+   "no case": 275,
+   "not run": 0
+  },
+  "cm4-nucleo-embsim": {
+   "passed": 124,
+   "failed": 0,
+   "skipped": 2,
+   "no assertion": 0,
+   "no case": 251,
+   "not run": 0
+  },
+  "native-asan": {
+   "passed": 124,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 253,
+   "not run": 0
+  },
+  "native-clang": {
+   "passed": 124,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 253,
+   "not run": 0
+  },
+  "native-coverage": {
+   "passed": 124,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 253,
+   "not run": 0
+  },
+  "native-gcc": {
+   "passed": 124,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 253,
+   "not run": 0
+  },
+  "native-periodic": {
+   "passed": 124,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 253,
+   "not run": 0
+  },
+  "native-release": {
+   "passed": 124,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 253,
+   "not run": 0
+  },
+  "native-tiny": {
+   "passed": 101,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 276,
+   "not run": 0
+  },
+  "native-tsan": {
+   "passed": 124,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 253,
+   "not run": 0
+  },
+  "nucleo-f446re-hil": {
+   "passed": 0,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 0,
+   "not run": 377
+  },
+  "rv32-c3-embsim": {
+   "passed": 122,
+   "failed": 0,
+   "skipped": 2,
+   "no assertion": 0,
+   "no case": 253,
+   "not run": 0
+  },
+  "rv32-virt": {
+   "passed": 122,
+   "failed": 0,
+   "skipped": 2,
+   "no assertion": 0,
+   "no case": 253,
+   "not run": 0
+  },
+  "rv32-virt-release": {
+   "passed": 124,
+   "failed": 0,
+   "skipped": 0,
+   "no assertion": 0,
+   "no case": 253,
+   "not run": 0
+  },
+  "rv32-virt-tiny": {
+   "passed": 98,
+   "failed": 0,
+   "skipped": 2,
+   "no assertion": 0,
+   "no case": 277,
+   "not run": 0
+  }
+ },
+ "uncataloged": [
+  "KRN-MEM-009",
+  "KRN-SCH-001",
+  "KRN-SCH-002",
+  "KRN-SCH-003",
+  "KRN-SCH-004",
+  "KRN-SCH-008",
+  "KRN-SCH-009",
+  "KRN-SCH-016",
+  "KRN-SCH-017",
+  "KRN-SCH-018",
+  "KRN-SCH-019",
+  "KRN-SCH-021",
+  "KRN-SCH-041",
+  "KRN-SCH-043"
+ ],
+ "gaps": {
+  "requirements": 377,
+  "passing": 127,
+  "implemented": 39,
+  "implemented_without_case": [
+   "KRN-CAP-013",
+   "KRN-IPC-021",
+   "KRN-IPC-022",
+   "KRN-PART-024",
+   "KRN-PART-025",
+   "KRN-PART-026",
+   "KRN-PART-027",
+   "KRN-WQ-011"
+  ]
+ }
+}
\ No newline at end of file