Explore an experimental operating system called Theseus, designed to improve OS modularity and leverage the Rust programming language for enhanced safety and compiler-enforced invariants. Learn about its unique structure of tiny components with runtime-persistent bounds, intralingual approach, and state management techniques that enable live evolution and fault recovery for core OS components. Discover how Theseus addresses state spill, implements compiler-checked task invariants, and facilitates evolutionary mechanisms. Examine the system's performance, limitations, and comparisons with other operating systems like MINIX 3 and Linux. Gain insights into the challenges and benefits of designing an OS that prioritizes safety, modularity, and compiler-driven resource management.
Theseus - An Experiment in Operating System Structure and State Management
Overview
Syllabus
Intro
Initially motivated by study of state spill • State spill: the state of a software component undergoes a lasting change a result of interacting with another component Future correctness depends on those changed states
Establishes OS structure of many tiny components All components must have runtime-persistent bounds 2. Adopt intralingual OS design to empower Rust compiler Leverage language strengths to go beyond safety Shift responsibility of resource bookkeeping from OS into compiler 3. Avoids state spill or mitigates its effects
Maximally leverage/empower compiler • Take advantage of Rust's powerful abilities Rust compiler checks many built-in safety invariants
Matching compiler's execution model 1. Single address space environment
Intralingual OS implementation in brief (0) Use & prioritize safe code as much as possible 1. Identify invariants to prevent unsafe, incorrect resource usage Express semantics using existing language-level mechanisms • Enables compiler to subsume OS's resource-specific invariants 2. Preserve language-level context with lossless interfaces
Addressing state spill • Key technique: opaque exportation
Compiler-checked Task invariants 1. Spawning a new task must not violate safety 2. Accessing task states must always be safe and deadlock-free 3. Task states must be fully released in all execution paths 4. All memory reachable from a task must outlive that task
Theseus facilitates evolutionary mechanisms • Runtime-persistent bounds simplify cell swapping o Dynamic loader ensures non-overlapping memory bounds
Realizing availability via fault recovery • Many classes of faults prevented by Rust safety & intralinguality Focus on transient hardware-induced faults beneath the language level
Brief evaluation overview • Live evolution case studies • Fault recovery experiments Injecting faults into Theseus Comparison with MINIX 3 microkernel • Cost of intralingual and spill-free design • Microbenchmark comparison with Linux
Live Evolution: sync + async "IPC" Theseus advances evolution beyond monolithic/microkernel OSes Safe, joint evolution of user-kernel interfaces and functionality Evolution of core components that must exist in microkernel • Do microkernels need to change? Change histories say yes
Cost of intralinguality & state spill freedom Mapped Pages performs better Safe heap: up to 22% overhead due to allocation bookkeeping
Limitations at a glance • Unsafety is a necessary evil + detect infectious unsafe code • Reliance on safe language Must trust Rust compiler and core/alloe libraries • Intralinguality not always possible Nondeterministic runtime conditions, incorporating legacy code • Tension between state spill freedom and legacy compatibility Make decision on per subsystem basis, e.g. prefer legacy FS
Taught by
USENIX
