Applying Formal Verification to a Cache Coherence Protocol in TLS

Current hardware implementations of TLS (thread-level speculation) in both Hydra and Renau´s SESC simulator use a global component to check data dependence violations, e.g. L2 Cache or hardware list. Frequent memory accesses cause global component bottlenecks. In this paper, we propose a cache coherence protocol using a distributed data dependence violation checking mechanism for TLS. The proposed protocol extends the traditional MESI cache coherence protocol by including several methods to exceed the present limits of centralized violation checking methods. The protocol adds an invalidation vector to each private L1 cache to record threads that violate RAW data dependence. It also adds a versioning priority register that compares data versions. Added to each private L1 cache block is a snooping bit which indicates whether the thread possesses a bus snooping right for the block. The proposed protocol is much more complicated than the traditional MESI protocol and hard to be completely verified only through simulation. So we applied formal verification to the proposed cache protocol to confirm its correctness. The verification result shows that the proposed protocol will function correctly in TLS system.