Verifying Cache Coherence with TLA


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.

©2002-2018 U.C. Regents