系统与数据库2017cs.virginia.edu
用 Rust 编写内核的理由
The Case for Writing a Kernel in Rust
进阶 · 约 45 分钟读完前置知识：操作系统基础、Rust 所有权与类型系统、C 语言内核开发经验
导读
这篇论文（Tock OS 团队后续工作）论证用 Rust 编写操作系统内核的价值：Rust 的所有权与类型系统能在编译期提供内存安全和时间安全，避免 C 内核常见的漏洞。论文是此前 Tock 论文的延续，作者称已解决了前作中提出的诸多问题。
HN 关注点：HN 读者长期关注 Rust 在系统编程领域的可行性，这篇论文由 Tock 作者参与撰写，讨论焦点是 Rust 是否真的适合写内核。
后来怎么样
这篇论文及其前作推动了 Rust 在操作系统内核领域的应用，Tock OS 成为嵌入式领域有影响力的 Rust 内核，Rust 内核开发后来被 Linux、Windows 等主流系统采纳，成为业内公认的趋势。
HN 评论精选
这几条评论里：质疑 1 补充 2 亲历 1
补充提供论文背景：这是 Tock OS 团队的后续研究
注意本文合著者之一 Amit 是 Tock OS 的作者。这篇论文是之前 Tock 论文的后续：发表后 Amit 解决了其中提出的许多问题。此前在 HN 上也讨论过，Amit 刚刚还在 /r/rust 上补充了更多背景。
steveklabnik查看英文原文
Note that one of the co-authors of this paper, Amit, is the author of https://www.tockos.org/ This paper is sort of a successor to https://sing.stanford.edu/site/publications/levy-plos15-tock.pdf , a previous paper on this topic. After publication, Amit solved many of the issues presented there. It was previously discussed on HN https://news.ycombinator.com/item?id=14105884 Some more context https://www.reddit.com/r/rust/comments/655816/ownership_is_theft_experiences_building_an/dg7p2uf/ Amit left even more context just now on /r/rust: https://www.reddit.com/r/rust/comments/75xwib/the_case_for_writing_an_os_in_rust/do9wk3g/
补充推荐同类项目 Redox OS 作为参考
如果还没看过，推荐了解一下 Redox OS，一个用 Rust 写的微内核，还有对开发者的访谈视频。
jp_rider查看英文原文
If you haven't already, check out Redox OS [1,2]. It's a microkernel written in Rust. Here's a good interview with the developer [3]. [1] https://www.reddit.com/r/Redox/ [2] https://redox-os.org/ [3] https://www.youtube.com/watch?v=eH5JgMlNE8o
质疑质疑未提及 SPARK/Muen，建议混合 SPARK 与 Rust 提升安全保证
这是很好的工作。不过为什么相关工作里没提 Muen 分离内核？它用 SPARK 语言，可证明免疫多种缺陷，使用零运行时配置。Rust 用仿射类型改进了 Ada/SPARK，提供时间安全和更灵活的安全并发模型。我原以为 Rust 内核里会有一些可信组件可能影响安全性保证，一个思路是用 SPARK 写这些组件再通过 FFI 供 Rust 调用，或结合 CompCert/CakeML 等经过认证的编译器。
nickpsecurity查看英文原文
This is good work. I enjoyed reading it. I wonder, though, why Muen separation kernel wasn't mentioned in related work on kernels in safe languages. It uses the SPARK language so that it's provably immune to a number of defects. The Ada compilers can also give you as little or much runtime as you want with several "profiles" available. Muen uses the "minimal, Zero-Runtime" profile. Rust improves on Ada and SPARK with the affine types giving temporal safety plus more flexible model for safe concurrency than Ravenscar. CompSci work shows one can probably do that and info-flow security with contracts but that would be extra, specialist work for Ada/SPARK versus what's built-in to Rust already. Verbose, too. https://muen.codelabs.ch/ When I about the Rust kernels, I assumed there would be some trusted components in there which could screw them up on assurance side. Aside from full formal verification, one thing someone might want to try is writing those pieces in SPARK like Muen does. Make a direct port from any proven SPARK to Rust source. Alternatively, compile the SPARK into executable code that Rust calls with its FFI since C code can call SPARK code. Then, those untrusted portions are shown safe with one set of rules while the rest is shown safe with Rust's compiler. Optionally, convert those to an intermediate language of CompCert or CakeML compilers for certified compilation. This is how my Brute-Force Assurance model would attempt to handle each's limitations in a kernel project. Note: Only problem with using SPARK for that is the person doing it probably has to buy a license if the Rust kernel in question isn't GPL. SPARK is only free for use with GPL code. Frama-C is another option one might use to avoid that but SPARK is stronger offering.
亲历亲历者反驳：Rust 写内核体验不佳，最终退回 C
我试过用 Rust 写内核，最后还是改回了 C。我觉得它作为系统语言并不好用，整个过程都在和语言搏斗，硬把它掰成做它本不该做的事。
Sag0Sag0查看英文原文
I tried to write a kernel in rust but reverted back to c. I just feel that it is not very nice systems language. The entire time i felt like i was fighting to manipulate the language into doing something it wasn't supposed to do.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2017Hacker News 讨论帖181 分 · 58 评
同领域还值得读
I/O 比 CPU 更快——让我们划分资源并消除操作系统抽象
I/O Is Faster Than CPU – Let’s Partition Resources and Eliminate OS Abstractions
指出在现代服务器硬件上 I/O 速度已接近甚至超过 CPU，传统操作系统抽象反而成为瓶颈。
系统与数据库2019 · 817 分 · 277 评进阶 · 约 30 分钟编辑精选使用 io_uring 的高效 I/O
Efficient IO with io_uring
由 Linux 内核开发者 Jens Axboe 撰写，介绍 Linux 新的异步 I/O 接口 io_uring。
系统与数据库2019 · 426 分 · 96 评进阶 · 约 45 分钟编辑精选线程对大多数用途而言是个坏主意（1995）
Threads Are a Bad Idea for Most Purposes (1995)
这篇 1995 年的文章由 John Ousterhout 撰写，讨论为什么线程对大多数用途而言是坏主意，并主张事件驱动编程通常更简单、更高效。
系统与数据库2017 · 423 分 · 382 评进阶 · 约 25 分钟编辑精选学习型索引结构之论证
The Case for Learned Index Structures
提出把索引看作一种"模型"：既然 B-tree 等结构本质上是在学习数据的分布，就可以用机器学习模型（如回归模型、神经网络）来近似键到位置的映射，从而替代 B-tree、哈希索引…
系统与数据库2017 · 398 分 · 66 评 · 引用 25进阶 · 约 60 分钟编辑精选FoundationDB：一个分布式、解耦的事务型键值存储
FoundationDB: A distributed, unbundled, transactional key value store
介绍 FoundationDB：一个分布式、解耦设计的事务性键值存储。
系统与数据库2021 · 283 分 · 99 评进阶 · 约 90 分钟编辑精选