Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement
Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement
复制标题
通过参数组合细化验证令牌一致性实现的安全性
DOI：
10.1007/978-3-540-30579-8_9
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Milo M. K. Martin
中科院分区：
文献类型：
--
作者：
S. Burckhardt;R. Alur;Milo M. K. Martin
我们将组合推理和可达性分析相结合，以形式化地验证一种最新的缓存一致性协议的安全性。该协议是令牌一致性的一种详细实现，这是一种将正确性和性能解耦的方法。首先，我们提出一个形式化的抽象规范，它捕捉了令牌一致性的安全基础，并突出了缓存控制器状态以及它们所交换消息内容的对称性。然后，我们证明这个抽象规范是一致的，并检查协议设计者提出的实现是否是该抽象规范的一种细化。我们的细化证明在缓存控制器的数量方面是参数化的，并且是组合性的，因为它使用一种特殊形式的假设 - 保证推理将细化检查简化到单个控制器。各个细化义务通过细化映射和可达性分析来履行。虽然形式化证明证实了设计者关于令牌一致性易于验证的直观说法，但我们报告了在实现中以及伴随的修改中存在的几个错误，这些错误在之前大量的模拟中被遗漏了。
We combine compositional reasoning and reachability analysis to formally verify the safety of a recent cache coherence protocol. The protocol is a detailed implementation of token coherence, an approach that decouples correctness and performance. First, we present a formal and abstract specification that captures the safety substrate of token coherence, and highlights the symmetry in states of the cache controllers and contents of the messages they exchange. Then, we prove that this abstract specification is coherent, and check whether the implementation proposed by the protocol designers is a refinement of the abstract specification. Our refinement proof is parametric in the number of cache controllers, and is compositional as it reduces the refinement checks to individual controllers using a specialized form of assume-guarantee reasoning. The individual refinement obligations are discharged using refinement maps and reachability analysis. While the formal proof justifies the intuitive claim by the designers about the ease of verifiability of token coherence, we report on several bugs in the implementation, and accompanying modifications, that were missed by extensive prior simulations.