Lec 1 Advanced OS Overview Course Overview Course Scheduling Rethink OS Components Tendency of OS -- Performance Tendency of OS -- Reliability Tendency of OS -- Correctness Lec 2 OS Architecture Oeverview History Monolithic Kernel -- UNIX MicroKernel -- Mach&L4 ExoKernel -- Xok+ExOS Lec3+4 System Virtualization Overview Introduction Traditional Virtualization Challenges Virtualization Technologies -CPU Virtualization Technologies -Mmeory Virtualization Technologies -I/O Optimization of VMM -- intro LightVM: My VM is Lighter (and Safer) than your Container Dune: Safe User-level Access to Privileged CPU Features Lec5+6 OS/System API/Interface Introduction Rethinking the Library OS from the Top Down DPDK: Accelerating the I/O Path Safe and Secure Drivers in High-Level Languages Lec 7+8 OS Kernel and HLL Introduction Multiprogramming a 64 kB Computer Safely and Efficiently The benefits and costs of writing a POSIX kernel in a high-level language Lec9+10 OS for MultiCore Architecture Introduction How to analyze the OS bottleneck for multicore arch How to optimize the OS for multicore arch Optimizing the OS performance from MIT's research Scalable Kernel TCP Design and Implementation for Short-Lived Connections Lec 11+12 OS/System Security Introduction Improving Integer Security for Systems with KINT PF-Miner: A new paired functions mining method for Android kernel in error paths RID: Finding Reference Count Bugs with Inconsistent Path Pair Checking Lec 13+14 Correctness: OS/System Verification Introduction seL4: Formal Verification of an OS Kernel Jitk: A trustworthy in-kernel interpreter infrastructure Hyperkernel: Push-Button Verification of an OS Kernel. Lec 15+16 Invited Talks From Visitors & Students