Anil Madhavapeddy 谈 MirageOS 与操作系统的演进

Ron Minsky 欢迎系统研究者、工程师和长期合作者 Anil Madhavapeddy 做客。两人与 Jason Hickey 合著了 Real World OCaml。他们首先讨论 MirageOS，这是 Madhavapeddy 探索更安全地构建互联网基础设施时开发的项目。

Madhavapeddy 回忆 2000 年代初，互联网蠕虫利用主要由 C 编写的系统中的缓冲区溢出和其他内存错误。作为剑桥大学的研究生，他希望用高级语言重写常见互联网协议，同时保留 Unix 编程的实用特性。

他选择 OCaml，因为它支持原生编译、容易调试，并有一层轻量的操作系统接口。他用 OCaml 重写 DNS 和 SSH，发现它们的性能可以与 C 实现相当，同时允许利用模型检查和早期验证技术进行高层推理。

但编译器仍然生成依赖庞大操作系统的应用。Madhavapeddy 问：一个用安全语言精心构建的应用，为什么还需要携带通用内核中数百万行 C 代码？

MirageOS 将编译扩展到操作系统组件。应用逻辑和配置与处理网络、存储和驱动的 OCaml 程序库组合，生成一个专门的可启动系统，也就是 unikernel。它为特定应用构建，而不是包含通用操作系统的所有服务。

项目从研究实验发展成拥有许多协议和文件系统实现的社区。Minsky 将这个想法称为作为库的操作系统，接着问操作系统究竟做什么。

Madhavapeddy 解释说，传统内核负责协调硬件访问，为进程提供隔离的资源访问。库操作系统则以链接的程序库提供系统功能。对于独占运行环境的专用应用，这很合理；但对于运行许多互不信任应用的桌面，传统操作系统仍然更合适。

Minsky 将 MirageOS 放在远离原有多用户操作系统理想的更大转变中。虚拟机和容器往往为应用打包并复制整套软件栈，而不是让用户简单共享一个操作系统。他问，既然环境已经变化这么大，为什么还要保留所有原来的抽象？

Madhavapeddy 认为这是抽象层随需求演进的结果。Xen 的最初目标是在一台物理机器上以较低开销运行多个隔离的操作系统实例，而无需重写数据库等应用。

Xen 使用半虚拟化：对客户机内核的一部分进行适配，让它与负责协调真实硬件访问的虚拟机监控程序协作。这样多个操作系统栈就能共享一台物理服务器，整合原本利用率不足的机器。在这种视角下，用户变成了启动整个操作系统的人。

Xen 最初源于剑桥酒吧里的一个赌约：有人认为 Keir Fraser 不可能在一个周末内修改 Linux。原型后来发展成更大的项目；Madhavapeddy 随后在 XenSource 工作，将其产品化，包括开发 Windows 和 Linux 驱动并处理众多兼容性边界情况。

为了在没有完整 Windows 或 Linux 安装负担的情况下测试 Xen，团队构建了一个运行底层功能的最小操作系统。Madhavapeddy 与 Thomas Gazagnaire 将 OCaml 运行时链接进去，以进行更复杂的测试，之后又加入 TCP/IP 和 HTTP 库。MirageOS 从这些实验中自然成长起来。

Madhavapeddy 认为，在投入产品化的艰苦工作之前，一次大胆尝试可以先验证研究假设。他说，MirageOS 程序库后来通过基础设施触及大量用户，虽然它们常常作为其他系统的一部分悄然运行。

Minsky 问，这些历史偶然产生的抽象是否合适。Madhavapeddy 说，Mirage 团队从不认为接口已经最终定型。OCaml 模块签名描述类型和操作，不同实现分别满足这些签名，使接口和实现都能演进。

例如，名为 flow 的 Mirage 网络接口可以使用 Linux 套接字实现，也可以使用纯 OCaml TCP/IP 栈实现。应用使用相同接口，却能选择不同后端。随着硬件、安全模型和分布式系统需求变化，团队可以逐步修改接口和调整实现。

Minsky 强调，Mirage 程序不一定始终以独立内核运行：它也可以使用普通宿主操作系统。同一组抽象让应用可以部署在多种环境中，从传统 Unix 进程到专用目标皆可。

Madhavapeddy 以太阳能网站为例。团队先在 Raspberry Pi 上使用普通 OCaml 和 Linux 开发 Web 服务器，再测量能源消耗。通过转向需要较少操作系统服务的受限 Mirage 接口，应用可以面向 ESP32 等能源预算更低、能力更少的小设备。

他说，这种迭代方式也减少了内核开发的神秘感：程序员可以编写 OCaml 并生成定制的可启动内核。Minsky 重视利用丰富语言抽象并省略不需要的组件，从而生成更小的系统，并有可能减少攻击面。

Minsky 指出，大多数程序员依赖语言工具，却没有太多能力修改它们。与语言社区合作可能使改进这些基础成为可能。Madhavapeddy 希望构建能够长期存在的系统，他将不断刷新的系统与具有清晰可理解属性的持久系统作比较。

Minsky 问到一个明显缺点：如果一切都必须用 OCaml 编写，系统如何利用更广泛的软件世界？Madhavapeddy 同意多种语言是必要的。他重视稳定语义和编译旧 OCaml 代码的能力，并指出外部接口和新兴 WebAssembly 互操作是连接不同语言的方法。

Minsky 提醒说，当语言必须容纳彼此的复杂性时，互操作可能损害简洁性。Madhavapeddy 同意端到端保证需要谨慎处理。例如在 Tezos unikernel 工作中，必须有意识地分层并连接 OCaml 的垃圾回收模型和 Rust 的生命周期模型；这不是打开构建系统开关就能神奇解决的。

Docker for Mac 和 Windows 提供了 Mirage 的另一个用途。Madhavapeddy 介绍了连接 Linux 容器与宿主文件系统和网络服务的转换层。通过将流量转换为普通宿主调用，系统可以避免经企业防火墙和杀毒配置桥接网络时的一些摩擦。

他说部署后支持请求大幅减少，但也强调了让 Go 和 OCaml 值安全互操作所需的工程工作。Minsky 认为这再次展示了 Mirage 的灵活性：其组件不仅可以构成完整的裸机内核，也可以成为操作系统之间的适配层。

Madhavapeddy 回忆，Heartbleed 之后，开发者编写了 OCaml TLS 栈，并创建 Bitcoin piñata：一个持有私钥的公开 unikernel，任何能攻破它的人都可以获得奖励。他说该系统抵御了许多攻击，在拒绝服务导致崩溃后可以快速重启，Bitcoin 最终捐给了慈善机构。

Minsky 询问 Madhavapeddy 参与的系统有多广泛。Madhavapeddy 提到 Xen 管理基础设施和 Docker 的桌面产品，同时将这些安装与编译成 JavaScript 用于 Web 应用的 OCaml 衍生代码区分开来。他还介绍了计划将 Mirage 用于气候感测设备和安全网络基础设施。

谈到如何进入计算领域，Madhavapeddy 说自己接受工程师训练，最初预计从事电气工程。一个可编程的在线 MUD 让他参加了一场聚会，并意外获得了与 NASA 的 Mars Polar Lander 项目有关的实习机会。

他帮助建立基础设施，以应对预计公众对着陆事件的关注。最初的 Solaris 机器遭到入侵后，他改用 OpenBSD，运行过程中发现漏洞并提交补丁。补丁被接受让他更深入地参与开源系统工作。

着陆器失联后，Madhavapeddy 回到剑桥攻读博士。他在那里参与 Xen，并更认真地使用 OCaml 编写前面提到的协议栈。开源代码成为一套可携带的工具，让他能在学术、工业和政府项目之间使用。

剑桥教授 ML 家族语言，让学生接触 OCaml，学习数据结构、递归和基础知识。Madhavapeddy 还发现，2000 年代初它适合实际的 Unix 系统工作。随着可复用代码不断积累，继续扩展它比用另一门语言重写全部内容越来越有吸引力。

Minsky 质疑在 C 主导领域时，OCaml 是否真是显而易见的系统语言。Madhavapeddy 同意这一质疑，并说自己希望当初能更早推广 OCaml。约在 2005 年，进展放缓且工具有限，即使在 XenSource 内部也难以推广。

XenSource 被 Citrix 收购后，Madhavapeddy 带着资金和构建 MirageOS 的抱负回到学术界。他也发现 OCaml 编译器团队需要有人帮助处理漏洞报告、工具和维护。改善语言生态会直接支持 Mirage，因此他帮助在剑桥建立了 OCaml Labs。

剑桥的知识产权安排让员工更容易发布开源代码。Minsky 赞扬大学支持艰难的协调和维护工作；这些工作不一定像传统学术研究，也未必直接带来终身教职。

Minsky 将 OCaml Labs 描述为连接项目的纽带：Merlin、OCamlFormat 和 Dune 起源不同，但协作帮助它们成为共同维护的工具。Madhavapeddy 补充说，大学培养的人才随后进入其他组织，使知识和贡献者在生态中持续流动。

他们转向多核 OCaml。在对话时，在共享堆上并行运行多个 OCaml 线程已经是一个长期目标。Minsky 问为什么花了这么久；Madhavapeddy 说，扩展现有语言同时保持其语义，会暴露数量惊人的边界情况。

2013 年的一项早期计划被证明过于乐观。后来工业用户要求团队定义内存模型，解释并发线程访问同一个值时会发生什么。由此产生的局部数据竞争自由研究，为多核设计提供了更清晰的语义基础。

垃圾回收器也是一项重大挑战：多个核心可能触发回收，而整个过程中都必须保持类型安全。团队比较不同设计，同时保护现有单核代码不出现显著变慢。Madhavapeddy 说，经过多年工作，最初 10%–20% 的性能损失降到了百分之几。

团队逐步将各部分并入多个 OCaml 版本，而不是创建不兼容的分支。Madhavapeddy 对未来 OCaml 5.0 的目标是让几乎所有现有代码都能编译且性能损失很小，同时由域提供共享堆并行。

Minsky 问，与 Java 相比，实际工作的程序员会获得什么。Madhavapeddy 希望提供更少意外的内存模型和熟悉的高层并行库。他指出，一旦程序依赖语言语义，就很难收回，因此团队在选择模型之前研究了早期设计。

谈到数据竞争，Madhavapeddy 将 C++ 的未定义行为与他描述的 OCaml 保证作比较：竞争会产生后果，但影响在空间和时间上有界，而不是任意扩散到整个程序。Minsky 认为，让有缺陷的代码更容易推理很有价值，因为真实代码库总有错误。

被问及日期时，Madhavapeddy 说，支持域的实验编译器已经可以通过 opam 与稳定编译器并行安装。开发者可以尝试现有项目并报告漏洞。他还介绍了一个更实验性的效果处理器分支，用于管理阻塞 I/O 等操作。

他概述的 2021 年路线图目标是先在 OCaml 5.0 中引入域，随后提供效果的运行时支持，最终提供语言级效果处理器。他将其描述为多年计划，而非固定发布时间表，并邀请用户测试开源分支。

Minsky 区分了大致对应物理核心的并行域，与域内众多轻量级并发任务。Madhavapeddy 将这些任务称为纤程：效果处理器允许用 OCaml 编写调度逻辑，可能让应用根据自身工作负载选择合适的策略。

他将这项工作与 MirageOS 联系起来。实验性的直接风格 I/O 栈 Eio 使用效果处理器和 Linux io_uring、Apple Grand Central Dispatch、Windows IOCP 等平台设施，对外呈现普通的 OCaml 代码。他将性能比较描述为当时对这项工作的观察。

Minsky 最后指出 MirageOS 与最新 OCaml 工作之间的联系。Madhavapeddy 的叙述回到了同一主题：将系统抽象转化为可复用、可编程的组件，同时保持运行实际应用的能力。