Papers and Presentations about Theseus
Over the years, Kevin Boos, Ramla Ijaz, and other Theseus collaborators have given many presentations about Theseus OS and related topics. This page offers a selected collection of the slide decks from those talks (including some video recordings), as well as a list of selected peer-reviewed academic publications and theses.
Selected Papers and Theses
-
[OSDI 2020] Theseus: an Experiment in Operating System Structure and State Management
- The main paper describing Theseus's design principles, implementation, evaluation, and limitations.
- Paper (PDF) — OSDI 2020 Video Talk — OSDI 2020 Short Video — Slides (PDF)
-
[KISV 2023] Leveraging Rust for Lightweight OS Correctness
- A paper about extending intralingual design and applying a hybrid approach (type systems plus formal verification) for proving lightweight correctness guarantees about Theseus's memory management subsystem.
- Paper (PDF)
-
Kevin Boos PhD Dissertation: Theseus: Rethinking Operating Systems Structure and State Management
-
Ramla Ijaz Master's Thesis: Exploring Intralingual Design in Operating Systems
Other published works
- [OSDI 2022] Poster: Correct and Performant Device Drivers via Intralingual Design
- An overview of in-progress work to use formal verification + intralingual design for better device drivers.
- Poster PDF
- [PLOS 2017] Theseus: A State Spill-free Operating System
- Paper PDF — a shorter, outdated ideas paper about early Theseus design.
- Superseded by the OSDI 2020 paper.
- [EuroSys 2017] A Characterization of State Spill in Modern Operating Systems
- Introduces and studies the concept of state spill.
- Motivation for our future work on Theseus.
Selected Presentations and Slide Decks
- Theseus: a Rust-native OS for Safety and Reliability (Sept 2023) – [Video talk]
- How Theseus uses Rust, plus Rust challenges (early 2022)
- How Safe-language OSes work, with Theseus examples — [Video Talk]
- Overview of Theseus Design (Late 2020)
- A Programmer's Introduction to Theseus
- Kevin Boos PhD Defense: Deep Dive into Theseus OS Research — [Video Talk]
- Ramla Ijaz Master's Defense: Deep Dive into Intralingual Design in Theseus
- Crate Loading/Management and Crate Namespaces in Theseus
- Supporting Unwinding and Exceptions/Panics in Theseus (Late 2019)
- Implementing Basic Application Support for Theseus (mid-2018)
- Supporting Multicore Processors on Theseus
- Realizing Dynamic Loading and Linking of Crates (Late 2017)