vCXLGen: Automated Synthesis and Verification of CXL Bridges for Heterogeneous Architectures

Compute Express Link (CXL) offers byte-addressable, cachecoherent 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.