[2013-PPT]From L3 to seL4 What Have We Learnt in 20 Years of L4 Microkernels

From L3 to seL4:What Have We Learnt in20 Years of L4 Microkernels? Kevin Elphinstone, Gernot Heiser NICTA and University of New South Wales1993Improving IPCby KernelDesign [SOSP]0 100ssCycles250 5.00121 0.7586 0.8645 0.10 2,000 1.3836 0.02151 0.64288 0.11301 0.09188 0.35316 0.32total kSLOC6.414.210.510.823.09.015.037.610.29394959697989900 01020304050607080910111213L3 → L4“X”Hazelnut PistachioL4/AlphaL4/MIPS seL4OKL4 µKernelOKL4 MicrovisorCodezeroP4 → PikeOSFiascoFiasco.OCL4-embed.NOVAGMD/IBM/Karlsruhe UNSW/NICTA DresdenCommercial Clone OK LabsL4 Family TreeAPI Inheritance Code InheritanceseL4: Unprecedented DependabilityIntegrityAbstract ModelC Imple-mentationConfiden-tialityAvailabilityBinary codeP r o o fP r o o fP r o o fFunctional correctness [SOSP’09]Integrity [ITP’11]Translation correctness [PLDI’13]• First & only OS kernel with security proofs to binary code• First & only protected- mode OS kernel withsound timeliness analysisTimeliness [RTSS’11, EuroSys’12]Non-interference[S&P’13]Wait Kernelcopy“Long” IPC• IPC page faults are nested exceptions ⇒ In-kernel concurrency – L4 executes with interrupts disabled for performance, no concurrency • Must invoke untrusted usermode page-fault handlers– potential for DOSing other thread• Timeouts to avoid DOS attacks– complexityReceiver address spaceSender address spaceKernel copyPage fault!Why have long IPC?• POSIX-style APIswrite (fd, buf, nbytes)• Usually prefer shared buffersL O NG I PCA B AN D ON E DTimeoutsThread 1Running BlockedThread 2Blocked RunningSend (dest, msg) Wait (src, msg) ….... Kernel copy Limit IPC blocking timeThread 1Running Blocked Rcv (NIL_THRD, delay)…....Timedwait• No theory/heuristics for determining timeouts • Typically server reply with zero TO, else ∞ • Can do timed wait with timer syscallI P C T i m e o u t s A B A N D O N E D i ns e L 4, O K L 4Asynchronous Notifications…....Thread 1Running BlockedThread 2Blocked Runningw = Poll (…) …... w = Wait (…)…....Send (Thr_2, …) Send (Thr_2, …)• Delivers few bits (destructively)• Kernel only buffers single word • Maps well to interrupts, exceptionsServerClientDriverSyncAsync • Thread can wait for synchronous andasynchronous messages concurrentlyS y n c I P C c o m p l e m e n t e d w i th a s y n cIPC Destination NamingIPCClientServerClientServerLoadbalancerWorkersClientServerAll IPCs duplicated!Original L4 addressed IPC to threadsClient must do load balancing?RPC reply from wrong thread!• Inefficient designs• Poor information hiding• Covert channels [Shapiro ‘02]T h r e a d I D s r e p l a c e d b y I P C “e n d p o i n t s ” (p o r t s )Rcv IPC SendAsync EP0x010x100x300x310x110x010x00ChiefIPCCreateVirtual TCB ArrayTCBTCBVM Thread ID Fast TCB & stack lookupT C B p r o p e rK e r n e l s t a c kGet own TCB base by masking stack pointerTrades cache for TLB footprint and virtual address space• Not worthwhile on modern processors! • Stacks can dominate kernel memory use!Trades TLB footprint for cache and kernel memory“Lazy” Schedulingthread_t schedule() {foreach (prio in priorities) {foreach (thread in runQueue[prio]) {if (isRunnable(thread)) return thread; elseschedDequeue(thread); }}return idleThread; }• In IPC-based systems, threads block and unblock frequenty• Many ready queue manipulationsIdea: leave blocked threads in ready queue, schedulercleans upScheduler execution time is unbounded!“Benno scheduling”:• All threads on ready queue are runnable• All runnable threads in ready queue except the running oneProcess kernel Virtual TCB array Lazy scheduling Direct process switch Non-preemptible Non-portableNon-standard calling convention Assembler Synchronous IPCRich message structure, arbitrary out-of-line messages Zero-copy register messages User-mode page-fault handlers Threads as IPC destinations IPC timeoutsHierarchical IPC controlUser-mode device drivers Process hierarchyRecursive address-space construction。