摘要
提出了一种通过查找缓存一致性协议不变量来验证带参协议正确性的新方法.缓存一致性协议验证的难点在于必须证明协议对于任意大小的带参系统都成立.我们通过寻找不变量和协议规则之间的对应关系来计算辅助不变量,从而帮助推导验证缓存一致性协议.我们设计实现了一个不变量查找工具并将该工具应用到German协议上计算它们的辅助不变量并成功地验证了协议的安全性质.
We present a new method for computing invariants for cache coherence protocol in this paper. The verification of cache coherence protocols is always a challenge as we have to check the safety properties of cache coherence protocol with arbitrary nodes. By searching the relations between the invariants and the rules of cache coherence protocol, we can verify the cache coherence protocol with circular reasoning. Besides, we implement a tool to help us computing invariants for cache coherence protocol We also have experiments on how to apply our method to the German protocol with both control property and data property.
出处
《计算机系统应用》
2015年第11期173-178,共6页
Computer Systems & Applications
关键词
缓存一致性协议
带参系统
不变量查找
多核处理器
cache coherence protocol
parameterized system
invariant computing
multi-processor
