Completed
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ā¦
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ā¦