Completed
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 th…
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Theseus - An Experiment in Operating System Structure and State Management
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 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 th…
- 3 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 s…
- 4 Maximally leverage/empower compiler • Take advantage of Rust's powerful abilities Rust compiler checks many built-in safety invariants
- 5 Matching compiler's execution model 1. Single address space environment
- 6 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…
- 7 Addressing state spill • Key technique: opaque exportation
- 8 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 p…
- 9 Theseus facilitates evolutionary mechanisms • Runtime-persistent bounds simplify cell swapping o Dynamic loader ensures non-overlapping memory bounds
- 10 Realizing availability via fault recovery • Many classes of faults prevented by Rust safety & intralinguality Focus on transient hardware-induced faults beneath the language level
- 11 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 • M…
- 12 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 mu…
- 13 Cost of intralinguality & state spill freedom Mapped Pages performs better Safe heap: up to 22% overhead due to allocation bookkeeping
- 14 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 possi…
