Reading
The first paper describes an operating system engineered entirely in Rust, and explains the safety benefits of its design. The second paper reports on a more incremental, but more widely deployed, use of Rust, namely Rust-for-Linux.
-
“RedLeaf: Isolation and communication in a safe operating system”, Vikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel, Zhaofeng Li, Gerd Zellweger, Anton Burtsev (OSDI 2020) (presentation available)
-
“An empirical study of Rust-for-Linux: The success, dissatisfaction, and compromise”, Hongyu Li, Liwei Guo, Yexuan Yang, Shangguang Wang, Mengwei Xu (2024 USENIX Annual Technical Conference) (presentation available)
Despite its ungrammatical English, this paper received Best Paper at USENIX Annual Technical Conference 2024; give it a chance.
The remaining paper is optional reading (we will try not to assign 3 papers on Wednesday classes), but consider taking a look, especially if you’re interested in Rust or speculative OS redesigns. I find §7.2 pretty cool.
- OPTIONAL. “Theseus: An experiment in operating system structure and state management”, Kevin Boos, Namitha Liyanage, Ramla Ijaz, Lin Zhong (OSDI 2020) (presentation available)
Reading questions
- A critical aspect of safety in object-oriented languages is that the compiler ensures each object’s destructor (or finalizer) is called before the object is deallocated. This allows an object to clean up related objects. But the RedLeaf microkernel will sometimes deallocate objects without calling their destructors. When does it do this, and in what ways is this safe?
- The Rust-for-Linux paper offers several examples of Rust programming
complexity in the kernel context, e.g.,
Pin<Box<SpinLock<Box<Ring<RxDesc>>>>>. Do you think RedLeaf’s implementation avoids this complexity? Why or why not?
Further reading
-
“Multiprogramming a 64 kB computer safely and efficiently”, Amit Levy, Bradford Campbell, Branden Ghena, Daniel B. Giffin, Pat Pannuto, Prabal Dutta, Philip Levis (SOSP 2017)
A slightly earlier Rust OS for microcontrollers. Interesting and in some ways more practical than Theseus, it’s not our main paper because it focuses more on issues of embedded systems.
-
“Singularity: Rethinking the software stack”, Galen C. Hunt, James R. Larus (ACM SIGOPS Operating Systems Review, April 2007)
Like Theseus, Singularity proposed to replace hardware protection with language-level protection, but in its case the language was largely C#. As a Microsoft Research project, Singularity demonstrated some excellent engineering. The paper above is a summary; the research paper “Language support for fast and reliable message-based communication in Singularity OS” (Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R. Larus, Steven Levi (Eurosys 2006)) won a EuroSys Test of Time Award.