# KRN-SYNC requirements ::::{req} Common wait mechanism :id: KRN-SYNC-001 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Blocking synchronization shall use the common kernel wait mechanism. **Rationale:** One protocol under every primitive (SPEC-004) means one set of race rules, one model, one set of tests. **Status:** Accepted 2026-10-07 **Verification:** Analysis: every blocking entry in `kernel/sync/` calls `embk_wait_prepare` and `embk_wait_commit` or `embk_block_on`; a grep in CI rejects any other path to `BLOCKED`. **Trace:** SPEC-005 §1; SPEC-004; v0.1 §8.6 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Explicit, validated ownership :id: KRN-SYNC-002 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: KRN-SYNC-008 Mutex ownership shall be explicit and validated where configuration permits. **Rationale:** A mutex is not a semaphore; unlock by a non-owner is the classic silent corruption. **Status:** Accepted 2026-10-07 **Verification:** Test: `misuse/mutex_unlock_non_owner` in checked and release builds (TEST-010); `sync/mutex_is_owner`. **Trace:** SPEC-005 §3.1, §3.3; KRN-SYNC-008 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Priority inheritance available :id: KRN-SYNC-003 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md The mutex subsystem shall support priority inheritance for configurations that enable real-time mutexes. **Rationale:** Priority inversion is a first-class real-time problem (v0.1 §8.3). **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/pi_classic_inversion` checks that the medium-priority thread never runs while the high one waits on the low one's mutex; model scenario `classic_inversion`. **Trace:** SPEC-005 §2, §3.2; ADR-028 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Nested dependency chains :id: KRN-SYNC-004 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: KRN-SYNC-009 Priority inheritance shall support nested dependency chains. **Rationale:** H waits for A held by M, M waits for B held by L: H's priority must reach L (v0.1 §8.3). **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/pi_nested_chain` to depth 3; model scenario `nested_chain_timeout`. **Trace:** SPEC-005 §2.2; KRN-SYNC-009, 019 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} ISR-safe signaling is distinct :id: KRN-SYNC-005 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: KRN-IRQ-010 ISR-safe signaling operations shall be distinct from blocking thread-only operations. **Rationale:** The ISR-safe path has no ownership and no inheritance; the annotation is the contract (SPEC-001 §5.2). **Status:** Accepted 2026-10-07 **Verification:** Analysis: `tools/apidoc` checks that `give`, `set`, `clear` carry `@ctx thread isr` and every `lock`, `take`, `wait` carries `@ctx thread`. **Trace:** SPEC-005 §1; SPEC-001 §5.2; KRN-IRQ-010 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Deterministic wait ordering :id: KRN-SYNC-006 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: KRN-WAIT-001 Synchronization object wait ordering shall be documented and deterministic. **Rationale:** Schedulability analysis needs to know who wakes first. **Status:** Accepted 2026-10-07 **Verification:** Test: the `wait/order_*` group runs against every primitive of SPEC-005. **Trace:** SPEC-005 §1; KRN-WAIT-001, 002 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} No hidden allocation :id: KRN-SYNC-007 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: KRN-WAIT-010 No synchronization primitive used on a real-time path shall require hidden dynamic allocation after initialization. **Rationale:** Determinism and the tiny profile. **Status:** Accepted 2026-10-07 **Verification:** Analysis: no allocator symbol is reachable from `kernel/sync/` (link-map check in CI). **Trace:** SPEC-005 §1; KRN-WAIT-010; KRN-MEM [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Unlock by a non-owner :id: KRN-SYNC-008 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Unlock by a non-owner shall be a kernel fault in checked builds and `EMB_EPERM` in release builds. **Rationale:** Misuse, per SPEC-001 §5.3. **Status:** Accepted 2026-10-07 **Verification:** Test: `misuse/mutex_unlock_non_owner`. **Trace:** SPEC-005 §3.3, §11 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Transitive inheritance with a depth bound :id: KRN-SYNC-009 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Priority inheritance shall be transitive through chains of mutexes with a configurable maximum depth; exceeding it is a kernel fault in checked builds. **Rationale:** Unbounded walks are a latency hazard; the bound is a design parameter. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/pi_depth_bound` builds a chain of `CONFIG_EMB_PI_MAX_DEPTH + 1` and checks the fault (checked) and the truncation trace event (release). **Trace:** SPEC-005 §2.2; ADR-028 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Recomputation on unlock :id: KRN-SYNC-010 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md On unlock, the owner's effective priority shall be recomputed as the maximum of its base priority and the highest priority waiter across all mutexes it still owns. **Rationale:** The one-mutex simplification of other kernels (R-001 §5) is wrong as soon as two mutexes are held. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/pi_two_mutexes_restore`; model invariant `eff == effective(base, owned)`. **Trace:** SPEC-005 §2.1, §3.3 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Owner termination :id: KRN-SYNC-011 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: KRN-SYNC-025 When a mutex owner terminates while owning mutexes, the behavior is a configuration choice: fault (default) or release-with-`EMB_EOWNERDEAD` delivered to the next owner. **Rationale:** Both are legitimate: a fault for systems where it must never happen, recovery for systems that restart partitions. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/owner_death_fault`, `sync/owner_death_release_with_waiter`, `sync/owner_death_release_no_waiter`; model scenarios `owner_death_*`. **Trace:** SPEC-005 §3.6; KRN-SYNC-025 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Ceiling protocol on the same object type :id: KRN-SYNC-012 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Priority ceiling protocol shall be available as a per-mutex option on the same object type, using the effective-priority mechanism. **Rationale:** One mutex type, two protocols; the effective-priority machinery already exists. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/ceiling_lock_raises`, `sync/ceiling_unlock_restores`; model scenario `ceiling_mutex`. **Trace:** SPEC-005 §3.4; ADR-030 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Recursive locking is an option :id: KRN-SYNC-013 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: KRN-SYNC-023 Recursive locking shall be a per-mutex creation option, disabled by default. **Rationale:** Recursion hides locking-discipline errors; it is offered, not default. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/mutex_recursive`, `sync/mutex_nonrecursive_self_relock`. **Trace:** SPEC-005 §3.2; KRN-SYNC-023 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Owned-mutex list and immediate recomputation :id: KRN-SYNC-014 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Each thread shall keep an intrusive list of the mutexes it owns; the recomputation of KRN-SYNC-010 shall use it and shall run at unlock, at waiter timeout or cancel, and at waiter priority change, immediately and not deferred to the waiter's resumption. **Rationale:** Deferred drops leave a thread boosted for an unbounded time (Zephyr's documented limitation, R-001 §5). **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/pi_timeout_disinherits_immediately` checks the owner's priority in the same tick as the timeout; model scenario `nested_chain_timeout`. **Trace:** SPEC-005 §2.3, §3.3; ADR-028 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Deadlock detection :id: KRN-SYNC-015 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: KRN-SYNC-024 The inheritance walk shall detect a cycle that returns to the caller and shall report `EMB_EDEADLK` (kernel-reserved status range) in release builds and fault in checked builds. **Rationale:** The walk visits the chain anyway; detection is free. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/deadlock_two_lockers`; model scenario `deadlock_two_lockers` (every terminal state has a detected cycle, none a silent one). **Trace:** SPEC-005 §3.5; KRN-SYNC-024 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Any unlock order :id: KRN-SYNC-016 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Mutexes may be unlocked in any order; there is no LIFO requirement. **Rationale:** ChibiOS's LIFO rule is a usability trap (R-001 §5); the owned list makes any order cheap. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/unlock_non_lifo`. **Trace:** SPEC-005 §3.3 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Static ceilings from the system description :id: KRN-SYNC-017 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md A ceiling mutex declared in the system description shall receive its ceiling from the generator as the highest base priority among its declared users; locking it shall raise effective priority to the ceiling; a queue-free optimization shall additionally prove the UP execution restrictions in SPEC-005 §3.4, including no blocking/yield/suspension/budget-induced ineligibility while held. M1 retains wait queues and owned-list scans. **Rationale:** RTIC's compile-time ceilings for threads in a C kernel (ADR-030). **Status:** Accepted 2026-10-07 **Verification:** Test: generator test `hw/gen_ceiling` plus `sync/ceiling_static_no_queue` on the tiny profile. **Trace:** SPEC-005 §3.4; ADR-030 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Effective priority definition :id: KRN-SYNC-018 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md A thread's effective priority shall be the maximum of its scheduling base priority, the effective priority of the highest waiter on each `INHERIT` mutex it owns, and the ceiling of each `CEILING` mutex it owns; a change shall be applied to the ready structure, to the thread's wait-queue position, or to the reschedule decision in the operation that caused it. **Rationale:** One definition that every operation recomputes; no incremental bookkeeping that can drift. **Status:** Accepted 2026-10-07 **Verification:** Analysis: model invariant checked after every step; checked builds assert it after every priority-touching operation (SPEC-005 §11). **Trace:** SPEC-005 §2.1 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Propagation in both directions :id: KRN-SYNC-019 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md A change of a thread's effective priority shall propagate along the chain of `INHERIT` mutexes it waits on, for raises and for lowerings, in the same operation, stopping where a hop's effective priority does not change or at the configured depth. **Rationale:** Non-propagated lowerings leave distant owners boosted (Zephyr); propagating both keeps the invariant of KRN-SYNC-018 global. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/pi_chain_lowering`; model scenarios `nested_chain_timeout`, `waiter_priority_change`. **Trace:** SPEC-005 §2.2 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Mutex lock cost :id: KRN-SYNC-020 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Lock/unlock timing shall include owned-mutex append/remove/recomputation, wait insertion or requeue, separate deadlock traversal, inheritance depth and configured scheduler scans. M1 shall be documented as holding one caller section across propagation; per-hop sections and constant-time uncontended bookkeeping shall not be claimed without implementation and evidence. **Rationale:** R-003 target T9. **Status:** Accepted 2026-10-07 **Verification:** Benchmark: harness operation "mutex lock and unlock uncontended; contended with chains of depth 1, 2, 4" (TEST-012); monitor of ADR-034 for section lengths. **Trace:** SPEC-005 §3.2, §2.2; R-003 §4 T9 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Hand-off on unlock :id: KRN-SYNC-021 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Unlock shall transfer ownership to the highest waiter in the same step as its wake; the new owner shall inherit from the remaining waiters at once; a thread that arrives between the unlock and the new owner's run shall not acquire the mutex. **Rationale:** No barging, wait-order fairness (KRN-WAIT-012). **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/mutex_no_barging`; model scenario `two_waiters_handoff`. **Trace:** SPEC-005 §3.3 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Waiter removal hook :id: KRN-SYNC-022 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md A mutex's wait queue shall carry the inherit flag; the wait protocol shall call the mutex's waiters-changed hook after any dequeue or requeue that is not a hand-off, and the hook shall recompute the owner's chain. **Rationale:** Timeout, cancellation, destroy, and priority change all change the owner's contribution; one hook covers them. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/pi_cancel_disinherits`, `sync/pi_destroy_disinherits`; model scenario `cancel_waiter_disinherits`. **Trace:** SPEC-005 §3.3; SPEC-004 §5.2 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Recursion and self-relock :id: KRN-SYNC-023 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md A `RECURSIVE` mutex shall count nested locks by its owner up to 255 and return `EMB_EOVERFLOW` beyond; a non-recursive mutex locked again by its owner shall return `EMB_EDEADLK` (fault in checked builds). **Rationale:** Self-deadlock is the most common mutex bug; it must not hang. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/mutex_recursive_depth`, `misuse/mutex_self_relock`. **Trace:** SPEC-005 §3.2 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} `EMB_EDEADLK` :id: KRN-SYNC-024 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md `EMB_EDEADLK` shall be defined with value -32 in the kernel-reserved status range; it shall be returned for a detected cycle through `INHERIT` mutexes and for a non-recursive self-relock; cycles through `NONE` mutexes are not detected and the documentation shall say so. **Rationale:** A stable code for a condition that is always a program error. **Status:** Accepted 2026-10-07 **Verification:** Analysis: `emb/status.h` and `emb_status_name()`; Test: `sync/deadlock_two_lockers`. **Trace:** SPEC-005 §3.1, §3.5; SPEC-001 §4.2 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Owner death policies :id: KRN-SYNC-025 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: KRN-SYNC-011 `CONFIG_EMB_MUTEX_OWNER_DEATH=FAULT` (default) shall fault in checked builds and record a non-fatal crash-record event in release builds while releasing the mutexes; `RELEASE` shall hand each owned mutex to its highest waiter with `EMB_EOWNERDEAD` or mark it inconsistent so that the next lock returns `EMB_EOWNERDEAD`; the inconsistent mark shall be cleared by the recovering owner's unlock or by `emb_mutex_mark_consistent()`. **Rationale:** Robust-mutex semantics simple enough for an MCU; the next owner always learns that state may be inconsistent. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/owner_death_*`; model scenarios `owner_death_with_waiter`, `owner_death_no_waiter`. **Trace:** SPEC-005 §3.6; KRN-SYNC-011; 08 Q5 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Ceiling rules :id: KRN-SYNC-026 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: KRN-SYNC-017 Locking a `CEILING` mutex shall raise the caller's effective priority to the ceiling immediately; a caller whose base priority exceeds the ceiling, or that is not a declared user of a statically declared mutex, is misuse (`EMB_EPERM` in release builds); a future `CONFIG_EMB_MUTEX_CEILING_STATIC_ONLY` optimization shall omit a wait queue only after enforcing the complete restrictions of SPEC-005 §3.4; it is unimplemented in M1. **Rationale:** Immediate-ceiling guarantees require an analyzed execution/resource model; declared users alone do not establish no contention or deadlock freedom. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/ceiling_*`, `misuse/ceiling_violation`; footprint test on the tiny profile. **Trace:** SPEC-005 §3.4; KRN-SYNC-017 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} No ISR operation on mutexes :id: KRN-SYNC-027 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Mutexes, condition variables, and barriers shall have no ISR-callable operation; semaphores and event flags shall have ISR-safe `give`, `set`, and `clear`. **Rationale:** An ISR cannot own anything, so it cannot participate in inheritance (R-001 §5, FreeRTOS). **Status:** Accepted 2026-10-07 **Verification:** Analysis: `@ctx` annotations; Test: `misuse/mutex_from_isr`. **Trace:** SPEC-005 §1, §3.1, §11 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Semaphore semantics :id: KRN-SYNC-028 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md A semaphore shall have a configurable count width (8, 16, or 32 bits), an initial count and a maximum; `give` with a waiter shall hand the unit over without touching the count, otherwise increment, returning `EMB_EOVERFLOW` at the maximum unless `SATURATE` is set; `take` shall decrement when positive else wait; the kernel shall offer no `give_all` and no `reset`. **Rationale:** Hand-off gives fairness; the bound makes binary semaphores a configuration, not a type; resets with waiters are the hazard ADR-020 refuses. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/sem_*`; model: the semaphore of `tools/model` with unit conservation. **Trace:** SPEC-005 §4 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Event flag semantics :id: KRN-SYNC-029 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Each event waiter shall carry its own mask and mode; `set` shall wake every satisfied waiter in queue order, handing it the satisfied bits, and shall apply a waiter's `CLEAR` before evaluating the next waiter; `clear` shall never wake; `set` shall be ISR-safe and O(waiters on that group). **Rationale:** Deterministic consumption of overlapping bits; a single batch wake. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/event_any_all_clear`, `sync/event_overlapping_clear_order`. **Trace:** SPEC-005 §5 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Condition variable semantics :id: KRN-SYNC-030 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md `cond_wait` shall require ownership with recursion count 1, shall enqueue and then fully unlock the mutex atomically with respect to `signal`, and shall relock the mutex before returning on every result; `signal` shall wake the highest waiter and `broadcast` all; the kernel shall never wake a condition waiter without a signal or broadcast. **Rationale:** Classic, analyzable semantics; the relock-always rule is what callers can reason about. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/cond_*` including relock after timeout; `misuse/cond_wait_not_owner`. **Trace:** SPEC-005 §6 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Barrier semantics :id: KRN-SYNC-031 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md With `CONFIG_EMB_BARRIER`, the arrival that completes the count shall wake all waiters with one reschedule and return serial to exactly one caller; a waiter that times out or is canceled shall leave the barrier without releasing the others. **Rationale:** Phase synchronization for parallel work on multicore targets. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/barrier_*`. **Trace:** SPEC-005 §7 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Priority change preserves contributions :id: KRN-SYNC-032 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Changing a thread's base priority shall preserve inherited and ceiling contributions and shall propagate along the chain the thread waits on; a thread's visible priority shall be queryable as base and as effective. **Rationale:** Setting the priority of a boosted owner must not drop the boost (ChibiOS gets this right; several others do not). **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/set_priority_keeps_boost`, `sync/set_priority_of_waiter_propagates`; model scenario `waiter_priority_change`. **Trace:** SPEC-005 §10, §2.3 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Spinlock rules :id: KRN-SYNC-033 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Spinlocks shall be acquired with interrupts masked, shall never be held across a blocking call or a preemption point, shall not be recursive, shall follow the declared lock order, and shall compile to the critical section on uniprocessor builds; checked SMP builds shall validate these rules. **Rationale:** SMP correctness depends on discipline that only a validator keeps honest. **Status:** Accepted 2026-10-07 **Verification:** Analysis: spinlock validator; Test: SMP `misuse/spin_*`. **Trace:** SPEC-005 §8; SPEC-002 §4.3; KRN-SMP-002 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Atomics :id: KRN-SYNC-034 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md The atomics API shall provide 32-bit and pointer-sized operations with explicit memory orders on 32-bit targets, 8-bit hardware atomics on AVR with 32-bit operations implemented by critical section, and no 64-bit atomic type. **Rationale:** 09 §6; KRN-TIM-016. **Status:** Accepted 2026-10-07 **Verification:** Test: `sync/atomic_*` on every architecture; Analysis: no 64-bit atomic builtin in the link map. **Trace:** SPEC-005 §9 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Binding on semaphores and events :id: KRN-SYNC-035 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md Semaphores and event groups shall support the notification binding of ADR-027; a count transition from zero to one, or a set that leaves changed nonzero bits after serving direct waiters, shall signal the binding; a transition consumed by a hand-off shall not. **Rationale:** Multi-object wait without poll objects (KRN-NOTIF-004). **Status:** Accepted 2026-10-07 **Verification:** Test: `notif/bind_sem`, `notif/bind_event`; model scenario `binding_hook`. **Trace:** SPEC-005 §4.2, §5.2; SPEC-004 §6.3 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Trace and statistics :id: KRN-SYNC-036 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: OBS-005 Lock, unlock with hand-off target, every inheritance change with its cause, depth-exceeded, deadlock-detected, semaphore give with hand-off, event set with woken count, and condition signal shall be trace events; contention counts, maximum boost, and maximum walk depth shall be optional statistics. **Rationale:** Inheritance bugs are invisible without a trace that names the cause. **Status:** Accepted 2026-10-07 **Verification:** Test: the trace decoder reconstructs every priority change of the conformance run. **Trace:** SPEC-005 §12; OBS-005 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Tiny profile options :id: KRN-SYNC-037 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md The tiny profile shall offer inheritance as an option (default on), ceiling mutexes without a wait queue, 8-bit semaphore counts and event bits, and shall build condition variables and barriers only when configured. **Rationale:** Footprint targets T1 and T2 with correctness kept by default. **Status:** Accepted 2026-10-07 **Verification:** Test: footprint of the tiny reference configuration; conformance `sync/` group on it. **Trace:** SPEC-005 §13; ADR-036 [Normative source](../../requirements/KRN-SYNC.md). :::: ::::{req} Model coverage for inheritance :id: KRN-SYNC-038 :status: Accepted :evidence: not evaluated :design_source: requirements/KRN-SYNC.md :links: KRN-WAIT-007 The reference model shall include the mutex with inheritance, ceiling, recursion, hand-off, owner death, and deadlock detection, and shall be explored exhaustively over at least: the three-thread inversion, a two-level chain with timeout, deadlock in both lock orders, owner death with and without a waiter, a waiter's priority change, and cancellation of a waiter. **Rationale:** The algorithm's correctness claims (R-001 §5 columns) are checked by exploration before implementation. **Status:** Accepted 2026-10-07 **Verification:** Analysis: `tools/model/tests/test_explore.py` covers the listed scenarios; CI runs it. **Trace:** SPEC-005 §15; KRN-WAIT-007; TEST-008 [Normative source](../../requirements/KRN-SYNC.md). ::::