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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
P. A. Abdulla, K. Cerāns, B. Jonsson, Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc. LICS’96, pp. 313–321, 1996.
P. A. Abdulla, B. Jonsson. Verifying Networks of Timed Processes (Extended Abstract). In Proc. TACAS’ 98, pp. 298–312. Springer, 1998.
P. A. Abdulla, B. Jonsson. Channel Representations in Protocol Verification. In Proc. CONCUR 2001, pp. 1–15. Springer, 2001.
P. A. Abdulla, A. Nylén. Better is Better than Well: On Efficient Verification of Infinite-State Systems. In Proc. LICS 2000, pp. 132–140, 2000.
P. A. Archibald, J. Baer. Cache Coherence Protocols: Evaluation Using a Multiprocessor Simulation Model. TOCS 4(4): 273–298. 1986.
T. Arons, A. Pnueli, S. Ruah, Y. Xu, L. Zuck Parameterized Verification with Automatically Computed Inductive Assertions. In Proc. CAV’ 01, pp. 221–234, 2001.
K. Baukus, S. Bensalem, Y. Lakhnech, K. Stahl. Abstracting WS1S Systems to Verify Parameterized Networks. In Proc. TACAS’ 00, pp. 188–203, 2000.
K. Baukus, K. Stahl, S. Bensalem, Y. Lakhnech. Networks of Processes with Parameterized State Space. In Proc. VEPAS’ 01, ENTCS vol. 50, issue 4, 2001.
A. Bouajjani, B. Jonsson, M. Nilsson, T. Touilli. Regular Model Checking. In Proc. CAV’00, pp. 403–418, 2000.
M. Bozzano, G. Delzanno. Beyond Parameterized Verification. In Proc. TACAS’02, April 2002.
I. Cervesato, N. A. Durgin, P. Lincoln, J. C. Mitchell, A. Scedrov. A Meta-notation for Protocol Analysis. In Proc. CSFW 1999, pp. 55–69, 1999.
E. Clarke, O. Grumberg, S. Jha. Verifying Parameterized Networks. TOPLAS 19(5): 726–750, 1997.
G. Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. In Proc. CAV 2000, pp. 53–68, 2000.
G. Delzanno. An assertional language for systems parametric in several dimensions. In Proc. VEPAS 2001, ENTCS 50(4), 2001.
E. A. Emerson, K. S. Namjoshi. On Model Checking for Non-deterministic Infinite-state Systems. In Proc. LICS’ 98, pp. 70–80, 1998.
J. Esparza, A. Finkel, R. Mayr. On the Verification of Broadcast Protocols. In Proc. LICS’99, pp. 352–359, 1999.
A. Finkel, P. Schnoebelen. Well-structured transition systems everywhere! TCS, 256(1–2):63–92, 2001.
K. Fisler, C. Girault. Modelling and Model Checking a Distributed Shared Memory Consistency Protocol. In Proc. ICATPN’ 98, pp. 84–103, 2001.
G. Highman. Ordering by Divisibility in Abstract Algebras. Proc. London Math. Soc., 2:326–336, 1952.
K. Li, P. Hudak. Memory Coherence in Shared Virtual Memory Systems. TOCS 7(4): 321–359, 1989.
D. Mentré, D. Le Métayer, T. Priol. Formalization and Verification of Coherence Protocols with the Gamma Framework. In Proc. PDSE 2000, pp. 105–113, 2000.
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar. Symbolic Model Checking with Rich Assertional Languages. In Proc. CAV’97, pp. 424–435, 1997.
A. P. Sistla, V. Gyuris. Parametrized Verification of Linear Networks using Automata as Invariants. Formal Aspects of Computing, 11(4):402–425, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bozzano, M., Delzanno, G. (2002). Algorithmic Verification of Invalidation-Based Protocols. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_22
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive