Checking Cache-Coherence Protocols with TLA+

We have a great deal of experience using the specification language TLA+ and its model checker TLC to analyze protocols designed at Digital and Compaq (both now part of HP). The tools and technique...