A Programming Model for Disaggregated Memory over CXL

A new datacenter technology called CXL lets many machines share one giant pool of memory that any of them can read and write with ordinary loads and stores — but it comes with no rulebook, so no one can say what a program built on it will actually do, especially when one machine crashes while others keep running; this work from TU Munich and Tel Aviv writes that rulebook, CXL0, the first formal programming model for CXL, boiling its tangle of low-level operations down to one load, three stores, and two flushes with precise meanings, and uses it to prove a general recipe that makes any correct concurrent algorithm survive partial crashes without a redesign.

The argument in one glance

Problem

CXL gives many machines one shared memory pool, but no rulebook

CXL lets machines across a datacenter share cache-coherent memory pools accessed with simple loads and stores. But it breaks two single-machine assumptions — heterogeneous compute units share the memory so no single memory model governs concurrency, and nodes can crash independently — and it comes with no programming model, so no one can reason about what a system on top will do.
What people did

Reuse existing shared-memory and persistent-memory techniques

Apply the memory models, data structures, and crash-consistency methods developed for single-machine shared memory and non-volatile main memory to programs running over CXL.
Why it fell short

Those techniques do not transfer to disaggregation

CXL inflates the system model: multiple machines share the same volatile and persistent memory, and any of them can crash on its own. Existing single-machine solutions assume one memory model and one failure domain, so they do not automatically carry over, and legacy multi-threaded code is not guaranteed to stay correct once its memory is disaggregated.
This paper's idea

Give CXL a formal programming model, and a proven transformation (CXL0)

CXL0 is the first programming model for concurrent programs over CXL. It distills CXL's low-level transactions into a small set of primitives — one load, three stores, and two flushes — with precise operational semantics derived from the CXL specification, captures a wide range of current and future CXL setups, and is validated on real hardware. Using it, the authors present and formally prove a general transformation that makes any linearizable algorithm durable under partial crashes, with no redesign.

Why this problem is worth solving

CXL is poised to reshape how datacenters are built, precisely by erasing the boundary between machines and memory.

In a traditional server, compute and memory are bought and bolted together, so each machine must be provisioned for its peak memory needs, leaving memory underused most of the time. Disaggregated memory separates the two: compute nodes and memory nodes are distinct, memory is pooled across the datacenter, and each can scale independently, giving more flexibility, better utilization, and even a kind of fault tolerance since memory can outlive the compute unit using it. CXL, for Compute Express Link, is the emerging open industry standard that makes this practical. Backed by the major cloud providers and widely expected to become the future datacenter interconnect, CXL lets a machine access external and remote memory coherently, and gives a uniform way to reach every kind of memory in the system — local DRAM, remote DRAM, even solid-state storage — through simple loads and stores at cache-line granularity. In effect, the entire memory of all participating machines can be treated as one large, unified, shared main memory. That is a genuinely new capability, and it is why so much is expected of CXL.

The same unification that makes CXL powerful quietly invalidates the assumptions programmers rely on.

When a single, centralized machine becomes a distributed but coherent pool, two things that were always true stop being true. First, heterogeneous compute units — CPUs, GPUs, accelerators of every kind — now access the same memory, and each may have its own internal memory model, so the outcome of concurrent operations is no longer governed by any single, well-understood set of rules. Second, the system is no longer a single failure domain: instead of every component crashing together, individual nodes can crash independently while the rest keep running, which means a computation can be caught half-finished with some of its updates lost and others not. Decades of failure-aware research exist, but almost all of it targets full-system crashes on one machine, so it does not automatically transfer to a setting where several machines share the same volatile and persistent memory. On top of all this, CXL simply has no general programming model. A programmer cannot say what consistency guarantees a memory access provides, whether the local memory model survives the communication protocol, whether an existing multi-threaded program remains correct once disaggregated, or how to recover a consistent state after a crash. Without answers, it is impossible to reason about the correctness of any system built on CXL.

What people did before, and where it broke

Program CXL memory with informal, ad-hoc reasoning. Use the loads and stores CXL exposes and hope the intuition from a single machine carries over. Where it broke. There is no defined memory model, so nobody can actually say what a concurrent execution guarantees, and correctness becomes guesswork.
Reuse single-machine persistent-memory techniques. Apply the correctness criteria, data structures, and flush-based crash-consistency methods built for non-volatile main memory. Where it broke. Those assume one memory model and one failure domain; CXL lets multiple machines share the same memory and crash independently, so the solutions do not automatically transfer.
Port legacy multi-threaded shared-memory code as-is. Run existing concurrent programs directly on the disaggregated pool. Where it broke. Programs correct under single-machine shared memory are not guaranteed to remain correct once the memory is disaggregated and partial crashes are possible.
The gap. No formal programming model let anyone reason about consistency and crash behavior over CXL, and no general method made existing concurrent code crash-resilient in this setting. Providing both is what CXL0 does.

How CXL0 works

From single-machine shared memory to a formal model for disaggregated CXL

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Write down a precise programming model so CXL can be reasoned about. The heart of the work is turning CXL from an informal collection of loads and stores into a formal programming model, CXL0, with operational semantics derived from a careful reading of the CXL specification — a mathematical definition of exactly how each memory operation behaves, so the correctness of a concurrent program can actually be analyzed. Writing the rules of a concurrent memory system down precisely enough that its behavior can be reasoned about rigorously, rather than left to intuition, is the same discipline the GPU memory-model work covered elsewhere on this site follows, expressing what the hardware guarantees as an exact, checkable specification instead of an informal understanding that breaks down on the hard cases.

Model the disaggregated coherent pool as it really is. CXL0 treats the whole system as distributed, cache-coherent, shared memory in which each node emits sequences of CXL transactions and any node can crash on its own, abstracting away each machine’s internal memory model while capturing what happens across the pool. Modeling a machine built from cache-coherent shared memory spanning separate, heterogeneous components — the very substrate CXL and its coherent interconnects create — is the same setting the fused-kernel operating-system work covered elsewhere on this site is built for, treating a collection of distinct machines joined by coherent shared memory as one system whose correctness must be reasoned about as a whole.

Give explicit control over when data reaches durable memory. CXL0’s three stores and two flushes distinguish exactly where a value has landed — local cache, remote cache, or physical memory — and the durability transformation uses them to flush only the writes that must survive a crash, tagged by whether they are shared and whether they need to persist, rather than persisting everything. Exposing explicit primitives that control when modified data is pushed out to durable memory, and paying that cost only where it is actually needed, is the same design the user-controlled-writeback work covered elsewhere on this site is built around, giving software precise say over which cache lines are written back and skipping the writebacks that would accomplish nothing.

Following a data structure through the CXL0 transformation

Making a linearizable data structure durable under partial crashes

A trace of the CXL0 durability transformation, following the paper's adaptation of FliT to the partial-crash model.

Step 1 of 5

Start from a correct concurrent data structure

Begin with an existing linearizable concurrent data structure — correct under concurrency, but written assuming one machine and that any crash takes everything down together.

Linearizable means its concurrent history fits a single consistent timeline.

Why it works

You cannot reason about a system without a model of it. Because CXL exposes loads and stores but never defines their guarantees → programmers cannot tell what a concurrent execution will do → so a precise programming model is a prerequisite for building anything correct on CXL.
A small set of primitives tames a complex specification. Because CXL’s specification has many low-level transaction types → collapsing them into one load, three stores, and two flushes with defined behavior → so the essential behaviors can be reasoned about without drowning in protocol detail.
The store and flush variants capture where data actually is. Because a value may sit in a local cache, a remote cache, or physical memory → distinguishing local, remote, and memory stores and flushes → so a programmer can control, and reason about, when data becomes durable or visible.
Partial crashes need a different notion of correctness. Because nodes can crash independently rather than all at once → durability must hold per subsystem, not for the whole system at once → so the model and transformation target durable linearizability under partial crashes specifically.
A general transformation reuses existing code. Because the transformation requires only that an algorithm be linearizable → any such algorithm inherits durability without being redesigned → so legacy concurrent code can be made crash-resilient on CXL by construction.

What it costs (trade-offs and scope)

The model abstracts away the internal memory model. CXL0 deliberately models each node as emitting CXL transactions and abstracts away each machine’s own internal memory model. This keeps the model tractable and general, but it means questions purely about a node’s internal ordering are outside its scope.
The transformation targets safety, not liveness. Following the approach it adapts, the transformation proves durable linearizability, a safety property, and assumes the original data structure is non-blocking to handle liveness, leaving liveness concerns to the programmer.
It applies to linearizable, non-blocking algorithms. The general transformation requires the original algorithm to already be linearizable (and, for liveness, non-blocking). Algorithms outside that class are not covered by the automatic transformation.
CXL itself has gaps the model exposes. The authors identify limitations of the current CXL specification for concurrent programming, notably a lack of ordering primitives, and they argue the specification’s optional global persistent flush does not reliably provide strong persistence, so some desirable guarantees depend on hardware features beyond the base standard.
The hardware evaluation is early. The paper validates the model with latency measurements of the CXL0 primitives on real hardware and a roadmap of configurations, which confirm the predicted trends, but it is an initial measurement study rather than a large-scale performance evaluation of complete systems.
It is a foundation, not a finished stack. CXL0 is intended as a stepping stone for designing and programming systems on CXL; realizing its benefits requires building real systems and tools on top of the model.

The evaluation

Three ways to program memory across machines

Property	Single-machine shared memory	Message-passing distributed
Access style
A memory model to reason with	Yes, one machine's
Heterogeneous machines share memory
Handles independent (partial) crashes	No, single failure domain	By hand, per protocol
Reuse legacy linearizable code with durability	Not crash-durable	No, must rewrite

Three ways to program memory across machines, framed by the paper. Single-machine shared memory offers simple loads and stores and a memory model to reason with, but only for one machine and one failure domain. Traditional distributed systems use explicit message passing and hand-craft their fault tolerance per protocol. CXL0 targets CXL's new middle ground: a cache-coherent, disaggregated memory pool that heterogeneous machines share with simple loads and stores, but where nodes can crash independently. CXL0 supplies the missing formal programming model — one load, three stores, and two flushes with precise operational semantics — shown to capture a wide range of current and future CXL setups and validated with latency measurements of each primitive on real hardware. On top of it, the paper gives a general, formally proven transformation that makes any linearizable algorithm durable under partial crashes without redesign. This is a foundational modeling result validated on hardware, rather than a large-scale performance study of complete systems.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This is a foundations paper, and its value should be judged as such. CXL is arriving fast and promises to turn a datacenter’s memory into one shared, coherent pool reachable with ordinary loads and stores — but it ships without a programming model, which means no one can rigorously say what a concurrent program over CXL guarantees, or how it behaves when one node crashes while others keep running. CXL0 fills that gap. It reads the CXL specification carefully and distills its many low-level transactions into a small, comprehensible set of primitives — one load, three stores, and two flushes — and gives them precise operational semantics, including the non-deterministic cache evictions the hardware may perform. That formal model is the real contribution: it lets programmers reason about consistency and recovery on CXL for the first time, and the authors show it captures a wide range of current and future CXL configurations and back it with latency measurements of each primitive on real hardware. To demonstrate the model’s usefulness, they present and formally prove a general transformation that takes any linearizable concurrent algorithm and makes it durable under the partial-crash model, so legacy code can inherit crash resilience without a redesign. Read the scope precisely. The model abstracts away each node’s internal memory model; the transformation proves a safety property and leaves liveness to the programmer, applying to linearizable, non-blocking algorithms; the work also surfaces real gaps in CXL itself, such as its lack of ordering primitives and the weakness of its optional global persistent flush; and the hardware results are an initial measurement study, not a full systems evaluation. The durable idea is that a new hardware substrate needs a precise programming model before anything correct can be built on it, and that with such a model in hand, a single proven transformation can carry a whole class of existing algorithms safely into the new world.

Background

Why new hardware needs a formal model before software can trust it

It helps to see CXL0 within a recurring pattern: whenever hardware changes what is possible — a new interconnect, a new memory technology, a new coherence domain — software cannot be built on it safely until someone writes down, precisely, what it guarantees. Intuition carried over from the old world quietly fails, usually on exactly the concurrent and crash cases that matter most. A precise, checkable account of what the hardware promises about concurrent memory, rather than folklore, is what lets real programs be verified against it. CXL0 does this for disaggregated memory, and then goes a step further, showing that once the model exists it becomes a tool: a general, proven transformation can upgrade an entire class of algorithms to a stronger correctness guarantee — here, durability under partial crashes — the same way the trusted-network-card work covered elsewhere on this site offers a general recipe that lifts any crash-tolerant protocol to tolerate malicious faults. The common thread is that rigor at the foundation pays compounding dividends: a precise model turns a murky new substrate into something programmers can reason about, and a proven transformation turns that understanding into resilience for code that was never written with the new hazards in mind. As disaggregation and heterogeneity spread, the systems that succeed will be the ones built on models this explicit.

If you remember only three things

1. CXL is an emerging open standard that wires processing and memory devices across a datacenter into cache-coherent, shared memory pools, letting many machines access a huge disaggregated memory with simple loads and stores. This breaks two single-machine assumptions: heterogeneous compute units (CPUs, GPUs, accelerators) now share the memory, so no single memory model governs concurrent outcomes, and the system is no longer one failure domain, so nodes can crash independently and catch a computation half-finished. Critically, CXL ships with no programming model, so programmers cannot say what consistency a memory access provides, whether legacy multi-threaded code stays correct once disaggregated, or how to recover after a crash — making it impossible to reason about correctness.
2. CXL0 is the first programming model for concurrent programs over CXL. It distills CXL's many low-level transactions into a small set of primitives — one load, three stores (local, remote, and memory, distinguished by where the value must land), and two flushes (local and remote) — and gives them precise operational semantics derived from the CXL specification, including the non-deterministic cache evictions the hardware may perform. It models the system as distributed, cache-coherent, shared memory with independent subsystem crashes, abstracting away each node's internal memory model, and is shown to capture a wide range of current and future CXL setups, with latency measurements of each primitive on real hardware confirming the predicted trends.
3. To show the model's usefulness, the authors present and formally prove a general transformation that makes any linearizable concurrent algorithm durably linearizable under the partial-crash model — so completed operations are guaranteed to persist before returning — enhancing legacy code with crash resilience without a redesign. It adapts the FliT transformation, classifying accesses as shared or private and tagging only those that must persist so it does not blindly flush everything. Scope: the model abstracts away internal memory models, the transformation proves safety (assuming non-blocking algorithms for liveness), CXL itself is shown to lack ordering primitives and a reliable global persistent flush, and the hardware results are an initial measurement study. The durable lesson is that a new hardware substrate needs a precise programming model before correct software can be built on it, and that a single proven transformation can then carry a whole class of algorithms safely into the new setting.

Check yourself

Check your understanding

1. What two single-machine assumptions does CXL break, and why does that matter?
2. What is CXL0, and what does it provide?
3. Why does CXL0 distinguish three kinds of store and two kinds of flush?
4. How does the paper demonstrate CXL0 is useful, and what is notable about the result?

Sources

The paper is “A Programming Model for Disaggregated Memory over CXL” by Gal Assa, Moritz Lumme, Lucas Burgi, Michal Friedman, and Ori Lahav, published at ASPLOS 2026, DOI 10.1145/3779212.3790121. The authors are at the Technion, ETH Zurich, the Technical University of Munich, and Tel Aviv University.

This explainer is based on the full text of the paper, obtained from the authors’ open-access arXiv version (arXiv:2407.16300), which corresponds to the CC-BY version of record. The problem framing (disaggregated memory and its benefits; CXL as an emerging open standard for cache-coherent shared memory pools accessed by simple loads and stores; and the two broken assumptions — the loss of a single memory model when heterogeneous compute units share memory, and the loss of a single failure domain when nodes can crash independently — together with the absence of any programming model), the CXL0 model (the abstraction of CXL transactions into one load, three store primitives distinguished by where a value must reach — local cache, remote cache, or physical memory — and two flush primitives, the treatment of non-deterministic cache evictions and the optional global persistent flush, and the operational semantics derived from the CXL specification), the demonstration that the model captures current and future CXL setups together with the initial latency measurements of the primitives on real hardware, and the durability transformation (the adaptation of FliT to the partial-crash model, its classification of shared and private accesses and use of a persistence flag, its guarantee of durable linearizability, and the formal proof of its correctness) are all drawn directly from the paper. Background explanations of disaggregated memory, cache coherence, persistent-memory programming, flushes and memory barriers, and linearizability are standard and provided to make the paper’s contribution understandable.