KRN-SYNC - Synchronization¶
Documentation revision: 2026-10-14 (ADR-039; M1 amendment log). Existing status dates record original design acceptance, not validation of the revised wording. New implementation obligations remain Proposed until implemented and verified.
Group KRN-SYNC. Design: docs/specs/SPEC-005-synchronization.md. Related groups: KRN-WAIT (the protocol every primitive here uses), KRN-SCH (effective priority in the ready structure), KRN-THR (priority change, termination), KRN-TP (demotion versus inheritance), KRN-NOTIF (binding), KRN-SMP (spinlocks), KRN-OBJ (destroy).
KRN-SYNC-001 to 007 originate in the v0.1 specification (§8.6); KRN-SYNC-008 to 017 in docs/architecture/03-kernel-architecture.md §5.2 (014 to 017 added by ADR-028 and ADR-030). All are restated here as the authoritative copy. New requirements start at 018.
Requirements¶
KRN-SYNC-001 Common wait mechanism¶
Statement. 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
KRN-SYNC-002 Explicit, validated ownership¶
Statement. 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
KRN-SYNC-003 Priority inheritance available¶
Statement. 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
KRN-SYNC-004 Nested dependency chains¶
Statement. 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
KRN-SYNC-005 ISR-safe signaling is distinct¶
Statement. 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
KRN-SYNC-006 Deterministic wait ordering¶
Statement. 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
KRN-SYNC-008 Unlock by a non-owner¶
Statement. 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
KRN-SYNC-009 Transitive inheritance with a depth bound¶
Statement. 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
KRN-SYNC-010 Recomputation on unlock¶
Statement. 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
KRN-SYNC-011 Owner termination¶
Statement. 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
KRN-SYNC-012 Ceiling protocol on the same object type¶
Statement. 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
KRN-SYNC-013 Recursive locking is an option¶
Statement. 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
KRN-SYNC-014 Owned-mutex list and immediate recomputation¶
Statement. 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
KRN-SYNC-015 Deadlock detection¶
Statement. 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
KRN-SYNC-016 Any unlock order¶
Statement. 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
KRN-SYNC-017 Static ceilings from the system description¶
Statement. 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
KRN-SYNC-018 Effective priority definition¶
Statement. 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
KRN-SYNC-019 Propagation in both directions¶
Statement. 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
KRN-SYNC-020 Mutex lock cost¶
Statement. 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
KRN-SYNC-021 Hand-off on unlock¶
Statement. 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
KRN-SYNC-022 Waiter removal hook¶
Statement. 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
KRN-SYNC-023 Recursion and self-relock¶
Statement. 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
KRN-SYNC-024 EMB_EDEADLK¶
Statement. 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
KRN-SYNC-025 Owner death policies¶
Statement. 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
KRN-SYNC-026 Ceiling rules¶
Statement. 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
KRN-SYNC-027 No ISR operation on mutexes¶
Statement. 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
KRN-SYNC-028 Semaphore semantics¶
Statement. 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
KRN-SYNC-029 Event flag semantics¶
Statement. 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
KRN-SYNC-030 Condition variable semantics¶
Statement. 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
KRN-SYNC-031 Barrier semantics¶
Statement. 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
KRN-SYNC-032 Priority change preserves contributions¶
Statement. 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
KRN-SYNC-033 Spinlock rules¶
Statement. 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
KRN-SYNC-034 Atomics¶
Statement. 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
KRN-SYNC-035 Binding on semaphores and events¶
Statement. 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
KRN-SYNC-036 Trace and statistics¶
Statement. 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
KRN-SYNC-037 Tiny profile options¶
Statement. 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
KRN-SYNC-038 Model coverage for inheritance¶
Statement. 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