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.