Microkernels

1 .Microkernels: From Mach to seL4 (Lecture 18, cs262a) Ali Godsi & Ion Stoica, UC Berkeley March 21, 2018

2 .Papers “Microkernel Operating System Architecure and Mach”, D . Black, D. Golub , D. Julin , R. Rashid, R. Draves , R. Dean, A. Forin , J. Barrera, H. Tokuda , G. Malan, and D. Bohman ( https://amplab.github.io/cs262a-fall2016/notes/ Mach.pdf ) “seL4 : Formal Verification of an OS Kernel ”, Gerwin Klein , Kevin Elphinstone, Gernot Heiser , June Andronick , David Cock, Philip Derrin , Dhammika Elkaduwe , Kai Engelhardt , Rafal Kolanski , Michael Norrish, Thomas Sewell, Harvey Tuch , Simon Winwood , ( https:// www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf )

3 .David Patterson – Turing Award winner (2017) For RISC (Reduce Instruction Set Computer) project SPARC processor from Sun (now Oracle) ARM (Acorn Risc Machine) Every processor today has a RISC architecture at its core Lots of other impactful work: RAID, Recovery Oriented Computing, etc.

4 .Key Observation (~1985) Mondern OSes at that time (e.g ., Unix, OS/2) primarily distinguished by the programming environment they provide and not by the way they manage resources Opportunity: F actor out the common part Make it easier to build new OSes

5 .Microkernels separates OS in two parts Part of OS that control basic hardware resources (i.e.. microkernel) Part of OS that determine unique characteristics of application environment (e.g., file system)

6 .What problem do they try to solve? Portability: Environment mostly independent on the instruction set architecture Extensibility & customization: Can easily add new versions of environments Enable environments to evolve faster (decouples them from microkernel ) Can simultaneously provide environments emulating interfaces Sounds familiar? Microkernel as a narrow waist (anchor point) of OSes P rovide hardware independence, similar to data independence in relational data models

7 .What problem do they try to solve? Easier to provide better functionality and performance for kernel: Real-time: no need to maintain lock for extended periods of time; environments are preemptable Multiprocessor support: simpler functionality  easier to parallelize Multicomputer support: simpler functionality  easier to distribute Security: simpler functionality  easier to secure Flexibility (network accessibility): System environment can run remotely

8 .( https://en.wikipedia.org/wiki/ Microkernel )

9 .Mach Goal: show that microkernels can be as efficient as monolithic operating systems: “ … achieving the levels of functionality and performance expected and required of commercial products” Sounds familiar? Similar goals as System R and Ingress: Show that a conceptually superior solution (i.e., relational model) admit efficient implementations that can match the performance of existing solutions (i.e., network and hierarchical models)

10 .Mach Developed at CMU Led by Rick Rashid Founded Microsoft Research Initial release: 1985 Big impact (as we will see) Rick Rashid

11 .What does a microkernel (Mach) do? Task and thread management: Task (process) unit of allocation Thread, unit of execution Implements CPU scheduling: exposed to apps Applications/environments can implement their own scheduling policies Inter-process communication (IPC) Between threads via ports Secured by capabilities

12 .What does a microkernel (Mach) do ? Memory object management: Essentially virtual memory Persistent store accessed via IPC System call redirection: Enable to trap system calls and transfer control to user mode Essentially enable applications to modify/extend the behavior and functionality of system calls, e.g., Enable binary emulation of environments, tracing, debugging

13 .What else does a microkernel (Mach) do ? Device support: Implemented using IPC (devices are contacted via ports) Support both synchronous and asynchronous devices User multiprocessing: Essentially a user level thread package, with wait()/signal() primitives One or more user threads can map to same kernel thread Multicomputer support: Can map transparently tasks/resources on different nodes in a cluster

14 .Mach 2.5 Contains BSD code compatibility code, e.g., one-to-one mapping between tasks and processes Some commercial success: NeXT Steve Jobs’ company after he left Apple Used by Tim Berners-Lee to develop WWW Encore, OSF (Open Software Foundation), …

15 .Mach 3 Eliminate BSD code R ewrite IPC to improve performance RPC on (then) contemporary workstations: 95 usec Expose device interface Provide more control to user applications via continuation: A ddress of an user function to be called when thread is rescheduled plus some data: essentially a callback Enable application to save restore state, so that the microkernel doesn’t need to do it, e.g., saving and restoring register state

16 .OSes and Application Programs Mach allows application to implement: Paging Control data cached by virtual memory … Redirection allows call traps to link directly to executable binaries without modifying he kernel! Just need an emulation library

17 .Emulation Libraries Translator for system services and a cache for their results Converts app calls to Mach calls Invoke functionality of the environment (e.g., OS) and reply to app Typically linked to app to avoid another context switching

18 .OSes Environment Architectures Fully implemented in the emulation library Simple, single user systems (e.g., MS-DoS ) As a server (see previous slide) Native OSes : use the code of the original systems Used to implement both MacOS , and DOS Emulation library also v irtualizes the physical resources

19 .Performance: Mach 2.5 vs 3.0 Virtually the same as Mach 2.5, and commercial Unix systems of that time SunOS 4.1 and Ultrix 4.1 Why? I/O dominated tasks (read, write, compile) Microbenchmarks would have been nice, e.g.: IPC Cost of a page fault

20 .OSF/1 Unix Server Even more modularity: different OS functionalities implemented as different servers, e.g., IPC, process management, file server, etc S erver proxies on client side for optimization

21 .L3  seL4

22 .How it started? (1993) Microkernels (e.g., Mach) still too slow Mostly because IPCs Tide was turning towards monolithic kernels Jochen Liedtke (GMD – Society for Mathematics and Information technology ) aimed to show that IPC can be supper-fast Jochen Liedtke

23 .How fast?

24 .How did he do it? Synchronous IPC  Rendezvous model s end( dest , msg ) Running Thread src Thread dest wait( src , msg ) Running Running Running Wait … Kernel copy Kernel executes in sender’s context copies memory data directly to receiver ( single-copy ) leaves message registers unchanged during context switch ( zero copy )

25 .One-way IPC cost over years

26 .Minimalist design “A concept is tolerated inside the microkernel only if moving it outside the kernel, i.e. permitting competing implementations , would prevent the implementation of the system’s required functionality” Sounds familiar? “ Don ’ t implement anything in the network that can be implemented correctly by the hosts” -- radical interpretation of the e2e argument!

27 .Source Lines of Code

28 .L4 family tree

29 .L4 family tree “The Secure Enclave runs an Apple-customized version of the L4 microkernel family ” - iOS Security, Apple Inc , 2015 ( www.apple.com/business/docs/ iOS_Security_Guide.pdf )