KRN-IPC requirements¶
IPC primitives that block shall use the common wait mechanism. Rationale: One protocol (SPEC-004) under every primitive. Status: Accepted 2026-10-07 Verification: Analysis: every blocking entry in Trace: SPEC-007 §1; SPEC-004; v0.1 §9.4 |
Queue capacity and memory use shall be determinable from configuration and application allocation. Rationale: No hidden allocation on an MCU. Status: Accepted 2026-10-07 Verification: Analysis: Trace: SPEC-007 §2.1, §3.1, §4.1; 03 §9.2 |
ISR-safe IPC operations shall never block. Rationale: SPEC-001 §5.2. Status: Accepted 2026-10-07 Verification: Analysis: Trace: SPEC-007 §1, §7 |
Zero-copy APIs, if provided, shall define ownership and lifetime rules explicitly. Rationale: Lifetime hazards are the price of zero copy (v0.1 §9.3). Status: Accepted 2026-10-07 Verification: Analysis: SPEC-007 §4.3 rules; Test: checked-build Trace: SPEC-007 §4.3 |
Wake ordering for multiple waiters shall be deterministic and documented. Rationale: Analyzability. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-007 §2.2, §3.2, §4.2; KRN-WAIT-001, 002 |
Zero-copy transfer shall move ownership explicitly; a transferred block shall not be accessed by the sender after transfer. Rationale: 03 §6.5. Status: Accepted 2026-10-07 Verification: Test: checked-build Trace: SPEC-007 §4.3 |
Buffer pools shall be bounded and allocation shall be O(1). Rationale: Real-time paths. Status: Accepted 2026-10-07 Verification: Benchmark: pool alloc and free in the harness; Analysis: intrusive free list. Trace: SPEC-007 §4.2 |
Cross-partition and cross-core messaging shall use the same handle, timeout, and wake semantics as intra-image queues. Rationale: One mental model from a single image to a multi-core, multi-partition system. Status: Accepted 2026-10-07 (FUTURE feature; the constraint binds the queue API now) Verification: Analysis at port specification time: the port API is a superset of the queue API. Trace: SPEC-007 §5; 03 §6.6 |
Cross-partition buffers larger than the configured copy threshold shall be transferred by lease, validated on every access, and revoked by the client’s wake. Rationale: ADR-032. Status: Accepted 2026-10-07 (FUTURE feature) Verification: Deferred to the port specification. Trace: SPEC-007 §5; ADR-032 |
A message queue shall copy fixed-size items by value into a caller-provided ring; send with a waiting receiver shall copy directly into the receiver and wake it; receive that frees a slot shall move a waiting sender’s item into it and wake the sender; a woken thread shall not re-check; a full queue shall return Rationale: Hand-off semantics (KRN-WAIT-012) applied to both sides; no silent drops (R-001 §6, RIOT). Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-007 §2.2 |
Rationale: Simplicity and bounded masking (R-003 T7) without a reservation protocol. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-007 §2.2, §2.3 |
Rationale: Urgent messages without a second queue (03 §6.3). Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-007 §2.2 |
A pipe shall write as much as fits and block for the remainder when the timeout allows, reporting the partial count on timeout; read shall return once Rationale: Partial transfers with per-call minimums are what stream consumers need (Zephyr pipe rewrite, R-001 §6). Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-007 §3.2 |
Pipe copies shall run in chunks of at most Rationale: Bounded masking for general pipes; a lock-free fast path for the common single-producer single-consumer case (FreeRTOS stream buffers). Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-007 §3.2 |
Rationale: A defined end-of-stream and a defined restart. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-007 §3.2 |
A pool shall keep an intrusive O(1) free list; Rationale: 03 §6.5, §9.2. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-007 §4.2 |
Checked builds shall track each block’s owner (thread, Rationale: Zero-copy bugs are found in development at no production cost. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-007 §4.3, §7 |
Message queues (receive side, empty to non-empty), pipes (fill reaching Rationale: KRN-NOTIF-004. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-007 §2.2, §3.2, §4.2; SPEC-006 §3 |
Rationale: Word copies and intrusive free lists need alignment the application should not have to compute. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-007 §2.1, §4.1, §7 |
Send, receive, blocked send, pipe write, read and close, pool alloc, free and transfer shall be trace events; high-water occupancy, blocked-send counts, minimum pool availability and blocks outstanding shall be optional statistics; the debug descriptor shall export ring and free-list layouts. Rationale: Queue sizing and leak hunting need these numbers. Status: Accepted 2026-10-07 Verification: Test: trace decoder; statistics API test. Trace: SPEC-007 §8; OBS-005, OBS-008 |
The tiny profile shall offer message queues and pools with 8-bit counts under Rationale: Footprint targets T1 and T2. Status: Accepted 2026-10-07 Verification: Footprint test of the tiny reference configuration. Trace: SPEC-007 §9 |
Message queues and pools shall be added to the reference model with their M2 conformance tests, with conservation properties (every item received exactly once or still in the ring; every block owned by one party or free). Rationale: The same evidence standard as semaphores and mutexes. Status: Accepted 2026-10-07 Verification: Analysis: Trace: SPEC-007 §10; KRN-WAIT-007 |