Paper Info
Title
A Proof of Correctness for the Tardis Cache Coherence Protocol
Abstract
We prove the correctness of a recently-proposed cache coherence protocol, Tardis, which is simple, yet scalable to high processor counts, because it only requires O(logN) storage per cacheline for an N-processor system. We prove that Tardis follows the sequential consistency model and is both deadlock- and livelock-free. Our proof is based on simple and intuitive invariants of the system and thus applies to any system scale and many variants of Tardis.
Year
Venue
Field
2015
CoRR
Sequential consistency,Computer science,Correctness,Deadlock,Parallel computing,Theoretical computer science,Invariant (mathematics),Cache coherence,Scalability,Distributed computing
DocType
Volume
Citations 
Journal
abs/1505.06459
4
PageRank 
References 
Authors
0.40
17
3
Name
Order
Citations
PageRank
Xiangyao Yu127016.17
Muralidaran Vijayaraghavan215712.51
Srinivas Devadas386061146.30