Abstract
We propose new, tractably (in some cases provably) efficient algorithmic methods for exact (sound and complete) parameterized reasoning about cache coherence protocols. For reasoning about general snoopy cache protocols, we introduce the guarded broadcast protocols model and show how an abstract history graph construction can be used to reason about safety properties for this framework. Although the worst case size of the abstract history graph can be exponential in the size of the transition diagram of the given protocol, the actual size is small for standard cache protocols as is evidenced by our experimental results. The framework can handle all 8 of the cache protocols in [19] as well as their split-transaction versions. We next identify a framework called initialized broadcast protocols suitable for reasoning about invalidation-based snoopy cache protocols and show how to reduce reasoning about such systems with an arbitrary number of caches to a system with at most 7 caches. This yields a provably polynomial time algorithm for the parameterized verification of invalidation based snoopy protocols. Our results apply to both safety and liveness properties. Finally, we present a methodology for reducing parameterized reasoning about directory based protocols to snoopy protocols, thus leveraging techniques developed for verifying snoopy protocols to directory based ones, which are typically are much harder to reason about. We demonstrate by reducing reasoning about a directory based protocol suggested by German [17] to the ESI snoopy protocol, a modification of the MSI snoopy protocol.
This work was supported in part by NSF grants CCR-009-8141 & CCR-020-5483, and SRC contract 2002-TJ-1026.
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
Abdulla, P., Cerans, K., Jonsson, B., Tsay, Y.K.: General Decidability Theorems for Infinite State Systems. In: LICS (1996)
Abdulla, P., Boujjani, A., Jonsson, B., Nilsson, M.: Handling global conditions in parameterized systems verification. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 134–145. Springer, Heidelberg (1999)
Abdulla, P., Jonsson, B.: On the existence of network invariants for verifying parameterized systems. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 180–197. Springer, Heidelberg (1999)
Baukus, K., Lakhnech, Y., Stahl, K.: Parameterized Verification of a Cache Coherence Protocols: Safety and Liveness. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 317–330. Springer, Heidelberg (2002)
Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about Networks with Many Identical Finite State Processes. Information and Control 81(1), 13–31 (1989)
Clarke, E.M., Grumberg, O., Hirashi, H., Jha, S., Long, D.E., McMillan, K.L., Ness, L.A.: Verification of the Futurebus+cache coherence protocol. In: Proc. 11th Int. Symp. on Computer Hardware Description Languages and their Applications (1993)
Culler, D.E., Singh, J.P.: Parallel Computer Architecture:A Hardware/Software Approach. Morgan Kaufmann Publishers, San Francisco (1998)
Delzanno, G.: Automatic Verification of Parameterized Cache Coherence Protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 51–68. Springer, Heidelberg (2000)
Emerson, E.A., Kahlon, V.: Reducing Model Checking of the Many to the Few. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, Springer, Heidelberg (2000)
Emerson, E.A., Kahlon, V.: Model Checking Large-Scale and Parameterized Resource Allocation Systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 251. Springer, Heidelberg (2002)
Emerson, E.A., Kahlon, V.: Rapid Parameterized Model Checking of Snoopy Cache Protocols. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 144–159. Springer, Heidelberg (2003)
Emerson, E.A., Kahlon, V.: Model Checking Guarded Protocols. In: LICS 2003 (2003)
Emerson, E.A., Namjoshi, K.S.: Reasoning about Rings. In: POPL, pp. 85–94 (1995)
Emerson, E.A., Namjoshi, K.S.: On Model Checking for Non-Deterministic Infinite-State Systems. In: LICS 1998 (1998)
Emerson, E.A., Namjoshi, K.S.: Automatic Verification of Parameterized Synchronous Systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)
Esparza, J., Finkel, A., Mayr, R.: On the Verification of Broadcast Protocols. In: LICS 1999 (1999)
German, S.M.: Private communication
German, S.M., Sistla, A.P.: Reasoning about Systems with Many Processes. J. ACM 39(3) (July 1992)
Handy, J.: The Cache Memory Book. Academic Press, London (1993)
Kurshan, R.P., McMillan, K.L.: A Structural Induction Theorem for Processes. In: PODC, pp. 239–247 (1989)
Maidl, M.: A Unifying Model Checking Approach for Safety Properties of Parameterized Systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 311. Springer, Heidelberg (2001)
McMillan, K., Schwalbe, J.: Formal Verification of the Gigamax Cache Consistency Protocol. In: Proc. Int. Symp. on Shared Memory Multiprocessors, pp. 242–251 (1991)
Pnueli, A., Ruah, S., Zuck, L.: Automatic Deductive Verification with Invisible Invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 82. Springer, Heidelberg (2001)
Pong, F., Dubois, M.: A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems 6(8) (August 1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emerson, E.A., Kahlon, V. (2003). Exact and Efficient Verification of Parameterized Cache Coherence Protocols. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive