Title: Automatic Verification of Cache Coherence Protocols (Preliminary results)
Cache coherence protocols are used to maintain data consistency in
commercial multiprocessor systems equipped with local fast caches.
We propose a new method to verify safety properties for coherence protocols at the behaviour level. We consider multiprocessors with many identical caches. We use arithmetic constraints to represent possibly infinite sets of global states modulo symmetries. We use symbolic model checkers for infinite-state systems based on real arithmetics to perform backward reachability analysis over the resulting integer systems. In preliminary experiments we have automatically verified safety properties for parameterized versions of write-invalidate and write-update cache coherence policies like the Mesi, Synapse, Berkeley RISC, University of Illinois, DEC Firefly and Xerox PARC Dragon protocols.
Description of the experiments.