2015/05/24 by Xiangyao Yu, Yu, Xiangyao, Muralidaran Vijayaraghavan +3 · 1 citation
Computer Science · Engineering · #Advanced Memory and Neural Computing #Distributed #Distributed systems and fault tolerance #FOS: Computer and information sciences #Parallel #Parallel Computing and Optimization Techniques #and Cluster Computing (cs.DC)
paper · pdf · doi:10.48550/arxiv.1505.06459
openalex publication_date 2015/05/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.