针对弱内存模型的惰性缓存一致性协议验证
计算机科学中的逻辑
2017-05-24 v1
摘要
在本文中，我们针对 TSO-CC 这一现代惰性缓存一致性协议，验证了其设计所基于的内存一致性模型 TSO。我们首先展示了 TSO-CC（具有固定数量的处理器）与一种新型有限状态操作模型之间的弱模拟关系，该模型展现了 TSO-CC 的惰性并满足 TSO，从而实现了这一验证。然后，我们通过现有的参数化技术对此进行了扩展，允许对无限数量的处理器进行验证。该方法完全在模型检查器中执行，不需要外部工具，且验证者几乎不需要具备形式化验证方法的深入知识。
引用
@article{arxiv.1705.08262,
title = {Verification of a lazy cache coherence protocol against a weak memory model},
author = {Christopher J. Banks and Marco Elver and Ruth Hoffmann and Susmit Sarkar and Paul Jackson and Vijay Nagarajan},
journal= {arXiv preprint arXiv:1705.08262},
year = {2017}
}
备注
10 pages