# Specification amendments recorded during M1

Implementation found the points below where the code departs from, or sharpens, an accepted specification. The affected specifications now include the contract corrections from this table (reconciliation 2026-10-14); this page retains the historical audit trail and implementation locations. The status page identifies unimplemented target designs. New documentation corrections A23 to A28 are recorded below (05 §6: a semantics change updates the specification, the model, and the suite together).

Compiler restrictions in this historical record, including A20's typedef-alignment premise, refer to the then-reviewed EmbCC snapshot. The [current capability review](../engineering/embcc-capability-review.md) supersedes those compiler premises; the storage-member alignment correction itself remains necessary.

| # | Specification | Amendment | Where in the code |
|---|---|---|---|
| A1 | SPEC-001 §7.3 | Compile-time detection of a constant that overflows the tick type is not provided by the `EMB_MS()` family: it needs a compiler-specific construct, and the generic forms must stay valid C11 and C++17. Saturation applies to constants as to runtime values; `emb_duration_is_saturated()` reports it. | `include/emb/time.h` |
| A2 | SPEC-003 §5.2, KRN-TIM-022 | In the 32-bit profile a `_until` deadline more than `EMB_TIMEOUT_MAX_TICKS` ahead is indistinguishable from a past instant and takes the past-deadline path (yield, `EMB_OK`); `EMB_EOVERFLOW` is unreachable there and the requirement is restated as: the finite-timeout forms clamp at `2^31 - 1` ticks. `emb_instant_add()` wraps in the 32-bit profile (the instant space is circular) and saturates in the 64-bit profile (SPEC-001 §7.3). | `kernel/thread/thread.c`, `kernel/time/time.c` |
| A3 | SPEC-011 §4 | `emb_arch_kernel_start(first, idle)` receives the first thread and the idle context instead of a bare stack pointer, so a port without an idle thread turns the pre-kernel stack into the idle context's stack itself (SPEC-012 §3). | `include/emb/arch.h` |
| A4 | SPEC-011 §5 | Two additions to the context contract: `emb_arch_switch_final(next)`, the exiting thread's last switch (no save); and `embk_thread_launch(entry, arg)`, the kernel's launch hook that every initial frame enters (it starts the fresh context's kernel state, calls `entry(arg)`, and exits the thread with code 0). `emb_arch_context_init` therefore takes no exit function. | `include/emb/arch.h`, `kernel/thread/thread.c` |
| A5 | SPEC-011 §6, SPEC-002 §6.2 | `embk_isr_exit()` returns the context to resume, never NULL: the running thread when the decision did not change. A port may exchange unconditionally (the AVR epilogue has no branch and no label) or compare with its own current. | `kernel/exec/exec.c`, `arch/avr/include/emb_arch.h`, `arch/native/native_port.c` |
| A6 | SPEC-012 §4.1, §4.2 | The saved frame is 35 bytes (return address 2, r0, SREG, r1, r2 to r31); the manifest's 37 keeps two bytes for the call into the switch routine. The initial frame returns into `embk_thread_launch` with `entry` in r24:r25 and `arg` in r22:r23; no separate exit address is pushed. | `arch/avr/avr_context.c` |
| A7 | SPEC-012 §4.4 | The `EMB_ISR` epilogue ends with `ret`, not `reti`: the restored SREG carries the resumed context's own I bit, and `reti` would enable interrupts inside a switched-to thread's critical section. The interrupted context's saved SREG has I forced set (`set; bld r0, 7`), so interrupts re-enable for it with the one-instruction delay. | `arch/avr/include/emb_arch.h` |
| A8 | SPEC-012 §8, HW-006 | GCC for AVR lets the `progmem` attribute override an explicit section, so registration-table entries are declared `EMB_TABLE_CONST` (plain `const` plus the section `.progmem.<name>`), read with `EMB_FLASH_READ_*`, and bracketed by the board's linker script. The script is hand-derived from the toolchain's avr5 script in M1 and generated from M3. | `include/emb/compiler.h`, `boards/arduino/arduino_uno/arduino_uno.ld` |
| A9 | SPEC-002 §4.1, SPEC-011 §3 | `emb_irq_key_t` is defined by the port: `uint8_t` on AVR (the saved SREG), `unsigned int` elsewhere. | `arch/*/include/emb_arch.h` |
| A10 | SPEC-004 §2.1 | `wait_object` is not stored: the object is recovered from `wait_queue` through the queue's flags (`EMBK_WAIT_INHERIT` names a mutex). In checked builds the control block also records the critical-section depth of the switched-out context (`lock_depth`), restored by the scheduler at every switch, because that depth belongs to the context and not to the CPU. | `kernel/include/embk/kernel.h`, `kernel/sched/sched.c` |
| A11 | SPEC-002 §12, 03 §10.2 | `CONFIG_EMB_FAULT_WHERE` selects whether the faulting function's name is recorded; off on the tiny profile, where the strings would cost RAM on avr-gcc. | `kernel/Kconfig` |
| A12 | SPEC-013 §5, §12 | Kernel-aware handlers on the native port are static functions bound with `emb_irq_connect()`; `EMB_ISR(name)` declares one. The conformance suite reaches software interrupts through the test framework's slot layer, which on AVR is the USART data-register-empty interrupt. | `arch/native/include/emb_arch.h`, `tests/framework/` |
| A13 | SPEC-001 §8 | `kernel.h` (kernel init and start, the initialization table, `EMB_CHECK`) and `trace.h` (the trace sink of the M1 subset) are added to the public header list; `arch.h` holds the port contract and is not public API. | `include/emb/` |
| A14 | SPEC-012 §5, SIM-002 | QEMU takes a pending interrupt after `sei` or `out SREG` only when it returns to its main loop (a translation-block chain break), not one instruction later as the hardware does. The unlock stays `out SREG, key`; the test framework's `emb_test_irq_settle()` re-asserts the pending source after an unlock so that a conformance test can assert the order of events on the emulator too. | `tests/framework/platform_avr.c`, `tests/conformance/test_irq.c` |
| A15 | SPEC-004 §8, SPEC-003 §5.1 | The timeout node carries no wait generation on the uniprocessor kernel: a timeout is disarmed in the same critical section that ends the wait, so an expiry never meets a finished wait. The thread's `wait_gen` stays; the SMP form (SPEC-004 §8) adds the in-flight generation to the node. On the tiny profile the timeout list is singly linked (bounded by the table's thread count): `next == NULL` is not armed, the last node points to itself. | `kernel/include/embk/kernel.h`, `kernel/time/time.c` |
| A16 | SPEC-008 §5, SPEC-009 §2 | A terminated thread's exit code lives in `wake_data` (no waker writes it after exit); the wake result and the notification mode of the current wait live in the thread's type-specific `obj.flags` bits; the object header has no padding byte. Together with A15 the tiny-profile control block is 32 bytes (R-003 T2). | `kernel/include/embk/kernel.h` |
| A17 | SPEC-012 §13, R-003 T1 | The AVR reference build adds `-mrelax` and `-mcall-prologues` (avr-gcc, part of the measured configuration); the footprint gate measures `samples/footprint_t1` under `configs/footprint-t1.conf`, the T1 feature set (scheduler, notifications, sleep and timeouts, one semaphore; no mutex, no trace). | `cmake/toolchains/avr-gcc.cmake`, `tools/footprint/thresholds-avr-uno-t1.json` |
| A18 | SPEC-006 §3 | `emb_sem_bind_notify()` is `prekernel thread` context, not `thread` only: bindings are part of object construction and the initialization table runs before the kernel starts. | `kernel/sync/sem.c`, `include/emb/sem.h` |
| A19 | SPEC-015 §4, SPEC-006 §3.2 | Every outcome of a wait operation is traced, including the immediate ones (`EMB_NO_WAIT`, a pending cancellation, a second joiner, a self-join, a recursive re-lock) and the misuse results that fault in checked builds, so that the differential bridge sees each operation end; a notification set through a semaphore binding to a terminated thread is dropped like a direct one. The timer interrupt traces `EMB_TRACE_TICK`. | `kernel/sync/`, `kernel/notify/notify.c`, `kernel/thread/thread.c`, `kernel/time/time.c` |
| A20 | SPEC-009 §4 | The generated storage unions carry the probed alignment on their byte member (`EMB_ALIGNED(EMB_<OBJ>_STORAGE_ALIGN)`; on a member, not the typedef, which EmbCC refuses, 09 §4): the `emb_max_align_t` member alone gave 8 on x86-64 where the thread control block needs 16, which only static placement had hidden. | `tools/storage/gen_storage.py` |
| A21 | SPEC-004 §5.1, SPEC-003 §5.2 | The reference model fixes a relative timeout's deadline when the call is made (`now + timeout` in section 1) and expires an already-due deadline at arming, as the kernel does; it computed the deadline in section 2 before, which the differential bridge exposed as a divergence when a tick landed between the sections. Kernel unchanged. | `tools/model/embmodel/kernel.py` |
| A22 | SIM-002, SIM-003 | Emulated boards run QEMU with `-icount shift=N,sleep=off` (N per board, close to the real part's instruction rate): virtual time follows executed instructions, so a host stall cannot make overdue tick interrupts fire back to back. Conformance timing on emulators is then deterministic; it is still never evidence of real timing (SIM-003). | `boards/*/*/board.cmake`, `tools/qemu/run_qemu.py` |
| A23 | SPEC-006 §3 | Public binding takes a nonzero single application-bit mask, not a bit index; binding is prekernel/thread context. Binding existing readiness does not emit an initial edge; consumers must drain existing readiness before waiting. M1 semaphore binding has no unbind operation, and pointer-mode binding storage must outlive the reference. | `include/emb/sem.h`, `kernel/sync/sem.c` |
| A24 | SPEC-009 §5.2, SPEC-008 §4 | Static table wrappers run during `emb_kernel_init()`, before scheduler start, not automatically before `main()`. | `kernel/exec/exec.c` |
| A25 | SPEC-005 §2.2, §3.2, R-003 T7/T9 | M1 inheritance propagation runs within one caller-held critical section; owned-list scans, waiter requeue, tiny scheduler scans, and separate deadlock traversal contribute to the full bound. No PI hop-section option exists. | `kernel/sync/mutex.c`, `kernel/sched/sched.c` |
| A26 | SPEC-001 §3, API-008 | Current APIs with output results place typed timeout/deadline before trailing `out_*` arguments; timeout discovery must use types/metadata, not assume it is always last. | `include/emb/notify.h`, `include/emb/thread.h` |
| A27 | SPEC-012 §4.2/§14, ARCH-AVR-003 | The actual restore tail is `out SREG; pop r0; ret`; the older atomic out/ret-only description omitted the pop. Pending IRQ behavior throughout the tail requires physical validation rather than inference from the one-instruction delay or QEMU. | `arch/avr/include/emb_arch.h` (`EMBN_AVR_RESTORE`) |
| A28 | SPEC-014 §4/§11, HW-011 | Example flash slots now respect F407 erase boundaries; independent writes require erase-unit separation. The data-only board example stays on F407; F407 and F446 are distinct SoCs. Generator/CLI operations remain planned. | Documentation design refinement; hardware generator is unimplemented |