Verifying Cache Coherence with TLA

Abstract

TLA (The Temporal Logic of Actions) is a logic for specifying and reasoning about concurrent systems. I will explain TLA briefly and show how it is used to specify a simple memory and a simple caching scheme. I will then describe our experience using TLA to verify the cache coherence protocols for Compaq's forthcoming alpha-based multiprocessors.