The Hitchhiker's Guide to Operating Systems
summary
This work claims that treating programs and OS components as state transition systems improves OS teaching. It implements a minimal OS model with nine system calls covering process isolation, thread concurrency, and crash consistency and ships a Python-based emulator that boots Linux for advanced students. It produces a model checker and interactive state space explorer that exhaustively enumerates reachable states, models nondeterministic disk persistence to check crash safety, and uses symbolic merging to tame state explosion; course results report high engagement.
AI-written summary · about
chapters (9)
- 0:00Teaching operating systems
- 2:50State machines and recursion
- 5:42Process APIs with state machines
- 7:28Debugging OS with state machines
- 9:34State machines in compiler optimizations
- 10:40Executable state machine emulators
- 13:49Model checking state transitions
- 15:57Symbolic execution for verification
- 17:43Course impact and future