In this section we’ll discuss kernels and programming languages: the benefits and costs that derive from writing much of an operating systems kernel in a language that’s not assembly, C, or C++. Our focus will be these two research papers.
Singularity: “Singularity: Rethinking the Software Stack.” Galen C. Hunt and James R. Larus. In ACM SIGOPS Operating Systems Review 41(2), Apr. 2007. Link — Singularity project page
Every operating system embodies a collection of design decisions. Many of the decisions behind today’s most popular operating systems have remained unchanged, even as hardware and software have evolved. Operating systems form the foundation of almost every software stack, so inadequacies in present systems have a pervasive impact. This paper describes the efforts of the Singularity project to re-examine these design choices in light of advances in programming languages and verification tools. Singularity systems incorporate three key architectural features: software-isolated processes for protection of programs and system services, contract-based channels for communication, and manifest-based programs for verification of system properties. We describe this foundation in detail and sketch the ongoing research in experimental systems that build upon it.
Tock (embedded Rust OS): “Multiprogramming a 64 kB Computer Safely and Efficiently.” Amit Levy, Bradford Campbell, Branden Ghena, Daniel B. Giffin, Pat Pannuto, Prabal Dutta, and Philip Levis. In Proc. SOSP 2017. Link
Low-power microcontrollers lack some of the hardware features and memory resources that enable multiprogrammable systems. Accordingly, microcontroller-based operating systems have not provided important features like fault isolation, dynamic memory allocation, and flexible concurrency. However, an emerging class of embedded applications are software platforms, rather than single purpose devices, and need these multiprogramming features. Tock, a new operating system for low-power platforms, takes advantage of limited hardware-protection mechanisms as well as the type-safety features of the Rust programming language to provide a multiprogramming environment for microcontrollers. Tock isolates software faults, provides memory protection, and efficiently manages memory for dynamic application workloads written in any language. It achieves this while retaining the dependability requirements of long-running applications.
You should focus on sections 2 and 3 (except 3.4 and 3.6) and 4.2 of Singularity and sections 1-4 of Tock.
How to read research papers
There are as many ways to read research papers as there are people. It’s very difficult for me (Eddie) to read papers other than sequentially, starting at the beginning. However, particularly at the beginning of your career, sequential reading can get you really lost. You want to skim for the high points, then read again for more depth.
Take a look at S. Keshav’s “How to Read a Paper” (local copy). This is wise advice; I especially recommend following his advice for the first pass. This pass aims to develop a mental framework for the paper as soon as possible. Once that framework is in place, reading for content and ideas becomes much easier.
You might also be interested in Michael Mitzenmacher’s paper-reading instructions.