Affordable Access

Cache coherence verification with TLA%

IFIP Lecture Notes in Computer Science (LNCS)
Publication Date
  • Design
  • Engineering


We used the specification language TLA+ to analyze the correctness of two cache-coherence protocols for shared-memory multiprocessors based on two generations (EV6 and EV7) of the Alpha processor. A memory model defines the relationship between the values written by one processor and the values read by another, and a cache-coherence protocol manipulates the caches to preserve this relationship. The cache-coherence protocol is a fundamental component of any shared-memory multiprocessor design. Proving that the coherence protocol implements the memory model is a high-leverage application of formal methods. The analysis of the first protocol was largely a research project, but the analysis of the second protocol was a part of the engineers' own verification process.Full Text at Springer, may require registration or fee

There are no comments yet on this publication. Be the first to share your thoughts.


Seen <100 times