Repository navigation
M2: bring the merged stack (#22–#39) into main - #40
Merged
Merged
Conversation
emb_sem_init() and emb_mutex_init() reset whatever storage they were given, so initializing storage that still held an active object lost its waiters, owner and bindings without a diagnostic (the KRN-OBJ-007 gap recorded by the M2-02 contract review). CONFIG_EMB_OBJ_LIST (KRN-OBJ-011, default y except on the tiny profile) keeps every active semaphore and mutex on a per-type list from init to destroy. Init looks the storage up in that list under the scheduler lock and refuses a live object: EMB_FAULT_API_LIFECYCLE in checked builds, EMB_EBUSY in release, as thread init already does. The check compares addresses only, so uninitialized storage cannot be mistaken for a live object. The lists are statically initialized and usable before emb_kernel_init(). Without the list the outcome stays undefined. embk_list_contains() replaces the open-coded thread-list walk. Three thread tests and the mutex deadlock test now destroy the objects they create instead of leaving them live for the next test to re-init. New cases sem_storage_reuse_requires_destroy and mutex_storage_reuse_requires_destroy check refusal, the untouched live object (waiter, owner) and reuse after destroy. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
ADR-045 records why semaphore and mutex init detect live storage through per-type lists rather than header reads, and why every type refuses with EMB_EBUSY. KRN-OBJ-007 is amended accordingly (EMB_EBUSY, detection scope per configuration) and KRN-OBJ-011 is marked partially implemented. SPEC-009 §6, §7 and the §8 misuse table follow. The init annotations of emb_sem_init(), emb_mutex_init() and emb_thread_init() now state the refusal and the list-walk costs; thread init's walk of the all-threads list had not been mentioned. docs/engineering/m2-02-object-lifecycle.md is the review the last M2-02 checklist items asked for: the defect, the decision, the per-object init/destroy/reuse table, the cost review, storage and code size deltas, and the executed evidence. STATUS, the changelog and the checklist are updated. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
…eport The report listed AVR, RV32 and the EmbSIM suites as not run locally. They now ran: RV32 and AVR under QEMU and the three EmbSIM boards all pass. On avr-uno-t1 the kernel code is identical to main's with the same compiler. The local avr-gcc 14.4 measures 4,126 bytes of kernel text on both, above the 4,096-byte gate that CI measures with gcc-avr 7.3, so the report states which compiler the gate applies to. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
The historical cancel_waiter_disinherits seed-5 report named no binary, placement or output. Bounded triage found no divergence in 56,000 current-source runs and none in 4,200 runs of the rebuilt reporting source, where the seed-3 control still failed as expected. The four classifications in timing-and-evidence.md assume a recoverable input, so the item could never be checked off. timing-and-evidence.md now defines a separate disposition for such reports: "not reproducible: input unavailable, cause unknown". It is neither a classification nor a fix. It requires a recorded bounded attempt, named reopen triggers, and continued listing among the known limits. The project owner applied it to this report on 2026-10-27. The M2-01 checklist item is checked. The triage, investigation, timer-correction and evidence-workflow pages, STATUS, the model README and the changelog now state the disposition and the reopen triggers. Dated evidence records keep their original wording. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
The footprint gate's per-thread figure was the size of the embk_idle_thread symbol, which equals sizeof(embk_thread_t) only while idle is a full control block. Slimming the tiny idle context, the next RAM-headroom step, would have turned tcb_max into a measurement of the idle record instead of the application TCB. --storage-h reads EMB_THREAD_STORAGE_SIZE from the build's generated <emb/storage.h>, the layout probe that SPEC-012 §13 names as the source of the TCB size. The idle symbol is reported separately as the idle context, which counts in kernel static RAM. Without --storage-h the old symbol-based figure is kept and labelled as such. The JSON report gains tcb_source and idle_context. The Cortex-M, RISC-V and AVR footprint steps pass --storage-h, and tools/footprint/test_footprint.py (map attribution, header parsing, thresholds, missing size) runs in the lint job. Same figures as before on cm4-an386 (TCB 120), rv32-virt (120) and avr-uno-t1 (32, kernel RAM 64). Signed-off-by: teo1747 <motsoujunior17@gmail.com>
R-003 T2 counts the idle context in the tiny kernel's fixed 64 bytes, and footprint_t1 sat at that limit with a full 32-byte control block for idle. Idle never blocks, times out, takes notifications, joins or changes priority. The scheduler, the switch path and diagnostics read only its leading fields: arch, obj, the priority/state bytes, tflags, cancel_disable, the index where not packed, and lock_depth in checked builds. The idle context now has its own type tag, EMBK_OBJ_IDLE, on every profile, so no handle resolves to it. emb_thread_self() returns EMB_HANDLE_NULL in the idle context; before, it handed out a handle that emb_notify_set() and the queries accepted. With the table scheduler and no idle thread, kernel/sched/idle_context.c allocates only the prefix in front of wait_gen, as an aligned byte array. Every other translation unit still declares a full embk_thread_t, so the compiler never sees an access through a smaller object; static assertions pin the fields used. Idle initialization clears only the prefix, and the checked stack-guard check skips the idle context. Ports already touch only idle->arch. A prefix-sized object reached through a cast was rejected: GCC 14's -Warray-bounds flags even in-prefix accesses through it. The definition/declaration mismatch is a recorded rule 8.3/8.4 deviation (ADR-050), which an LTO build would report. avr-uno-t1 (avr-gcc 14.4.0): kernel static RAM 64 -> 43 bytes, idle context 32 -> 11, kernel text 4126 -> 4082; avr-uno 69 -> 46 and avr-uno-release 67 -> 44 bytes. The new case idle_context_is_not_an_application_thread checks handle rejection, the null self handle and the 0xFE trace index. KRN-THR-026, SPEC-008 §11, SPEC-011, the AVR port page, STATUS, the checklist and the changelog are updated. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
The lint job's clang-format 18.1.3 lays out a braced initializer in a macro over several lines; 18.1.8, used locally, kept it on one. No code change. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
Two of the small RAM savings in the M2 tiny-headroom work, and the lowered gate. The table scheduler's thread array had a slot for idle that nothing read after init: idle's level 0 is never in the ready set or a wait bitmap. EMBK_TABLE_SLOT(p) now addresses slot p - 1, an offset the compiler folds into the symbol address. A checked-build assertion guards that bit 0 never reaches a table scan. 2 bytes on AVR. CONFIG_EMB_FAULT_HOOK_RUNTIME (default y) keeps emb_fault_set_hook(). With n the kernel calls emb_fault_hook(), which the application defines, and keeps no pointer in RAM. A weak empty default exists where the compiler has weak symbols; EMB_HAS_WEAK reports which. The native tests that set a hook at run time keep the default, so only configs/footprint-t1.conf selects n. emb_fault_hook gets API ID 83. 2 bytes on AVR. Packing the per-CPU flags into one byte was evaluated and not done. The masked reads would be inlined into every public entry and cost more flash than the one or two bytes saved, and flash is the tighter T1 budget. avr-uno-t1 kernel static RAM is now 39 bytes (43 after the slim idle context, 64 before) and its gate is lowered to that value. The first_execution gates follow their baseline-plus-10-percent rule: 48 (checked, 44 measured) and 46 (release, 42). R-003, ADR-036's note, SPEC-008 §14, KRN-THR-029, the AVR port page, the checklist and the changelog are updated. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
Reading the specifications for the M2 primitives turned up places where
accepted documents disagree with each other or with the code. They are
recorded as A29 to A33 in a new AMENDMENTS-M2 page and applied in
place:
A29 KRN-TIM-035 required EMB_EOVERFLOW for a _until deadline out of the
32-bit range, which A2 and KRN-TIM-022 make unreachable; removed.
A30 SPEC-004 §9 gave EMB_EINVAL as the release status of a blocking wait
from ISR or under the scheduler lock; it is EMB_EPERM everywhere else
and in EMBK_API_REQUIRE_CAN_BLOCK.
A31 ADR-027 still described a binding as a bit index; it is a one-bit
mask (A23).
A32 KRN-NOTIF-012 cited binding cases in test_sem.c; the case is in
test_notify.c.
A33 KRN-NOTIF-009 is accepted but unbind is not implemented yet; the
status says so until M2-03 lands.
No code changes.
Signed-off-by: teo1747 <motsoujunior17@gmail.com>
A semaphore's notification binding stored a raw thread pointer, and nothing tied the target's lifetime to it. With no unbind, a thread could be destroyed, and its storage reinitialized, while a semaphore still named it; the next give wrote into whatever the storage had become. - emb_sem_unbind_notify() removes the binding: EMB_OK, or EMB_ENOENT (API ID 84, KRN-NOTIF-013). - Each thread counts the bindings that name it (bind_refs). Bind refuses a terminated target (EMB_ESTATE), a kernel thread (EMB_EPERM) and a full count (EMB_ENOMEM). emb_thread_destroy() is misuse while the count is nonzero. Unbinding, or destroying the semaphore, releases the target (KRN-NOTIF-014, ADR-046). - The binding is an embk_binding_t in each ready-state object (A36). A binding signal is the notify_set trace record with the bound object as its third argument (A35). - The table profile is uniprocessor only, so its unread wait generation goes, and the byte holds the count: the AVR TCB stays at 32 bytes (A34). footprint_t1 kernel text drops 6 bytes. The reference model gains BindNotify, UnbindNotify and ThreadDestroy, with results compared through a separate status map, and the invariant that no binding names a destroyed thread. The new BINDING scenario group covers unbind racing an ISR give, a bound target's destroy, the object's destroy releasing it, terminated and INACTIVE targets, a suspended target and rebinding. The runner and bridge carry the new operations; existing encodings are unchanged, and destroyed threads are left out of the final-state comparison. KRN-NOTIF-009 is implemented for semaphores and KRN-NOTIF-012 accepted. SPEC-006 §3 documents the teardown order and SPEC-008 §8 the destroy rule. The user guide, STATUS, the checklist and the changelog are updated. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
Requirement citations in tests were thrown away at run time, and CTest saw one result per executable, so no tool could say which requirement an executed, asserting case had checked in which configuration. The framework now prints three new line types. The existing lines are unchanged, so the QEMU and EmbSIM runners still parse their summary. - EVIDENCE: once per run, with the suite (generated per executable by emb_add_test), the configuration hash, profile, board and checked mode. - req: the case's citations, buffered and printed after the body. Output inside a case cost the EmbSIM ports ticks and broke an elapsed-time check. - CASE: the outcome (passed, failed, skipped) with assertion and skip counts. Every assertion macro now counts once. tools/evidence/collect.py reads CTest's LastTest.log from any port and writes the cases with the source identity. Every CI test job collects and uploads it, even when tests fail. tools/evidence/matrix.py derives the requirement-by-configuration matrix with design status, evidence outcome, execution scope and coverage type in separate columns. Only citations printed by executed, asserting cases count. Configurations without evidence, among them the not-yet-possible NUCLEO-F446RE HIL run, appear as not run with their reason. The first matrix finds 14 cited identifiers (KRN-SCH-*, KRN-MEM-009) in groups whose migration is still pending and whose v0.1 text is not in the repository; they stay visible as uncataloged rows. All 18 local targets pass (native, QEMU Cortex-M/RV32/AVR, EmbSIM Uno, NUCLEO-F446RE and ESP32-C3), and the AVR test images still fit. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
The public headers' @time annotations name cost inputs (waiters, armed timeouts, owned mutexes, PI work, table scans, batch wakes, callbacks, and so on), but nothing said how each input is bounded. Nothing noticed, either, when an annotation named an input no one had thought about. docs/engineering/resource-bounds.json is the reviewed inventory. It has 14 entries, each with its input, bound, limit, enforcement (configuration, admission, structural or application), whether it runs masked, its profile differences and its evidence. It maps the 25 public functions whose @time is not O(1) to the entries they depend on. Inputs the kernel does not limit (owned mutexes, active objects, stack size, callbacks) are marked as application obligations rather than presented as bounded. tools/evidence/check_bounds.py, run in the lint job, fails when a non-O(1) annotation has no entry, when an entry is incomplete or unknown, or when the rendered resource-bounds.md is stale. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
Event flags hold a word of bits that threads wait on with ANY or ALL of a mask, optionally clearing the bits that satisfied them (SPEC-005 §5, KRN-SYNC-029). Set and clear are ISR-safe; waits are thread-only with the usual timeout, absolute-deadline, cancellation and destroy outcomes. - Set ORs the bits and walks the waiters once in queue order. Each satisfied waiter is handed its bits, and a CLEAR waiter removes them before the next waiter is examined, so overlapping clearing waiters are served highest priority first. All of it runs in one section with one reschedule. A new embk_wait_iter walks list and bitmap queues in the same order as embk_wait_first(). - A waiter keeps its mask in wake_data and its mode in the thread's bit-wait mode bits, shared with notification waits (A38). The TCB does not grow. - A binding (KRN-SYNC-035) fires only for bits still set and changed after the direct waiters were served; unbind follows ADR-046. - A zero mask or an unknown mode bit is argument misuse; set and clear of zero bits are no-ops (A39). emb_event_attr_default() and unbind are added; there is no DEFINE macro yet (A40). - CONFIG_EMB_EVENT (on) and CONFIG_EMB_EVENT_BITS (8 tiny, 32 base). The footprint_t1 reference configuration leaves events out, and its footprint is unchanged. Storage, the ABI inventory, API IDs 85 to 94 and trace IDs 31/32 are added; NOTIFY_SET's trace comment now names the bound object (A35). The reference model gains Event state and EventSet/EventClear/ EventWait/EventDestroy, the invariant that no queued waiter is satisfied by the current bits, and an EVENT scenario group with exhaustive property tests. The runner and bridge carry event flags; existing encodings are unchanged, and a missing "events" key in archived captures reads as not configured. tests/conformance/ test_event.c covers the contract on every port. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
Condition variables (SPEC-005 §6, KRN-SYNC-030) under CONFIG_EMB_COND, on by default except on the tiny profile, and requiring mutexes. - A wait enqueues the caller and fully releases its mutex in one section, with hand-off and inheritance, so a signal sent after the release always finds the waiter. There is no stored signal and no spurious wakeup. Signal wakes the highest waiter; broadcast wakes all in queue order with one reschedule. Both are thread-only. - Every completion, including timeout, cancellation and destruction, relocks the mutex before returning. The relock goes through the mutex's own lock path (embk_mutex_lock_common) and defers cancellation (A41). EMB_EOWNERDEAD or a failed relock (EDEADLK, EDESTROYED) wins over the wait's result. A pending cancel or EMB_NO_WAIT returns before the mutex is released (A42). - The caller must own the mutex exactly once: not the owner is OWNER misuse, a recursive hold returns EMB_ESTATE. - mutex.c exposes its lock path and a release helper for this; emb_mutex_unlock() uses the helper. API IDs 95-101, trace IDs 33/34. The reference model gains Cond state and CondWait in three steps (wait on the condition, relock with cancellation deferred, report), plus CondSignal, CondBroadcast and CondDestroy. A ModelError is raised if a satisfied wait returns without the mutex. The blocking section now emits wait_begin before its enqueue hook, matching the kernel's trace order. The COND scenario group covers the lost-signal race, a relock after timeout, a cancel during the relock, broadcast and destroy. The runner and bridge carry condition variables; tiny and archived captures without a "conds" key skip them. tests/conformance/ test_cond.c covers the contract. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
KRN-IPC-022 asks for model scenarios before the M2 queue code. The reference model gains copy-by-value message queues (SPEC-007 §2): each queue has a ring of bounded capacity and two wait queues (receivers at 400 + 2i, senders at 401 + 2i). - MsgSend hands the item to the first waiting receiver, else stores it at the tail, else waits for a slot; a blocked sender keeps its item. - MsgRecv takes the head and, in the same section, moves the first waiting sender's item into the freed slot. - MsgSendFront never waits: a waiting receiver, else the head, else TIMEOUT. MsgPeek copies the head, or TIMEOUT when empty. - Send and receive are ISR-safe with EMB_NO_WAIT only. - MsgDestroy wakes both sides with DESTROYED and drops stored items. - The receive-side binding fires on the empty-to-nonempty transition, not on a hand-off. Invariants checked after every action: receivers wait only while the ring is empty, senders only while it is full, the ring never exceeds its capacity, and every accepted item is received once, still stored, or dropped by destroy. A mutation check of each (no refill from a waiting sender, a silent drop when full, storing past a waiting receiver, an uncounted drop at destroy) is caught by the new scenarios. The MSGQ scenario group is appended to the catalogue with exhaustive outcome tests. The bridge encodes the ops as qsend/qfront/qrecv/qpeek/ qdestroy with Q<id>=<capacity>[,fifo][,bind=t.b] and skips the group until a runner reports msgqs=1; existing encodings are unchanged. The evidence bundle format carries a "msgqs" key only when present. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
Message queues (SPEC-007 §2, KRN-IPC-010) under CONFIG_EMB_MSGQ, in include/emb/msgq.h and kernel/ipc/msgq.c, built on the model merged first (KRN-IPC-022). - Fixed-size items are copied by value through a caller-provided ring declared with EMB_MSGQ_RING(). Init refuses a missing, misaligned or undersized ring, an item size of 0 or above CONFIG_EMB_MSGQ_MAX_ITEM (64, tiny 16) and a capacity of 0 (A43). - A send to a waiting receiver copies into its out_item, whose pointer waits in wake_data, and leaves the ring untouched. A receive that frees a slot moves the first waiting sender's item, whose pointer waits in wake_data too, into the ring. A woken thread never re-checks, and each section copies at most two items. - send_front takes no timeout and is not a cancellation point; peek on an empty queue returns EMB_ETIMEDOUT; the unreachable receive branch for a sender waiting on an empty ring is gone (A44). - send, receive, send_front and peek work from ISRs with EMB_NO_WAIT; the _until forms are thread-only (A47). - The receive-side binding fires on empty to nonempty, not on a hand-off and not on a refill from a waiting sender (A46). - Destroy drops stored items and, with ABORT_WAITERS, wakes receivers and senders with EMB_EDESTROYED. - CONFIG_EMB_IPC_SMALL (y on tiny) keeps 8-bit counts: a capacity above 255 is refused (A45). Message queues are off in footprint_t1, whose measurement is unchanged (4,058 text, 39 RAM, 32-byte TCB on AVR). API IDs 102-114, trace IDs 35/36 (send, receive: caller, queue and status of every outcome), type tag 0x56. The runner gains Q<id>=<capacity>[,fifo][,bind=t.b], the qsend, qfront, qrecv, qpeek and qdestroy operations and the final ring contents; the bridge maps thread-context send and receive records to the end of the wait, drops ISR-context ones, and compares received data and rings. The model now reschedules after a send or receive that wakes a higher thread and traces send_front like a send. A new scenario, msgq_refill_does_not_signal_binding, catches a kernel that signals the binding on a refill, which the earlier group missed. tests/conformance/test_msgq.c has 11 cases; the resource-bound inventory gains item_copy and the msgq functions. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
The probe's message queue entries name embk_msgq_t, which only <embk/ipc.h> declares; the EmbCC native comparison would not compile. CI does not build that flow, so nothing caught it. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
Work queues (SPEC-006 §4, KRN-WQ) under CONFIG_EMB_WORKQ, in include/emb/work.h and kernel/work/, for the list scheduler. - A queue embeds its thread and constructs it through the application thread's checks, flagged EMBK_THREAD_KERNEL (ADR-048, A51): thread calls on its handle are refused, notifications to it are OWNER misuse, and emb_thread_exit() from a handler is a context fault. thread.c gains the shared construct, start, exit and release steps; T1 text shrinks by 2 bytes. - The thread drains the FIFO one item at a time, marked RUNNING while the handler runs outside the critical section, and waits on EMB_NOTIFY_K_WORK when it is empty. Submit is O(1) and ISR-safe: EEXIST while queued, kept for one more run while running on the same queue, EBUSY on another. - cancel reports PENDING, RUNNING or IDLE; cancel_sync and flush wait on a completion queue for the item or a stack marker. Both are misuse from the queue's own thread, and both fix their deadline at the call. - Destroy refuses a busy queue, stops the thread and waits, not cancelably, for it to exit; a racing submit or flush is ESTATE (A49). - emb_work_t wraps generated opaque storage (A48). - The system queue sits in its own object file with an init-table entry, so images link it only when they reference emb_workq_system() (A50). API IDs 115-124, trace IDs 37-40, type tag 0x57. The reference model gains work queues (A53): a queue thread whose program follows its state, the drain loop or a handler body of model operations. Invariants tie each item's state to the FIFOs and running items and every completion waiter to something that can complete. The WORKQ group covers FIFO order and idempotent submit, resubmission, cancel states, flush with a timeout and while a handler runs, ISR submit and destroy. The runner and bridge carry W, H and the work operations, and the bridge follows the queue thread's own trace. A seeded campaign found that flush computed its deadline after a tick could advance the clock inside its first section; the input is now a timer regression, and check_evidence counts the applicable regressions rather than four. tests/conformance/test_workq.c has 10 cases. The ABI probe now includes <embk/work.h>. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
The reset entry lived in .text.reset, which both RISC-V linker scripts place first. With -ffunction-sections, any C function named reset is emitted into the same section and can be linked in front of embn_rv_reset, so the hart starts in that function with sp = 0. A static helper named reset in a conformance test did exactly that on rv32-virt: the image faulted on its second instruction. The section is now .text.embn_rv_reset, a name only the reset entry can produce. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
Software timers (SPEC-003 §7, KRN-TIM-025) under CONFIG_EMB_TIMER, in include/emb/timer.h and kernel/time/timer.c, for the list scheduler. - Armed timers sit in their own deadline list (ADR-047). The expiry pass merges it with the thread timeouts: the earlier head first, a thread first on equal deadlines, and each timer at most once per pass (a timer armed already due during a pass waits for the next). The thread path is unchanged; tickless programming takes the earlier head. - A periodic timer re-arms from its previous deadline before the callback runs. Whole missed periods are skipped in closed form, one division, and counted as overruns (A56). - Callbacks run on a named work queue through an embedded work item. An expiry that finds the callback still queued, or running with its rerun already due, coalesces and counts an overrun. With EMB_TIMER_ISR_CONTEXT a callback runs in the expiry interrupt with the timeout lock released. A thread-context timer without a queue is ENOTSUP, so the system queue stays unlinked unless named (A55). - A named queue cannot be destroyed while a timer refers to it. - stop reports IDLE, PENDING or RUNNING; stop_sync waits for a running work-queue callback and is misuse from that callback. - destroy refuses an armed, queued or running timer; restart of a never-started timer is ESTATE (A54, A58). API IDs 125-136, trace IDs 41-43 (A59), type tag 0x58. workq.c exports its locked submit, cancel and cancel_sync paths for timers. The reference model gains timers (A60): ISR-context callbacks run model operations in the expiry pass, work-queue callbacks go through the embedded item, and the model checks that a periodic deadline stays on its first expiry's grid. A scenario horizon stops time from advancing while a thread could run once a periodic timer has run long enough, as the runner does. The TIMER group covers one-shot and periodic ISR timers, equal deadlines, a work-queue callback, stop and stop_sync of a running callback and overruns. The runner and bridge carry R sections and tstart, tstop and tsync. Timer starts, stops and expiries and handler starts and ends are now canonical events, so the bridge pins otherwise silent operations to their place in the kernel's trace. tests/conformance/test_timer.c has 7 cases; the native tickless one checks the closed-form catch-up by holding the timer interrupt off for nine ticks. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
Delayed work (SPEC-006 §4.3, KRN-WQ-003, KRN-WQ-007) when both work queues and software timers are configured, in include/emb/work.h and kernel/work/dwork.c. - emb_dwork_t is a public emb_work_t, the handler's argument, followed by opaque storage for an internal ISR_CONTEXT timer whose only action is the O(1) submit (A61). timer.c exposes the internal-timer init, arm and stop it needs. - The queue is named at schedule time and holds a timer reference while the delay runs, so it cannot be destroyed. The target doubles as the armed marker: a cancel between expiry and submit leaves nothing to submit. - schedule and schedule_at return EEXIST while the delay runs or the item is queued, and EBUSY while the handler runs on another queue; reschedule replaces a running delay. cancel reports PENDING for a stopped delay or a removed item; cancel_sync also waits for a running handler. API IDs 137-142, trace ID 44. The reference model gives a delayed item an internal timer that submits it and checks that the delay's target and its timer agree; it now also refuses to destroy a queue a timer names, as the kernel does. The DWORK group covers a delay that runs once, idempotent schedule, reschedule and cancel, and ISR scheduling. The runner carries K sections and dsched, dresched and dcancel. test_workq.c gains four delayed-work cases. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
…unner
- 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>
…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>
…izer
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>
Signed-off-by: teo1747 <motsoujunior17@gmail.com>
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>
- 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>
docs/engineering/m2-exit-review.md records: - every M2 checklist item with its pull requests (#21 to #39) and its evidence; - the reconciliation of the public API, annotations, complexity, configuration, model and requirement cards; - the five defects M2 found and where each is fixed; - the CI state; - the limits carried out of M2 (hardware, the tiny profile, primitives not built); - the remaining M3a work. The remaining checklist boxes are ticked. STATUS is reviewed as of the exit: binding sources, object lists, trace records and model coverage are brought up to date, and coverage reports no longer count as unimplemented. The roadmap's M2 entry says what was delivered and what was not, and the configuration guide lists the coverage preset and the kernel object options with their per-profile defaults. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
Signed-off-by: teo1747 <motsoujunior17@gmail.com>
The project owner reviewed the M2 contract changes by topic on 2026-10-31 and accepted all of them as written: amendments A29 to A61, including A55's explicit timer queue, and ADR-045, ADR-046, ADR-047, ADR-048 and ADR-050. The ADR statuses, the amendments page, the exit review, the roadmap and the changelog now say so. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
5 of 6 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This brings M2 into
main. The work was already reviewed and merged as #22–#39, but each of those merged into the branch below it in the stack, so only #21 reachedmain.Problem and result
#22–#39 were opened as stacked PRs, each based on the branch of the one before it. They were merged starting from the bottom of the stack, and GitHub does not retarget a PR to
mainwhen its base branch was itself merged by PR into another branch. So each change landed in its parent branch instead.docs/m2-11-exit, the top of the stack, now holds all of it.This PR merges
docs/m2-11-exitintomain. It changes 144 files (+13,184 / −426) and contains nothing that was not already reviewed in #22–#39.Validation
git merge-treeofmainwithdocs/m2-11-exitis conflict-free, and the merged tree is identical todocs/m2-11-exit.docs/m2-11-exitas docs(m2-11): M2 exit review #39: 25 checks, includingnative-coverage.docs/engineering/m2-exit-review.md.Review checklist
Signed-off-bytrailer (git commit -s); DCO is separate from cryptographic signing.Also in this PR
The last commit records the M2 contract decisions the project owner accepted on 2026-10-31: amendments A29 to A61 and ADR-045 to ADR-048 plus ADR-050. It changes documentation only.