一句话：首次在 Lean 中机器验证同步传播原则，证明其可为一大类异构一致性协议保证复合内存一致性模型。
现代处理器通过集成异构设备来提供统一共享内存，但用于组合不同一致性协议的事实设计模式一直缺乏形式基础，容易引入隐蔽的一致性错误。本文提出一种统一的一致性协议抽象，将上述设计模式形式化为“同步传播原则”（Principle of Synchronous Propagation），并在 Lean 证明助手中给出首个机器检查的正确性证明。中心定理表明：对一大类协议，同步传播足以保证复合内存一致性模型（Compound Memory Consistency Model）。该工作既为现有异构设计提供了长期缺失的可靠性保证，也提供了一个可复用、可组合的框架，用于验证未来异构系统的一致性协议。
Modern processors integrate heterogeneous devices to expose unified shared memory. Yet, the de-facto design pattern used to compose their disparate coherence protocols lacks a formal foundation. This leaves the door open for subtle consistency bugs, in a critical gap between practice and correctness. This paper provides the first formal, machine-checked proof that a de-facto design pattern, which we call the Principle of Synchronous Propagation, is correct. Leveraging a new unifying abstraction for coherence protocols, our central theorem (machine checked in Lean) proves that Synchronous Propagation is sufficient to guarantee the Compound Memory Consistency Model for a wide class of protocols. Our work provides long-needed assurance for current designs and delivers a reusable, compositional framework for verifying future heterogeneous systems.
@article{ZhangGSN26,
title = {A Formally Verified Foundation for Compositional Heterogeneous Coherence},
author = {An Qi Zhang and Andrés Goens and Daniel Sorin and Vijay Nagarajan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808350}
}