--- title: OSDI 2025 Digest venue: OSDI year: 2025 date: '2025-01-01' tags: [] paper_count: 13 draft: false --- 13 papers selected. --- ### Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols *Tony Nuda Zhang, Keshav Singh, Tej Chajed, Manos Kapritsos *et al.** **TL;DR** — Automates the construction of correctness proofs for distributed protocols that were previously considered undecidable, advancing the state of the art in verified systems. --- ### Mako: Speculative Distributed Transactions with Geo-Replication *Weihai Shen, Yang Cui, Siddhartha Sen 0001, Sebastian Angel *et al.** **TL;DR** — Combines speculative execution with geo-replication to deliver low-latency distributed transactions without sacrificing consistency, addressing a fundamental tension in wide-area systems. --- ### Low End-to-End Latency atop a Speculative Shared Log with Fix-Ante Ordering *Shreesha G. Bhat, Tony Hong, Xuhao Luo, Jiyu Hu *et al.** **TL;DR** — Introduces fix-ante ordering to achieve low latency on a shared log without sacrificing throughput, offering a new design point for log-based distributed storage. --- ### Okapi: Decoupling Data Striping and Redundancy Grouping in Cluster File Systems *Sanjith Athlur, Timothy Kim, Saurabh Kadekodi, Francisco Maturana *et al.** **TL;DR** — Challenges a long-standing coupling in erasure-coded cluster file systems, enabling independent optimization of striping and redundancy with measurable gains in production workloads. --- ### PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection *Hayley LeBlanc, Jacob R. Lorch, Chris Hawblitzel, Cheng Huang *et al.** **TL;DR** — Provides a tool-agnostic framework for formally verifying crash consistency and corruption detection in storage systems, raising the bar for storage software correctness. --- ### EMT: An OS Framework for New Memory Translation Architectures *Siyuan Chai 0001, Jiyuan Zhang 0003, Jongyul Kim 0001, Alan Wang *et al.** **TL;DR** — Defines an OS abstraction layer that decouples applications from hardware-specific memory translation mechanisms, enabling future memory architectures to be adopted without OS rewrites. --- ### XSched: Preemptive Scheduling for Diverse XPUs *Weihang Shen, Mingcong Han, Jialong Liu, Rong Chen 0001 *et al.** **TL;DR** — Generalises preemptive scheduling to heterogeneous accelerators (XPUs), providing a unified OS-level mechanism for fair and responsive multi-tenant accelerator sharing. --- ### Extending Applications Safely and Efficiently *Yusheng Zheng, Tong Yu, Yiwei Yang 0002, Yanpeng Hu *et al.** **TL;DR** — Presents a principled model for safe, efficient application extensibility that generalises beyond eBPF, with implications for the design of future OS extension mechanisms. --- ### NanoFlow: Towards Optimal Large Language Model Serving Throughput *Kan Zhu, Yufei Gao, Yilong Zhao 0002, Liangyu Zhao *et al.** **TL;DR** — Analytically characterises the throughput ceiling for LLM serving and proposes a system that approaches that bound through fine-grained intra-device parallelism. --- ### WaferLLM: Large Language Model Inference at Wafer Scale *Congjie He, Yeqi Huang, Pei Mu 0003, Ziming Miao *et al.** **TL;DR** — Demonstrates end-to-end LLM inference on wafer-scale hardware, tackling novel challenges in memory, communication, and fault tolerance at an unprecedented scale of integration. --- ### Mirage: A Multi-Level Superoptimizer for Tensor Programs *Mengdi Wu, Xinhao Cheng, Shengyu Liu, Chunan Shi *et al.** **TL;DR** — Extends tensor program superoptimisation to multiple abstraction levels, discovering non-obvious kernel fusions that outperform hand-tuned implementations for ML workloads. --- ### Training with Confidence: Catching Silent Errors in Deep Learning Training with Automated Proactive Checks *Yuxuan Jiang 0016, Ziming Zhou, Boyu Xu 0005, Beijie Liu *et al.** **TL;DR** — Addresses the underappreciated problem of silent hardware and software errors in large-scale DL training, providing automated proactive checks that catch failures before they corrupt long training runs. --- ### Compass: Encrypted Semantic Search with High Accuracy *Jinhao Zhu, Liana Patel, Matei Zaharia, Raluca Ada Popa* **TL;DR** — Enables accurate semantic (vector) search over encrypted data, bridging the gap between privacy-preserving computation and modern retrieval workloads in cloud-hosted RAG systems.