使用 Guarded Action Language 对缓存一致性协议进行建模
计算机科学中的逻辑
2018-03-29 v1 硬件体系结构
摘要
我们提出了一个为验证硬件 Tera-Scale ARchitecture (TSAR) 而构建的形式化模型，重点关注其分布式混合缓存一致性协议（DHCCP）。该协议本质上是异步、并发和分布式的，这使得经典的设计验证（例如通过测试）变得困难。因此，我们应用形式化方法证明了该协议的基本性质，例如无死锁、最终共识和公平性。
引用
@article{arxiv.1803.10323,
title = {Modeling a Cache Coherence Protocol with the Guarded Action Language},
author = {Quentin L. Meunier and Yann Thierry-Mieg and Emmanuelle Encrenaz},
journal= {arXiv preprint arXiv:1803.10323},
year = {2018}
}
备注
In Proceedings MARS/VPT 2018, arXiv:1803.08668