Cloud

13 papers selected. ASTERINAS: A Linux ABI-Compatible, Rust-Based Framekernel OS with a Small and Sound TCB Yuke Peng, Hongliang Tian, Junyang Zhang, Ruihan Li et al. TL;DR — A production-grade OS kernel written in Rust that exposes a full Linux ABI while confining unsafe code to a small, formally-audited framekernel core. Why notable — ASTERINAS demonstrates that Linux compatibility and memory-safety guarantees are not mutually exclusive — unsafe Rust is isolated to under 5 kloc of framework code, giving systems operators a credible path toward a safer Linux-compatible kernel without sacrificing application portability. ...

13 papers selected. PRED: Performance-oriented Random Early Detection for Consistently Stable Performance in Datacenters Xinle Du, Tong Li 0014, Guangmeng Zhou, Zhuotao Liu et al. TL;DR — PRED redesigns AQM by making drop probability a direct function of per-flow performance targets rather than queue length, eliminating the instability of classic RED in modern datacenter workloads. Why notable — RED has been a cornerstone of congestion control for decades; PRED’s performance-centric reformulation challenges a long-held design axiom and demonstrates significantly lower tail latency at scale. It opens the door to intent-driven AQM as a first-class primitive in datacenter switches. ...

13 papers selected. Empowering WebAssembly with Thin Kernel Interfaces Arjun Ramesh, Tianshu Huang, Ben L. Titzer, Anthony Rowe 0001 TL;DR — A new OS interface design exposes thin, capability-based kernel primitives directly to WebAssembly modules, eliminating the POSIX translation layer. Why notable — WebAssembly is increasingly used beyond the browser as a portable, sandboxed compute substrate; this work shows that rethinking the system interface from scratch yields significantly lower overhead and better safety properties than layering Wasm on top of POSIX. ...

11 papers selected. Chasing Lightspeed Consensus: Fast Wide-Area Byzantine Replication with Mercury Christian Berger 0006, Lívio Rodrigues, Hans P. Reiser, Vinicius Vielmo Cogo et al. TL;DR — Mercury is a wide-area Byzantine fault-tolerant replication protocol that minimises latency by exploiting geographic locality and pipelining to approach the theoretical lightspeed bound. Why notable — Achieving near-lightspeed latency in Byzantine replication across wide-area networks has been a long-standing open challenge; Mercury’s design demonstrates it is practically attainable. The result raises the bar for what production BFT middleware can deliver in geo-distributed deployments. ...

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. ...