一句话：提出 CXL 桥抽象并实现 vCXLGen，可从机器可读的一致性协议规范自动合成并组合验证异构 CXL 桥。
CXL 支持跨主机、字节寻址且缓存一致的远程内存访问，但其规范缺乏保证异构主机间安全互操作的机制：不同主机可能采用不同的缓存一致性协议和内存一致性模型，形成语义鸿沟，阻碍 CXL 在异构数据中心的部署。本文提出 CXL 桥抽象，在主机与 CXL 之间调和缓存一致性协议和内存一致性模型的差异，并实现 vCXLGen。其核心贡献包括：从机器可读的缓存一致性协议规范自动合成 CXL 桥，以及面向活性性质的可扩展组合式形式验证。评估表明，vCXLGen 支持 SWMR 和松一致性等多种协议且易于扩展；合成桥性能与手工设计的同构协议相当；形式验证严格证明了合成桥的安全性与活性，并在复杂异构系统的活性验证上取得良好可扩展性。
Compute Express Link (CXL) offers byte-addressable, cache-coherent remote memory accesses across multiple hosts. Unfortunately, the CXL specification lacks mechanisms to ensure safe interoperability between heterogeneous host architectures with diverse cache coherence (CC) protocols and memory consistency models (MCMs). This semantic gap poses fundamental challenges and a significant barrier to adopting CXL in modern heterogeneous data centers. We propose CXL bridges, an abstraction that interposes between hosts and CXL to reconcile differences in CC protocols and MCMs. We present vCXLGen, the first system that automatically synthesizes and verifies these CXL bridges. We make two core contributions: (1) a fully automated approach to synthesize CXL bridges from machine-readable CC protocol specifications, and (2) a compositional formal verification approach for scalable model-checking of liveness properties. Our evaluation shows that vCXLGen is general, i.e., it supports diverse protocols (both SWMR and relaxed consistency) and is easily extensible when integrating new protocols, such as CXL.mem. Our performance evaluations indicate that synthesised bridges achieve comparable results to manually designed homogeneous protocols. Finally, for correctness, our formal verification rigorously proves the safety and liveness of synthesized bridges, all while achieving significant scalability in liveness verification of complex heterogeneous systems.
@inproceedings{LefortPCSD0OB26,
title = {vCXLGen: Automated Synthesis and Verification of CXL Bridges for Heterogeneous Architectures},
author = {Anatole Lefort and Julian Pritzi and Nicolò Carpentieri and David Schall and Simon Dittrich and Soham Chakraborty and Nicolai Oswald and Pramod Bhatotia},
booktitle = {ASPLOS},
year = {2026},
doi = {10.1145/3779212.3790245}
}