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.


You are not logged in 
Contact 
©2002-2017 U.C. Regents