Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification

  • Sudhindra Pandav
  • Konrad Slind
  • Ganesh Gopalakrishnan
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


We propose a heuristic-based method for discovering inductive invariants in the parameterized verification of safety properties. The promise of the method stems from powerful heuristics we have identified for verifying the cache coherence of directory based protocols. The heuristics are based on syntactic analysis of counterexamples generated during verification, combined with simple static analysis of the predicates involved in the counterexamples to construct and refine inductive invariants. The heuristics were effective in filtering irrelevant predicates as well as keeping the sizes of the generated inductive invariants small. Contributions are: (i) the method is an efficient strategy for discovering inductive invariants for practical verification; (ii) the heuristics scaled smoothly from two small to one large cache coherence protocol (of complexity similar to commercial cache coherence protocols); (iii) the heuristics generate relevant auxiliary invariants which are easily verifiable in few seconds; and (iv) the method does not depend on special verification frameworks and so can be adapted for other verification tools. The case studies include German, FLASH, and a new protocol called German-Ring. The properties verified include mutual exclusion and data consistency.


Decision Procedure Transition Rule Mutual Exclusion Safety Property Directory Variable 
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.


  1. 1.
    Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)Google Scholar
  2. 2.
    German, S.: Personal CommunicationGoogle Scholar
  3. 3.
    Siegel, T.J., Pfeffer, E., Magee, J.A.: The IBM eServer z990 microprocessor. IBM J. Res. Dev. 48(3-4), 295–309 (2004)Google Scholar
  4. 4.
    Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78–92. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    German, S., Wegbreit, B.: A synthesizer of inductive assertions. IEEE Trans. Software Eng. 1(1), 68–75 (1975)Google Scholar
  6. 6.
    Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Safety. Springer, Heidelberg (1995)Google Scholar
  7. 7.
    Tiwari, A., Rueß, H., Saïdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 113–127. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  8. 8.
    Bjorner, N., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theor. Comput. Sci. 173(1), 49–87 (1997)CrossRefMathSciNetGoogle Scholar
  9. 9.
    Bensalem, S., Lakhnech, Y., Saïdi, H.: Powerful techniques for the automatic generation of invariants. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 323–335. Springer, Heidelberg (1996)Google Scholar
  10. 10.
    Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 19–32. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  11. 11.
    Baukus, K., Lakhnech, Y., Stahl, K.: Parameterized verification of a cache coherence protocol: Safety and liveness. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 317–330. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Das, S., Dill, D., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  13. 13.
    Lahiri, S.K., Bryant, R.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 135–147. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. 14.
    Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  15. 15.
    Park, S., Dill, D.L.: Verification of flash cache coherence protocol by aggregation of distributed transactions. In: SPAA 1996, pp. 288–296. ACM Press, New York (1996)CrossRefGoogle Scholar
  16. 16.
    Mannava, P.K., Chou, C.T., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382–398. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    McMillan, K.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 179–195. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  18. 18.
    Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 247–262. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  19. 19.
    Bingham, J.D., Hu, A.J.: Empirically efficient verification for a class of infinite-state systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 77–92. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  20. 20.
    Lahiri, S.: Personal CommunicationGoogle Scholar
  21. 21.
    Pandav, S., Slind, K., Gopalakrishnan, G.: Mutual exclusion property verification of FLASH cache coherence protocol. Technical Report UUCS-04-010, School of Computing, University of Utah (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Sudhindra Pandav
    • 1
  • Konrad Slind
    • 1
  • Ganesh Gopalakrishnan
    • 1
  1. 1.School of ComputingUniversity of Utah 

Personalised recommendations