Speaker:
Giorgio Delzanno
Title:
Automatic Verification of Cache Coherence Protocols (Preliminary
results)
Abstract.
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.