--- title: SOSP 2024 Digest venue: SOSP year: 2024 date: '2024-11-05' tags: - operating-systems - distributed-systems - storage - cloud - formal-verification - ml-systems - security - serverless paper_count: 13 draft: false --- 13 papers selected. --- ### Verus: A Practical Foundation for Systems Verification *Andrea Lattuada 0001, Travis Hance, Jay Bosamiya, Matthias Brun 0002 *et al.** **TL;DR** — Verus is a Rust-based verification framework that makes formal proofs of low-level systems code tractable at scale, covering memory safety, functional correctness, and concurrency. **Why notable** — Formal verification of real systems code has long been impractical; Verus closes the usability gap by integrating SMT-based proofs directly into a systems programming language, making it the most broadly applicable verification tool for the OS community to date. [→ Read paper](https://doi.org/10.1145/3694715.3695952) --- ### Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation *Anish Athalye, Henry Corrigan-Gibbs, M. Frans Kaashoek, Joseph Tassarotti *et al.** **TL;DR** — A modular verification methodology lets developers prove end-to-end that a system leaks no sensitive information, bridging the gap from high-level spec all the way to circuit-level hardware behavior. **Why notable** — Side-channel leakage across abstraction layers is notoriously hard to reason about; this work provides a principled, mechanized framework to do so, setting a new bar for hardware-software co-verification of secure systems. [→ Read paper](https://doi.org/10.1145/3694715.3695956) --- ### Autobahn: Seamless high speed BFT *Neil Giridharan, Florian Suri-Payer, Ittai Abraham, Lorenzo Alvisi *et al.** **TL;DR** — Autobahn is a BFT consensus protocol that achieves high throughput under normal operation while seamlessly falling back to a slow path during faults, eliminating the throughput cliff common in prior BFT designs. **Why notable** — Byzantine fault-tolerant systems have historically traded peak performance for safety margins; Autobahn's seamless transition between fast and slow paths closes that gap and is likely to influence the next generation of production BFT deployments. [→ Read paper](https://doi.org/10.1145/3694715.3695942) --- ### Fast, Flexible, and Practical Kernel Extensions *Kumar Kartikeya Dwivedi, Rishabh R. Iyer, Sanidhya Kashyap* **TL;DR** — A new kernel extension framework surpasses eBPF's safety and flexibility constraints by using a combination of ahead-of-time compilation and a lean verification layer, enabling complex kernel extensions with near-native performance. **Why notable** — eBPF has become ubiquitous for in-kernel programmability, but its verifier fundamentally limits expressiveness; this work re-examines those trade-offs and offers a path toward richer, safer kernel extensions with broad applicability to networking, tracing, and storage. [→ Read paper](https://doi.org/10.1145/3694715.3695950) --- ### Tiered Memory Management: Access Latency is the Key! *Midhul Vuppalapati, Rachit Agarwal 0001* **TL;DR** — A principled tiered-memory manager that tracks per-page access latency rather than access frequency achieves substantially better performance for modern workloads on heterogeneous DRAM/CXL/NVM memory hierarchies. **Why notable** — As CXL-attached memory becomes mainstream, frequency-based page migration policies inherited from NUMA systems are increasingly inadequate; this paper reframes the problem around latency and provides a practical, deployable design. [→ Read paper](https://doi.org/10.1145/3694715.3695968) --- ### Fast & Safe IO Memory Protection *Benny Rubin, Saksham Agarwal, Qizhe Cai, Rachit Agarwal 0001* **TL;DR** — A hardware-software co-design eliminates the performance overhead of IOMMU-based DMA isolation by allowing safe, fine-grained IO memory protection without full page-table walks on the critical path. **Why notable** — DMA attacks remain a real threat yet IOMMU protection is widely disabled in production because of latency costs; this work makes protection affordable and is directly relevant to cloud, NIC, and storage subsystem designers. [→ Read paper](https://doi.org/10.1145/3694715.3695943) --- ### SWARM: Replicating Shared Disaggregated-Memory Data in No Time *Antoine Murat, Clément Burgelin, Athanasios Xygkis, Igor Zablotchi *et al.** **TL;DR** — SWARM replicates data in disaggregated-memory clusters with near-zero latency overhead by exploiting one-sided RDMA operations and a carefully designed protocol that avoids coordination on the read path. **Why notable** — Disaggregated memory is an emerging data-center architecture; providing fault tolerance without sacrificing its key latency advantage is an open problem, and SWARM's approach is both novel and practically relevant. [→ Read paper](https://doi.org/10.1145/3694715.3695945) --- ### Morph: Efficient File-Lifetime Redundancy Management for Cluster File Systems *Timothy Kim, Sanjith Athlur, Saurabh Kadekodi, Francisco Maturana *et al.** **TL;DR** — Morph dynamically transitions files through redundancy schemes (replication → erasure coding) based on observed file age and access patterns, substantially reducing storage overhead in large-scale cluster file systems. **Why notable** — Static redundancy policies waste significant capacity in practice; Morph's lifecycle-aware approach is validated at Google scale and provides a compelling template for storage systems serving diverse workloads. [→ Read paper](https://doi.org/10.1145/3694715.3695981) --- ### PowerInfer: Fast Large Language Model Serving with a Consumer-grade GPU *Yixin Song, Zeyu Mi, Haotong Xie, Haibo Chen 0001* **TL;DR** — PowerInfer exploits the activation sparsity of LLMs to partition computation between a consumer GPU and CPU, achieving high inference throughput without data-center hardware. **Why notable** — Democratizing LLM inference beyond cloud hardware is a pressing systems challenge; PowerInfer's sparsity-aware approach delivers surprising performance on commodity hardware and has already influenced a wave of follow-on work. [→ Read paper](https://doi.org/10.1145/3694715.3695964) --- ### LoongServe: Efficiently Serving Long-Context Large Language Models with Elastic Sequence Parallelism *Bingyang Wu, Shengyu Liu, Yinmin Zhong, Peng Sun 0006 *et al.** **TL;DR** — LoongServe introduces elastic sequence parallelism that dynamically adjusts the number of workers handling each long-context request to minimize GPU idle time and satisfy latency SLOs. **Why notable** — Long-context inference strains fixed parallelism strategies, creating severe resource fragmentation; LoongServe's elasticity primitive addresses this gap and is directly applicable to production LLM serving infrastructure. [→ Read paper](https://doi.org/10.1145/3694715.3695948) --- ### Unifying serverless and microservice workloads with SigmaOS *Ariel Szekely, Adam Belay, Robert Morris 0005, M. Frans Kaashoek* **TL;DR** — SigmaOS is an OS-level abstraction that treats serverless functions and microservices as first-class, interchangeable computational units, simplifying resource management and improving utilization for mixed workloads. **Why notable** — The artificial split between serverless and microservice programming models imposes significant operational complexity; SigmaOS's unified abstraction from the MIT systems group offers a clean architectural answer with demonstrated performance gains. [→ Read paper](https://doi.org/10.1145/3694715.3695947) --- ### Cookie Monster: Efficient On-Device Budgeting for Differentially-Private Ad-Measurement Systems *Pierre Tholoniat, Kelly Kostopoulou, Peter McNeely, Prabhpreet Singh Sodhi *et al.** **TL;DR** — Cookie Monster implements practical on-device differential-privacy budget management for ad attribution, showing that strong privacy guarantees can be enforced locally without destroying ad-measurement utility. **Why notable** — Browser vendors are actively replacing third-party cookies with privacy-preserving attribution APIs; this paper provides rigorous analysis of the privacy-utility trade-off and offers deployable techniques relevant to both industry standards and future OS-level privacy primitives. [→ Read paper](https://doi.org/10.1145/3694715.3695965) --- ### Efficient Reproduction of Fault-Induced Failures in Distributed Systems with Feedback-Driven Fault Injection *Jia Pan, Haoze Wu, Tanakorn Leesatapornwongsa, Suman Nath *et al.** **TL;DR** — A feedback-guided fault injection framework automatically reproduces complex distributed-system failures triggered by rare fault combinations, dramatically reducing the manual effort needed to diagnose and fix them. **Why notable** — Fault-induced failures in distributed systems are notoriously hard to reproduce; the paper's closed-loop search strategy is a methodological advance for reliability testing and is likely to influence both academic research and industrial chaos-engineering tools. [→ Read paper](https://doi.org/10.1145/3694715.3695979)