The SOSP’26 conference has published its list of accepted papers. I was preparing to share that list when I noticed that many of the papers already have preprint versions available on arXiv or elsewhere. This blog post therefore reproduces the list here, with all the preprint papers I could find. Note some of the titles are probably not final; they sometimes use generic names (ex., “SystemX”) that sound like anonymized versions. Similarly, the papers have probably changed since their preprint versions.

The bar plot above illustrates the variety of research areas covered. The research areas are taken from last year’s schedule and I categorized the papers based on the titles only, so take with a grain of salt. For papers touching multiple research areas, I took what I viewed as the main area1.



A Few GPUs, A Whole Lotta Scale: Faithful LLM Training Emulation with CrystalLLM

Shaoke Xi, ChonLam Lao (Alibaba Group), Boyi Jia (Shanghai Jiao Tong University and Alibaba Group), Jiaqi Gao, Zhipeng Zhang, Jiamin Cao (Alibaba Group), Brian Sutioso (Harvard University), Erci Xu (Shanghai Jiao Tong University), Minlan Yu (Harvard University), Kui Ren (Zhejiang University), Yong Li, Zhengping Qian, Ennan Zhai, Jingren Zhou (Alibaba Group)
 Paper   Abstract 
Large language model (LLM) training today runs on clusters spanning thousands of GPUs. While this scale enables rapid model advances, developing, debugging, and performance-tuning, the training framework inevitably becomes complex and costly. This is because engineers often need to reproduce production behaviors to diagnose failures or evaluate optimizations, thereby demanding frequent and even exclusive access to production-scale clusters—which becomes increasingly hard given that the majority of GPUs are already committed to production workloads. Simulation relies on complex performance models that are difficult to maintain, and downscaled experiments often fail to capture scale-dependent behaviors.

We present PrismLLM to decouple large-scale execution from the need to access large clusters, enabling engineers to run and observe ranks of interest under faithful large-scale behavior using only a few GPUs. PrismLLM constructs a high-fidelity execution graph via a slicing-based approach that captures computation, communication, and dependencies of the target scale. Then, PrismLLM performs hybrid emulation where selected ranks execute the original program while the remaining are replayed as virtual participants.

Experiments on large-scale LLM training workloads show that PrismLLM accurately reproduces performance and memory behavior, achieving only 0.58% average error in iteration time and less than 0.01% error in peak GPU memory usage. PrismLLM can emulate clusters of up to 8192 GPUs using fewer than 1% of the physical GPUs required by the original deployment.

AgileLog: A Forkable Shared Log for Agents on Data Streams

Shreesha G. Bhat, Tony Hong, Michael A Noguera, Aishwarya Ganesan, Ramnatthan Alagappan (University of Illinois Urbana-Champaign)
 Paper   Abstract 
In modern data-streaming systems, alongside traditional programs, a new type of entity has emerged that can interact with streaming data: AI agents. Unlike traditional programs, AI agents use LLM reasoning to accomplish high-level tasks specified in natural language over streaming data. Unfortunately, current streaming systems cannot fully support agents: they lack the fundamental mechanisms to avoid the performance interference caused by agentic tasks and to safely handle agentic writes. We argue that the shared log, the core abstraction underlying streaming data, must support creating forks of itself, and that such a forkable shared log serves as a great substrate for agents acting on streaming data. We propose AgileLog, a new shared log abstraction that provides novel forking primitives for agentic use cases. We design Bolt, an implementation of the AgileLog abstraction, that uses novel techniques to make forks cheap, and provide logical and performance isolation.

Ahead-of-time Analysis of Shell Program Effects

Lukas Lazarek, Evangelos Lamprou, George Kapetanakis, Anirudh Narsipur, Eric Zhao, Zhiwen Zheng (Brown University), Michael Greenberg (Stevens Institute of Technology), Konstantinos Kallas (University of California, Los Angeles), Nikos Vasilakis (Brown University)
 Paper   Abstract 
The Unix shell remains a core system substrate across system administration, automation, and software development. Shell programs, however, are prone to subtle, severe, and often irreversible effects that are difficult to predict. The challenge stems from the shell's unique execution model, its reliance on external computation and state, its highly dynamic expansion semantics, and the complex interactions among these features. This paper presents SaSh, a system that statically analyzes shell programs to identify errors in their execution before they occur. SaSh introduces an optimistic symbolic execution engine for shell programs that limits path explosion and focuses on high-impact failures. It tracks the effects of external commands over a filesystem model, and approximates shell word expansion using a tailored abstract domain. SaSh quickly identifies bugs even in large programs with a risk-directed exploration strategy, steering its analysis to program fragments likely to exhibit dangerous behavior. Applied to 61 buggy programs, including several high-profile disasters, SaSh identifies all but one instance of unwanted behavior with no false positives, going far beyond the current state-of-the-art. Furthermore, SaSh has already yielded 70 bug reports in 44 open-source projects such as PyTorch, the P4 Compiler, Kubernetes, and vLLM, including bugs that can lead to irreversible data loss.

Anchor: Mitigating Shallow Disruptions with Decoupled Memory

Haoyi Ma, Shiwei Gao (Tsinghua University), Youmin Chen (Shanghai Jiao Tong University), Junrong Huang, Youyou Lu, Jiwu Shu (Tsinghua University)

Ave: Guiding Agentic GPU Optimization with Data Flow Invariants

Haohui Mai (HKUST), Xiaoyan Guo (University of Chinese Academy of Sciences, China), Xiangyun Ding (University of California, Riverside), Daifeng Li (University of Science and Technology of China), Qiuchu Yu (University of Chinese Academy of Sciences, China), Chenzhun Guo (Xi'an jiaotong university, China), Cong Wang (Tsinghua University), Jiacheng Zhao (University of Chinese Academy of Sciences, China), Christos Kozyrakis (Stanford University), Binhang Yuan (HKUST)
 Paper   Abstract 
Recent LLM-based coding agents can generate functionally correct GPU kernels across diverse workloads, yet their performance remains far below that of manually optimized libraries on critical computations such as matrix multiplication, attention, and Mixture-of-Experts (MoE). This gap is fundamental: peak GPU performance requires coordinated reasoning over tightly coupled optimizations, including tiling, shared-memory staging, software pipelining, and instruction scheduling, while existing agents rely on sparse pass/fail feedback from unit tests, leaving them unable to diagnose violations of global constraints.

We present Argus, an agentic framework that addresses this limitation through data-flow invariants, i.e., compile-time specifications that encode how data must be choreographed throughout a kernel's execution. Argus introduces a tile-based, Pythonic DSL that exposes hardware instructions and compiler policies while hiding low-level representations, maintaining both expressivity and learnability for LLMs. The DSL introduces tag functions to propagate symbolic annotations through data and control flow, and tag assertions to enforce relational constraints at use sites, centralizing global correctness properties. When violations occur, the compiler returns concrete counterexamples that identify the thread, data element, and program point, providing dense, structured feedback for targeted fixes. Invariants are verified at compile time via abstract interpretation over a layout algebra and SMT solving, incurring zero runtime overhead. An in-context reinforcement learning (ICRL) planner further learns to select optimizations and synthesize effective invariants, supported by a curated knowledge base of GPU-specific optimization techniques.

We evaluate Argus on the AMD MI300X GPU across GEMM, flash attention, and MoE kernels that together account for over 90% of GPU time in LLM inference. The generated kernels achieve 99–104% of the effective throughput of state-of-the-art hand-optimized assembly implementations and are 2–1543× faster than existing agentic systems in geometric-mean throughput across the evaluated workload families. Argus further generalizes to 200 KernelBench tasks, producing correct kernels for 100% of Level 1 and 90% of Level 2 problems.

Batched in Back: Characterizing and Optimizing Offline LLM Inference in Production with ACDC

Leping Yang (Shanghai Jiao Tong University), Xue Li, Kun Qian (Alibaba Group), Erci Xu (Shanghai Jiao Tong University), Mingzhen Han, Haoran Zhu, Tao He, Zuolong Yin, Ennan Zhai, Wenyuan Yu, Jingren Zhou (Alibaba Group), Guangtao Xue (Shanghai Jiao Tong University)

Beyond Utilization: Energy-Conscious GPU Sharing for Inference Serving

Prasoon Sinha, Dimitrios Liakopoulos, Nathan Lemma, Neeraja J. Yadwadkar (The University of Texas at Austin)

Big Bird: Resilient Privacy Budgeting Across Untrusted Web Domains

Pierre Tholoniat, Alison Caulfield, Giorgio Cavicchioli, Mark Chen (Columbia University), Benjamin Case (Meta Inc.), Asaf Cidon, Roxana Geambasu (Columbia University), Mathias Lécuyer (University of British Columbia), Martin Thomson (Mozilla)
 Paper   Abstract 
The W3C Attribution API is an emerging standard for privacy-preserving advertising measurement. Its current privacy architecture enforces individual differential privacy (IDP) independently for each domain (e.g., an advertiser) issuing queries. We show that this guarantee is unsound under realistic system behavior: it fails under cross-querier data adaptivity and can also fail when shared limits are enforced across queriers. The issue is not the on-device accounting model itself – device-epoch IDP – but treating each querying domain in isolation.

We propose Big Bird, a privacy-budget manager that makes global device-epoch IDP – enforced jointly across all domains – both sound and deployable for Attribution. Big Bird addresses the main obstacle to global enforcement in open multi-querier systems: denial-of-service depletion of a shared global budget by Sybil web domains. Its key insight is that benign Attribution workloads have a stock-and-flow structure: impressions create potential privacy loss, conversions realize it, and meaningful budget consumption should be tied to genuine user actions across distinct web domains. Big Bird enforces this structure with privacy-loss-based quotas on impression and conversion sites and a per-user-action cap on how many quotas can be activated, ensuring that adversarial impact scales with genuine user interactions rather than with the number of Sybil domains.

We implement Big Bird in Rust, integrate it into Firefox's Attribution prototype, and evaluate it theoretically and empirically on real ad-tech data. We show that Big Bird provides rigorous global device-epoch IDP, formal resilience to depletion attacks, and utility for benign queriers under attack.

Borges: A Low-Latency Distributed Shared Log on a CXL Memory/SSD Hybrid

Haowei Chen, Yiming Xiang (The University of Texas at Austin), Zhipeng Jia (Anthropic PBC), Yan Sun, Nam Sung Kim (UIUC), Emmett Witchel (The University of Texas at Austin)

Cerium: A Multi-GPU Framework for Terabyte-Scale Encrypted Inference

Siddharth Jayashankar (Carnegie Mellon University), Joshua Kim (University of Texas at Austin), Michael Sullivan (NVIDIA), Wenting Zheng, Dimitrios Skarlatos (Carnegie Mellon University)
 Paper   Abstract 
Encrypted AI using fully homomorphic encryption (FHE) provides strong privacy guarantees; but its slow performance has limited practical deployment. Recent works proposed ASICs to accelerate FHE, but require expensive advanced manufacturing processes that constrain their accessibility. GPUs are a far more accessible platform, but achieving ASIC-level performance using GPUs has remained elusive. Furthermore, state-of-the-art approaches primarily focus on small models that fit comfortably within a single device. Supporting large models such as LLMs in FHE introduces a dramatic increase in computational complexity that requires optimized GPU kernels, along with managing terabyte-scale memory footprints that far exceed the capacity of a single GPU.

This paper presents Cerium, a multi-GPU framework for FHE inference on large models. Cerium integrates a domain-specific language, an optimizing compiler, and a runtime system to automatically generate high-performance GPU kernels, manage terabyte-scale memory footprints, and parallelize computation across multiple GPUs. It introduces new IR constructs, compiler passes, sparse polynomial representations, memory-efficient data layouts, and communication-aware parallelization techniques that together enable encrypted inference for models ranging from small CNNs to Llama3-8B.

We build Cerium on NVIDIA GPUs and demonstrate significant performance gains. For small models, Cerium outperforms expert-written hand-optimized GPU libraries by up to 2.25 times. Cerium achieves performance competitive with state-of-the-art FHE ASICs, outright matching prior FHE ASIC CraterLake. It is the first GPU system to execute bootstrapping in under 10 milliseconds, achieving 7.5 milliseconds, and is the first to demonstrate encrypted inference for BERT-Base and Llama3-8B in 8 seconds and 134 seconds, respectively.

Cohort: Decentralized PIR

Jonathan Weiss, Yossi Gilad (Hebrew University of Jerusalem)

Computation is Fast, Use Threadlet!

Yiming Yao, Xiaohe Qin (Peking University and Beijing Tongming Lake Information Technology Application Innovation Center (TLAIC)), Yi Fan (Peking University), Yuanlong Li (EPFL), Kang Hu, Liujia Li (Peking University), Xiaolin Wang, Tao Xie (Peking University and Beijing Tongming Lake Information Technology Application Innovation Center (TLAIC)), Zhenlin Wang (Michigan Technological University), Yuval Tamir (UCLA), Yingwei Luo, Diyu Zhou (Peking University and Beijing Tongming Lake Information Technology Application Innovation Center (TLAIC))

CryptDough: A Unified Analytics Engine for Secure Multiparty Computation

Muhammad Faisal, Alessandra Lanz, Sam Buxbaum, Adam Godel, Vasiliki Kalavri, Mayank Varia, John Liagouris (Boston University)
 Paper   Abstract 
We present CryptDough, a unified analytics engine for secure multiparty computation (MPC). CryptDough enables multiple distrusting parties to jointly execute a data analysis pipeline on their private inputs and learn nothing beyond the result (e.g., aggregate statistics). Unlike existing MPC solutions that support a single threat model or workload type, CryptDough provides built-in support for cross-domain analytics (relational, time series, ML inference) under various threat models, all within the same system runtime.

CryptDough contributes (i) a hierarchical system design that facilitates modularity and extensibility through progressive lowering of abstractions, and (ii) the concept of virtual vectors that enable users to write single-threaded code across all layers of the software stack, while pushing the complexity of communication, parallelization, and memory management down to the execution engine. We show that CryptDough generalizes the functionality of state-of-the-art MPC systems and remains competitive on the analytics they support, often outperforming them by more than 2×.

DDB: Source-Level Interactive Debugging for Distributed Applications

Yibo Yan, Junzhou He, Seo Jin Park (University of Southern California)
 Paper   Abstract 
Interactive debugging is an effective tool for understanding program behavior at the source level, allowing developers to pause execution, navigate the call stack, and inspect runtime state. However, interactive debuggers are designed for single-process execution, and interactive debugging has been widely considered impractical for distributed systems. Call stacks stop at process boundaries, debugging state fails to survive infrastructure dynamics, and, most critically, debugger-induced execution pauses trigger catastrophic timeout cascades that destroy the intended debug flow. Consequently, developers are forced to abandon live hypothesis testing in favor of unwieldy and iterative log-and-redeploy cycles.

We present DDB, a source-level interactive debugger that extends interactive debugging capabilities to distributed applications. We show that each of these challenges admits a targeted solution. To bridge disjoint processes, Distributed Backtrace (DBT) embeds compact causality metadata in every RPC and reconstructs a unified call stack across RPC boundaries. To manage the lifecycle of a distributed session, an intent-preserving control plane automatically coordinates and propagates breakpoints across dynamic process sets. To make pausing safe, Pause-Erased Time (PET) virtualizes each process's clock, decoupling logical time from physical pauses and preventing timeout cascades. DDB integrates with an RPC framework in 10–60 lines of code. Evaluated on gRPC, ServiceWeaver, Nu, and Quicksand across up to 122 processes, DDB achieves 30 ms median cross-RPC backtrace latency, sub-5 ms time jump under repeated execution pauses, and adds 1–5% throughput overhead, comparable to attaching a single-process debugger. In a controlled user study, DDB achieves a 100% fault localization success rate (compared to 38.5% for baseline tools) with a median localization time of ∼8 minutes.

DiFlow: A System for Micro-Serving Text-to-Image Diffusion Workflows

Lingyun Yang (Hong Kong University of Science and Technology & Alibaba Group & Shanghai Jiao Tong University), Suyi Li, Tianyu Feng, Xiaoxiao Jiang (Hong Kong University of Science and Technology), Zhipeng Di, Weiyi Lu, Kan Liu, Yinghao Yu, Tao Lan, Guodong Yang, Lin Qu, Liping Zhang (Alibaba Group), Wei Wang (Hong Kong University of Science and Technology)
 Paper   Abstract 
Text-to-image generation executes a diffusion workflow comprising multiple models centered on a base diffusion model. Existing serving systems treat each workflow as an opaque monolith, provisioning, placing, and scaling all constituent models together, which obscures internal dataflow, prevents model sharing, and enforces coarse-grained resource management. In this paper, we make a case for micro-serving diffusion workflows with LegoDiffusion, a system that decomposes a workflow into loosely coupled model-execution nodes that can be independently managed and scheduled. By explicitly managing individual model inference, LegoDiffusion unlocks cluster-scale optimizations, including per-model scaling, model sharing, and adaptive model parallelism. Collectively, LegoDiffusion outperforms existing diffusion workflow serving systems, sustaining up to 3× higher request rates and tolerating up to 8× higher burst traffic.

DISCO*: DIstributed and SCalable Oblivious Joins and Oblivious Primitives

Apostolos Mavrogiannakis (University of California, Santa Cruz), Xian Wang (Hong Kong University of Science and Technology), Ioannis Demertzis (University of California, Santa Cruz), Dimitrios Papadopoulos (Hong Kong University of Science & Technology), Minos Garofalakis (ATHENA Research Center & Technical University of Crete)
 Abstract 
In recent years, Trusted Execution Environments (TEEs) have reshaped the landscape of secure cloud computing, enabling clients to outsource computation without trusting the cloud provider. Yet, TEEs face critical limitations, such as vulnerability to side-channel and leakage-abuse attacks. To address the security implications, recent advancements in the literature combine hardware enclaves with oblivious computation. This combination of hardware and software security offers strong security guarantees; however, existing oblivious computation approaches struggle to meet the performance and scalability demands of real-world deployments.

In this work, we present DISCO, the first scalable, distributed, and fully oblivious database system that seamlessly combines hardware enclaves with cutting-edge oblivious primitives and novel optimizations that significantly reduce inter-server communication overheads. What distinguishes DISCO from prior work is a suite of distributed frameworks that unlock parallel computation and fundamentally shift the design paradigm of distributed oblivious systems, enabling practical deployment at scales that were unattainable with previous solutions.

We provide a thorough evaluation of the performance of our system on both synthetic and real-world datasets. Our evaluation demonstrates that our design significantly reduces the gap between theory and practice, achieving 88× speedup over Jodes and 180× over SODA on non-foreign key joins with N=2²⁵ elements. Most importantly, we report, for the first time, results for computations at the terabyte scale.

Disk-Based LSMs: An Unexpectedly Good Index for Partly Coherent CXL Memory

Kiran Hombal, Jiyu Hu (University of Illinois Urbana-Champaign), Marcos K. Aguilera (NVIDIA), Aishwarya Ganesan, Ramnatthan Alagappan (University of Illinois Urbana-Champaign)
 Paper   Abstract 
We consider the design of an in-memory range index for systems with CXL shared memory in which only a small part of the memory is cache coherent. While existing index data structures can be ported to such a setting using a software-coherence approach, the result performs poorly. We find that the key reason is that such data structures have a large updatable surface area—the part of the data structure that can be modified in-place. We propose a new design that, perhaps surprisingly, is based on log-structured merge trees (LSMs)—data structures originally designed for disks rather than memory. We further enhance LSMs by allowing in-place updates to the upper level of the LSM. The resulting data structure outperforms state-of-the-art schemes based on Adaptive Radix Trees (ARTs) and B-trees ported to our setting, achieving up to 9.4× higher peak throughput over in-memory indexes and up to 15.1× over existing CXL systems.

Don't Let AI Agents YOLO Your Files: Information and Control in Agent-Native Filesystems

Shawn (Wanxiang) Zhong, Junxuan Liao (University of Wisconsin-Madison), Jing Liu (Microsoft Research), Mai Zheng (Iowa State University), Andrea Arpaci-Dusseau (University of Wisconsin-Madison), Remzi Arpaci-Dusseau (University of Wisconsin–Madison)
 Paper   Abstract 
Distributed protocols are notoriously difficult to verify correctly. Proving safety typically requires inductive invariants that both imply the desired property and are preserved by every protocol transition; yet inferring such invariants remains a major bottleneck: existing approaches either restrict the protocol models to a decidable fragment of first-order logic or demand expert-crafted templates.

We present IC3Syn, a neuro-symbolic framework that synthesizes inductive invariants by executing an IC3-style process over TLA+ states with the assistance of Large Language Models (LLMs). At large, IC3Syn combines a symbolic IC3 controller, which decomposes invariant synthesis into focused blocking tasks and an LLM which provides protocol-level reasoning that IC3 alone lacks for TLA+ specifications. This integration enables a disciplined yet flexible search for invariants without imposing logical restrictions or requiring manual templates.

We evaluate IC3Syn on 29 distributed protocols spanning consensus, reconfiguration and client–server systems, and compare it against Endive, IC3PO, SWISS and DistAI. IC3Syn discovers candidate invariants for all 29 protocols, including MongoLoglessDynamicRaft (MLDR), an industrial-scale Raft-based reconfiguration protocol for which none of the compared tools reports a solution, as well as one complex Paxos variant. In each case, the invariants synthesized on finite instances are shown in TLAPS to be inductive for the full unbounded protocol, thereby establishing safety.

Efficient GPU Multitasking with Morphable Kernels

Tingxu Ren, Ruwen Fan, Hao Guo, Minhui Xie, Shiwei Gao, Jiwu Shu, Youyou Lu (Tsinghua University)

GAZE: Rearchitecting Log-Structured Filesystem for Garbage Collection on Zoned Namespace Flash Storage

Juwon Kim, Hwanseok Yoo, Seung Won Yoo, Youjip Won (Korea Advanced Institute of Science and Technology)

I3DP: Neuro-symbolic Inductive Invariant Inference for Distributed Protocols

Weining Cao, Guangyuan Wu, Yuan Yao (Nanjing University), Hengfeng Wei (Hunan University), Taolue Chen (Birkbeck, University of London), Xiaoxing Ma (Nanjing University)
 Paper   Abstract 
Distributed protocols are notoriously difficult to verify correctly. Proving safety typically requires inductive invariants that both imply the desired property and are preserved by every protocol transition; yet inferring such invariants remains a major bottleneck: existing approaches either restrict the protocol models to a decidable fragment of first-order logic or demand expert-crafted templates.

We present IC3Syn, a neuro-symbolic framework that synthesizes inductive invariants by executing an IC3-style process over TLA+ states with the assistance of Large Language Models (LLMs). At large, IC3Syn combines a symbolic IC3 controller, which decomposes invariant synthesis into focused blocking tasks and an LLM which provides protocol-level reasoning that IC3 alone lacks for TLA+ specifications. This integration enables a disciplined yet flexible search for invariants without imposing logical restrictions or requiring manual templates.

We evaluate IC3Syn on 29 distributed protocols spanning consensus, reconfiguration and client–server systems, and compare it against Endive, IC3PO, SWISS and DistAI. IC3Syn discovers candidate invariants for all 29 protocols, including MongoLoglessDynamicRaft (MLDR), an industrial-scale Raft-based reconfiguration protocol for which none of the compared tools reports a solution, as well as one complex Paxos variant. In each case, the invariants synthesized on finite instances are shown in TLAPS to be inductive for the full unbounded protocol, thereby establishing safety.

It's the Kernel's Fault! Custom Page Fault Handling With bpf_fault

Tal Zussman, Riju Dey, Hasan Zengin, Yiming Fang (Columbia University), David Hildenbrand (Technical University of Munich and Arm Germany GmbH), Asaf Cidon (Columbia University)
 Paper   Abstract 
Page faults, which occur when a program accesses a virtual memory page that is not mapped to physical memory, are traditionally handled by the operating system. However, many applications benefit from running custom page fault handling logic. For example, some applications may seek to prefill newly-faulted pages with content, or intercept writes in order to make a copy of the original contents. Linux's userfaultfd interface enables some of these use cases by offloading fault handling to userspace. Unfortunately, it suffers from significant limitations, namely high overhead, poor scalability, and a design that precludes its use in libraries.

We present bpf_fault, a framework that allows applications to run page fault handlers directly within the Linux kernel using eBPF. By eliminating the overheads and complexity associated with userfaultfd, bpf_fault reduces fault latency by 2.8–6.1× and eliminates userfaultfd's scalability bottleneck. We integrate bpf_fault with several applications, such as VM live snapshots in Firecracker, which eliminates tail latency spikes caused by snapshots. By leveraging bpf_fault, we also design a novel lazy dynamic linking mechanism for Linux that defers relocations to fault time, a use case impossible with userfaultfd, which reduces dirty memory usage of widely-used applications like Chrome and Clang by up to 50%. Together, these results demonstrate that eBPF-based fault handling can improve performance and reduce resource usage in widely-deployed applications.

Janus: Multi-LLM Serving at Production Scale

Tianbao Zhou (Peking University), Yi Wang (JD Company), Yu Zhou (UCAS), Zirui Liu, Zhiming Wang, Yebo Peng (Peking University), Yongfu Wang (USTC), Yi Zhang, Jinrun Yin, Kemeng Tian (Peking University), Fangcheng Fu (SJTU), Tongxuan Liu, Tao Peng (JD Company), Tong Yang, Bin Cui, Xupeng Miao (Peking University), Ke Zhang (JD Company)
 Paper   Abstract 
Production LLM serving multiplexes hundreds of heterogeneous models on shared clusters, exposing three challenges that existing systems fail to address simultaneously: unpredictable bursts, power-law application popularity, and heterogeneous yet complementary resource demands. We present Janus, a Service–Engine co-designed multi-model serving system built around dual-timescale scheduling. At the Service layer, a Model Scheduler driven by a Performance Oracle combines vector bin-packing every 30 seconds for steady-state colocation with elastic scaling every 0.5 seconds. A new LST-IMH Request Scheduler maximizes SLO attainment with a proven 2-approximation guarantee. At the Engine layer, xTensor virtualizes HBM, while a three-state model lifecycle and device-to-device (D2D) fork enable elastic multi-model colocation and sub-second burst scaleout. We deploy Janus on a 768-device production cluster serving 62 applications and 45.6 M requests/day, and evaluate it with a 603 K-request open-loop replay sampled from that production day. Janus maintains 0.97–1.0 SLO attainment, versus 0.80–0.92 for the strongest baseline, while using 13,440 device-hours/day, 27% less than static Serverless-LLM. Janus is available as open source at https://github.com/Janus2026/Janus.

Linux AGX: An Adaptive GPU eXtension to Linux Fair Scheduling for Physical AI and Robotic Systems

Soheil Shirvani, Cong Liu (University of California Riverside)

LLM-42: Enabling Determinism in LLM Inference with Verified Speculation

Raja Gond (Microsoft Research), Aditya K Kamath (University of Washington), Ramachandran Ramjee, Ashish Panwar (Microsoft Research)
 Paper   Abstract 
In LLM inference, the same prompt may yield different outputs across different runs. At the system level, this non-determinism arises from floating-point non-associativity combined with dynamic batching and GPU kernels whose reduction orders vary with batch size. A straightforward way to eliminate non-determinism is to disable dynamic batching during inference, but doing so severely degrades throughput. Another approach is to make kernels batch-invariant; however, this tightly couples determinism to kernel design, requiring new implementations. This coupling also imposes fixed runtime overheads, regardless of how much of the workload actually requires determinism.

Inspired by ideas from speculative decoding, we present LLM-42—a scheduling-based approach to enable determinism in LLM inference. Our key observation is that if a sequence is in a consistent state, the next emitted token is likely to be consistent even with dynamic batching. Moreover, most GPU kernels use shape-consistent reductions. Leveraging these insights, LLM-42 decodes tokens using a non-deterministic fast path and enforces determinism via a lightweight verify–rollback loop. The verifier replays candidate tokens under a fixed-shape reduction schedule, commits those that are guaranteed to be consistent across runs, and rolls back those violating determinism. LLM-42 mostly reuses existing kernels unchanged and incurs overhead only in proportion to the traffic that requires determinism.

Lion: Modular Verification of Async Runtime Liveness

Ti Zhou, Zihao Zhang, Omar Chowdhury, Shuai Mu (Stony Brook University)

LMTracer: Fine-Grained and Real-Time Performance Profiling for Production LLM Systems

Wei Liu (Rank Computing and Tsinghua University), Yongchao He, Bohan Zhao, Hongyi Wang, Zhenhua Li (Tsinghua University), Junping Zhao (Rank Computing)

M2K: Making the Model-Kernel Interface Explicit for Reliable CUDA Kernel Verification

Mengting He, Shihao Xia (The Pennsylvania State University), Haomin Jia (SKLP, Institute of Computing Technology, Chinese Academy of Sciences), Wenfei Wu (Peking University), Linhai Song (SKLP, Institute of Computing Technology, Chinese Academy of Sciences)
 Paper   Abstract 
The widespread adoption of large language models (LLMs) has made GPU-accelerated inference a critical part of modern computing infrastructure. Production inference systems rely on CUDA kernels to implement core transformer operations, yet these kernels are highly susceptible to memory-safety bugs due to model-dependent tensor layouts, intricate memory indexing, and massive thread-level parallelism. Such bugs can corrupt model weights, crash inference services, or even enable adversarial attacks. Existing techniques either depend on unavailable hardware, incur high overhead, or fail to handle kernel inputs with variable lengths, and none can effectively detect CUDA memory bugs in LLM inference systems.

This paper presents Model2Kernel, the first practical system for automatically verifying the memory safety of CUDA kernels used in LLM inference. Model2Kernel performs model-aware dynamic analysis to determine how each model invokes kernels and to classify kernel arguments as either fixed by the model architecture or controlled by model users. Using this information, Model2Kernel then applies CUDA-specialized symbolic execution, supported by new abstractions for dynamic tensor memory and thread identifiers, to accurately pinpoint memory bugs in kernels. In the evaluation on CUDA kernels and models from vLLM, Hugging Face, and recent LLM research papers, Model2Kernel discovers 353 previously unknown bugs while producing only nine false positives, demonstrating its effectiveness.

MCon: Building an Elastic Cloud for Android Applications with Framework Consolidation

Jiaxing Qiu, Zijie Zhou, Zhenhua Li, Hongyi Wang, Zizhang Liu, Yunhao Liu (Tsinghua University), Yumeng Liang (China Telecom Cloud Computing Research Institute), Jie Wu (China Telecom Cloud Computing Research Institute & Temple University), Wen Xia (Harbin Institute of Technology, Shenzhen), Tianyin Xu (University of Illinois Urbana-Champaign)

MeshRT: Compile-Time Governed Wafer-Scale Runtime for Low-Latency High-Throughput Inference

Congjie He, Le Xu, Zhan Lu, Yeqi Huang, Haocheng Xiao, Cheng Deng (University of Edinburgh), Lingxiao Ma, Ziming Miao, Fan Yang (Microsoft Research), Luo Mai (University of Edinburgh)

On-site, Non-speculative Failure Diagnosis with CLODS

Rishikesh Devsot (YScope), Yi Fan Yu (University of Toronto), ChenXing Yang (University of Toronto and YScope), Ellen Shi (University of Toronto), Ding Yuan (University of Toronto and YScope)

PirateShip: Append-Only Ledgers for (Mostly) Trusted Execution Environments

Shubham Mishra (University of California, Berkeley), João Gonçalves (INESC-ID & IST U. Lisboa), Chawinphat Tankuranand, Natacha Crooks, Neil Giridharan (UC Berkeley), Heidi Howard, Chris Jensen (Azure Research, Microsoft)
 Paper   Abstract 
Distributed ledgers are increasingly relied upon by industry to provide trustworthy accountability, strong integrity- protection, and high availability for critical data without centralizing trust. Recently, distributed append-only logs are opting for a layered approach, combining crash-fault-tolerant (CFT) consensus with hardware-based Trusted Execution Environments (TEEs) for greater resiliency. Unfortunately, hardware TEEs can be subject to (rare) attacks, undermining the very guarantees that distributed ledgers are carefully designed to achieve. In response, we present Proteus, a new distributed consensus protocol that cautiously trusts the guarantees of TEEs. Proteus carefully embeds a Byzantine fault-tolerant (BFT) protocol inside of a CFT protocol with no additional messages. This is made possible through careful refactoring of both the CFT and BFT protocols such that their structure aligns. Proteus achieves performance in line with regular TEE-enabled consensus protocols, while guaranteeing integrity in the face of TEE platform compromises.

ProbeFS: Hierarchical DNA File Systems via Biochemical Content Addressability and Parallelism

Ruihan Li, Yuankun Zhang, Mingkai Dong, Yaya Hao, Fei Wang, Chunhai Fan, Haibo Chen (Shanghai Jiao Tong University)

QProf: Fleetwide Transitive Cost Profiling of Warehouse-Scale Services

Sam (Likun) Xi, Ali Sheikh, Alexey Alexandrov, Ning Wang, Vance Lankhaar, Tipp Moseley, Parthasarathy Ranganathan (Google)

RPCShield: Defending Microservices Against Cascading Failures

Milind Chabbi, Sonal Mahajan (Uber Technologies), Ivan Beschastnikh (University of British Columbia), René Just (University of Washington), Yuxin Wang, Yufan Xu (Uber Technologies), Elton Pinto (Georgia Institute of Technology), Seemanta Saha (Uber Technologies), Manu Sridharan (University of California, Riverside), Abhishek Jha, Sandeep Koushik Sheshadri, Mayank Bansal (Uber Technologies)

SANDHI: Fine-grained Merging for Memory Efficient Multi-Model Serving

Vima Gupta, Oytun Kuday Duran, Nandan Suresh Meda, Ikhyun An (Georgia Institute of Technology), Ganesh Ananthanarayanan (Microsoft), Anand Iyer (Georgia Institute of Technology)

Scalable Context Orchestration for Serving LLMs Over Voice

Linyi Jiang (Shanghai Jiao Tong University, AgenticSys), Silvery D. Fu (AgenticSys), Yifei Zhu (Shanghai Jiao Tong University)
 Paper   Abstract 
Voice AI applications are gaining popularity as advances in large language models (LLMs) enable more natural and accessible spoken interactions. Serving these applications requires accounting not only for what users say, but also for how they speak (e.g., speaking rate) and the conditions under which their audio is captured and transmitted (e.g., background noise and packet loss). However, existing LLM systems represent conversation context as a flat, growing sequence of messages, leaving voice-specific context implicit in the audio. As a result, they can generate responses that are poorly aligned with user preferences, degrade interaction quality under adverse environmental conditions, and incur high costs over long voice sessions.

We present llmovoice, a context-management middleware that explicitly models voice context and orchestrates its use. At each turn, llmovoice constructs a bounded voice context from the current user input, relevant interaction history, and explicit paralinguistic and environmental states. It then uses the serving LLM to reason over this context and generate runtime directives that guide how the system responds. We evaluate llmovoice on real-world voice applications and benchmarks. It reduces speaking-rate alignment error by 52.4%, lowers the false-interruption rate from 46.0% to 0.9% under packet loss, and reduces model usage cost by 79.2%. For long sessions, llmovoice reduces per-turn cost by up to 24.9× while retaining up to 98.7% of baseline answer quality.

Scheduling Linux Threads under I/O Chiplet Wall Using cSwitch

Seunghyun An, Joontaek Oh, Ming Liu (University of Wisconsin-Madison)

Sintr: Safe Interactive Transactions in the Presence of Byzantine Clients

Austin T. Li, Daniel H. Lee, Lorenzo Alvisi (Cornell University), Natacha Crooks (UC Berkeley), Florian Suri-Payer (Cornell University / Databricks)
 Paper   Abstract 
Byzantine fault-tolerant (BFT) systems are, in principle, an appealing foundation for transactional applications involving mutually distrustful participants. Yet their adoption has been hampered by two persistent stumbling blocks—performance and developer convenience—which are often in tension with one another. Recent systems show promising progress on both fronts by shifting to a client-centric architecture; clients execute transactions locally and concurrently, while the system resolves any data conflicts to maintain database serializability.

We argue that, in its current form, this approach introduces a critical vulnerability: it leaves the integrity of the database exposed to Byzantine clients, which may issue malicious or incorrect transactions. We address this threat with Sintr, a framework that prevents Byzantine clients from compromising database integrity by executing rogue transactions. Sintr combines redundant execution to validate transaction outcomes with a flexible, heterogeneous policy framework for expressing an application's data integrity requirements. We apply Sintr to harden several existing BFT database systems and find that it imposes only modest overheads—3%–16% in throughput and 3%–21% in latency.

Skill VM: Write Once, Run Everywhere Efficiently

Le Chen, Erhu Feng, Yubin Xia, Haibo Chen (Shanghai Jiao Tong University)
 Paper   Abstract 
LLM agents increasingly adopt skills as a reusable unit of composition. While skills are shared across diverse agent platforms, current systems treat them as raw context, causing the same skill to behave inconsistently for different agents. This fragility undermines skill portability and execution efficiency.

To address this challenge, we analyze 118,000 skills and draw inspiration from traditional compiler design. We treat skills as code and LLMs as heterogeneous processors. To make portability actionable, we decompose a skill's requirements into a set of primitive capabilities, and measure how well each model-harness pair supports them. Based on these capability profiles, we propose SkVM, a compilation and runtime system designed for portable and efficient skill execution. At compile time, SkVM performs capability-based compilation, environment binding, and concurrency extraction. At runtime, SkVM applies JIT code solidification and adaptive recompilation for performance optimization.

We evaluate SkVM across eight LLMs of varying scales and three agent harnesses, covering SkillsBench and representative skill tasks. Results demonstrate that SkVM significantly improves task completion rates across different models and environments while reducing token consumption by up to 40%. In terms of performance, SkVM achieves up to 3.2× speedup with enhanced parallelism, and 19–50× latency reduction through code solidification.

Smaran: Serving Authenticated Time Travel Queries

Asim Nepal, Shistata Subedi (University of Oregon), Shubham Mishra (University of California, Berkeley), Suyash Gupta (University of Oregon), Aniket Kate (Purdue University), Hein Meling (University of Stavanger)
 Paper   Abstract 
Time-travel queries ask what data looked like at a past time or over an interval. Modern databases support time-travel queries, but this support is insufficient for applications that cannot trust the query server, such as secure messaging and decentralized applications, where clients need proofs that the returned results are correct. Existing approaches either require aggregating evidence from multiple auditors, incur per-step proof costs that scale linearly with history length, or impose massive storage and communication costs.

In this paper, we introduce Smaran, an authenticated data structure that enables servers to answer time-travel queries efficiently with a constant number of fixed-size proofs, independent of the query range. Smaran achieves this through a novel integration of segment trees with vector commitments, sidestepping scalability challenges as history grows via a hierarchical architecture, and avoiding redundancy by introducing versioned vector commitments.

Sockeye: Bug-finding and proofs for platform configurations and hardware based on reference manuals

Ben Fiedler, Sedan Abdelgawad, Teymour Aldridge, Viktor Fukala, Jan Häussermann, Gamal Hassan, Lars Leuthold, Konstantin Lucny, Max Wierse, Samuel Gruetter, Timothy Roscoe (ETH Zurich)
 Paper   Abstract 
The ever increasing complexity of hardware platforms poses a challenge to systems programmers. Correctly programming a multitude of components, providing functionality and security, is difficult: semantics of individual units are described in prose, underspecified, and prone to inaccuracies. Rigorous statements about platform security are often impossible.

We introduce a domain-specific language to describe hardware semantics, assumptions about software behavior, and desired security properties. We then create machine-readable specifications for a diverse set of eight platforms from their reference manuals, and formally prove their (in-)security. In addition to security proofs about memory confidentiality and integrity, we discover a handful of documentation errors. Finally, our analysis also revealed a vulnerability on a real-world server chip, which was confirmed by the vendor to apply to a wide family of deployed network appliances. Our tooling offers system integrators a way of formally describing security properties for whole platforms, and the means to find counterexamples, or proving them correct.

StarfishOS: Revisiting Single System Image on CXL with State-partitioned Microkernel

Fangnuo Wu (Institute of Parallel and Distributed Systems, Shanghai Jiao Tong University), Jingsheng Yan, Mingkai Dong, Wenjun Cai (Shanghai Jiao Tong University), Jingwei Xu (Institute of Parallel and Distributed Systems, Shanghai Jiao Tong University), Tong Xin, Haibo Chen (Shanghai Jiao Tong University)
 Paper   Abstract 
Single System Image (SSI) offers an attractive OS abstraction that enables single-machine applications to transparently execute on multiple machines and utilize pod-wide resources. The emergence of Compute Express Link (CXL) shifts cross-machine synchronization from message passing to coherent shared memory, potentially removing SSI's long-standing performance barrier. However, placing state in slow CXL memory degrades performance and makes the system vulnerable to partial failures, since inconsistent CXL-resident state may block or crash the whole system.

We observe that microkernels' small kernel-state footprint and capability-based state management make OS state explicit enough to partition and minimize what resides in CXL. We therefore propose the state-partitioned microkernel and realize it in StarfishOS, the first OS-level SSI to use CXL shared memory while preserving both efficiency and OS-level partial-failure resilience through minimal, recoverable CXL state. Evaluation shows that applications can transparently scale to the full pod on StarfishOS with up to 4× and 2× speedup compared to their distributed and CXL-optimized versions. Moreover, StarfishOS utilizes all stranded CPU resources by running applications across machines

State-Aware Fuzzing of JavaScript Engines with LLM-Guided Instrumentation

Wai Kin Wong (Hong Kong University of Science and Technology), Dongwei Xiao (The Hong Kong University of Science and Technology), Anthony Cheuk Tung LAI (VX Research Limited), Ping Fan Ke (Singapore Management University), Shuai Wang (Hong Kong University of Science and Technology)

StreamEP: Straggler-Tolerant MoE Decoding without Communication Barriers

Yizhuo Liang, Shaoyu Wang (University of Southern California), Jaeyong Song (Seoul National University), Yanqi Zhou (Google DeepMind), Geon-Woo Kim (The University of Texas at Austin), Guangrong He, Seo Jin Park (University of Southern California)
 Paper   Abstract 
Mixture-of-Experts (MoE) architectures scale large language models (LLMs) to hundreds of billions of parameters. Serving a single MoE model requires multiple GPUs operating in parallel, typically through tensor parallelism (TP) or expert parallelism (EP). The optimal choice depends on the number of in-flight requests: TP is faster at low concurrency, whereas EP wins at high concurrency. Production workloads cross this boundary continually: online serving sees bursty arrivals that subside into quiet periods, and reinforcement-learning rollouts begin as a high-concurrency burst that decays into a long tail of stragglers. Pinning either layout therefore forfeits performance when the workload crosses to the other side.

We present Moebius, a serving system that switches between EP and TP at runtime without restarting the engine or dropping in-flight requests. Our key insight is that EP and TP are two layouts of one model, not two models: they compute the same function over byte-identical expert weights and KV cache, so a switch changes only which rank owns each slice. Moving those owner-changed slices is the sole irreducible cost, and modern high-bandwidth GPU interconnects make it fast enough to do between decode steps without draining in-flight requests. Moebius preserves each parallelism's runtime resident, and reshards the single copy of expert weights and KV cache at fixed addresses with fused GPU-to-GPU transfer kernels. On 8×H200 GPUs serving Qwen3-235B-A22B, Moebius matches the better static parallelism at every operating point, and beats it on RL rollouts by 1.16–1.25× across steps. Each switch completes in 215–434 ms, and Moebius holds both layouts resident with only 2.4% memory overhead.

Tamias: Feedback-Guided Systematic Concurrency Exploration for Transparent Distributed System Fuzzing

Congyu Liu, Yaoxu Song, Pedro Fonseca, Yongle Zhang (Purdue University)

Taming Dynamism on GPUs: Cross-SM Kernel Fusion via SM Cooperation and Just-in-Time Reduction

Jingkai He, Guangda Sun, TianJian Li, Dong Du, Yubin Xia, Haibo Chen (Shanghai Jiao Tong University)

Taming Inference Workloads at Global Scale: Foundation Model Serving in Amazon Bedrock

Pratik Pankaj Raichura, Somu Perianayagam, Rama Krishna Sandeep Pokkunuri, Divya Jain (Amazon Web Services)

TensorDex: A Compact, Tensor-Centric Storage System for Modern AI Models

Tingfeng Lan, Zirui Wang (University of Virginia), Yunjia Zheng (Harvard University), Zhaoyuan Su (University of Virginia), Juncheng Yang (Harvard University), Yue Cheng (University of Virginia)
 Paper   Abstract 
Modern model hubs now store tens of petabytes of large language models (LLMs), with fine-tuned variants overwhelmingly dominating storage footprint. While delta compression is a natural fit for reducing redundancy, existing approaches fail in practice: model lineage metadata is often missing or unreliable, and naive pairing strategies lead to poor compression quality. Our analysis of real-world repositories reveals two fundamental findings: effective compression requires data-driven pairing rather than metadata-based heuristics, and redundancy emerges at the fine-grained tensor level rather than the model level.

This paper presents TStore, a tensor-centric storage system that rethinks model storage compression by treating tensors—not models—as the first-class citizen for delta compression. TStore decomposes models into tensors, predicts tensor-pairwise compressibility using compact bit-level fingerprints that capture tensor content, and incrementally organizes tensors into multi-center clusters that adapt as new models arrive. Together, these components form an end-to-end model compression pipeline that continuously uncovers cross-tensor redundancy at scale. Evaluations on a real-world trace of 2,890 randomly sampled Hugging Face models show that TStore reduces storage footprint by 70.5%, 37% lower than state-of-the-art design. Meanwhile, it achieves 22.9 GB/s compression and 28.4 GB/s decompression throughput, which are 3.86× and 1.49× faster than the next-best system, respectively.

TensorHub: Scalable and Elastic Weight Transfer for LLM RL Training

Chenhao Ye (University of Wisconsin–Madison), Huaizheng Zhang, Mingcong Han, Baoquan Zhong, Xiang Li, Qixiang Chen, Xinyi Zhang, Weidong Zhang, Kaihua Jiang, Wang Zhang, Sun He, Wencong Xiao (ByteDance Seed), Andrea Arpaci-Dusseau, Remzi Arpaci-Dusseau (University of Wisconsin–Madison)
 Paper   Abstract 
Modern LLM reinforcement learning (RL) workloads require a highly efficient weight transfer system to scale training across heterogeneous computational resources. However, existing weight transfer approaches either fail to provide flexibility for dynamically scaling clusters or incur fundamental data movement overhead, resulting in poor performance.

We introduce Reference-Oriented Storage (ROS), a new storage abstraction for RL weight transfer that exploits the highly replicated model weights in place. ROS presents the illusion that certain versions of the model weights are stored and can be fetched on demand. Underneath, ROS does not physically store any copies of the weights; instead, it tracks the workers that hold these weights on GPUs for inference. Upon request, ROS directly uses them to serve reads. We build TensorHub, a production-quality system that extends the ROS idea with topology-optimized transfer, strong consistency, and fault tolerance. Evaluation shows that TensorHub fully saturates RDMA bandwidth and adapts to three distinct rollout workloads with minimal engineering effort. Specifically, TensorHub reduces total GPU stall time by up to 6.7× for standalone rollouts, accelerates weight update for elastic rollout by 4.8×, and cuts cross-datacenter rollout stall time by 19×. TensorHub has been deployed in production to support cutting-edge RL training.

Testing Custom Control Planes Without the Cluster

Tim Goodwin, Lindsey Kuper, Andi Quinn (University of California, Santa Cruz)

Tierce: Observability-Driven Tiered Memory Management for Colocated Workloads

Hanchen Xu, Berkay Inceisci, Hao Li, Zhenyu Zhang, Huaicheng Li (Virginia Tech)
 Paper   Abstract 
Tiered memory systems rely on hardware signals to estimate page criticality and decide which pages should remain in fast memory. Colocation corrupts these estimates at two points: shared LLC interference changes whether accesses reach memory, and downstream memory contention changes their stall cost. Both effects blend colocated workloads' behavior into shared page-criticality estimates, creating a fundamental observability gap for tiered memory management. We present Tierce, an observability substrate for colocated tiered memory. Tierce estimates workload-local exposed stall by measuring per-workload memory-level parallelism and scoring pages by realized access latency. It bounds LLC interference with explicit cache-way allocation. Across 8 colocated pairs that run four foreground workloads against a bandwidth-intensive and a bursty, phase-varying co-runner, Tierce outperforms PACT, the best prior art, on every pair, by 2.2% to 12.6%.

Turning Linux into a High-Performance Library OS with Flux

Kaifu Tian, Youjie Zheng, Yiren Zhang, Yuyang You, Keyang Hu (Tsinghua University), Kang Chen (Peking University, Tsinghua University), Yu Chen (Tsinghua University)

TuxBot: Semantic-Aware Online OS Tuning with LLMs

Georgios Liargkovas, Mihir Nitin Joshi (Columbia University), Hubertus Franke (IBM Research), Kostis Kaffes (Columbia University)
 Paper   Abstract 
Online OS tuning can improve long-running services, but existing controllers are poorly matched to live hosts. They treat scheduler, power, memory, and I/O controls as black-box variables and optimize a scalar reward. This view ignores cross-knob policy structure, breaks down when application metrics are unavailable, and can send a running service into degraded regions that persist after the bad setting is removed. We present TuxBot, a host-side framework for steady-state OS tuning with bounded language-model guidance. TuxBot turns knob schemas, telemetry, current configuration, recent action–response history, and retrieved prior runs into a compact decision context. A fast loop proposes low-latency updates, a slower loop periodically revises the search strategy, and every proposed change passes through typed validation before reaching kernel or sysctl interfaces. This lets the controller reason about OS-control meaning and indirect performance signals while keeping model cost, latency, and authority constrained. We evaluate TuxBot on 13 live workloads from five benchmark suites while tuning up to 41 Linux parameters. Across the suite, TuxBot improves stable-phase performance by 72.5% over default settings and by 153.3% relative to the strongest non-LLM baseline. A 30-window session costs about $0.20 in model calls. With only host-level metrics, TuxBot still outperforms baselines given direct application objectives by 93.7 percentage points, while avoiding severe degraded regions reached by structure-blind exploration.

Validating a Production Cloud Object Store with Lightweight Formal Methods

Vimuth Fernando, Rajeev Joshi, Bernhard Kragl (Amazon Web Services), Julien Mascart (Meta), Matthew Russo, Sarek Skotåm, Colin Walker, Jake Wires (Amazon Web Services)

Validating Rust Compilers with Trait-Type Constraint Graph

Xin Lai, Ming Wen, Xiaofei Liao, Hai Jin (Huazhong University of Science and Technology)

Verifying a high-performance distributed transaction system using permissioned state machines

Yun-Sheng Chang (MIT), Joseph Tassarotti (New York University), Frans Kaashoek, Nickolai Zeldovich (MIT)
 Paper   Abstract 
Tulip is a high-performance distributed transaction system that uses sharding for scalability, replication within each shard for fault tolerance, and TAPIR-style inconsistent replication for high performance. Tulip comes with a machine-checked proof of correctness showing that its implementation meets a simple specification identical to a local strictly serializable transaction system, abstracting away implementation details such as crash recovery, multi-versioning, replication, sharding, and coordinator recovery.

The contribution of this paper is the permissioned state machine (PSM) approach, which extends TLA-style protocol reasoning with ideas from concurrent separation logic. PSM enables the developer to specify and verify complex protocols, such as Tulip, by breaking them down into smaller modules. PSM makes all dependencies between modules explicit using permissions, which limits the ways these modules can interact, and thereby reduces proof effort.

The prototype of Tulip consists of 3,956 lines of Go code, achieving performance competitive with that of TAPIR. Tulip’s proof is decomposed into 10 types of modules; the majority of logical proof steps (“actions”) involve just one module, demonstrating that PSM enables local reasoning.

VoliStorM: A Crash-Consistent I/O Cache with Two Kernels Instead of Two Caches

Jana Toljaga, Nicolas Derumigny, Tara Aggoun, Mathieu Bacou, Gaël Thomas (Samovar, Inria, Télécom SudParis, Institut Polytechnique de Paris)

Wavel: A Fast and Efficient Compilation System for Wafer-Scale Accelerators

Yeqi Huang, Congjie He, Haocheng Xiao, Yanwei Ye, Yi-Chieh Wang, Boyao Song, Yangshen Deng (University of Edinburgh), Ziming Miao, Lingxiao Ma, Fan Yang (Microsoft Research), Luo Mai (University of Edinburgh)

Welder: Compositional Liveness Verification of Cluster Control Planes

Zhizhen Cathy Cai, Nikhil Date, Jiawei Tyler Gu (University of Illinois Urbana-Champaign), Cody Rivera, Tej Chajed (University of Wisconsin-Madison), Oded Padon (Weizmann Institute of Science), Tianyin Xu (University of Illinois Urbana-Champaign), Xudong Sun (University of Toronto)
 Paper   Abstract 
We present the first compositional approach to formally verifying cluster control planes such as Kubernetes. Control planes are large, distributed systems composed of interacting controllers with subtle liveness and safety dependencies. Our approach, Welder, emphasizes compositionality to make verification manageable and scalable. Welder makes threefold contributions on specification, proof, and implementation. First, Welder provides a general specification called COmpositional REconciliation (CORE). CORE states that a set of controllers collectively reconcile the cluster state correctly, precluding bugs in both individual controllers and cross-controller interactions. CORE is an open specification that enables compositional verification: if two compatible sets of controllers each implement CORE, so does their composition. Second, Welder introduces new proof techniques for compositional liveness reasoning about controller interactions, including liveness dependencies and interference. Third, we mechanize Welder as a framework and use it to implement and verify a fraction of the Kubernetes control plane—three core controllers and one custom controller. The verified controllers can readily be deployed in Kubernetes platforms with comparable performance to (unverified) official ones. Welder enables a progressive way to verify cluster control planes by gradually verifying that each controller implements CORE.

XTRA: Unifying Cache Coherence and Concurrency Control for Distributed Transactions in a CXL Pod

Zhijun Yang, Yu Hua, Ming Zhang, Menglei Chen, Xumin Chen, Aoyang Tong (Huazhong University of Science and Technology)
 Paper   Abstract 
Distributed transactions on CXL memory pools allow hosts to directly access shared data, bypassing message-based coordination. However, the limited cross-host hardware cache coherence (HCC) in CXL hinders synchronization for consistency and concurrency control across large memory pools. To overcome this limitation, we present XTRA, a novel synchronization architecture that efficiently scales CXL distributed TRAnsactions. XTRA decouples the synchronization state from individual data records, consolidating it into a compact directory within the HCC region, while keeping data in the large non-coherent pool. Distributed transactions leverage this decoupled directory to coordinate concurrent access across the entire shared pool. To ensure efficient and consistent access, XTRA unifies cache coherence with concurrency control by exploiting their semantic redundancy, directly repurposing transactional conflict detection to guarantee cache freshness lazily upon read. Furthermore, by using software mutual exclusion to manage the directory, XTRA's decoupled synchronization generalizes to commodity CXL memory without HCC, while preserving upper-layer protocols. Extensive evaluations demonstrate that XTRA improves throughput by up to 15.6× over state-of-the-art systems and reduces P50/P99 latency by up to 4.0×/283.9×.

You Can Always Get What You Want: CPU Virtualization Made Fast and Free

Yun Wang (Shanghai Jiao Tong University), Xingguo Jia, Ben Luo, Kenan Liu, Shengdong Dai, Jingdong Han, Weihao Chen (Alibaba Group), Xingzi Yu, Chenggang Wu (Shanghai Jiao Tong University), Yibin Shen, Jiesheng Wu (Alibaba Group), Tao Song, Zhengwei Qi, Haibing Guan (Shanghai Jiao Tong University)


  1. For example, if a paper introduces a new filesystem for LLM inference, I classified it as Storage & Databases rather than LLM Inference, considering that LLM Inference is “simply” the domain of application in this case. ↩