ATC/OSDI’25 Technical Sessions

-

ATC and OSDI ran in parallel. As is tradition, OSDI was single-track; ATC had two parallel tracks. The schedules and papers are online as linked above.

USENIX is awesome: it has been open access for its conference proceedings since 2008. So you can access all the paper pdfs through the links above now. I believe the presentation videos will be made available soon as well. Kudos to USENIX!

I attended the OSDI opening remarks delivered by the PC chairs, Lidong Zhou (Microsoft) and Yuan Yuan Zhou (UCSD). OSDI saw 339 submissions this year, which is up 20% from last year. Of those, 53 were accepted, for an acceptance rate of 16%. The TPC worked through Christmas to keep the publication machine running. We really are a bunch of workaholics. Who needs family time when you have rebuttals to respond to?

OSDI gave two best paper awards:

  • Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols. Tony Nuda Zhang and Keshav Singh, University of Michigan; Tej Chajed, University of Wisconsin-Madison; Manos Kapritsos, University of Michigan; Bryan Parno, Carnegie Mellon University
  • Building Bridges: Safe Interactions with Foreign (programming) Languages through OmniGlot. Leon Schuermann and Jack Toubes, Princeton University; Tyler Potyondy and Pat Pannuto, University of California San Diego; Mae Milano and Amit Levy, Princeton University

The Distinguished Artifact award went to: PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection. Hayley LeBlanc, University of Texas at Austin; Jacob R. Lorch and Chris Hawblitzel, Microsoft Research; Cheng Huang and Yiheng Tao, Microsoft; Nickolai Zeldovich, MIT CSAIL and Microsoft Research; Vijay Chidambaram, University of Texas at Austin

2026 OSDI' will be in Seattle organized by Eddie Kohler (Harvard)  and Amar Phanishayee (Meta).


Emery Berger’s Keynote: Accelerating software development, the LLM revolution

Deniz Altinbuken (ATC cochair) introduced the OSDI/ATC-joint keynote speaker: Professor Emery Berger of Umass Amherst, who is also an Amazon scholar. Emery's Plasma lab is a birthplace of many interesting projects: Scalene, Hoard, DieHard. Emery is sigma. I mean, he has an ACM Sigma distinguished service award, and he is an ACM fellow. He is also the creator of cs-ranking, which he keeps getting occasional hate mail every now and then. 

Emery gives great talks. I think this was the best presentation across all OSDI and ATC sessions. What is Emery's secret? Like other good speakers, rehearsing crazy number of times and preparing really well.

His talk was about the coming Cambrian explosion of LLM-augmented developer tools. Here’s the gist: "Traditional software development is the dinosaur. LLMs is the asteroid. Cambrian explosion is coming for tooling, not just apps. So let’s evolve in order not to go extinct."

He first introduced the framework he used repeatedly for the new generation of LLM-enhanced tools coming out of his lab.

  • Evolve.
  • Exploit a niche.
  • Ensure fitness.

He argued throughout the talk that AI-assisted tools can deliver the best of both worlds precision from PL, and flexibility from LLMs.

Scalene: Evolving the Profiler. Emery's group LLM-augmented Scalene their Python profiler tool, to not only pinpoint inefficiencies in your code but also to explain why your code is slow and provide suggestions on how to fix them. Common suggestions include: replace interpreted loops with native libraries, vectorize, use GPU. LLMs help generate optimization suggestions with surprising performance boosts (sometimes 90x). That was evolve (adopt LLMs), and exploit a niche (profiler knows where code is inefficient, why it is inefficient). The ensure fitness comes from running the optimized code against the original. 

chatDBG: Evolving a Debugger. Most developers don’t use debuggers. Print statements are more popular. Why? Because debuggers are clunky and stagnant. chatDBG changes this. It turns the debugger into a conversational assistant. You can type "why" at the prompt, and it gives you the root cause and a proposed fix. You can query code slices, symbol declarations, even ask for documentation. The LLM has access to dynamic program state and source context provided by the debugger, and external knowledge provided by huge real world training. Success rates improved with more context: 25% (default stack), 50% (with "why"), 75–80% (with targeted queries). Safety is enforced using containers and command whitelists. Again: evolve the interface, exploit the niche (source + state + knowledge), ensure fitness (bounded functionality and testable fixes).

cwhy: Evolving a Compiler. C++ compiler errors are notoriously incomprehensible. cwhy wraps around Clang++ and gives human-readable explanations with concrete fix suggestions. It uses git diffs to localize the cause and context of the error. The assumption: if it compiled yesterday and not today, something broke in the diff. cwhy figures out what and suggests ways to fix it. It even handles things like regex errors. This tool impressed a library author so much that they adopted it after cwhy fixed a bug in their freshly published code.

coverup: Evolving a Coverage Tool. Writing good tests is hard and thankless. Coverage reports only cause guilt-trips. LLMs can write tests, but cannot methodically increase coverage. Coverup is a next-gen testing assistant.  It builds on slipcover (Plasma's coverage analysis tool), then uses LLMs to generate new test cases that increase branch coverage methodically.

flowco: Rethinking Notebooks. Jupyter notebooks are the lingua franca of data science. But they're also a mess: brittle, unstructured, and difficult to maintain. Flowco reimagines notebooks as dataflow graphs. Each step (load, clean, wrangle, visualize) is a node in the graph/pipeline. LLMs guide code generation at each step. Combined with pre/post condition checks, you get a smart notebook that requires no code but ensures correct workflows. The metaphor shift from script to graph is what enables notebooks to evolve.


The talk was a tour-de-force across many tools showing how LLMs can help them evolve and improve significantly. Emery is doing a big service building these tools to help all developers. Based on my interactions with talented coders, I have come to conclude that LLMs actually boost performance way more for experts than beginners. I think these tools will help all kinds of developers, not just experts. 


Using Provenance Invariance to automate proofs

This paper was one of the standout papers from OSDI'25, and winner of a Best Paper Award. The lead author, Tony Zhang, inow an engineer at Databricks, was a PhD student at University of Michigan and a MongoDB PhD Fellow. He delivered a sharp, polished talk. Here is my reconstruction from my notes.

Distributed protocols are notoriously hard to get right. Testing can show the presence of bugs but never their absence. Formal verification can give stronger correctness guarantees, but only if you can manage to prove your protocol satisfies a desired safety property. This involves crafting an inductive invariant: one that holds initially, implies the safety property, and is closed under protocol transitions.

Coming up with a suitable inductive invariant is hard. It's an iterative process: guess, check, fail, refine, repeat. You often start with a property you care about (say, agreement), only to find it isn’t inductive. Then you strengthen it with auxiliary lemmas and conditions. If you are skilled and somewhat lucky, you eventually get there. I wrote a bit about this loop back in 2019, after SOSP’19 on an earlier effort on this problem.

Basilisk’s goal is to short-circuit this painful invariant discovery loop using provenance invariants. Provenance invariants relate a local variable at a node to its provenance: the causal step or message that caused the variable to have its current value. For example, instead of guessing an invariant like "If replica A has voted yes, then replica B must also have voted yes," Basilisk works backwards to discover why A voted yes and then connects that cause to B’s state. Sort of history variables on steroids. By tracing data dependencies across steps and messages, Basilisk derives inter-host invariants that explain not just what the state is, but how it came to be.

Basilisk builds on the authors' prior work Kondo, which had two types of invariants:

  • Protocol invariants (expressive but hard to generate automatically)
  • Regular invariants (mechanically derivable but low-level)

Basilisk generalizes this by introducing host provenance (HP) and network provenance (NP). HP traces a variable's value to a local decision; NP traces it to a message received. Together, these form a causal chain, or witness, which Basilisk uses to justify why a state is safe.

The provenance invariants replace the original inductive invariant. Then Basilisk proves that these provenance invariants imply the desired property. All of this is implemented in a toolchain that extends the Dafny language and verifier. Protocols are modeled as async state machines in Dafny, Basilisk analyzes them, and outputs inductive invariants along with machine-checkable proofs. Basilisk was evaluated on 16 distributed protocols, including heavyweights like Paxos, MultiPaxos, and various consensus and replication variants.


Tigon: A Distributed Database for a CXL Pod

Traditional distributed databases synchronize over the network. This means network overhead, message exchange complexity, and coordination cost. Tigon replaces that network with a CXL memory pod. Instead of using sockets and RPCs, nodes coordinate using inter-host atomic instructions and hardware cache coherence. The only downside is this is only a single-rack-scale database design, which also comes with unavailability disadvantages.

There are still challenges remaining with this architecture. The CXL memory has higher latency (250–400ns) and lower bandwidth than local DRAM. It also provides limited hardware cache coherence capacity. Tigon addresses this with a hybrid architecture: partitioned and shared. All control-plane synchronization is done via CXL-coherent memory. And messages are only exchanged for data movement. 

To minimize coherence pressure, they compact metadata into 8-byte words and piggyback coordination info. They also show how to eliminate two-phase commit by taking advantage of reconstructability during crash recovery. The system is single-rack and does not replicate. It's built on a fail-stop assumption, and scaling (adding/removing nodes) requires restart. Evaluated on TPC-C and a YCSB variant using simulation experiments (since the hardware is not there), Tigon outperforms existing CXL-based shared-nothing DBs by up to 2.5x, and RDMA-based systems by up to 18.5x.


Mako: Speculative Distributed Transactions with Geo-Replication

Geo-replicated transactions are hard. The cost of consensus across data centers kills latency and throughput. Mako sidesteps this by decoupling execution from replication. Transactions execute speculatively using two-phase commit (2PC, Tupac) locally, without waiting for cross-region consensus. Replication happens in the background to achieve fault-tolerance.

The core idea is to allow transactions to commit optimistically and only roll back if replication later fails. This opens the door to cascading aborts, and Mako tries to alleviate unbounded rollback problem by tracking transactional dependencies using vector clocks.

Ok, but there is another problem. How do you get consensus among nodes on roll back when the speculative/optimistic execution fails. This was not explained during the talk, and I brought this up during Q&A. The answer seems to be using epochs and sealing, and doing this in a delayed manner. This could open more problems. I haven't read the paper to understand how this works.   


Skybridge: Bounded Staleness in Distributed Caches

From Meta (I guess we are not calling it Facebook anymore), this paper addresses the pain of eventual consistency in global cache layers. Eventual is fine for most cases, until it's not. Products like Facebook and Instagram rely on caches being mostly up-to-date. Inconsistencies may cause some occasional weird bugs, user confusion, and degraded experience.

Skybridge is an out-of-band replication stream layered on top of the main async replication pipeline. It adds redundancy without relying on the same code paths, avoiding correlated failures. Skybridge focuses only on timely delivery of updates, not durability.

Skybridge itself is also eventual consistency, but being lightweight it gives you bounded consistency almost always. By leveraging Bloom filter-based synchronization, Skybridge provides a 2-second bounded staleness window for 99.99998% of writes (vs. 99.993% with the baseline). All that, at just 0.54% of the cache deployment size because of reduced scope in this superposed/layered system.


SpecLog: Low End-to-End Latency atop a Speculative Shared Log

Shared logs are foundational in modern distributed systems (e.g., Corfu, Scalog, Boki). They are deployed in Meta (formerly Facebook) as I discussed here earlier. But their latency is often too high for real-time workloads because coordination delays application progress. SpecLog proposes speculative delivery: let applications start processing records before the final global order is fixed.

To make this safe, they introduce Fix-Ante Ordering: a mechanism that deterministically assigns quotas to each shard ahead of time. If each shard sticks to its quota, the global cut is predictable. If not, speculation may fail and need rollback. Their implementation, Belfast, shows 3.5x faster delivery latency and 1.6x improvement in end-to-end latency over existing shared logs.

This is conceptually similar to moving Scalog’s ordering step upfront and letting applications run optimistically. As I noted back in my Scalog post, removing coordination from the critical path is the holy grail. SpecLog pushes this further by betting on speculative execution + predictable quotas. Again, I haven't read the papers to analyze disadvantages. 


Comments

Post a Comment

Popular posts from this blog

Hints for Distributed Systems Design

-
This is with apologies to Butler Lampson, who published the " Hints for computer system design " paper 40 years ago in SOSP'83. I don't claim to match that work of course. I just thought I could draft this post to organize my thinking about designing distributed systems and get feedback from others. I start with the same  disclaimer Lampson gave. These hints are not novel, not foolproof recipes, not laws of design, not precisely formulated, and not always appropriate. They are just hints.  They are context dependent, and some of them may be controversial. That being said, I have seen these hints successfully applied in distributed systems design throughout my 25 years in the field, starting from the theory of distributed systems (98-01), immersing into the practice of wireless sensor networks (01-11), and working on cloud computing systems both in the academia and industry ever since. These heuristic principles have been applied knowingly or unknowingly and has proven...
Read more >>

My Time at MIT

-
Image
Twenty years ago, in 2004-2005, I spent a year at MIT’s Computer Science department as a postdoc working with Professor Nancy Lynch. It was an extraordinary experience. Life at MIT felt like paradise, and leaving felt like being cast out. MIT Culture MIT’s Stata Center was the best CS building in the world at the time. Designed by Frank Gehry, it was a striking abstract architecture masterpiece ( although like all abstractions it was a bit leaky ). Furniture from Herman Miller complemented this design. I remember seeing price tags of $400 on simple yellow chairs. The building buzzed with activity.  Every two weeks, postdocs were invited to the faculty lunch on Thursdays, and alternating weeks we had group lunches. Free food seemed to materialize somewhere in the building almost daily, and the food trucks outside were also good. MIT thrived on constant research discussions, collaborations, and talks. Research talks were advertised on posters at the urinals, as a practical touch of M...
Read more >>

Making database systems usable

-
Image
C. J. Date's Sigmod 1983 keynote, "Database Usability", was prescient. Usability is the most important thing to the customers. They care less about impressive benchmarks or clever algorithms, and more about whether they can operate and use a database efficiently to query, update, analyze, and persist their data with minimal headache. (BTW, does anyone have a link to the contents of this Sigmod'83 talk? There is no transcript around, except for this short abstract .) The paper we cover today is from Sigmod 2007. It takes on the database usability problem raised in that 1983 keynote head-on, and calls out that the king is still naked.  Let's give some context for the year 2007. Yes, XML format was still popular then. The use-case in the paper is XQuery. The paper does not contain any  reference to json. MongoDB would be released in 2009 with the document model; and that seems to be great timing for some of the usability pains mentioned in the paper! Web 2.0 was in ...
Read more >>

Looming Liability Machines (LLMs)

-
As part of our zoom reading group ( wow, 4.5 years old now ), we discussed a paper that uses LLMs for automatic root cause analysis (RCA) for cloud incidents. This was a pretty straightforward application of LLMs. The proposed system employs an LLM to match incoming incidents to incident handlers based on their alert types, predicts the incident's root cause category, and provides an explanatory narrative. The only customization is through prompt-engineering. Since this is a custom domain, I think a more principled and custom-designed  machine learning system would be more appropriate rather than adopting LLMs. Anyways, the use of LLMs for RCAs spooked me vicerally. I couldn't find the exact words during the paper discussion, but I can articulate this better now. Let me explain. RCA is serious business Root cause analysis (RCA) is the process of identifying the underlying causes of a problem/incident, rather than just addressing its symptoms. One RCA heuristic is asking 5 Why...
Read more >>

Advice to the young

-
Image
I notice I haven't written any advice posts recently. Here is a collection of my advice posts pre 2020. I've been feeling all this elderly wisdom pent up in me, ready to pour at any moment. So here it goes. Get ready to quench your thirst from my fount of wisdom. No man, think for yourself, only get what works for you. It is called foundations, not theory Foundations of computer science (or rather any field of study) are the most important topics you can learn. These lay down the frame of thinking/perspective for that area of study. Yet, I am saddened to hear these called as "theory", and labeled as "unpractical". This couldn't be farther from the truth. Take a look at how I recommend studying distributed systems . Don't you dare call this "theory" and "unpractical". This lays the bedrock that you build your practice on. Don't skimp on the foundations. Don't build your home on quicksand. Keep your hands dirty, your mind cl...
Read more >>

Learning about distributed systems: where to start?

-
This is definitely not a "learn distributed systems in 21 days" post. I recommend a principled, from the foundations-up, studying of distributed systems, which will take a good three months in the first pass, and many more months to build competence after that. If you are practical and coding oriented you may not like my advice much. You may object saying, "Shouldn't I learn distributed systems with coding and hands on? Why can I not get started by deploying a Hadoop cluster, or studying the Raft code." I think that is the wrong way to go about learning distributed systems, because seeing similar code and programming language constructs will make you think this is familiar territory, and will give you a false sense of security. But, nothing can be further from the truth. Distributed systems need radically different software than centralized systems do.  --A. Tannenbaum This quotation is literally the first sentence in my distributed systems syllabus. Inst...
Read more >>

Scalable OLTP in the Cloud: What’s the BIG DEAL?

-
Image
This paper is from Pat Helland, the apostate philosopher of database systems, overall a superb person, and a good friend of mine. The paper appeared this week at CIDR'24. (Check out the program for other interesting papers). The motivating question behind this work is: " What are the asymptotic limits to scale for cloud OLTP (OnLine Transaction Processing) systems? " Pat says that the CIDR 2023 paper "Is Scalable OLTP in the Cloud a Solved Problem?" prompted this question.  The answer to the question? Pat says that the answer lies in the joint responsibility of database and the application. If you know of Pat's work, which I have summarized several in this blog , you would know that Pat has been advocating along these lines before. But this paper provides a very crisp, specific, concrete answer. Read on for my summary of the paper. Disclaimer: This is a wisdom and technical information/detail packed 13-page paper, so I will try my best to summarize the sa...
Read more >>

Foundational distributed systems papers

-
I talked about the importance of reading foundational papers last week. To followup, here is my compilation of foundational papers in the distributed systems area. (I focused on the core distributed systems area, and did not cover networking, security, distributed ledgers, verification work etc. I even left out distributed transactions, I hope to cover them at a later date.)  I classified the papers by subject, and listed them in chronological order. I also listed expository papers and blog posts at the end of each section. Time and State in Distributed Systems Time, Clocks, and the Ordering of Events in a Distributed System. Leslie Lamport, Commn. of the ACM,  1978. Distributed Snapshots: Determining Global States of a Distributed System. K. Mani Chandy Leslie Lamport, ACM Transactions on Computer Systems, 1985. Virtual Time and Global States of Distributed Systems.  Mattern, F. 1988. Practical uses of synchronized clocks in distributed systems. B. Liskov, 1991. Exp...
Read more >>

Distributed Transactions at Scale in Amazon DynamoDB

-
Image
This paper appeared in July at USENIX ATC 2023. If you haven't read about the architecture and operation of DynamoDB, please first read my summary of the DynamoDB ATC 2022 paper . The big omission in that paper was discussion about transactions. This paper amends that. It is great to see DynamoDB, and AWS in general, is publishing/sharing more widely than before. Overview A killer feature of DynamoDB is predictability at any scale. Do read Marc Brooker's post to fully appreciate this feature. Aligned with this predictability tenet, when adding transactions to DynamoDB, the first and primary constraint was to preserve the predictable high performance of single-key reads/writes at any scale. The second big constraint was to implement transactions using update in-place operation without multi-version concurrency control. The reason for this was they didn't want to mock with the storage layer which did not support multi-versioning. Satisfying both of the above constraints may s...
Read more >>

Linearizability: A Correctness Condition for Concurrent Objects

-
Image
This paper is from Herlihy and Wing appeared in ACM Transactions on Programming Languages and Systems 1990. This is the canonical reference for the linearizability definition. I had not read this paper in detail before, so I thought it would be good to go to the source to see if there are additional delightful surprises in the original text. Hence, this post. I will dive into a technical analysis of the paper first, and then discuss some of my takes toward the end. I had written an accessible explanation of linearizability earlier; you may want to read that first. I will assume an understanding of linearizability to keep this review at reasonable length. Introduction I love how the old papers just barge in with the model, without bothered by pleasantries such as motivation of the problem. These are the first two sentences of the introduction. "A concurrent system consists of a collection of sequential processes that communicate through shared typed objects . This model encompass...
Read more >>