content updates, various fixes

site/content/digests/SOSP-2024/index.md

@@ -0,0 +1,176 @@
+---
+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)
+