Coursework.

A position paper arguing that traditional OS abstractions (files, processes, sockets) harm performance, reliability, and adaptability by preventing applications from tailoring resource management. Advocates lowering the OS interface to bare hardware — the seed idea for the Exokernel architecture — where the kernel only securely multiplexes hardware while library OSes implement policy.

Introduces layered OS design using the THE system as a case study: hardware sits at layer 0, memory management at layer 1, process abstraction at layer 2, I/O device management at layer 3, and the user program at layer 4. Each layer is verified independently, and semaphores appear here as a formal synchronization primitive for the first time.

Presents Opal, a single-address-space OS for 64-bit architectures that decouples addressability from protection. Rather than isolating processes in separate address spaces, Opal uses segments and capabilities to grant fine-grained protection within one shared 64-bit address space, enabling efficient pointer-based sharing without expensive context switches.

Establishes policy/mechanism separation as a foundational OS design principle, demonstrated through the Hydra kernel at CMU. The kernel provides only mechanisms (scheduling, paging, protection); all policy is delegated to higher-level components. The paper shows this concretely for three subsystems: CPU scheduling, paging, and protection, proving that a minimal kernel can support diverse policies without modification.

Arrakis splits the OS into a control plane (the kernel, for configuration and resource allocation) and a data plane (user space, for all I/O). Applications use SR-IOV hardware virtualization to access network and storage devices directly without kernel involvement on the critical path. Redis achieves 2–5× throughput improvement and 9× latency reduction over Linux.

Exposes five low-level virtual memory primitives (trap, prot1, protn, unprot, dirty) to user programs, enabling user-level implementations of garbage collection, persistent stores, shared virtual memory, and data-compression paging — without kernel modifications. The paper demonstrates that VM hardware, usually hidden behind the OS, is a rich substrate for user-level systems software.

Ingens treats memory contiguity as a first-class OS resource and tracks actual page utilization before promoting to huge pages. Linux's Transparent Huge Pages (THP) often promotes eagerly, causing bloat and stalls; Ingens coordinates promotion with access patterns to deliver up to 18% throughput improvement and 41% reduction in tail latency.

BVT lets latency-sensitive threads 'borrow' virtual time from the future by warping their effective virtual time backward, letting them preempt other threads immediately upon waking. The borrowed time is repaid later, so long-run fairness is maintained while interactive threads get sub-millisecond scheduling response.

SEDA (Staged Event-Driven Architecture) structures internet services as a pipeline of event-driven stages connected by queues. Each stage has a thread pool and a controller that dynamically adjusts concurrency based on queue depth, enabling graceful degradation under overload without thread-per-request overhead.

Establishes a theoretical principle: whenever interface operations commute (their results are order-independent for any interleaving), there exists an implementation with conflict-free memory accesses that scales to many cores. Introduces COMMUTER to generate commutativity conditions from specs and evaluates against POSIX and the sv6 kernel.

Hyperkernel encodes OS kernel handlers as finite, loop-free SMT queries and uses Z3 to automatically verify isolation: a process can only access its own memory. The 'push-button' approach requires no manual proof annotations — if Z3 discharges the queries, the kernel is verified. Hyperkernel verifies a complete, bootable OS in under a minute.

F2FS is a log-structured file system designed around NAND flash characteristics: sequential writes for performance, multi-head logging to avoid GC pressure, and a node address table (NAT) that eliminates LFS's wandering-tree update problem. Now the default filesystem for Android devices.

RacerX uses flow-sensitive interprocedural static analysis to infer locking disciplines and flag violations as potential race conditions or deadlocks. It found hundreds of bugs in Linux, FreeBSD, and commercial OS kernels, including 12 serious previously-unknown races, demonstrating that static analysis can surface concurrency bugs at scale without running the code.

Introduces futexes (fast userspace mutexes), the synchronization primitive underlying pthreads on Linux today. In the uncontended case, locking and unlocking are pure userspace atomic operations with no kernel involvement. Only when a thread must actually wait does it make a syscall, minimizing kernel overhead for the common case.

Applies model checking to verify concurrency correctness in the Asterinas Rust OS kernel using PlusCal specifications. CONVEROS uncovered 20 bugs across 12 critical concurrency modules — including deadlocks and atomicity violations — with a specification-to-code ratio of 0.3–2.3, demonstrating that model checking is practical for production-scale Rust kernels.

Describes BTRFS's copy-on-write B-tree structure that supports snapshots, checksums, transparent compression, and built-in RAID — all in a single filesystem. COW guarantees that an in-progress write never overwrites live data, enabling crash-consistent snapshots at near-zero cost and self-healing through per-block checksums.

WiscKey redesigns LSM-tree key-value stores for SSDs by keeping only keys in the tree and storing values in a separate append-only log. This eliminates value write amplification during compaction while exploiting SSD's cheap random reads. Achieves up to 8× faster sequential loads and 3.6× faster random lookups than LevelDB.

Addresses the tension between keeping memory as huge pages (for TLB performance) and releasing memory back to the OS (for efficiency at warehouse scale). Introduces adaptive subrelease — breaking up huge pages only when demand warrants — that maintains 98% huge-page coverage vs. 87% without it, while still returning memory promptly. Deployed in Google's TCMalloc.

SCONE runs Linux containers inside Intel SGX enclaves, protecting application memory and secrets from a compromised host OS or hypervisor. To avoid expensive enclave transitions on every syscall, it uses shielded execution with asynchronous system call forwarding and transparent I/O encryption, achieving 0.6×–1.2× native throughput.

Erebor provides intra-kernel privilege isolation inside confidential VMs, preventing an untrusted guest OS kernel from accessing sensitive application data. The sandbox is drop-in compatible with existing cloud deployments and imposes only 4.5%–13.2% performance overhead, extending confidential computing guarantees to the guest OS threat model.

LAKE enables ML inference inside the OS kernel, allowing subsystems like I/O scheduling and memory management to make data-driven decisions. It introduces a kernel-space ML runtime with support for hardware accelerators and achieves 95% inference speedup for I/O latency prediction while avoiding the cost of user-kernel context switches for inference.

Kleio manages page placement in tiered memory systems (DRAM + NVM or HBM + DDR) by combining history-based heuristics with a recurrent neural network for access-pattern prediction. It reduces the performance gap with an oracle page scheduler by 80%, deploying the RNN selectively to amortize inference cost.