The 32nd ACM Symposium on Operating Systems Principles ended on October 2 at the Clarion Congress Hotel in Prague, with workshops on September 29 and the main program starting the next day. The accepted-papers page on the SIGOPS site lists more than 60 papers, and the same site still showed award winners as to be determined when this review was prepared. That makes this a reading list rather than a verdict: a guide to which accepted papers deserve a cloud architect’s attention before the proceedings settle into the usual hierarchy of citations.
One caveat governs everything below. The descriptions here come from paper titles, author affiliations and the program page, not from a close reading of every PDF. Where a title makes a claim, treat it as the authors’ claim and check the paper before relying on it.
Verification moves toward the control plane
The densest cluster in the program is verification and testing of the software that runs cloud infrastructure, and it points somewhere specific: away from kernels and file systems, toward control planes and protocols.
Several titles make the shift visible. Welder: Compositional Liveness Verification of Cluster Control Planes (University of Illinois Urbana-Champaign, Wisconsin-Madison, Weizmann Institute and Toronto authors) takes on the property that matters most to anyone who has watched a Kubernetes-style reconciler fail to converge: not that nothing bad happens, but that something good eventually does. Testing Custom Control Planes Without the Cluster (UC Santa Cruz) addresses the same class of software from the testing side, and Lion: Modular Verification of Async Runtime Liveness (Stony Brook) reaches down to the async runtimes those controllers are written in.
Two papers speak to protocol-level assurance. I3DP: Neuro-symbolic Inductive Invariant Inference for Distributed Protocols (Nanjing University, Hunan University and Birkbeck) targets the step that makes protocol proofs expensive, finding the inductive invariant. Verifying a High-Performance Distributed Transaction System Using Permissioned State Machines (MIT and NYU) goes after a full transaction system rather than a toy protocol.
The industrial entry is Validating a Production Cloud Object Store with Lightweight Formal Methods, from Amazon Web Services authors with a co-author at Meta. It follows the 2021 SOSP best-paper-winning ShardStore work on Amazon S3, which reported that lightweight formal methods prevented 16 issues from reaching production. A new paper on the same theme from a production team is worth reading for what has held up over five years of ongoing development.
For architects, the practical question these papers share is whether specifications and code stay in step. A companion article on this site, Formal Verification of Distributed Protocols in Practice, takes that gap up directly.
LLM serving is now a production-operations topic
The second cluster is serving, and its character has changed. Earlier systems-conference serving papers tended to argue for a mechanism on a benchmark. Several accepted papers this year describe what happens at fleet scale.
Taming Inference Workloads at Global Scale: Foundation Model Serving in Amazon Bedrock comes from AWS authors and, going by the title, describes a managed multi-tenant service rather than a research prototype. Janus: Multi-LLM Serving at Production Scale (Peking University and JD) and Batched in Back: Characterizing and Optimizing Offline LLM Inference in Production with ACDC (Alibaba and Shanghai Jiao Tong) are likewise framed around production deployments. The offline-batch angle is the less glamorous half of inference economics and one that cloud buyers rarely see characterized.
Two more titles speak to sharing hardware. Beyond Utilization: Energy-Conscious GPU Sharing for Inference Serving (UT Austin) argues for treating energy as a scheduling input, and SANDHI: Fine-grained Merging for Memory Efficient Multi-Model Serving (Georgia Tech and Microsoft) addresses the memory cost of hosting many models. If you run a shared GPU pool, these are the papers closest to your capacity-planning spreadsheet.
On the training side, A Few GPUs, A Whole Lotta Scale: Faithful LLM Training Emulation with CrystalLLM (Alibaba, Shanghai Jiao Tong, Harvard and Zhejiang) proposes emulating large training runs on a few GPUs. Anyone who plans cluster purchases or network designs without a spare thousand accelerators to experiment on should look at what fidelity it claims.
Shared logs, CXL and the next storage layer
A third thread concerns the substrate under distributed databases. AgileLog: A Forkable Shared Log for Agents on Data Streams (Illinois) and Borges: A Low-Latency Distributed Shared Log on a CXL Memory/SSD Hybrid (UT Austin, Illinois and others) both build on the shared-log abstraction that has underpinned replicated state for years, one adapting it to agent workloads and the other to CXL-attached memory.
CXL appears elsewhere too: Disk-Based LSMs: An Unexpectedly Good Index for Partly Coherent CXL Memory, XTRA: Unifying Cache Coherence and Concurrency Control for Distributed Transactions in a CXL Pod (Huazhong) and StarfishOS: Revisiting Single System Image on CXL with State-partitioned Microkernel (Shanghai Jiao Tong). Cloud architects do not need to design for CXL pods this year, but the single-system-image idea has a long history in distributed-systems research, and its return under a new hardware assumption is a reminder of how often the field revisits old abstractions when the cost model shifts.
On the storage side, TensorDex: A Compact, Tensor-Centric Storage System for Modern AI Models (Virginia and Harvard) targets how model weights are stored, which matters to anyone paying to keep many checkpoints.
Operating what you already run
The last group is the least fashionable and arguably the most useful for operations teams.
RPCShield: Defending Microservices Against Cascading Failures has Uber authors and a University of British Columbia co-author, and cascading failure is the failure mode that turns a single slow dependency into an outage. QProf: Fleetwide Transitive Cost Profiling of Warehouse-Scale Services comes from Google and treats cost attribution across a call graph as a profiling problem. On-site, Non-speculative Failure Diagnosis with CLODS (YScope and Toronto) and LMTracer: Fine-Grained and Real-Time Performance Profiling for Production LLM Systems (Tsinghua and Rank Computing) round out the diagnosis and profiling theme. DDB: Source-Level Interactive Debugging for Distributed Applications (USC) is the sort of tool that sounds obvious until you realize how rarely distributed debugging works well.
How to triage the list
A workable order for a platform or architecture team is to start with whichever cluster matches a decision you are about to make. If you are choosing how much assurance to demand of your own control-plane code, read the verification papers and note how much of the effort each one assumes. If you are sizing an inference fleet, read the production-serving papers and compare their workload descriptions against your own traffic before trusting any headline number. If you operate a large microservice estate, RPCShield and QProf are the shortest path from the program to a concrete change.
Two checks apply to all of them. Confirm the artifact status, since SOSP runs a Distinguished Artifact Award and available code makes a claim far easier to test. And wait for the final proceedings before quoting numbers, because the numbers in an accepted-papers listing do not exist yet; they live in the PDFs.
