Vincent Lannurien
d822cdaa6a
All checks were successful
Build and deploy static pages / build-and-push (push) Successful in 19s
125 lines
4.6 KiB
Markdown
125 lines
4.6 KiB
Markdown
---
|
|
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.
|
|
|