--- title: SOSP 2025 Digest venue: SOSP year: 2025 date: '2025-01-01' tags: [] paper_count: 14 draft: false --- 14 papers selected. --- ### LithOS: An Operating System for Efficient Machine Learning on GPUs *Patrick H. Coppock, Brian Zhang, Eliot H. Solomon, Vasilis Kypriotis *et al.** **TL;DR** — Designs a dedicated OS for GPU ML workloads, rethinking scheduling and resource management at the kernel level for accelerator-centric computing. --- ### CHERIoT RTOS: An OS for Fine-Grained Memory-Safe Compartments on Low-Cost Embedded Devices *Saar Amar, Tony Chen, David Chisnall, Nathaniel Wesley Filardo *et al.** **TL;DR** — Demonstrates hardware-capability-based fine-grained memory safety and compartmentalisation on constrained embedded devices, setting a new bar for secure IoT OSes. --- ### Atmosphere: Practical Verified Kernels with Rust and Verus *Xiangdong Chen, Zhaofeng Li 0004, Jerry Zhang, Vikram Narayanan *et al.** **TL;DR** — Shows that practical kernel verification is achievable using Rust and the Verus verifier, bridging the gap between formal methods and production OS development. --- ### TickTock: Verified Isolation in a Production Embedded OS *Vivien Rindisbacher, Evan Johnson 0001, Nico Lehmann, Tyler Potyondy *et al.** **TL;DR** — Delivers machine-checked proofs of isolation properties for a real embedded OS, providing strong security guarantees without sacrificing production deployability. --- ### μFork: Supporting POSIX fork Within a Single-Address-Space OS *John Alistair Kressel, Hugo Lefeuvre, Pierre Olivier* **TL;DR** — Reconciles the POSIX fork abstraction with unikernel/single-address-space designs, addressing a long-standing compatibility obstacle for library OS deployments. --- ### Scalable Address Spaces using Concurrent Interval Skiplist *Tae Woo Kim, Youngjin Kwon, Jeehoon Kang* **TL;DR** — Tackles the fundamental kernel scalability problem of virtual memory area management by replacing the VMA red-black tree with a concurrent interval skiplist, yielding significant mmap/munmap throughput gains. --- ### cache_ext: Customizing the Page Cache with eBPF *Tal Zussman, Ioannis Zarkadas, Jeremy Carin, Andrew Cheng *et al.** **TL;DR** — Extends the eBPF programmability model to the OS page cache, enabling application-specific caching policies without kernel modifications. --- ### Aeolia: A Fast and Secure Userspace Interrupt-Based Storage Stack *Chuandong Li 0004, Ran Yi 0004, Zonghao Zhang, Jing Liu 0074 *et al.** **TL;DR** — Redesigns the storage I/O path around userspace interrupts, achieving high throughput and low latency while preserving strong isolation properties. --- ### Sleeping with One Eye Open: Fast, Sustainable Storage with Sandman *Yanbo Zhou, Erci Xu, Anisa Su, Jim Harris *et al.** **TL;DR** — Introduces a storage system that aggressively power-gates flash devices while maintaining low latency, addressing sustainability concerns for large-scale storage deployments. --- ### Oasis: Pooling PCIe Devices Over CXL to Boost Utilization *Yuhong Zhong, Daniel S. Berger, Pantea Zardoshti, Enrique Saurez *et al.** **TL;DR** — Exploits CXL interconnects to pool PCIe devices across servers, significantly improving device utilisation and laying groundwork for memory-semantic datacenter architectures. --- ### Scalable Far Memory: Balancing Faults and Evictions *Yueyang Pan, Yash Lala, Musa Unal, Yujie Ren *et al.** **TL;DR** — Provides a rigorous analysis of the fault-vs-eviction trade-off in far-memory systems and proposes mechanisms that scale to production datacenter workloads. --- ### Tiga: Accelerating Geo-Distributed Transactions with Synchronized Clocks *Jinkun Geng, Shuai Mu 0001, Anirudh Sivaraman, Balaji Prabhakar* **TL;DR** — Exploits hardware clock synchronisation to cut coordination overhead in geo-distributed transactions, achieving latency close to the theoretical network minimum. --- ### Pesto: Cooking up High Performance BFT Queries *Florian Suri-Payer, Neil Giridharan, Liam Arzola, Shir Cohen *et al.** **TL;DR** — Advances Byzantine fault-tolerant systems by separating the query path from consensus, enabling high-throughput reads without weakening safety guarantees. --- ### Orthrus: Efficient and Timely Detection of Silent User Data Corruption in the Cloud with Resource-Adaptive Computation Validation *Chenxiao Liu, Zhenting Zhu, Quanxi Li, Yanwen Xia *et al.** **TL;DR** — Detects silent data corruption at cloud scale using resource-adaptive redundant computation, addressing a critical and hard-to-diagnose reliability threat in hyperscale infrastructure.