Nothing Special   »   [go: up one dir, main page]

skip to main content
research-article
Open access

Mechanizing the CMP Abstraction for Parameterized Verification

Published: 29 April 2024 Publication History

Abstract

Parameterized verification is a challenging problem that is known to be undecidable in the general case.  ‍is a widely-used method for parameterized verification, originally proposed by Chou, Mannava and Park in 2004. It involves abstracting the protocol to a small fixed number of nodes, and strengthening by auxiliary invariants to refine the abstraction. In most of the existing applications of CMP, the abstraction and strengthening procedures are carried out manually, which can be tedious and error-prone. Existing theoretical justification of the  ‍method is also done at a high level, without detailed descriptions of abstraction and strengthening rules. In this paper, we present a formally verified theory of  ‍in Isabelle/HOL, with detailed, syntax-directed procedure for abstraction and strengthening that is proven correct. The formalization also includes correctness of symmetry reduction and assume-guarantee reasoning. We also describe a tool AutoCMP for automatically carrying out abstraction and strengthening in, as well as generating Isabelle proof scripts showing their correctness. We applied the tool to a number of parameterized protocols, and discovered some inaccuracies in previous manual applications of  ‍to the FLASH cache coherence protocol.

References

[1]
Parosh Aziz Abdulla, A. Prasad Sistla, and Muralidhar Talupur. 2018. Model Checking Parameterized Systems. In Handbook of Model Checking. 685–725.
[2]
Krzysztof R. Apt and Dexter Kozen. 1986. Limits for Automatic Verification of Finite-State Concurrent Systems. Inform. Process. Lett., 22, 6 (1986), 307–309.
[3]
Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, and Lenore D. Zuck. 2001. Parameterized Verification with Automatically Computed Inductive Assertions. In Proc. 13th International Conference on Computer Aided Verification (CAV’01) (Lecture Notes in Computer Science, Vol. 2102). Springer, 221–234.
[4]
Jialun Cao, Yongjian Li, and Jun Pang. 2018. L-CMP: An automatic learning-based parameterized verification tool (Tool Demo). In Proc. 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE’18). ACM Press, 892–895.
[5]
J. Cao, Y. Li, and J. Pang. 2019. A learning-based framework for automatic parameterized verification. In Proc. 37th IEEE International Conference on Computer Design (ICCD’19). IEEE CS, 450–459.
[6]
Xiaofang Chen and Ganesh Gopalakrishnan. 2006. A General Compositional Approach to Verifying Hierarchical Cache Coherence Protocols. Technical Report, School of Computing, University of Utah.
[7]
Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, and Ching-Tsun Chou. 2006. Reducing Verification Complexity of a Multicore Coherence Protocol using Assume/guarantee. In Proc. 6th International Conference on Formal Methods in Computer Aided Design (FMCAD’06). IEEE Computer Society, 81–88.
[8]
Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park. 2004. A Simple Method for Parameterized Verification of Cache Coherence Protocols. In Proc. 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD’04) (Lecture Notes in Computer Science, Vol. 3312). Springer, 382–398.
[9]
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2003. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. J. ACM, 50, 5 (2003), 752–794. issn:0004-5411
[10]
Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. 2018. Handbook of Model Checking. Springer.
[11]
Ariel Cohen and Kedar S. Namjoshi. 2009. Local Proofs for Global Safety Properties. Formal Methods in System Design, 34, 2 (2009), 104–125.
[12]
Sylvain Conchon, David Declerck, and Fatiha Zaïdi. 2018. Cubicle-W: Parameterized Model Checking on Weak Memory. In Proc. 9th International Joint Conference on Automated Reasoning (IJCAR’18) (Lecture Notes in Computer Science, Vol. 10900). 152–160.
[13]
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, and Fatiha Zaïdi. 2012. Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. In Proc. 24th International Conference on Computer Aided Verification (CAV’12) (Lecture Notes in Computer Science, Vol. 7358). Springer, 718–724.
[14]
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, and Fatiha Zaïdi. 2013. Invariants for Finite Instances and Beyond. In Proc. 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD’13). IEEE Computer Society, 61–68.
[15]
David L. Dill. 1996. The Murphi Verification System. In Proc. 8th International Conference on Computer Aided Verification (CAV’96) (Lecture Notes in Computer Science, Vol. 1102). Springer, 390–393.
[16]
Michael Emmi, Rupak Majumdar, and Roman Manevich. 2010. Parameterized Verification of Transactional Memories. In Proc. 31th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’10). ACM Press, 134–145.
[17]
Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. 2013. A Fully Verified Executable LTL Model Checker. In Proc. 25th International Conference on Computer Aided Verification (CAV’13) (Lecture Notes in Computer Science, Vol. 8044). Springer, 463–478.
[18]
Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski. 2017. Thread Modularity at Many Levels: A Pearl in Compositional Verification. In Proc. 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17). ACM Press, 473–485.
[19]
Peter Huber, Arne M. Jensen, Leif O. Jepsen, and Kurt Jensen. 1984. Towards Reachability Trees for High-level Petri Nets. In Proc. 6th European Workshop on Applications and Theory in Petri Nets (Lecture Notes in Computer Science, Vol. 188). Springer, 215–233.
[20]
C. Norris Ip and David L. Dill. 1993. Efficient Verification of Symmetric Concurrent Systems. In Proc. International Conference on Computer Design (ICCD’93). IEEE Computer Soceity, 230–234.
[21]
C. Norris Ip and David L. Dill. 1996. Better Verification through Symmetry. Formal Methods in System Design, 9, 1/2 (1996), 41–75.
[22]
Sava Krstic. 2005. Parameterized System Verification with Guard Strengthening and Parameter Abstraction. Proc. 4th Workshop on Automated Verification of Infinite State Systems (AVIS’05).
[23]
Shuvendu K. Lahiri and Randal E. Bryant. 2004. Constructing Quantified Invariants via Predicate Abstraction. In Proc. 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’04) (Lecture Notes in Computer Science, Vol. 2937). Springer, 267–281.
[24]
Yongjian Li, Kaiqiang Duan, Yi Lv, Jun Pang, and Shaowei Cai. 2016. A Novel Approach to Parameterized Verification of Cache Coherence Protocols. In Proc. 34th IEEE International Conference on Computer Design (ICCD’16). IEEE Computer Society, 560–567.
[25]
Yongjian Li and Zimin Li. 2022. ILCMP source code. https://gitee.com/dust_capacity_i/ILCMP.git
[26]
Yongjian Li, Zimin Li, Bohua Zhan, and Jun Pang. 2023. autoCMP. https://github.com/forSubmission238/autoCMP
[27]
Kenneth L. McMillan. 1999. Verification of Infinite State Systems by Compositional Model Checking. In Proc. 10th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’99) (Lecture Notes in Computer Science, Vol. 1703). Springer, 219–234.
[28]
Kenneth L. McMillan. 2001. Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. In Proc. 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’01) (Lecture Notes in Computer Science, Vol. 2144). Springer, 179–195.
[29]
Kenneth L. McMillan. 2008. Quantified Invariant Generation using An Interpolating Saturation Prover. In Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08) (Lecture Notes in Computer Science, Vol. 4963). Springer, 413–427.
[30]
Kenneth L. McMillan. 2016. Modular Specification and Verification of a Cache-coherent Interface. In Proc. 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD’16). IEEE, 109–116.
[31]
Kenneth L. McMillan. 2018. Eager Abstraction for Symbolic Model Checking. In Proc. 30th International Conference on Computer Aided Verification (CAV’18) (Lecture Notes in Computer Science, Vol. 10981). Springer, 191–208.
[32]
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL - A Proof Assistant for Higher-Order Logic (Lecture Notes in Computer Science, Vol. 2283). Springer.
[33]
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: Safety Verification by Interactive Generalization. In Proc. 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’18). ACM Press, 614–630.
[34]
Sudhindra Pandav, Konrad Slind, and Ganesh Gopalakrishnan. 2005. Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification. In Proc. 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’05) (Lecture Notes in Computer Science, Vol. 3725). Springer, 317–331.
[35]
Seungjoon Park and David L Dill. 1996. Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. In Proc. 8th ACM Symposium on Parallel Algorithms and Architectures (SPAA’96). ACM, 288–296.
[36]
Amir Pnueli, Sitvanit Ruah, and Lenore D. Zuck. 2001. Automatic Deductive Verification with Invisible Invariants. In Proc. 7th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01) (Lecture Notes in Computer Science, Vol. 2031). Springer, 82–97.
[37]
Amir Pnueli and Elad Shahar. 1996. A Platform for Combining Deductive with Algorithmic Verification. In Proc. 8th International Conference on Computer Aided Verification (CAV’96) (Lecture Notes in Computer Science, Vol. 1102). Springer, 184–195.
[38]
Peter H Starke. 1991. Reachability analysis of Petri Nets using Symmetries. Systems Analysis Modelling Simulation, 8, 4-5 (1991), 293–303.
[39]
Murali Talupur and Mark R. Tuttle. 2008. Going with the Flow: Parameterized Verification using Message Flows. In Proc. 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD’08). IEEE Computer Society, 1–8.
[40]
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. 2018. Modularity for Decidability of Deductive Verification with Applications to Distributed Systems. In Proc. 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’18). ACM Press, 662–677.
[41]
Ashish Tiwari, Harald Rueß, Hassen Saïdi, and Natarajan Shankar. 2001. A Technique for Invariant Generation. In Proc. 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01) (Lecture Notes in Computer Science, Vol. 2031). Springer, 113–127.
[42]
Pierre Wolper. 1986. Expressing Interesting Properties of Programs in Propositional Temporal Logic. In Proc. 13th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’86). ACM Press, 184–193.
[43]
Pierre Wolper and Vinciane Lovinfosse. 1989. Verifying Properties of Large Sets of Processes with Network Invariants. In Proc. 1st International Conference on Computer Aided Verification (CAV’89) (Lecture Notes in Computer Science, Vol. 407). Springer, 60–80.

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages  Volume 8, Issue OOPSLA1
April 2024
1492 pages
EISSN:2475-1421
DOI:10.1145/3554316
Issue’s Table of Contents
This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 April 2024
Published in PACMPL Volume 8, Issue OOPSLA1

Permissions

Request permissions for this article.

Check for updates

Badges

Author Tags

  1. Isabelle/HOL
  2. Parameterized verification
  3. cache coherence protocols
  4. invariants
  5. model checking
  6. theorem proving

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • 0
    Total Citations
  • 136
    Total Downloads
  • Downloads (Last 12 months)136
  • Downloads (Last 6 weeks)36
Reflects downloads up to 14 Nov 2024

Other Metrics

Citations

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media