L4 — Liedtke 用 12KB 内核反驳"微内核必然慢"

是什么

L4 是 1993-1995 年 Jochen Liedtke 在德国 GMD 写的第二代微内核。论文用一句话总结：微内核慢不是因为架构，是因为之前的人写得不好。

日常类比：1990 年前后业界已经判了微内核”死刑”——大家觉得”消息传递这条路就是慢”。Liedtke 像一个赛车工程师跑去说：“你们的车不是设计有问题，是火花塞、轮胎、变速箱全都凑合用——我重做一遍，跑给你们看”。结果他做的 L4 IPC 在 486 上跑出 5 µs（约 250 个 CPU cycle），比当时最有名的 Mach 微内核快 20 倍。

整个 L4 微内核源码加起来约 12 KB——比 Mach 小 25 倍，比 Linux 内核小四个数量级。

为什么重要

不理解 L4，下面这些事都没法解释：

为什么 1990s 末业界突然又开始相信微内核——L4 用数据砸醒了所有人
为什么 seL4（2009 年第一个被数学证明完全正确的内核）能存在——因为 L4 把内核做得足够小，证明才在工程上可行
为什么手机基带处理器、汽车 ECU、Apple Secure Enclave 跑的都是类 L4 微内核——TCB（trusted computing base）小才好审计
为什么”microkernel vs monolithic”这场争论 30 年还没死——L4 把”微内核必然慢”这个判决推翻后，争论就变成了”哪种更值得”

核心要点

L4 的设计哲学可以拆成三块：

最小性原则：一个东西能放在内核外，就放在外面。判断方法是问”把它拿出去，系统还能不能完成必需功能？能拿出去就拿”。这条原则替代了 Mach 时代”什么有用就放进去”的工程惯性。
三件事必须留在内核里：地址空间（address space）、线程与 IPC、唯一标识符（unique identifier）。Liedtke 论证：这三样如果放外面，性能或安全有一样会塌。其余一切（驱动、文件系统、网络栈、调度策略）都做成用户态服务。
处理器特定性是必需，不是缺陷：L4/x86 和 L4/Alpha 内部实现完全不同才正常。Mach 追求”一份代码跨架构”，结果每个架构都不快；L4 给每个 ISA 重写关键路径，反而每个架构都跑到极限。

三块加起来叫 第二代微内核。

实践案例

案例 1：IPC 怎么从 100 µs 砍到 5 µs

Mach IPC 慢的根源：消息走内存 buffer、过 scheduler 选下一个线程、地址空间切换刷 TLB。每一步都是几百 cycle。

L4 的优化（每条都对应一项硬件细节）：

短消息走寄存器：≤ 8 word 的消息直接塞进 EAX/EBX/ECX 等 CPU 寄存器，receiver 从寄存器里读。不走内存，不存在 cache miss。
direct process switch：sender 调 IPC 时，内核不回去问 scheduler”下一个跑谁”，直接把 CPU 给 receiver。省掉调度开销。
small address space 复用 TLB：x86 段寄存器允许多个进程共享同一张 page table，仅靠段隔离。切进程不刷 TLB，省下几千 cycle。
关键路径手写汇编：IPC fastpath 全部用汇编写死，约 100 行。每条指令都被数过。

结果：486DX-50 上完整 IPC 往返 10 µs，单向 5 µs，约 250 个 CPU cycle。

案例 2：最小性原则怎么用

考察”是否把分页（paging）放进内核”:

拿出去会怎样：用户态 pager 接收 page fault 消息 → 决定从哪里加载页 → 通过 IPC 告诉内核映射哪一页。
系统功能受影响吗：不受影响。内核只需要”能在被告知时把 X 页映射到 Y 地址”，至于策略（LRU/FIFO/工作集）完全可以放外面。
结论：分页策略留在用户态，内核只保留机制。

这就是 mechanism vs policy 的彻底分离，也是 L4 比 Mach 小 25 倍的关键来源。

案例 3：内核大小为什么这么夸张地小

L4 全部代码 ≈ 12 KB（含所有架构相关的汇编）。对比：

Mach 3.0：约 300 KB
Linux 1.0（同期 1994）：约 170 KB（仅 kernel 核心）
现代 Linux：> 30 MB

为什么 L4 能这么小？因为它只做三件事：切地址空间、切线程、传消息。文件系统？用户态。网络？用户态。驱动？用户态。看起来”什么都没有”，但这正是 Liedtke 想要的：内核越小，TCB 越小，性能越能压榨到硬件极限。

案例 4：Liedtke 是怎么想到这些的

Liedtke 不是从理论出发，而是从 cycle 计数倒推架构。论文里有大段表格列出”在 486 上，写一个寄存器要几 cycle，TLB miss 要几 cycle，segment register reload 要几 cycle”。然后他把 IPC 拆成一长串硬件操作，每一项问”能不能省”。

这种”先量化每条硬件指令的成本，再决定架构”的工作方式，今天看叫 mechanical sympathy（与机器共情），是 high-performance 系统编程的核心姿态。Linux 调度器、Java HotSpot、Redis 单线程模型、Disruptor lock-free 队列，全都是同一个套路的产物。

踩过的坑

“L4 论文是首次提出微内核”——错。微内核概念 1970 年 Brinch Hansen 就有了，Mach 1986 已经成型。L4 的贡献是救活这个被业界判死的方向，不是发明它。
“微内核因消息传递所以慢”——L4 实测反驳。消息传递本身不慢，慢的是粗糙实现。Liedtke 在论文里花 1/3 篇幅做 cache、TLB、register 的微观分析，证明”100 cycle IPC”是硬件允许的。
L4 数据被质疑过。早期测试是单核、小工作集；多核 + 大数据场景下与 Linux 差距没那么戏剧化。但 sel4（L4 后代）在 2010s 重新做的多核测试仍然显示微内核可以打平 Linux。
小 address space 这招只在 x86 段式架构成立。换到 ARM、Alpha 就要换实现——这恰好印证了 Liedtke 的”处理器特定性是必需”主张。
“L4 IPC 5 µs 所以可以做通用 OS”——结论太快。L4 证明了”足够快”，但没证明”生态能起来”。30 年过去，桌面/服务器仍是 monolithic Linux 的天下。L4 的真正主场是嵌入式 + 安全场景，那里 12 KB 内核 + 可证明性的价值远大于”驱动多不多”。
微内核的 IPC 快也救不了 monolithic 系统调用慢。这是后来 Linux 阵营的反击：你 IPC 5 µs 我 syscall 1 µs，凭什么要切？这场争论今天演化成 io_uring、eBPF、user-space 网络栈等”在 Linux 内做微内核优化”的方向。

适用 vs 不适用场景

适用：

高安全场景（航天、军用、金融 HSM、汽车 ECU）——TCB 小才好审计/认证
需要形式化验证的系统（seL4 是 L4 的直系后代）
嵌入式实时系统（QNX、PikeOS 都是类 L4 思路）
虚拟化平台底座（早期 Xen 借鉴了 L4 的 IPC 路径）

不适用：

通用桌面/服务器 OS（Linux 生态太强，重写所有驱动不现实）
性能瓶颈在 CPU 计算而非系统调用的负载（HPC、批处理）——微内核优势体现不出来
团队没有汇编+硬件调优能力——L4 的快是手工抠出来的，照搬代码不会自动快

历史小故事（可跳过）

1986：CMU 发布 Mach，第一代微内核标杆。OSF/1 商业化。
1990-1992：Mach 性能差被业界普遍接受。HURD 项目延期。学界出现”微内核已死”的论调。
1993：Liedtke 在 GMD 写出 L3，IPC 已显著快于 Mach。
1995：SOSP 发表 “On µ-Kernel Construction”，L4 IPC 5 µs，差距拉开 20 倍。论文成为微内核复兴的转折点。
2009：NICTA 团队基于 L4 思路写出 seL4，并用 Isabelle/HOL 给出机器证明——首个被严格证明正确的通用 OS 内核。
2014 至今：seL4 进 OKL4，部署在 20 亿+ 设备的基带和 TEE 上。Liedtke 2001 年因白血病去世，没看到这一天。

现代回响

虽然 L4 论文是 1995 年的，但它的影响在今天反而更密集：

seL4 (2009)：L4 的形式化验证版，是世界上第一个被数学证明完全正确的通用 OS 内核。能做到这一点的前提就是 L4 把内核做得足够小。
OKL4 / Apple Secure Enclave / Google Trusty TEE：手机里那颗”专门管指纹和加密”的小处理器，跑的就是类 L4 微内核。全球部署量超过 20 亿台。
Fuchsia / Zircon：Google 下一代 OS 内核，思路上明显继承 L4——尽量小、message-passing 为核心、capability-based 安全。
虚拟化与 unikernel：Type-1 hypervisor（Xen 早期）、unikernel（MirageOS）、library OS 都把”最小 TCB”作为核心卖点，Liedtke 的最小性原则是它们的共同祖师。

值得记的一件事：Liedtke 2001 年因白血病去世，48 岁。他没看到 seL4 的证明完成（2009），也没看到自己的设计跑在 20 亿台设备上。但他在 1995 年那篇 12 页的论文，几乎一手扭转了一个领域的走向。

学到什么

架构论辩离不开实现质量——Liedtke 最深的洞见：你不能脱离硬件谈”X 必然慢”，得把 X 写到极限再下结论。
最小性原则是可操作的工程判据：能拿出去就拿出去，反过来就是”特性蔓延”的天然刹车。
机制 vs 策略的分离不是哲学口号，是 TCB 减小的具体路径。L4 把 paging 策略踢出内核，立刻少 100+ KB 代码。
处理器特定性 vs 可移植性没有标准答案——L4 选了”每个 ISA 重写关键路径”，换来 20 倍性能。Mach 选了反向，被淘汰。
从硬件 cycle 倒推架构是高性能系统编程的根本姿态。先数清楚每条指令几 cycle，再讨论架构能不能成立——而不是反过来。

关联

mach-1986 —— Mach 第一代慢，L4 第二代快 20 倍，是微内核两个时代的分水岭
hyperkernel-2017 —— 受 seL4 影响的可验证 hypervisor，继承”小内核才能证明”的传统
certikos-2016 —— 同为形式化验证内核，与 seL4 是 L4 思路的两条平行后代
the-os-1968 —— THE 系统的”分层”思想是微内核哲学的远祖
paxos-1998 —— 同样是”先把假设打碎，再用工程证明”的论文风格
ssa —— 同时代另一个”看似学术，其实彻底改变工业”的概念