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 |