CXLMC: Model Checking CXL Shared Memory Programs

CXL lets many machines share one pool of remote memory, and to hide the latency they cache it — but if a machine crashes before writing its dirty cache lines back to the shared device, its latest changes vanish, and the crash-consistent data structures meant to survive this are notoriously easy to get wrong; this paper (UC Irvine — Yutong Guo, Conan Truong, Brian Demsky) presents CXLMC, the first model checker that systematically explores partial-failure executions of x86 CXL shared-memory programs to catch these bugs, finding 24 bugs in 8 applications, 7 of them new.

The argument in one glance

Problem

Cached shared memory can silently lose a crashed machine's latest writes

Compute Express Link (CXL) shared memory lets many machines in a cluster read and write one shared pool of remote DRAM in a cache-coherent way, so software can communicate and share large datasets efficiently. To hide the latency of reaching that remote memory, machines cache it locally. But caching creates a durability hazard. When a compute node writes to a cache line, the newest value may live only in that node's cache, not yet written back to the shared memory device. If the node then crashes before flushing, those latest stores are simply lost, and any other machine that relied on them now sees stale or inconsistent data. CXL has a global persistent flush mechanism, but it is aimed at power outages, not the many other ways a node can fail (a bad power supply, motherboard, or CXL transceiver). To survive failures, programmers build crash-consistent data structures, carefully inserting flush and fence instructions so the structure stays consistent even if a machine dies mid-operation. The trouble is that writing such code correctly is extremely hard: a single misplaced or missing flush can leave a lurking bug, and these bugs are very hard to find by testing, because they only manifest under specific, rare crash timings. As clusters grow to thousands of machines, a single crash corrupting a shared index could take down the whole cluster.
What people did

Reuse persistent-memory crash-consistency checkers

This looks like a solved problem, because persistent memory (PM) faces the same basic hazard — data cached but not yet made durable when a crash hits — and researchers have built many tools to find crash-consistency bugs in PM programs. One especially effective family uses constraint-based model checking, systematically exploring the possible crash outcomes rather than relying on lucky test timing.
Why it fell short

CXL's partial, concurrent failures do not fit the persistent-memory model

The PM tools do not directly transfer, because CXL shared memory fails differently. Persistent memory assumes a complete-failure model: the whole system stops at once, and any crash happens before or after an operation, never during. CXL shared memory has a partial-failure model: one compute node can crash while the others keep running, so a failure can occur concurrently with a data structure operation, and even while another machine is running recovery code for a previous failure — a situation impossible in PM. This makes the space of things that can go wrong far larger and more tangled. It also changes the consistency details: in CXL, a remote read of a cache line tells you the line was written back to the shared device, information a checker can exploit. A PM checker that assumes total failure and no concurrency with recovery will simply miss the failure scenarios that are unique and central to CXL. And naively adapting one by enumerating every post-crash state explodes combinatorially, made worse by partial failure, since at every step any subset of the running machines might fail. What was missing was a model checker built for the CXL failure and consistency model that stays tractable.
This paper's idea

Adapt constraint-based model checking to CXL partial failures

CXLMC is the first model checker for crash-consistency bugs in CXL shared-memory programs, targeting the x86-CXL platform. It instruments a C or C++ program with an LLVM pass so that every memory access, fence, and flush calls into CXLMC, then runs each simulated machine as a separate process (with multiple threads per process for multiple cores), emulating store buffers, local caches, the x86-TSO memory model with flush instructions, and — crucially — the partial failure of any subset of compute nodes at any point, including during recovery. To keep this tractable, CXLMC adapts a constraint-based technique from persistent-memory model checking: rather than eagerly enumerating every post-crash state (which explodes), it uses cache line constraint refinement, lazily tracking, for each cache line, the interval of time in which its last write-back to the device could have happened. It only explores executions that differ in a way observable through post-failure loads, so for the common commit-store pattern (where one store makes a group of prior stores visible) just two executions are needed — one where a failure happens before the commit is written back, and one where it does not. A post-failure load then resolves its value lazily within the current constraint interval, refining it as it goes. CXLMC is sound: every execution it reports is feasible under the model, so every bug it finds is a real bug. Applied to adapted RECIPE and CXL-SHM benchmarks, CXLMC found 24 bugs in 8 applications, 7 of them previously unknown.

Why this problem is worth solving

CXL shared memory is poised to hold the coordination structures a whole cluster depends on, so a single crash-consistency bug there can be catastrophic.

CXL shared memory is an emerging standard, with the specification designed to let thousands of machines share memory coherently, and researchers are already proposing to build database indices, message buffers for cross-node communication, and shared object stores on top of it. These are exactly the kinds of core, shared data structures that many machines depend on simultaneously. That concentration is what makes correctness under failure so critical: if a single machine crash can corrupt a shared index because its latest writes were cached but never flushed, then one node’s failure does not just stop that node — it can leave the shared structure inconsistent and bring down the entire cluster that relies on it. As clusters scale up, machine failures become not a rare event but an expected one, so the software must tolerate them. Getting crash consistency right in this setting is therefore foundational to whether CXL shared memory can be trusted for the coordination roles it is aimed at.

The reason this is hard is that the bugs hide in rare crash timings, and CXL’s failure model multiplies those timings beyond what testing or prior tools cover.

A crash-consistency bug only appears if a machine dies at just the wrong instant — after some stores but before a crucial flush — and ordinary testing almost never hits that exact interleaving, so the bug ships and lurks. The historical lesson from persistent memory is stark: correct crash-consistent code is very hard to write by hand, and once tools existed to explore crash timings systematically, they found on the order of hundreds of bugs in a small set of benchmarks. CXL makes the search harder in two ways. Its partial-failure model means that at any moment, any subset of the running machines could fail independently, so the set of crash scenarios is vastly larger than a single all-at-once crash. And failures can overlap with recovery — a machine can die while another is still recovering from an earlier death — a nested, concurrent situation persistent-memory tools never had to consider. A checker that naively lists every possible post-crash state drowns in this combinatorial explosion. So the crux is not just to explore crash outcomes, but to do it in a way that stays tractable under partial, concurrent failures while still being sound. That is the problem CXLMC solves.

What people did before, and where it broke

Write crash-consistent structures by hand with flush and fence instructions. Carefully place the instructions so the structure survives a crash. Where it broke. It is extremely error-prone; a single missing or misplaced flush leaves a bug that testing rarely triggers, so bugs ship undetected.
Test the code and hope to hit a bad crash timing. Run the program and crash it at various points. Where it broke. Crash-consistency bugs only manifest at rare, specific interleavings, so ordinary testing almost never exposes them.
Reuse a persistent-memory crash-consistency checker. Apply an existing PM model checker to the CXL code. Where it broke. PM tools assume a complete-failure model with no concurrency between failure and recovery, so they miss CXL’s partial, concurrent failures — the scenarios that matter most here.
Eagerly enumerate all post-crash states. List every possible combination of lost and persisted cache lines after a crash. Where it broke. The number of states grows exponentially, and partial failure makes it worse (any subset of machines can fail at any step), so the search is intractable.
The gap. No model checker was built for the CXL failure and consistency model, able to explore partial, concurrent failures soundly without exploding.

How CXLMC works

Systematically exploring the crashes a CXL program can suffer

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

The idea

Verify a program whose behavior is nondeterministic by exploring its outcomes systematically. CXLMC treats a crash as a source of nondeterminism — the exact set of lost cache lines is not fixed — and its job is to soundly cover the space of what could happen rather than trusting a single run. Systematically reasoning over all the behaviors a nondeterministic program can exhibit, to prove properties or expose failures that a single execution would miss, is the same undertaking the work on verification of nondeterministic quantum programs covered elsewhere on this site pursues, confronting the full space of possible outcomes head-on. CXLMC does this for crash nondeterminism in CXL shared memory, guaranteeing that every execution it reports is one the real system could produce.

Make crash consistency the property under test. At its heart CXLMC is checking one specific, hard-won kind of correctness: that a data structure stays consistent even when a machine dies before its cached writes reach durable shared memory. Building a tool whose whole purpose is to check that state survives a failure correctly, rather than only that a program is correct when nothing fails, is the same principle the work on checking crash consistency of non-volatile memory covered elsewhere on this site is built on, treating what remains after a crash as a first-class correctness question. CXLMC brings this discipline to CXL, where the failures are partial and can even overlap with recovery.

Prune the enormous search space to only the cases that can differ. The key to staying tractable is not exploring every conceivable post-crash state but only those that lead to observably different behavior — lazily resolving a load’s value within a constraint interval and collapsing equivalent outcomes. Cutting a combinatorial exploration down to the small set of candidates that actually matter, and refusing to spend effort on the rest, is the same idea the work on a draft-then-verify exploration mechanism (Pruner) covered elsewhere on this site develops, aggressively shrinking a search space to what is worth examining. CXLMC’s cache line constraint refinement is exactly such a pruning: the common commit-store pattern collapses to just two executions instead of exponentially many.

Following a crash through CXLMC

Catching a crash-consistency bug in a shared data structure

A trace, drawn from the paper, of how CXLMC explores a partial-failure execution.

Step 1 of 5

Two machines share a crash-consistent structure

The program is instrumented, and two simulated machines share one CXL memory pool holding a crash-consistent data structure that uses flush and fence instructions to stay consistent across failures.

CXLMC runs each machine as a process and emulates its caches under x86-TSO.

Why it works

Emulating the real machine model explores real executions. A checker built on wrong assumptions finds phantom bugs → but CXLMC instruments every memory operation and emulates store buffers, caches, and x86-TSO with flushes → so the executions it explores are ones the actual hardware could produce.
Modeling partial, concurrent failure finds CXL-specific bugs. Persistent-memory checkers assume total failure and no failure during recovery → but CXLMC lets any subset of nodes fail at any point, even amid recovery → so it exposes the failure scenarios unique to CXL sharing.
Constraint refinement tames the state explosion. Enumerating every post-crash state grows exponentially and worsens under partial failure → but tracking a time interval for each line’s last write-back and exploring only observably-different executions → keeps the search tractable.
Lazy resolution collapses the commit-store pattern. Materializing every possible last-flush position for every line is hopeless → but resolving a post-failure load’s value lazily within its interval → reduces the common commit-store pattern to just two executions.
Soundness makes every report actionable. A tool that emits false alarms wastes developer time → but CXLMC only explores executions feasible under the memory and failure model → so every bug it reports is a real bug worth fixing.

What it costs (trade-offs and scope)

It checks crash nondeterminism, not concurrency nondeterminism. To scale to longer executions, CXLMC explores the nondeterminism from crashes but not from thread interleavings; it can generate multiple random schedules to compensate, but a bug that needs a specific interleaving may be missed unless that schedule is sampled.
It is tied to the x86-TSO model and specific flush semantics. CXLMC is built on an x86 persistent-memory formalization (a Px86sim-style model), and since the CXL memory model is not yet standardized beyond cache coherence, its exact semantics were chosen in consultation with hardware engineers; cross-machine mixed memory models and abstract CXL operations without an x86 mapping are out of scope.
It is not complete in the strong sense. CXLMC guarantees at least one execution per reads-from equivalence class for a fixed schedule, and some bugs it finds may not be realizable on every processor (for example, because of eviction policies the architectural model does not guarantee) — those are still real bugs to fix, but coverage is not exhaustive over all processors.
Programs must fit its assumptions and be instrumentable. It targets C and C++ instrumented via LLVM, assumes machines share a single non-persistent memory device, and does not model a compute node losing access to its own local memory region; some benchmarks required rewrites, and a few could not be fully fixed to measure.
It checks crashes and assertions, so deeper correctness needs assertions. By default CXLMC flags unintended crashes or existing assertion failures; verifying richer properties (like a specific consistency invariant) requires the programmer to supply assertions, though the design is extensible to properties such as robustness.

The evaluation

Finding crash-consistency bugs in CXL shared-memory programs

Property	Manual review / testing	Persistent-memory checkers	CXLMC
Explores crash timings
Partial, concurrent failure
State-space blowup
False alarms
Bugs found

A comparison of ways to find crash-consistency bugs in CXL shared-memory programs. CXLMC is the first model checker for the CXL setting, modeling partial and concurrent failures that persistent-memory tools do not, keeping the search tractable with cache line constraint refinement, and reporting only real bugs (soundness). It found 24 bugs in 8 applications, 7 of them previously unknown, running each benchmark in at most about a minute.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This explainer is based on the paper’s full text (the authors’ copy hosted at UC Irvine, of the ASPLOS 2026 paper). The tool described is the paper’s: CXLMC is the first model checker for crash-consistency bugs in x86-CXL shared-memory programs. It instruments programs with an LLVM pass, runs each simulated machine as a separate process (with threads for cores), and emulates store buffers, local caches, and the x86-TSO memory model with flush instructions, based on a Px86sim-style persistent-memory formalization chosen in discussion with hardware engineers. It models the CXL partial-failure setting, in which any subset of compute nodes can fail at any point, including during another machine’s recovery. To stay tractable, it adapts the constraint-based cache line constraint refinement technique (from the Jaaru persistent-memory checker) with a novel formulation for partial failures: it tracks, per cache line, the interval in which its last write-back could have occurred, and explores only executions that differ observably through post-failure loads, so the commit-store pattern reduces to two executions. CXLMC is sound (every reported execution is feasible under the model, so every bug is real) though not exhaustively complete. The paper reports finding 24 bugs in 8 applications (including 7 new bugs) across adapted RECIPE and CXL-SHM benchmarks, with the longest benchmark running in just under a minute; a GPF (global persistent flush) mode confirms that the RECIPE bugs stem specifically from lost cached values and partial failures. Exact algorithms, the formal model, benchmark details, and full results should be read from the paper.

Background

Why durable, shared state keeps needing verification tools

It helps to see CXLMC within a long arc: every time systems gain a new way to keep data across failures, they also gain a new, subtle class of bugs, and eventually a tool to hunt those bugs. Caches, write buffers, and reordering make hardware fast, but they also mean that at the instant of a crash, what is durably saved and what is lost depends on invisible timing that programmers reason about poorly. Persistent memory taught this lesson painfully — hand-written crash-consistent code was riddled with missing-flush bugs until systematic checkers arrived and found them by the hundreds. CXL shared memory reopens the same wound in a harder form, because now the failures are partial: one machine can die while others keep working and even while recovery is underway, so the space of ways things can go wrong is larger and more entangled than a single all-at-once crash. Understanding this new substrate well enough to build correct software on it is an ongoing effort, and the broad push to characterize how CXL memory actually behaves is the same terrain the work on systematic CXL memory characterization and performance analysis at scale covered elsewhere on this site occupies, mapping the ground that software must stand on. CXLMC contributes the correctness side of that understanding: a way to systematically and soundly explore the crashes a CXL program can suffer, so that the coordination structures a whole cluster depends on can be checked before a real failure exposes them.

If you remember only three things

1. CXL shared memory lets many machines share one pool of remote DRAM coherently, and caches it to hide latency — but if a compute node crashes before flushing its dirty cache lines to the device, its latest stores are lost. Crash-consistent data structures use flush and fence instructions to survive this, but they are extremely error-prone and their bugs evade ordinary testing, which rarely hits the exact bad crash timing. No tool existed for the CXL setting, whose partial-failure model (any subset of machines can fail at any point, even during another machine's recovery) differs fundamentally from persistent memory's total-failure model.
2. CXLMC is the first model checker for CXL crash-consistency bugs. It instruments C and C++ programs with LLVM, runs each simulated machine as a process (threads for cores), and emulates store buffers, caches, and x86-TSO with flushes, plus the partial failure of any subset of nodes. To avoid the exponential blowup of enumerating post-crash states, it adapts cache line constraint refinement: it tracks, per cache line, the interval in which its last write-back could have happened, and explores only executions that differ observably through post-failure loads — so the common commit-store pattern collapses to two executions. It is sound, so every bug it reports is real.
3. On adapted RECIPE and CXL-SHM benchmarks, CXLMC found 24 bugs in 8 applications, 7 of them new, with the longest run under a minute. A global-persistent-flush mode confirms the RECIPE bugs come specifically from lost cached values and partial failures. The trade-offs: it explores crash nondeterminism but not thread-interleaving nondeterminism (using random schedules to compensate), is tied to an x86-TSO-based model of the not-yet-standardized CXL semantics, is sound but not exhaustively complete, and checks crashes and assertions, so richer correctness properties require programmer-supplied assertions.

Check yourself

Check your understanding

1. Why can a machine crash in CXL shared memory silently lose that machine's most recent writes?
2. How does CXL's failure model differ from persistent memory's, and why does that matter for a checker?
3. What is cache line constraint refinement, and why does CXLMC need it?
4. Predict: CXLMC reports that a data structure hits an assertion failure after a particular partial-failure execution. How much should a developer trust this report, and why?

Sources

The paper is “CXLMC: Model Checking CXL Shared Memory Programs” by Yutong Guo, Conan Truong, and Brian Demsky (University of California, Irvine), published at ASPLOS 2026, DOI 10.1145/3779212.3790150. It is licensed CC BY, with an author copy hosted at UC Irvine’s Programming Languages Research Group.

This explainer is written from the paper’s full text (the authors’ hosted copy). CXLMC is the first model checker for crash-consistency bugs in x86-CXL shared-memory programs. It instruments C and C++ programs with an LLVM pass, runs each simulated machine as a separate process (with threads for cores), and emulates store buffers, local caches, and the x86-TSO memory model with flush instructions (based on a Px86sim-style formalization). It models CXL’s partial-failure setting, in which any subset of compute nodes can fail at any point, including during another machine’s recovery. To remain tractable, it adapts the constraint-based cache line constraint refinement technique from persistent-memory model checking with a novel formulation for partial failures: it tracks, per cache line, the interval in which its last write-back could have occurred, and explores only executions that differ observably through post-failure loads, reducing the commit-store pattern to two executions. CXLMC is sound (every reported execution is feasible, so every bug is real) though not exhaustively complete. The paper reports finding 24 bugs in 8 applications (including 7 new bugs) across adapted RECIPE and CXL-SHM benchmarks, with the longest benchmark running in just under a minute, and uses a global-persistent-flush mode to confirm that the RECIPE bugs stem specifically from lost cached values and partial failures. Numbers are the paper’s own; exact algorithms, the formal model, and full results should be confirmed in the paper.