Vincent Lannurien
d822cdaa6a
9.0 KiB
title, venue, year, date, tags, paper_count, draft
| title | venue | year | date | tags | paper_count | draft | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| SOSP 2024 Digest | SOSP | 2024 | 2024-11-05 |
|
13 | 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.