Completed
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…
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…
