Formalization and verification of coherence protocols with the gamma framework
Authors:
- Le MetayerLMLe Metayer
- Thierry PriolTPThierry Priol
- 1 January 2000
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 105-113
Abstract
This paper presents an approach to formalize coherence protocols for shared virtual memories as multiset rewriting systems. The global state of the protocol is represented as a multiset and rewriting rules are used to describe state changes. Invariants are expressed as properties on the cardinality of subsets which characterize specific relations. We present an automatic algorithm to check that a property is an invariant of a protocol. Both the formalization and the verification steps are illustrated on the Li and Hudak single-writer/multiple-readers coherence protocol.Keywords
This publication has 14 references indexed in Scilit:
- Verification of Cache Coherence Protocols by Aggregation of Distributed TransactionsTheory of Computing Systems, 1998
- Refining multiset transformersTheoretical Computer Science, 1998
- Verification techniques for cache coherence protocolsACM Computing Surveys, 1997
- Software architecture styles as graph grammars1996
- GAMMA AND THE CHEMICAL REACTION MODEL: TEN YEARS AFTER1996
- The reflexive CHAM and the join-calculus1996
- Scope consistency1996
- Using belief to reason about cache coherence1994
- Implementation and performance of Munin1991
- Memory coherence in shared virtual memory systems1986