Synchronous IPC
Synchronous inter-process communication (IPC) is a message-passing primitive in which the sender blocks until a receiver is ready to take the message, and the receiver blocks until a sender produces one. The kernel never buffers the payload; on the rendezvous, it copies a small message directly from one thread’s registers (or address space) into the other and unblocks both. The seL4 reference manual states it plainly: “IPC Endpoints uses a rendezvous model and as such is synchronous and blocking… message delivery only happens if a sender and a receiver rendezvous at the endpoint, and the kernel can deliver the message with a single copy (or without copying for short messages using only registers)” (seL4 reference manual §4.2). Jochen Liedtke made the argument concrete in 1993 by showing that a carefully implemented synchronous IPC on a 486DX-50 took 5 µs end to end, where Mach 3’s IPC on the same hardware took 115 µs (Liedtke, “Toward Real Microkernels,” CACM Sept 1996). Twenty years later, seL4’s hand-tuned fast path on an ARM11 hit a one-way cost of 188 cycles (Elphinstone & Heiser, “From L3 to seL4,” SOSP 2013, Table 1). The L4 family kept synchronous IPC as the only original communication primitive precisely because Liedtke argued it was the only one that could be made fast enough to justify the microkernel architecture; almost every microkernel-class system in production today (seL4, QNX Neutrino, OKL4 in its earlier generations, Fiasco.OC) descends from that decision.
Mental Model
The rendezvous is best read as a handshake at a shared meeting point, not as a queue. Whichever party arrives first pays the cost of waiting; whichever arrives second pays the cost of the actual transfer. The kernel maintains exactly one queue per endpoint, and at any moment the queue holds either blocked senders or blocked receivers, never both. As soon as the other party shows up, the kernel pairs them, copies the payload directly (sender’s context to receiver’s context), marks both threads runnable, and returns. There is no in-kernel mailbox.
sequenceDiagram autonumber participant S as Sender thread participant K as Microkernel<br/>(endpoint queue) participant R as Receiver thread Note over S,R: Case A: receiver arrives first R->>K: seL4_Recv(ep) K-->>R: block, enqueue on ep.recv_queue S->>K: seL4_Send(ep, msg in regs) K->>K: dequeue R, copy regs S→R,<br/>transfer badge, mark both runnable K-->>R: unblock with msg + badge K-->>S: unblock (send completed) Note over S,R: Case B: sender arrives first S->>K: seL4_Send(ep, msg in regs) K-->>S: block, enqueue on ep.send_queue R->>K: seL4_Recv(ep) K->>K: dequeue S, copy regs S→R,<br/>transfer badge, mark both runnable K-->>S: unblock (send completed) K-->>R: unblock with msg + badge
The rendezvous protocol of synchronous IPC, in the form used by seL4 and the L4 family. What it shows: there are exactly two interleavings of any synchronous IPC. Whichever party arrives first blocks and is enqueued on the endpoint; whichever arrives second triggers the actual transfer, which is a single in-kernel copy of the register payload (plus, optionally, an immutable badge that identifies the capability the sender invoked). The kernel does not own any of the data; it owns only the queues and the scheduling state. The insight to take: there is no buffering anywhere. The cost of the IPC is one queue manipulation plus one register-to-register copy plus a direct process switch to whichever side runs next.
What “Synchronous” Means Precisely
Three independent properties of an IPC mechanism get confused under the single word “synchronous.” It is worth pulling them apart:
- Blocking vs non-blocking. A blocking send waits if no receiver is ready. A non-blocking send returns immediately, succeeding or failing. seL4 exposes both flavors against the same endpoint:
seL4_Sendblocks,seL4_NBSend“performs a polling send on an endpoint. If the message cannot be delivered immediately, i.e., there is no receiver waiting on the destination Endpoint, the message is silently dropped” (seL4 reference manual §2.2). - Unbuffered (rendezvous) vs buffered (queued). A rendezvous mechanism owns no per-message storage in the kernel: it pairs a live sender with a live receiver, copies once, and is done. A queued mechanism (POSIX message queues, Mach ports, MPI buffered send) owns kernel storage in which messages sit while waiting for a consumer. Mach famously paid a large performance penalty for being queued; L4 made the opposite choice.
- One-way vs two-way (call/reply). A pure one-way send delivers the message and is done. A call combines send-then-receive-reply into a single primitive (
seL4_Call), which the kernel optimizes by reusing the caller’s scheduling slot for the callee (a direct process switch) and by stamping a single-use reply capability into the callee’s TCB so that the reply path is unforgeable (seL4 reference manual §4.2.4; Elphinstone & Heiser §4.3).
The phrase “synchronous IPC” in the L4 lineage means the conjunction blocking AND unbuffered; orthogonally, the primitive may be one-way (Send/Recv) or two-way (Call/ReplyRecv). OKL4 took a different path and dropped synchronous IPC entirely in favor of asynchronous notifications plus a separate bulk channel; QNX kept synchronous MsgSend/MsgReceive/MsgReply as the kernel’s only message primitive. The variance among modern systems is real.
The L4 Argument: Why Sync IPC Won
Liedtke’s 1996 CACM article articulated the argument that defined the second-generation microkernel field. The first-generation systems (Mach, Chorus) had IPC costs around 100 µs per call on contemporary 486 hardware, with a corresponding 50-66% application slowdown in benchmarks like AIM III and Chen-Bershad’s SOSP’93 study (Liedtke 1996). The conclusion at the time was that microkernels were fundamentally slow. Liedtke’s reply was that the slowness was an implementation defect, not an architectural property, and that the way to demonstrate it was to build a kernel whose only communication mechanism was a synchronous rendezvous and to drive its cost down to single-digit microseconds.
The argument for synchronous-only had four legs.
First, no kernel buffering. A queued IPC has to own memory for in-flight messages, which means it has to either pre-allocate a worst-case quota per client (expensive on small systems) or risk denial-of-service when one process floods another. A rendezvous never owns the data; the kernel touches only the queues of blocked threads and the registers that hold the payload. Liedtke noted that L4 in 1995 fit in 12 KB of code total (Liedtke 1996); a queued IPC alone would not have fit.
Second, single copy. The kernel runs in the sender’s context, looks up the destination thread, and copies the message directly from the sender’s registers (or address space) into the receiver’s. There is no intermediate buffer. For short messages this becomes zero-copy: the message lives in CPU registers throughout, and the kernel hands those registers across the context switch without ever writing them to memory.
Third, fast scheduling. With a queued IPC, every send requires the kernel to consult the scheduler (“which thread runs next?”). With a rendezvous, the answer is usually obvious: a send unblocks exactly one waiting receiver, and a Call from a higher-priority caller naturally hands its time slice to the callee. This is the direct process switch optimization, used by every L4-family kernel since the original (Elphinstone & Heiser §4.3).
Fourth, simple kernel state. Each endpoint is one queue head and a flag bit (“is this queue currently senders or receivers?”). No buffers, no head/tail pointers, no overflow logic. This matters acutely for formal verification: seL4 verifies roughly 10,000 lines of C against a 500,000-line Isabelle proof (Klein et al., “seL4: Formal Verification of an OS Kernel,” SOSP 2009), and the verification team explicitly cited synchronous IPC’s lack of in-kernel buffering as a reason the proof was tractable at all (Elphinstone & Heiser §3.2.2).
The numbers vindicated the argument. Liedtke’s L4 (1993) did an 8-byte one-way IPC in 5 µs on a 486DX-50, where Mach 3 took 115 µs on the same hardware (Liedtke 1996). The L3-to-seL4 retrospective tabulates the evolution across 20 years and many CPUs (the cycle counts being the more invariant measure since absolute time tracks CPU frequency):
| Kernel | Year | CPU | MHz | Cycles | µs |
|---|---|---|---|---|---|
| Original L4 | 1993 | i486 | 50 | 250 | 5.00 |
| Original L4 | 1997 | Pentium | 160 | 121 | 0.75 |
| L4/MIPS | 1997 | R4700 | 100 | 86 | 0.86 |
| L4/Alpha | 1997 | 21064 | 433 | 45 | 0.10 |
| Pistachio | 2005 | Itanium 2 | 1500 | 36 | 0.02 |
| OKL4 | 2007 | XScale 255 | 400 | 151 | 0.64 |
| seL4 | 2013 | ARM11 | 532 | 188 | 0.35 |
| seL4 | 2013 | Cortex-A9 | 1000 | 316 | 0.32 |
| seL4 | 2013 | Core i7 4770 (Haswell) | 3400 | 301 | 0.09 |
Source: Elphinstone & Heiser, “From L3 to seL4,” SOSP 2013, Table 1.
The salient observation: a verified C kernel with full capability-based access control on a modern ARM core delivers a synchronous IPC in around 200 cycles, which is in the same order of magnitude as a Linux system call (which has no protection-domain crossing) and substantially cheaper than the Mach RPC that originally killed the microkernel idea.
The seL4 Fast Path, Step by Step
The seL4 fast path is the most-tuned synchronous IPC implementation in the public literature. It is the canonical reference for what a sync-IPC primitive actually does in execution. The kernel attempts the fast path on every IPC call; if any precondition fails (the wrong message length, a present capability transfer, a destination thread of different priority), it falls back to the general slow path. The fast path is written in carefully ordered C with manual hints for the optimizer (Elphinstone & Heiser §4.7).
The steps for a one-way Send over an endpoint capability are:
- Trap entry. The user thread issues the system call. On ARM, this is
svc 0; on RISC-V,ecall. The CPU jumps to the kernel’s vector with the syscall number in a register and the IPC arguments in the message registers (typically the first 4 to 8 GPRs, see seL4 reference manual §4.1). - Capability lookup. The caller has named the destination by a capability pointer (CPtr), which is an integer indexed into the caller’s CSpace. The kernel walks the guarded-page-table CSpace structure (typically 1-3 nodes deep, fits in L1 cache for a hot client) to resolve the CPtr to the Endpoint capability (seL4 reference manual §3.3). Crucially the kernel checks the rights bits on the capability (Write for send, Read for receive, Grant for capability transfer).
- Endpoint state check. Read the endpoint object. If the endpoint has receivers blocked, the fast path can proceed. If it has senders blocked or is idle, the fast path bails out: a send with no receiver must enqueue the sender, which involves more state.
- Pair with the head receiver. Dequeue the first receiver from the endpoint’s queue. Note this is a TCB pointer, not a thread ID; seL4 stores TCBs at physical addresses, so the dereference is one load.
- Badge transfer. The endpoint capability the sender invoked may have been minted with a badge, an unforgeable per-capability tag (a 28-bit word on 32-bit platforms, 64 bits on 64-bit; seL4 reference manual §4.2.1). The kernel writes that badge into the receiver’s badge register, giving the receiver an integrity-protected indication of which capability the sender used. This is how a multi-client server tells its clients apart without needing per-client endpoints.
- Message-register copy. Copy the sender’s message registers (the message tag plus the first N message-register words, where N is the count carried in the tag) into the receiver’s message-register positions. On register-rich architectures, “copy” means renaming: the sender’s GPRs become the receiver’s GPRs across the context switch, with no memory traffic. On register-starved architectures (32-bit x86), the kernel spills some message registers to a per-thread IPC buffer page that is pinned in memory (Elphinstone & Heiser §3.2.2).
- Direct process switch. Mark the sender runnable (the send completed instantly) and the receiver running. Restore the receiver’s saved state (most of which is already in registers from step 6), update
current_thread, and execute the trap-return that the receiver would have done from its ownRecv. The scheduler is not invoked; the caller’s time slice is reused for the callee. - Trap exit into the receiver. The next instruction the CPU executes is the one after the receiver’s
Recvsyscall, with the message visible in its registers.
The whole path is roughly 200-300 instructions on a modern ARM core. Cache-line counting matters more than instruction counting: the hot path touches the sender’s TCB, the receiver’s TCB, the endpoint, the CSpace nodes for capability lookup, and the relevant page tables, which can fit in a small fixed L1 working set if the threads communicate frequently. This is the reason seL4 IPC numbers are reported in CPU cycles, not microseconds.
Configuration and Code: A Skeleton Synchronous IPC Implementation
A pared-down rendezvous implementation in Rust for a small RV32IMC microkernel, with the fast-path structure mirroring seL4’s:
pub struct Endpoint {
/// Either a list of blocked senders OR a list of blocked receivers.
/// Never both at once; the discriminant is implicit in the enum.
state: EndpointState,
}
enum EndpointState {
Idle,
SendersBlocked(LinkedList<TcbPtr>), // queue head/tail of senders
ReceiversBlocked(LinkedList<TcbPtr>), // queue head/tail of receivers
}
pub fn ipc_send(ep: &mut Endpoint, sender: TcbPtr, msg: &Message, badge: Badge) {
match &mut ep.state {
// Fast path: a receiver is already waiting.
EndpointState::ReceiversBlocked(q) => {
let receiver = q.pop_front().unwrap();
// Single copy: drop the message into the receiver's TCB.
receiver.msg_regs.copy_from(&msg);
receiver.badge_reg = badge;
receiver.state = Runnable;
sender.state = Runnable; // send completed
if q.is_empty() {
ep.state = EndpointState::Idle;
}
// Direct process switch: hand the CPU to receiver immediately.
switch_to(receiver);
}
// Slow path: no receiver. Block the sender on the endpoint.
EndpointState::Idle | EndpointState::SendersBlocked(_) => {
sender.pending_msg = msg.clone(); // stash in sender's own TCB
sender.pending_badge = badge;
sender.state = Blocked(BlockedOn::Endpoint(ep_ptr()));
ep.state.enqueue_sender(sender);
// Sender blocks: let the scheduler pick someone else.
scheduler::reschedule();
}
}
}
pub fn ipc_recv(ep: &mut Endpoint, receiver: TcbPtr) -> (Message, Badge) {
match &mut ep.state {
// Fast path: a sender is already waiting.
EndpointState::SendersBlocked(q) => {
let sender = q.pop_front().unwrap();
let msg = sender.pending_msg.take();
let badge = sender.pending_badge;
sender.state = Runnable; // send completed
if q.is_empty() {
ep.state = EndpointState::Idle;
}
(msg, badge)
}
// Slow path: block the receiver.
EndpointState::Idle | EndpointState::ReceiversBlocked(_) => {
receiver.state = Blocked(BlockedOn::Endpoint(ep_ptr()));
ep.state.enqueue_receiver(receiver);
scheduler::reschedule();
// When we are unblocked, the sender will have written into us.
(receiver.msg_regs.take(), receiver.badge_reg)
}
}
}Line-by-line: the Endpoint holds one queue, with the kernel implicitly knowing whether that queue is senders or receivers. The fast path for Send is the case where a receiver is already blocked. The kernel copies the message directly into the receiver’s TCB (which doubles as its message buffer when blocked) and switches to it without going through the scheduler. The slow path stashes the message in the sender’s own TCB and blocks the sender; when a receiver eventually arrives, it will pull the message from there. There is no separate kernel buffer at any point; total per-endpoint state is one queue head and the discriminant. This is roughly the structure of seL4’s endpoint.c (seL4 reference manual §4.2).
The optimized real seL4 version adds: a hand-unrolled fast path before this match (with the receiver-blocked case open-coded), badge transfer happening before scheduling state changes (so misordering does not race), and tail-call elision into the user-mode-return assembly. The whole hot path is around 9,000 ARM instructions of compiled kernel (Elphinstone & Heiser §3.1, footnote 4).
Comparison with Asynchronous and Channel-Based IPC
Synchronous IPC is one design point among several; the others are worth understanding because they trade away different properties.
Asynchronous notifications (seL4’s Notification objects, OKL4’s virtual IRQs, Mach’s notification messages) are non-blocking, non-buffered, and lossless in the bit-OR sense: a seL4_Signal sets bits in a per-notification word with no rendezvous. “The seL4_Signal() method updates the notification word by bit-wise or-ing it with the badge of the invoked notification capability. It also unblocks the first thread waiting on the notification (if any)” (seL4 reference manual §5.2). Asynchronous is the right primitive for interrupt delivery, for “wake me when any of these events occur” semantics, and for producer-consumer where the consumer can be slow without blocking the producer. The cost is that no payload travels along with the signal; you get a bit, not a message. seL4 explicitly added asynchronous notifications in the L4-embedded fork because pure synchronous IPC “forces a multi-threaded design onto otherwise simple systems, with the resulting synchronisation complexities” (Elphinstone & Heiser §3.2.1).
Queued message passing (POSIX mq_send, Mach ports, MPI’s buffered send mode) buffers messages in the kernel. The producer never blocks (until the queue fills); the consumer can collect at its leisure. The cost is exactly what Liedtke spent his career attacking: per-message kernel allocation, per-port quota, denial-of-service exposure when one client fills a server’s port, and the impossibility of single-copy delivery (the kernel has to allocate a buffer, copy in, and later copy out). Mach 3’s IPC was queued; its 115 µs per call was the inevitable consequence (Liedtke 1996).
Channels (Go channels, occam-2’s chan, Erlang process mailboxes, OKL4’s channel) are higher-level abstractions that may be implemented over either primitive. Go channels are user-space queued; occam channels are synchronous rendezvous in the CSP tradition; Erlang mailboxes are explicitly asynchronous and per-process. The word “channel” carries no inherent semantics about blocking, buffering, or copying; pinning down what a given system’s channel actually does requires reading the runtime.
Shared memory plus a doorbell is the standard alternative for high-bandwidth transfer. The two processes establish a shared physical page (in seL4, by retyping an Untyped memory frame and granting the receiver a Frame capability with the same physical backing). The producer writes the payload directly into the shared region and signals the consumer via either an asynchronous notification or a zero-byte synchronous IPC. The advantage is bulk transfer at memory-copy speed without per-byte kernel cost; the disadvantage is that the consumer must trust the producer (or impose its own format-validation overhead), and the protocol on top of the shared region (ring buffer, double-buffer, lock-free queue) is now user-space code. Modern microkernel systems lean on this pattern heavily: small control messages go over synchronous IPC; bulk data goes over shared memory with a sync-IPC doorbell.
The L4-family arc is informative. Original L4 had only synchronous IPC, with “long IPC” as an extension for messages exceeding the register file. L4-embedded (2003) removed long IPC because the temporary-mapping window it required was a verification disaster (Elphinstone & Heiser §3.2.2). seL4 added asynchronous notifications because pure sync IPC had forced multi-threading on every server. OKL4 dropped synchronous IPC entirely in favor of asynchronous notifications plus a separate channel for bulk transfer. NOVA added counting semaphores. Fiasco.OC kept both. The community’s collective conclusion across 20 years: sync IPC for control, shared memory for data, and async notification for events.
Where Sync IPC Hurts
The honest catalog of cases where rendezvous semantics are awkward or wrong.
Decoupled producer/consumer. A logging daemon that accepts diagnostic messages from many clients does not want each client to block until it consumes their message. The right primitive is a queue (the daemon owns it) or asynchronous notification (the daemon polls when convenient). Sync IPC forces either per-client buffering in the daemon (defeating the simplicity argument) or unbounded client blocking (defeating availability).
Batching. When a sender has 100 messages to ship, ten synchronous IPCs are ten kernel entries with ten context switches. A queued mechanism that lets the sender drop 100 messages with one syscall and the consumer pick them up with one syscall is dramatically more efficient. L4’s “long IPC” tried to address this; it was removed.
Multi-target broadcast. Sending a single message to N receivers under pure sync IPC requires N rendezvous, each completing only when its respective receiver arrives. There is no efficient broadcast primitive. Asynchronous notification handles this naturally (signal sets bits, wakes whoever is waiting).
Multi-core scaling. A synchronous Call from a thread on core A to a server on core B sequentialises the two cores: A blocks until B finishes. On single-core systems this was free (A was going to wait anyway), but on multi-core it wastes parallelism. Elphinstone and Heiser explicitly flag this: “the utility of synchronous IPC becomes more dubious in a multicore context: an RPC-like server invocation sequentialises client and server, which should be avoided if they are running on separate cores. We therefore expect communication protocols based on asynchronous notification to become more prevalent” (Elphinstone & Heiser §3.2.1).
Interrupt delivery. Hardware interrupts are inherently asynchronous, and the driver thread must not block the IRQ source while it processes a previous IRQ. Modern L4 kernels deliver interrupts as asynchronous notifications, not synchronous messages, even though older systems used virtual in-kernel threads to emulate sync delivery (Elphinstone & Heiser §3.3).
The Rendezvous Heritage: CSP, occam, Ada (and Why Erlang Is Not in This List)
The rendezvous semantics in synchronous IPC come straight out of C.A.R. Hoare’s Communicating Sequential Processes (1978). CSP defined concurrent computation as a network of processes that share no memory and communicate by named channels; the channel operation c!v (send) blocks until a matching c?x (receive) is ready, at which point the value transfers atomically and both processes continue. The semantics are explicitly rendezvous; there is no buffer.
The lineage that reaches operating-system IPC:
- CSP (Hoare 1978) defined the formal model.
- occam (INMOS, 1983) was the first programming language with CSP as its concurrency model; channels used
!and?exactly as Hoare wrote them, and the transputer hardware implemented the rendezvous in microcode. - Ada 83 added the
task/accept/entryrendezvous to a mainstream language. The Ada Reference Manual is explicit: “The Ada 83 rendezvous followed CSP [Hoare 78] by providing a dynamic approach to the problem” (Ada 83 Rationale §13.3). An Ada task with anaccept E do ... end E;block blocks until another task callsT.E(...), at which point both tasks rendezvous, the body runs in the acceptor’s context with parameters from the caller, and on completion both threads resume independently. This is operationally identical to the L4 sync-IPC handshake, just at language level rather than kernel level. - L4 (Liedtke 1993) brought the rendezvous model into a microkernel as the only primitive, with the L3 predecessor having already established it informally (Liedtke 1996).
Erlang is sometimes erroneously placed in this lineage. Erlang’s process model is not rendezvous: each process owns a private mailbox, sends are asynchronous and never block, and the receiving process inspects its mailbox at its leisure with pattern matching. Erlang is the actor model (Hewitt 1973), which is the asynchronous mailbox tradition and the explicit counterpoint to CSP. If you read “Erlang rendezvous” anywhere, the author is conflating two distinct families. The actor model and the CSP model are dual: actors are named, channels are anonymous; actors buffer, channels rendezvous; actors can drop messages, channels cannot.
Modern systems shuffle the two. Go’s channels are buffered (capacity zero gives CSP rendezvous; capacity N gives bounded queue). Akka is actor-flavored on the JVM. Rust’s std::sync::mpsc is multi-producer single-consumer queue. seL4’s sync IPC is the purest expression of CSP rendezvous in any operating system today.
QNX Neutrino: The Other Synchronous-IPC Production System
QNX Neutrino has shipped synchronous IPC as its only kernel message primitive since 1980, making it the longest-running production system with rendezvous semantics. The QNX system architecture documentation states: “Message passing (as implemented in MsgSend(), MsgReceive(), and MsgReply()) is synchronous and copies data” (QNX 7.1 System Architecture), and: “the messaging services copy a message directly from the address space of one thread to another without intermediate buffering, the message-delivery performance approaches the memory bandwidth” (QNX 7.0 Sync Messaging).
QNX differs from L4 in two interesting ways. First, QNX uses a channel/connection model rather than capabilities: a server creates a channel, clients open connections to that channel, and MsgSend(connection_id, ...) resolves through the connection table. The semantics of the actual message passing are the same as L4’s. Second, QNX has historically been the cleanest commercial example of a microkernel with sync IPC: the kernel (procnto) implements only thread scheduling, IPC, interrupt dispatch, and timers. Filesystems, networking, drivers, and the resource-manager API all live in user-space processes and talk to each other over MsgSend. QNX ships in over 275 million vehicles globally as the dominant car-infotainment OS, demonstrating that synchronous IPC scales to a real production OS at industrial volume.
Production Notes
- seL4 is the formally-verified poster child. The kernel is roughly 10,000 lines of C and 600 lines of assembly; functional correctness, integrity, and confidentiality are all proven; worst-case execution time has a sound upper bound (Klein et al. SOSP’09; seL4 whitepaper). The synchronous-IPC fast path on a Cortex-A9 runs in 316 cycles (Elphinstone & Heiser, Table 1); on Haswell, 301 cycles. Used in cross-domain defence solutions, the DARPA HACMS demonstrator (where seL4 secured an unmanned helicopter against a red team in flight), and a growing set of automotive systems (seL4 whitepaper §2.2).
- OKL4 is the only commercial L4 descendant that dropped synchronous IPC. Its current generation (“OKL4 Microvisor”) uses only asynchronous notifications plus a separate single-copy channel; the rationale was that synchronous IPC’s multi-threading requirement was a poor fit for the memory-constrained mobile baseband processors OKL4 targeted. Shipped on billions of Qualcomm cellular modems and Apple’s Secure Enclave (descended from L4-embedded) (Elphinstone & Heiser §3.2.1; Wikipedia, L4 microkernel family).
- QNX Neutrino has shipped synchronous IPC since 1980, currently in roughly 275 million vehicles, in industrial control, in medical devices, and as the operating system underneath Cisco IOS XR (QNX 7.1 docs).
- Fiasco.OC (TU Dresden) is the oldest continuously maintained L4 codebase; it retains synchronous IPC and adds virtual IRQs as a separate asynchronous primitive (Elphinstone & Heiser §3.2.1).
- The definitely-not-esp32 v1.0 microkernel implements synchronous IPC as its only message-passing primitive, mirroring L4’s original design. Endpoints are unbuffered, payloads are register-only (no IPC buffer page in v1.0 since payloads stay within the eight RISC-V argument registers
a0-a7), badges are 28-bit values transferred on send, and the fast path uses direct process switch from sender to receiver without consulting the scheduler. Asynchronous notification and shared-memory channels are explicit v2.0 stretch goals; v1.0 commits to “correct sync IPC and nothing else.” The whole IPC subsystem fits in roughly 400 lines of Rust.