Compute Express Link (CXL) lets multiple machines share byte-addressable, cache-coherent memory, but the standard says nothing about making different vendors' CPUs — each with its own cache-coherence protocol and memory-consistency model — work together over it, a semantic gap that blocks CXL in heterogeneous data centers; this paper (TU Munich and TU Delft — Anatole Lefort, Julian Pritzi, Nicolo Carpentieri, David Schall, Simon Dittrich, Soham Chakraborty, Nicolai Oswald, Pramod Bhatotia) proposes CXL bridges that sit between each host and CXL to reconcile those differences, and presents vCXLGen, the first system to automatically synthesize such a bridge from machine-readable protocol specifications and formally verify its safety and deadlock-freedom with a compositional model-checking approach that scales to complex heterogeneous systems, matching hand-designed homogeneous protocols in performance.
The argument in one glance
-
Problem
CXL lets machines share coherent memory, but different CPUs cannot safely agree
Compute Express Link (CXL) is an interconnect that lets multiple machines share memory that is byte-addressable and cache-coherent — you can read and write remote memory as if it were local, and the hardware keeps everyone's caches consistent. This unlocks memory pooling and disaggregation for data centers. But CXL only defines its own coherence protocol; it says nothing about how to make heterogeneous hosts interoperate safely. Different vendors' CPUs use different cache-coherence protocols, deeply baked into their designs, and different memory-consistency models — some enforce Single-Writer Multiple-Reader, others allow relaxed consistency. So when you connect diverse architectures to shared CXL memory, there is a semantic gap: each host speaks a different coherence dialect, and they disagree on the rules for what a shared read or write should see. Bridging that gap correctly is what stands between CXL's promise and its use in real heterogeneous data centers.
-
What people did
Design a bridge by hand to reconcile each pair of protocols
The natural response is to build a bridge: a piece of logic that sits between a host and CXL and translates between the host's coherence protocol and CXL's, reconciling their consistency models. In principle an engineer can design such a bridge for a given pair of protocols, working out how to map each transaction in one domain to the other so that coherence and the hosts' consistency guarantees are preserved.
-
Why it fell short
Hand-designing bridges is hard, error-prone, and must be redone as protocols change
Designing a correct bridge by hand is extremely difficult. A bridge must fuse two intricate coherence protocols into a single system-wide compound protocol, translating and propagating transactions across the boundary while preserving both safety (each host's memory-consistency model is honored, so programs see correct results) and liveness (no deadlock). Getting this right requires reasoning about the interleavings of two concurrent protocols, which is exactly the kind of thing humans get wrong, and a subtle mistake can cause silent data corruption or hangs. Worse, it does not scale: every new pair of architectures, and every revision of a protocol, needs a new hand-designed bridge and a fresh, painstaking correctness argument, and coherence protocols evolve frequently. So manual bridge design is both unreliable and unsustainable, which is why the semantic gap has remained a barrier to heterogeneous CXL.
-
This paper's idea
Automatically synthesize the bridge, and formally verify it, from specs
vCXLGen is the first system to automatically synthesize and verify CXL bridges. A CXL bridge is the abstraction it targets: logic interposed between a host and CXL that reconciles the host's local coherence protocol with CXL's. vCXLGen makes two contributions. First, automated synthesis: from machine-readable specifications of the local protocol and the CXL-defined global protocol, it generates the bridge as a finite state machine that correctly fuses them into a system-wide compound coherence protocol, propagating transactions across the domains by three rules — delegation (use native transaction flows to carry globally visible operations across), nesting atomicity (nested transactions appear atomic from the origin domain), and selective stalling (block or unblock requests as needed). Second, compositional formal verification: rather than model-check the whole heterogeneous system at once (which explodes), it verifies the bridge compositionally, proving safety (each host's consistency model is enforced) and liveness (deadlock-freedom) while scaling to complex systems. vCXLGen is general — it supports both SWMR and relaxed-consistency protocols and is easily extended to new ones like CXL.mem — and its synthesized bridges match manually designed homogeneous protocols in performance, all while being rigorously proved correct.
Why this problem is worth solving
CXL is poised to reshape how data centers use memory, but only if heterogeneous machines can share it safely. Compute Express Link is an interconnect standard that lets a processor access memory on another device or another host as if it were local: byte-addressable, so ordinary load and store instructions work on it, and cache-coherent, so the hardware keeps all the caches that hold a shared location consistent. This is powerful because it enables memory pooling and disaggregation — machines can draw from a shared pool of memory rather than each being stuck with its own, improving utilization and enabling new architectures. The catch is that cache coherence is enforced by a coherence protocol, a set of rules and message exchanges that decide, for every shared cache line, who may read or write it and when, and different CPU vendors implement different coherence protocols, tuned to their own memory subsystems and deeply embedded in their designs. On top of that, they expose different memory-consistency models — the guarantees a program gets about the order in which memory operations become visible — with some enforcing the strict Single-Writer Multiple-Reader discipline and others allowing weaker, relaxed orderings. CXL defines its own protocol (CXL.mem), but the specification does not say how a vendor’s architecture-specific protocol should combine with it, nor how to reconcile mismatched consistency models when diverse hosts touch the same shared memory. Without an answer, you cannot safely connect different architectures to shared CXL memory, which defeats much of the point of a shared memory fabric in a heterogeneous data center. Closing that gap is therefore essential to CXL actually delivering on heterogeneous memory sharing.
The reason the gap is so hard to close by hand is that fusing two coherence protocols correctly is a notoriously error-prone concurrency problem. A coherence protocol is a concurrent state machine: each cache line moves through states (modified, shared, invalid, and so on) driven by requests and responses, and correctness depends on all the possible interleavings of these transitions behaving well. Designing one protocol correctly is already hard; a CXL bridge must effectively merge two of them — a host’s local protocol and CXL’s global protocol — into a single compound protocol that spans both domains, translating each transaction in one into the right sequence in the other. It must do this while preserving two properties that are easy to violate. Safety means the host’s memory-consistency model is still honored end to end, so programs never observe an ordering the model forbids; a bug here silently corrupts results. Liveness means the combined system never deadlocks; a bug here hangs the machine. Reasoning about the interleavings of two concurrent protocols to guarantee both is exactly the task that overwhelms human designers, and the space of behaviors is vast. On top of the difficulty, there is a scaling problem: each new pairing of architectures and each revision of a protocol requires a fresh bridge and a fresh correctness argument, and coherence protocols and CXL itself keep evolving. So even a heroically careful manual design is a one-off that must be redone repeatedly. Both the difficulty and the churn point to the same solution: generate the bridge automatically from protocol specifications and verify it mechanically, which is what vCXLGen does.
What people did before, and where it broke
- Use CXL only within a single architecture. Share CXL memory only among homogeneous hosts that already speak the same coherence protocol. Where it broke. It avoids the semantic gap by giving up heterogeneity, which is exactly the multi-vendor sharing CXL was meant to enable in real data centers.
- Hand-design a bridge for a specific protocol pair. Have engineers craft logic that translates between one host protocol and CXL. Where it broke. Merging two concurrent coherence protocols correctly is extremely hard, so hand-designed bridges are error-prone, risking silent corruption or deadlock, and each is a bespoke effort.
- Manually argue correctness. Reason by hand, or with limited checking, that a bridge preserves safety and liveness. Where it broke. The interleaving space of two combined protocols is enormous, so human arguments miss cases, and there was no scalable way to formally verify liveness of the heterogeneous system.
- Redo the work for every change. Rebuild and re-verify a bridge whenever architectures are paired differently or a protocol is revised. Where it broke. Coherence protocols and CXL evolve frequently, so a per-instance manual approach cannot keep up.
- The gap. No system automatically synthesized a correct CXL bridge from protocol specifications and formally verified both its safety and its liveness at scale, so heterogeneous CXL had no reliable, sustainable path to interoperability.
How vCXLGen works
Generating and verifying a CXL bridge from protocol specifications
-
-
new
-
new
-
new
-
new
-
new
The idea
Make the coherence protocols formal inputs, and generate the bridge from them. The foundational move in vCXLGen is to treat each host’s coherence protocol and CXL’s protocol as machine-readable specifications and synthesize the bridge automatically, rather than having an engineer design it. This turns a bespoke, error-prone design task into a repeatable generation task, so a new architecture pairing or a revised protocol just means feeding in a new spec. Interposing a translating layer between two systems that speak different protocols so they can share resources coherently is the same bridging role the work on CXL-based memory pooling for cloud platforms covered elsewhere on this site is built on, composing memory across machines through a coherent interconnect. vCXLGen automates the construction of exactly the piece that makes such sharing safe across heterogeneous architectures, which pooling within one architecture did not have to solve.
Reconcile the consistency models, not just the messages. A correct bridge is not only about translating coherence messages; it must ensure that each host still sees the memory ordering its consistency model promises, whether that is strict Single-Writer Multiple-Reader or a relaxed model. vCXLGen’s synthesized compound protocol, governed by delegation, nesting atomicity, and selective stalling, is designed so the combined system preserves each host’s consistency guarantees. Reasoning precisely about what orderings of memory operations a system may expose, and building mechanisms that enforce the intended model, is the same discipline the work on a scoped, buffered persistency model for GPUs covered elsewhere on this site is built on, pinning down and enforcing an ordering guarantee in hardware. vCXLGen extends that reasoning across a heterogeneous boundary, making one side’s model hold even as transactions cross into another protocol’s domain.
Prove it correct at scale, compositionally. Because a fused coherence protocol has an enormous space of interleavings, ad hoc reasoning cannot establish correctness, so vCXLGen model-checks the bridge to prove both safety and liveness — but monolithic model-checking of a heterogeneous system explodes, so it verifies compositionally, checking components and composing the results to keep liveness verification tractable. Establishing a concurrency-correctness property by rigorous model-checking, and taming the state-space explosion so the verification actually scales, is the same challenge the work on scalable model-checking for crash-consistency verification covered elsewhere on this site confronts, making formal verification of a complex concurrent system feasible. vCXLGen applies compositional verification to coherence bridges, which is what lets it certify deadlock-freedom for complex heterogeneous systems that a naive checker could never handle.
Following a transaction through vCXLGen
Synthesizing and running a bridge between a MESI host and CXL
A trace, drawn from the paper, of how vCXLGen builds a bridge from specs and how a memory transaction crosses it.
Step 1 of 5
Provide the protocol specifications
vCXLGen is given machine-readable specifications of the host's local coherence protocol (say a MESI-style protocol) and CXL's global protocol. These formal descriptions are the inputs from which everything is generated and checked.
Formal specs replace an engineer's hand design as the source of truth.
Why it works
- Generating from specs replaces error-prone hand design. Merging two coherence protocols by hand is hard and mistakes corrupt or hang the system → but synthesizing the bridge from machine-readable specs makes it repeatable and mechanical → so a correct bridge can be produced without a bespoke, fallible design effort.
- The compound protocol preserves each host’s guarantees. Naively bridging messages could break a host’s memory-consistency model → but the synthesized protocol’s delegation, nesting-atomicity, and selective-stalling rules enforce the model across the boundary → so programs still see correct orderings.
- Model-checking catches interleaving bugs humans miss. The interleavings of two combined protocols are too many to reason about by hand → but model-checking exhaustively explores them → so subtle safety and liveness violations are found or proved absent.
- Compositional verification makes liveness proof scale. Checking the whole heterogeneous system monolithically explodes → but verifying components and composing the results keeps the state space tractable → so liveness can be proved even for complex heterogeneous systems.
- Automation absorbs protocol churn. Every new architecture pairing or protocol revision would need a fresh hand-built, hand-verified bridge → but feeding a new spec to vCXLGen regenerates and re-verifies the bridge → so the approach keeps up as protocols evolve.
What it costs (trade-offs and scope)
- It needs machine-readable protocol specifications. vCXLGen synthesizes and verifies from formal specs of the coherence protocols, so a protocol must be written in that machine-readable form; producing accurate specifications is required work, and the guarantees are relative to the specs being faithful to the real hardware.
- Verification scope is safety and liveness of the bridge. vCXLGen proves the synthesized bridge preserves each host’s consistency model (safety) and is deadlock-free (liveness); it does not, by itself, guarantee properties outside that model or the correctness of the underlying host protocols as specified, and the assurance rests on the model-checking assumptions.
- Synthesized bridges are compared to homogeneous designs. The performance evaluation shows synthesized bridges achieve results comparable to manually designed homogeneous protocols; that is a strong result, but it is a comparison on the paper’s workloads and configurations, and heterogeneous bridging still introduces the bridge into the coherence path.
- The demonstrated protocol diversity, while broad, is finite. vCXLGen supports both SWMR and relaxed-consistency protocols and is extensible to new ones like CXL.mem, but the evaluation covers a specific set; integrating a genuinely novel protocol still requires expressing it in the specification form and re-running synthesis and verification.
- It targets the coherence-bridging problem for CXL. vCXLGen addresses reconciling cache-coherence protocols and consistency models across heterogeneous hosts over CXL; other aspects of CXL system design (allocation, security, performance tuning of the fabric itself) are outside its stated scope.
The evaluation
Making heterogeneous hosts share coherent memory over CXL
| Property | Homogeneous CXL only | Hand-designed bridge | vCXLGen |
|---|---|---|---|
| Supports heterogeneous architectures | |||
| How the bridge is built | |||
| Correctness guarantee | |||
| Scales and adapts to new protocols | |||
| Reported outcome |
Check yourself
Check your understanding
1. Why does CXL struggle to connect heterogeneous machines despite offering coherent shared memory?
2. What is a CXL bridge, and what does vCXLGen do with it?
3. Why does vCXLGen verify bridges compositionally instead of all at once?
4. What did vCXLGen achieve, and what are its main caveats?
Sources
The paper is “vCXLGen: Automated Synthesis and Verification of CXL Bridges for Heterogeneous Architectures” by Anatole Lefort, Julian Pritzi, Nicolo Carpentieri, David Schall, Simon Dittrich, Soham Chakraborty, Nicolai Oswald, and Pramod Bhatotia (Technical University of Munich and Delft University of Technology), published at ASPLOS 2026 (Volume 2), DOI 10.1145/3779212.3790245. It received a Best Paper Award and is licensed CC BY.
This explainer is written from the paper’s full text (the authors’ PDF of the ASPLOS 2026 paper). The paper addresses the semantic gap that arises because Compute Express Link (CXL) offers byte-addressable, cache-coherent remote memory across multiple hosts but its specification lacks mechanisms to ensure safe interoperability between heterogeneous host architectures with diverse cache-coherence protocols and memory-consistency models. The paper proposes CXL bridges, an abstraction interposed between a host and CXL to reconcile these differences, and presents vCXLGen, the first system to automatically synthesize and verify them. Its two core contributions are a fully automated approach to synthesize CXL bridges from machine-readable cache-coherence protocol specifications — fusing the host’s local protocol and the CXL-defined global protocol into a system-wide compound coherence protocol as a finite state machine, propagating transactions across domains via delegation, nesting atomicity, and selective stalling — and a compositional formal-verification approach for scalable model-checking of liveness properties, alongside safety. The reported results are the paper’s own: vCXLGen is general, supporting both SWMR and relaxed-consistency protocols and easily extensible to new protocols such as CXL.mem; its synthesized bridges achieve performance comparable to manually designed homogeneous protocols; and its formal verification rigorously proves the safety and liveness of synthesized bridges while achieving significant scalability in liveness verification of complex heterogeneous systems. No numbers beyond the paper’s own have been introduced; exact synthesis and verification algorithms, the specification format, and the full evaluation should be confirmed in the paper, and artifacts are available.