We propose an extension of the model of Broadcast Protocols in which individual processes are allowed to have unbounded local data and to communicate via value passing. Our specification language is based on multiset rewriting over first order atomic formulas enriched with a mechanism for global synchronization to model broadcasts, and constraints to model the relations over internal data and value passing. For this new class of parameterized systems, we provide a symbolic validation procedure for checking safety properties, and termination conditions defined on special classes of multiset rewriting systems with linear constraints. We report here on practical experiments with coherence protocols for virtual shared memory, and multiprocessors systems in which the number of processors, pages or cache lines are left as parameters.

Algorithmic Verification of Invalidation-Based Protocols

Bozzano, Marco;Delzanno, Giorgio
2002

Abstract

We propose an extension of the model of Broadcast Protocols in which individual processes are allowed to have unbounded local data and to communicate via value passing. Our specification language is based on multiset rewriting over first order atomic formulas enriched with a mechanism for global synchronization to model broadcasts, and constraints to model the relations over internal data and value passing. For this new class of parameterized systems, we provide a symbolic validation procedure for checking safety properties, and termination conditions defined on special classes of multiset rewriting systems with linear constraints. We report here on practical experiments with coherence protocols for virtual shared memory, and multiprocessors systems in which the number of processors, pages or cache lines are left as parameters.
978-3-540-43997-4
978-3-540-45657-5
978-3-540-43997-4
978-3-540-45657-5
File in questo prodotto:
File Dimensione Formato  
cav02-1.pdf

solo utenti autorizzati

Tipologia: Documento in Pre-print
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 205.85 kB
Formato Adobe PDF
205.85 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/309027
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact