SPEC-007 - Inter-Thread Communication: Message Queues, Pipes, Buffer Pools, Ports

Implementation and release scope: Project status records the implemented subset; roadmap defines release gates. Acceptance of this design does not establish implementation, verification, or support. Reconciled 2026-10-14.

Status: Accepted 2026-10-07 by the project owner (“do all”), with the defaults of §11. Specification work item 6b of the roadmap (07 §3), added because M2 delivers message queues. Requirements: docs/requirements/KRN-IPC.md (KRN-IPC-001 to 005 from v0.1 §9.4 and 006 to 009 from 03 §6 restated; new from 010). Builds on: SPEC-004 (wait protocol, hand-off), SPEC-006 §3 (binding), SPEC-001 §5, §6 (contexts, handles, storage), SPEC-005 §4 (the semaphore as the pattern a queue repeats twice), 03 §6.3 to §6.6, §9.2; ADR-020, ADR-027, ADR-032 (leases). Research: R-001 §6: copy-by-value queues with direct copy into a waiting receiver (ThreadX, Zephyr, RTEMS) are the fast common case; FreeRTOS stream buffers show the lock-free single-producer single-consumer byte stream; Zephyr’s pipe rewrite shows partial transfers with per-call minimums; zero copy by ownership transfer (buffer pools) is the only zero-copy form that is safe inside one address space, and leases (Hubris) the only one that is safe across partitions.

1. Scope and terms

Primitive

Target design

Blocking (thread)

ISR-safe (thread isr, EMB_NO_WAIT only)

Section

Message queue

yes

send, receive, _until forms

send, send_front, receive, peek with EMB_NO_WAIT

§2

Pipe (byte stream)

yes, CONFIG_EMB_PIPE

write, read, _until forms

write, read with EMB_NO_WAIT

§3

Buffer pool

yes

alloc, alloc_until

alloc with EMB_NO_WAIT, free

§4

Port

FUTURE

request, reply

none

§5

A message is a fixed-size item copied by value. A block is a fixed-size buffer from a pool whose ownership moves with the message that carries its pointer (zero copy). A stream is bytes without message boundaries. Everything is caller-provided storage (KRN-IPC-002, 03 §9.2), every blocking operation is a thin layer over SPEC-004, and every ready transition can signal a binding (SPEC-006 §3).

2. Message queue

2.1 Interface

typedef struct emb_msgq_attr {
    const char *name;
    void       *storage;        /* ring buffer: capacity * item_size bytes, aligned to EMB_MSGQ_ALIGN */
    uint16_t    item_size;      /* 1 .. CONFIG_EMB_MSGQ_MAX_ITEM (default 64) */
    uint16_t    capacity;       /* >= 1 */
    uint8_t     flags;          /* EMB_OBJ_ABORT_WAITERS | EMB_OBJ_FIFO | EMB_MSGQ_OWNERSHIP */
    emb_pool_t  pool;           /* EMB_MSGQ_OWNERSHIP: the pool whose blocks travel in this queue */
} emb_msgq_attr_t;

#define EMB_MSGQ_RING(name, item_size, capacity)  /* declares aligned storage of the right size */

emb_status_t emb_msgq_init(emb_msgq_storage_t *storage, const emb_msgq_attr_t *attr, emb_msgq_t *out);  /* @ctx prekernel thread */
emb_status_t emb_msgq_destroy(emb_msgq_t q);
emb_status_t emb_msgq_send(emb_msgq_t q, const void *item, emb_timeout_t timeout);       /* @ctx thread; thread isr with EMB_NO_WAIT  @time O(1) + copy */
emb_status_t emb_msgq_send_until(emb_msgq_t q, const void *item, emb_instant_t deadline);
emb_status_t emb_msgq_send_front(emb_msgq_t q, const void *item);                         /* @ctx thread isr  EMB_NO_WAIT only: urgent, to the head */
emb_status_t emb_msgq_receive(emb_msgq_t q, void *out_item, emb_timeout_t timeout);      /* @ctx thread; thread isr with EMB_NO_WAIT */
emb_status_t emb_msgq_receive_until(emb_msgq_t q, void *out_item, emb_instant_t deadline);
emb_status_t emb_msgq_peek(emb_msgq_t q, void *out_item);                                 /* @ctx thread isr  copies the head without removing it */
uint16_t     emb_msgq_count(emb_msgq_t q);                                                /* @ctx thread isr  snapshot */
uint16_t     emb_msgq_free(emb_msgq_t q);
emb_status_t emb_msgq_bind_notify(emb_msgq_t q, emb_thread_t t, emb_notify_bits_t bit);            /* receive side: empty -> non-empty */

2.2 Semantics

  • Storage. The ring holds capacity items of item_size bytes; EMB_MSGQ_RING() declares it with the alignment the kernel needs for word copies. item_size above CONFIG_EMB_MSGQ_MAX_ITEM is EMB_EINVAL: large payloads travel as block pointers (§4), never as large copies.

  • Two wait queues: receivers (when empty) and senders (when full), both with the object’s wait policy (PRIORITY_FIFO default, EMB_OBJ_FIFO optional).

  • Send. If a receiver waits: copy the item directly into the receiver’s out_item and wake it with hand-off (the ring is untouched; no binding bit, SPEC-004 §6.3). Else if the ring has room: copy into the tail slot; if the ring was empty, signal the binding. Else: block on the senders’ queue; the receiver that frees a slot copies this sender’s item into the freed slot and wakes it (slot hand-off), so a woken sender never re-checks. The copy happens inside the object’s critical section; its cost is bounded by CONFIG_EMB_MSGQ_MAX_ITEM and is part of the masked-time budget (R-003 T7).

  • Send to front. Writes at the head (the next item received) and never blocks (EMB_ETIMEDOUT when full); for urgent messages (03 §6.3).

  • Receive. If the ring is non-empty: copy the head; then, if a sender waits, move its item into the freed tail slot and wake it. Else if a sender waits with the ring empty (capacity reached zero is impossible; this branch is for capacity consumed by send_front races and is kept for completeness): hand the sender’s item directly. Else block on the receivers’ queue; the hand-off delivers the item into out_item before the wake.

  • Peek copies the head without removing it; count and free are snapshots.

  • Ownership queues. With EMB_MSGQ_OWNERSHIP, items are block pointers of pool: send transfers the block’s ownership to the queue and receive assigns it to the receiver (§4.3). In checked builds the owner field of the block is checked and updated; release builds copy the pointer.

  • Destroy follows ADR-020: waiters wake with EMB_EDESTROYED only with EMB_OBJ_ABORT_WAITERS; items still in the ring are simply dropped (with OWNERSHIP, their blocks are returned to the pool).

  • ISR callers use EMB_NO_WAIT (SPEC-001 §5.2); a full queue returns EMB_ETIMEDOUT, never drops silently (RIOT’s msg_try_send drop is the behavior to avoid, R-001 §6).

2.3 Why copy by value

A copy of up to 64 bytes under the lock is cheaper and simpler than a reservation protocol, and it keeps the kernel free of application pointers that may dangle. Zero copy is the explicit, ownership-tracked path of §4, never an implicit optimization.

3. Pipe (CONFIG_EMB_PIPE)

3.1 Interface

typedef struct emb_pipe_attr {
    const char *name;
    uint8_t    *buffer;         /* caller-provided ring, `size` bytes */
    size_t      size;
    size_t      notify_trigger; /* binding fires when fill rises to >= trigger (default 1) */
    uint8_t     flags;          /* EMB_OBJ_ABORT_WAITERS | EMB_OBJ_FIFO | EMB_PIPE_SPSC */
} emb_pipe_attr_t;

emb_status_t emb_pipe_init(emb_pipe_storage_t *storage, const emb_pipe_attr_t *attr, emb_pipe_t *out);
emb_status_t emb_pipe_destroy(emb_pipe_t p);
emb_status_t emb_pipe_write(emb_pipe_t p, const void *data, size_t len, emb_timeout_t timeout, size_t *out_written);   /* @ctx thread; thread isr with EMB_NO_WAIT */
emb_status_t emb_pipe_read(emb_pipe_t p, void *buf, size_t len, size_t min_len, emb_timeout_t timeout, size_t *out_read);
emb_status_t emb_pipe_close(emb_pipe_t p);                      /* @ctx thread isr: no more writes; readers drain then see EMB_ESTATE */
emb_status_t emb_pipe_reset(emb_pipe_t p);                      /* @ctx thread: discard contents, wake waiters with EMB_ESTATE, reopen */
size_t       emb_pipe_fill(emb_pipe_t p);
emb_status_t emb_pipe_bind_notify(emb_pipe_t p, emb_thread_t t, emb_notify_bits_t bit);

3.2 Semantics

  • Write copies as much as fits, then, if len bytes were not all written and the timeout allows, blocks on the writers’ queue until space appears, repeating until all bytes are written or the timeout expires; out_written is always set; a partial write on timeout returns EMB_ETIMEDOUT with the partial count. With EMB_NO_WAIT it writes what fits and returns EMB_OK (or EMB_ETIMEDOUT if nothing fit).

  • Read returns as soon as at least min_len bytes are available (min_len <= len, min_len >= 1), reading up to len; otherwise it blocks until min_len is available or the timeout expires (out_read holds what was read, possibly nonzero on timeout when min_len was not reached but some bytes were). After close, a read returns the remaining bytes with EMB_OK and, once drained, EMB_ESTATE.

  • Chunking. Copies run inside the object’s critical section in chunks of at most CONFIG_EMB_PIPE_CHUNK bytes (default 32); between chunks the section is released. A write of at most one chunk is atomic with respect to other writers; longer writes may interleave with other writers at chunk boundaries. A pipe is a byte stream, not a framing mechanism: framing uses a message queue, or the EMB_PIPE_SPSC flag.

  • EMB_PIPE_SPSC. Exactly one writer and one reader are promised by the application (checked builds record and verify the identities). The data copy then runs without the critical section, publishing the head or tail index after the copy with release semantics (FreeRTOS stream buffer design, R-001 §6); only the wake-up registration takes the critical section. This is the fast path for UART-class producers and consumers (03 §6.4).

  • Wake-ups. A write that raises the fill past a blocked reader’s min_len wakes it with hand-off of the available count (the reader then copies in its own context, so no data copy is attributed to the writer); a read that frees space wakes the first blocked writer. Readers are served in wait order; a blocked reader keeps its position until satisfied or timed out.

  • Binding fires when the fill rises from below notify_trigger to at least it, unless a blocked reader consumed the transition.

  • Close stops writers (EMB_ESTATE), wakes blocked writers with EMB_ESTATE, and lets readers drain. Reset discards the contents, wakes every waiter with EMB_ESTATE, and reopens the pipe.

4. Buffer pool

4.1 Interface

typedef struct emb_pool_attr {
    const char *name;
    void       *storage;        /* block_count * block_size bytes, aligned to EMB_POOL_ALIGN */
    uint16_t    block_size;     /* >= sizeof(void *) and a multiple of EMB_POOL_ALIGN */
    uint16_t    block_count;
    uint8_t     flags;          /* EMB_OBJ_ABORT_WAITERS | EMB_OBJ_FIFO */
} emb_pool_attr_t;

#define EMB_POOL_STORAGE(name, block_size, block_count)

emb_status_t emb_pool_init(emb_pool_storage_t *storage, const emb_pool_attr_t *attr, emb_pool_t *out);
emb_status_t emb_pool_destroy(emb_pool_t p);
emb_status_t emb_pool_alloc(emb_pool_t p, emb_timeout_t timeout, void **out_block);     /* @ctx thread; thread isr with EMB_NO_WAIT  @time O(1) */
emb_status_t emb_pool_alloc_until(emb_pool_t p, emb_instant_t deadline, void **out_block);
emb_status_t emb_pool_free(emb_pool_t p, void *block);                                   /* @ctx thread isr  @time O(1) */
emb_status_t emb_pool_transfer(emb_pool_t p, void *block, emb_thread_t to);              /* @ctx thread isr  checked builds: move ownership */
uint16_t     emb_pool_available(emb_pool_t p);
emb_status_t emb_pool_bind_notify(emb_pool_t p, emb_thread_t t, emb_notify_bits_t bit);            /* exhausted -> available */

4.2 Semantics

  • The free list is intrusive through the first word of each free block: alloc and free are O(1) (KRN-IPC-007). block_size is at least a pointer and a multiple of the alignment; EMB_POOL_STORAGE() declares correctly sized storage.

  • alloc on an exhausted pool blocks on the pool’s wait queue; free with a waiter hands the block to the first waiter (hand-off, no free-list traffic, no binding bit); free without a waiter pushes the block and, if the pool was exhausted, signals the binding.

  • free of a pointer outside the pool’s storage, misaligned, or already free (checked builds keep a free bitmap) is misuse (EMB_FAULT_API_ARGUMENT, EMB_EINVAL).

  • Destroy with blocks outstanding is misuse (EMB_EBUSY): the kernel cannot reclaim memory it does not own.

4.3 Ownership (zero copy)

  • In checked builds every block carries an owner: the allocating thread, or IN_QUEUE while it travels in an EMB_MSGQ_OWNERSHIP queue, or the thread named by emb_pool_transfer. free and transfer by a non-owner, and send of a block the sender does not own, fault (EMB_FAULT_API_OWNER); release builds track nothing and pay nothing (KRN-IPC-006).

  • The rule for application code is the one 03 §6.5 states: after sending a block, the sender no longer touches it; the receiver frees it or sends it on. emb_pool_transfer covers hand-over paths that do not go through a queue (a callback that will free the block).

  • A thread that terminates while owning blocks (checked builds) is a lifecycle fault in the same way as a mutex owner (KRN-SYNC-025 pattern); release builds leak the block, which the statistics of §8 expose as “blocks outstanding”.

5. Ports (FUTURE)

A port is the cross-partition and cross-core message endpoint of 03 §6.6. It is not specified for 1.0; this section fixes only what earlier specifications already decided so that the queue API does not drift away from it:

  • A port presents send, receive, timeout, wake, and binding semantics identical to a message queue (KRN-IPC-008); within one image and partition a port is a message queue.

  • A request may carry up to CONFIG_EMB_PORT_MAX_LEASES lease descriptors over the client’s memory; the server accesses leased memory through validating kernel calls while the client is blocked in the request; the client’s wake revokes every lease (ADR-032, KRN-IPC-009). Messages up to the copy threshold (default 64 bytes, the same CONFIG_EMB_MSGQ_MAX_ITEM) are copied.

  • A server may run on the client’s budget across a port (ADR-029 donation, FUTURE).

  • Cross-core transport: a shared-memory ring plus a doorbell interrupt (04 §8.2).

6. Choosing among them

Need

Use

Completion flag from an ISR

notification (SPEC-006)

Small fixed records, several producers or consumers

message queue

Records larger than 64 bytes, or a DMA destination

buffer pool block, pointer through an ownership queue

Byte stream from a UART-class source

pipe, EMB_PIPE_SPSC when one producer and one consumer

Several sources into one consumer

bindings on each source, one notification wait

Across partitions or cores

port (FUTURE)

7. Misuse and checked-build diagnostics

Condition

Checked build

Release build

item_size zero or above CONFIG_EMB_MSGQ_MAX_ITEM; misaligned or undersized ring; min_len > len or zero

fault EMB_FAULT_API_ARGUMENT

EMB_EINVAL

blocking form from an ISR without EMB_NO_WAIT

fault EMB_FAULT_API_CONTEXT

EMB_EPERM

free, transfer, or ownership send by a non-owner; double free; pointer outside the pool

fault EMB_FAULT_API_OWNER or _ARGUMENT

EMB_EPERM / EMB_EINVAL (release builds do not detect ownership)

second writer or reader on an EMB_PIPE_SPSC pipe

fault EMB_FAULT_API_CONTEXT

undefined (documented)

write to a closed pipe; read of a closed, drained pipe

runtime condition

EMB_ESTATE

destroy with waiters without ABORT_WAITERS; pool destroy with blocks outstanding

fault EMB_FAULT_API_LIFECYCLE

EMB_EBUSY

ring or free-list corruption detected

fault EMB_FAULT_KERNEL_INVARIANT

undefined

8. Observability

Trace events: msgq_send(q, handed_to | slot), msgq_receive(q, from_slot | handed_from), msgq_full_block(q, thread), pipe_write(p, n), pipe_read(p, n), pipe_close(p), pool_alloc(p, block, thread), pool_free(p, block), pool_transfer(p, block, to). Statistics (optional): per queue and pipe, high-water occupancy, blocked-send count; per pool, minimum availability and blocks outstanding; the debug descriptor exports the ring and free-list layout so a debugger can list a queue’s contents and a pool’s owners.

9. Tiny profile

The target tiny configuration makes message queues and pools available once implemented (uint8_t counts when CONFIG_EMB_IPC_SMALL=y); pipes are off by default; CONFIG_EMB_MSGQ_MAX_ITEM defaults to 16; ownership tracking exists only in checked builds and costs nothing otherwise.

10. Reference model

Message queues repeat the semaphore pattern on two wait queues with hand-off in both directions; they are added to tools/model when the conformance tests for them are written (M2), with the property “every sent item is received exactly once or remains in the ring” mirroring the semaphore’s unit conservation. Pools likewise (“every block is owned by exactly one party or free”). Pipes are not modeled: their correctness properties are byte conservation and ordering, which the conformance suite checks directly.

11. Decisions taken at acceptance (2026-10-07)

  1. Message queues copy by value with the copy inside the critical section, bounded by CONFIG_EMB_MSGQ_MAX_ITEM (default 64, tiny 16). Larger payloads travel as pool blocks by pointer.

  2. Direct copy into a waiting receiver and slot hand-off to a waiting sender; a woken thread never re-checks.

  3. send_front is EMB_NO_WAIT only.

  4. Pipes copy in chunks of CONFIG_EMB_PIPE_CHUNK (default 32) under the critical section; writes longer than a chunk may interleave with other writers; EMB_PIPE_SPSC gives the lock-free copy path with one promised writer and reader.

  5. Pipe reads take a per-call min_len; the binding trigger is a per-pipe attribute.

  6. A closed pipe drains then returns EMB_ESTATE; reset wakes waiters with EMB_ESTATE and reopens.

  7. Buffer pools are intrusive O(1) free lists; ownership is tracked in checked builds only, including the IN_QUEUE state and emb_pool_transfer.

  8. No mailbox type: a message queue of pointers, or an ownership queue, is the mailbox.

  9. Ports stay FUTURE; §5 fixes only the compatibility constraints already decided.

  10. Message queues and pools join the reference model with their conformance tests in M2; pipes are not modeled.