KRN-SYNC requirements¶
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 Trace: SPEC-005 §1; SPEC-004; v0.1 §8.6 |
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: Trace: SPEC-005 §3.1, §3.3; KRN-SYNC-008 |
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: Trace: SPEC-005 §2, §3.2; ADR-028 |
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: Trace: SPEC-005 §2.2; KRN-SYNC-009, 019 |
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: Trace: SPEC-005 §1; SPEC-001 §5.2; KRN-IRQ-010 |
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 Trace: SPEC-005 §1; KRN-WAIT-001, 002 |
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 Trace: SPEC-005 §1; KRN-WAIT-010; KRN-MEM |
Unlock by a non-owner shall be a kernel fault in checked builds and Rationale: Misuse, per SPEC-001 §5.3. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-005 §3.3, §11 |
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: Trace: SPEC-005 §2.2; ADR-028 |
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: Trace: SPEC-005 §2.1, §3.3 |
When a mutex owner terminates while owning mutexes, the behavior is a configuration choice: fault (default) or release-with- 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: Trace: SPEC-005 §3.6; KRN-SYNC-025 |
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: Trace: SPEC-005 §3.4; ADR-030 |
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: Trace: SPEC-005 §3.2; KRN-SYNC-023 |
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: Trace: SPEC-005 §2.3, §3.3; ADR-028 |
The inheritance walk shall detect a cycle that returns to the caller and shall report Rationale: The walk visits the chain anyway; detection is free. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-005 §3.5; KRN-SYNC-024 |
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: Trace: SPEC-005 §3.3 |
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 Trace: SPEC-005 §3.4; ADR-030 |
A thread’s effective priority shall be the maximum of its scheduling base priority, the effective priority of the highest waiter on each 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 |
A change of a thread’s effective priority shall propagate along the chain of 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: Trace: SPEC-005 §2.2 |
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 |
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: Trace: SPEC-005 §3.3 |
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: Trace: SPEC-005 §3.3; SPEC-004 §5.2 |
A Rationale: Self-deadlock is the most common mutex bug; it must not hang. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-005 §3.2 |
Rationale: A stable code for a condition that is always a program error. Status: Accepted 2026-10-07 Verification: Analysis: Trace: SPEC-005 §3.1, §3.5; SPEC-001 §4.2 |
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: Trace: SPEC-005 §3.6; KRN-SYNC-011; 08 Q5 |
Locking a 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: Trace: SPEC-005 §3.4; KRN-SYNC-017 |
Mutexes, condition variables, and barriers shall have no ISR-callable operation; semaphores and event flags shall have ISR-safe Rationale: An ISR cannot own anything, so it cannot participate in inheritance (R-001 §5, FreeRTOS). Status: Accepted 2026-10-07 Verification: Analysis: Trace: SPEC-005 §1, §3.1, §11 |
A semaphore shall have a configurable count width (8, 16, or 32 bits), an initial count and a maximum; 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: Trace: SPEC-005 §4 |
Each event waiter shall carry its own mask and mode; Rationale: Deterministic consumption of overlapping bits; a single batch wake. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-005 §5 |
Rationale: Classic, analyzable semantics; the relock-always rule is what callers can reason about. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-005 §6 |
With Rationale: Phase synchronization for parallel work on multicore targets. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-005 §7 |
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: Trace: SPEC-005 §10, §2.3 |
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 Trace: SPEC-005 §8; SPEC-002 §4.3; KRN-SMP-002 |
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: Trace: SPEC-005 §9 |
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: Trace: SPEC-005 §4.2, §5.2; SPEC-004 §6.3 |
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 |
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 Trace: SPEC-005 §13; ADR-036 |
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: Trace: SPEC-005 §15; KRN-WAIT-007; TEST-008 |