Tardis 缓存一致性协议的正确性证明
分布式、并行与集群计算
2015-05-26 v1
摘要
我们证明了最近提出的缓存一致性协议 Tardis 的正确性，该协议简单且可扩展到高处理器数量，因为它对于一个 N 处理器系统仅需要每缓存行 O(logN) 的存储。我们证明 Tardis 遵循顺序一致性模型，且既无死锁也无活锁。我们的证明基于系统简单直观的不变量，因此适用于任意系统规模以及 Tardis 的许多变体。
引用
@article{arxiv.1505.06459,
title = {A Proof of Correctness for the Tardis Cache Coherence Protocol},
author = {Xiangyao Yu and Muralidaran Vijayaraghavan and Srinivas Devadas},
journal= {arXiv preprint arXiv:1505.06459},
year = {2015}
}
备注
16 pages, 2 figures