Parameterized verification of systems with component identities, using view abstraction
Author: 
Gavin LoweAuthors Info & Claims
Pages 287 - 324
Abstract
The parameterized verification problem seeks to verify all members of some collection of systems. We consider the parameterized verification problem applied to systems that are composed of an arbitrary number of component processes, together with some fixed processes. The components are taken from one or more families, each family representing one role in the system; all components within a family are symmetric to one another. Processes communicate via synchronous message passing. In particular, each component process has an identity, which may be included in messages, and passed to third parties. We extend Abdulla et al.’s technique of view abstraction, together with techniques based on symmetry reduction, to this setting. We give an algorithm and implementation that allows such systems to be verified for an arbitrary number of components: we do this for both safety and deadlock-freedom properties. We apply the techniques to a number of examples. We can model both active components, such as threads, and passive components, such as nodes in a linked list: thus our approach allows the verification of unbounded concurrent datatypes operated on by an unbounded number of threads. We show how to combine view abstraction with additional techniques in order to deal with other potentially infinite aspects of the analysis: for example, we deal with potentially infinite specifications, such as a datatype being a queue; and we deal with unbounded types of data stored in a datatype.
References
[1]
Abdulla, P., Jonsson, B., Nilsson, M., d’Orso J.: Regular model checking made simple and efficient. In: Proceedings of CONCUR’02, 13th International Conference on Concurrency Theory, Volume 2421 of LNCS, pp. 116–130 (2002)
[2]
Abdulla, P., Jonsson, B., Nilsson, M., Saksena M.: A survey of regular model checking. In: Proceedings of Concur, volume 3170 of LNCS, pp. 35–48 (2004)
[3]
Abdulla, P., Jonsson, B., Nilsson, M., Saksena M.: General decidability theorems for infinite-state systems. In: Proceedings of the Symposium on Logic in Computer Science, pp. 313–321, 08 (1996)
[4]
Abdulla Parosh, Haziza Frédéric, and Holík Lukáš Parameterized verification through view abstraction Int. J. Softw. Tools Technol. Transfer 2016 18 495-516
[5]
Abdulla, P.A., Jonsson, B., Trinh, C.Q.: Automated verification of linearization policies. In: Proceedings of SAS 2016, volume 9837 of LNCS, pp. 61–83. Springer (2016)
[6]
Abdulla, P.A., Jonsson, B., Trinh, C.Q.: Fragment abstraction for concurrent shape analysis. In: Proceedings of ESOP 2018, volume 10801 of LNCS, pp. 442–471. Springer (2018)
[7]
Abdullah Parosh, Haziza Frédéric, Holík Lukáš, Jonsson Bengt, and Rezine Ahmed An integrated specification and verification technique for highly concurrent data structures Int. J. Softw. Tools Technol. Transfer 2017 19 549-563
[8]
Amit, D., Rinetzky, N., Reps, T., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Computer Aided Verification, volume 4590 of LNCS, pp. 477–490. Springer (2007)
[9]
Apt KR and Kozen DC Limits for automatic verification of finite-state concurrent systems Inf. Process. Lett. 1986 22 6 307-309
[10]
Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.: Thread quantification for concurrent shape analysis. In: Proceedings of CAV 2008, volume 5123 of LNCS, pp. 399–413. Springer (2008)
[11]
Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously. In: Proceedings of TACAS 2016, volume 9636 of LNCS, pp. 480–496 (2016)
[12]
Bouajjani A, Emmi M, Enea C, and Hamza J On reducing linearizability to state reachability Inf. Comput. 2018 261 383-400
[13]
Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Proceedings of International Conference on Computer Aided Verification, volume 3114 of LNCS, pp. 372–386, (2004)
[14]
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Proceedings of the 12th International Conference on Computer Aided Verification, volume 1855 of LNCS, pp. 403–418 (2000)
[15]
Bošnački Dragan, Dams Dennis, and Holenderski Leszek Symmetric Spin Int. J. Softw. Tools Technol. Transfer 2002 4 92-106
[16]
Chakraborty, S., Henzinger, T.A., Sezgin, A., Sezgin, V.: Vafeiadis. Aspect-oriented linearizability proofs. Log. Methods Computer Sci. 11(1), (2015)
[17]
Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Proceedings of the 10th International Conference on Computer-Aided Verification (CAV ’98), pp. 147–158 (1998)
[18]
Clarke EM, Enders R, Filkorn T, and Jha S Exploiting symmetry in temporal logic model checking Formal Methods Syst. Des. 1996 9 77-104
[19]
Clarke, E. M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: Proceedings of the 6th Annual Association for Computing Machinery Symposium on Principles of Distributed Computing, pp. 294–303 (1987)
[20]
Dams D, Lakhnech Y, and Steffen M Iterating transducers J. Logic Algeb. Program. 2002 52–53 109-127
[21]
Delzanno, G., Raskin, J.-F., Van Begin, L.: Attacking symbolic state explosion. In: Computer Aided Verification, pp. 298–310 (2001)
[22]
Dodds, M., Haas, A., Kirsch, C.: A scalable, correct time-stamped stack. In: Proceedings of POPL 2015, pp. 233–246. ACM (2015)
[23]
Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the Symposium on Principles of Programming Languages (POPL ’95) (1995)
[24]
Emerson EA and Sistla AP Symmetry and model checking Formal Methods Syst. Des. 1996 9 105-131
[25]
Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P., Niksic F.: An SMT-based approach to coverability analysis. In: Proceedings of CAV 2014, volume 8559 of LNCS, pp. 603–619 (2014)
[26]
Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Proceedings of SPIN 2003, volume 2648 of LNCS, pp. 213–224 (2003)
[27]
German SM and Sistla AP Reasoning about systems with many processes J. ACM 1992 39 3 675-735
[28]
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol. Transf. (2015)
[29]
Gibson-Robinson Thomas and Lowe Gavin Symmetry reduction in CSP model checking Softw. Tools Technol. Transf. 2019 21 567-605
[30]
Goldsmith, M., Moffat, N., Roscoe, B., Whitworth, T., Zakiuddin, I.: Watchdog transformations for property-oriented model checking. In: Proceedings of Formal Methods Europe (FME 2003), volume 2805 of LNCS, pp. 600–616 (2003)
[31]
Haziza, F., Holík, L., Meyer, R., Wolff, S.: Pointer race freedom. In Jobstmann, V., Rustan, K., Leino, M. (eds.), Verification, Model Checking, and Abstract Interpretation, pp. 393–412 (2016)
[32]
Hendler, D., Shavit, N., Yerushalmi L.: A scalable lock-free stack algorithm. In: Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures, pp. 206–215 (2004)
[33]
Henzinger, T.A., Sezgin, A., Vafeiadis V.: Aspect-oriented linearization proofs. In: Proceedings of CONCUR 2013, volume 8052 of LNCS, pp. 242–256. Springer (2013)
[34]
Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann (2012)
[35]
Herlihy M and Wing JM Linearizability: a correctness condition for concurrent objects ACM Trans. Program. Lang. Syst. 1990 12 3 463-492
[36]
Holík, L., Tomáš, V., Roland Meyer, A., Sebastian, W.: Effect summaries for thread-modular analysis. In: Proceedings of SAS 2017, volume 10422 of LNCS, pp. 169–191. Springer (2017)
[37]
Ip CN and Dill DL Better verification through symmetry Formal Methods Syst. Des. 1996 9 41-75
[38]
Kaiser A, Kroening D, and Wahl T A widening approach to multithreaded program verification ACM Trans. Program. Lang. Syst. 2014 36 4 1-29
[39]
Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar E.: Symbolic model checking with rich assertional languages. Theoretical Computer Science, pp. 93–112 (2001)
[40]
Lowe, G.: View abstraction for systems with component identities. In: Proceedings of the International Symposium on Formal Methods (FM 2018), volume 10951 of LNCS, pp. 502–522. Springer (2018)
[41]
Lowe G Discovering and correcting a deadlock in a channel implementation Formal Aspects Comput. 2019 31 411-419
[42]
Lubachevsky B An approach to automating the verification of compact parallel coordination programs Acta Informatica 1984 21 2 125-169
[43]
Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Proceedings of VMCAI 2005, volume 3385 of LNCS, pp. 181–198. Springer (2005)
[44]
Mazur T and Lowe G CSP-based counter abstraction for systems with node identifiers Sci. Comput. Program. 2014 81 3-52
[45]
Meyer, R., Sebastian, W.: Decoupling lock-free data structures from memory reclamation for static analysis. In: Proceedings of the ACM on Programming Languages, 3(POPL) (2019)
[46]
Michael, M., Michael, S.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, pp. 267–275 (1996)
[47]
Moffat, N., Goldsmith, M., Roscoe. B.: A representative function approach to symmetry exploitation for csp refinement checking. In: Liu, S., Maibaum, T., Araki, K. (eds.), Formal Methods and Software Engineering, pp. 258–277, Berlin, Heidelberg (2008)
[48]
Oracle. LockSupport (Java SE9 & JDK 9). https://docs.oracle.com/javase/9/docs/api/java/util/concurrent/locks/LockSupport.html
[49]
Pnueli, A., Xu, J., Zuck L.D.: Liveness with (0, 1, )-counter abstraction. In: CAV’02: Proceedings of the 14th International Conference on Computer Aided Verification, pp. 107–122 (2002)
[50]
Roscoe, A.W.: Understanding Concurrent Systems. Springer (2010)
[51]
Roscoe, A.W., Creese, S.J.: Data independent induction over structured networks. In: Proceedings of PDPTA2000 (2000)
[52]
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. Trans. Program. Lang. Syst. (2002)
[53]
Sistla AP, Gyuris V, and Emerson EA SMC: A symmetry-based model checker for verification of safety and linveness properties ACM Trans. Softw. Eng. Methodol. 2000 9 2 133-166
[54]
Sufrin, B.: Communicating Scala Objects. In: Proceedings of Communicating Process Architectures (CPA) (2008)
[55]
Touili, T.: Regular model checking using widening techniques. In: Electronic Notes in Theoretical Computer Science, 50(4), Proceedings of VEPAS’01 (2001)
[56]
Treiber, R.K.: Systems programming: Coping with parallelism. Technical Report RJ 5118, IBM (1986)
[57]
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of LICS’86, pp. 332–344 (1986)
[58]
Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Proceedings of 10th International Conference on Computer Aided Verification, volume 1427 of LNCS (1998)
[59]
Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pp. 68–80 (1989)
[60]
Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: Thirteenth Annual ACM Symposium on Principles of Programming Languages, pp. 184–193 (1986)
Recommendations
Parameterized verification of transactional memories
PLDI '10We describe an automatic verification method to check whether transactional memories ensure strict serializability a key property assumed of the transactional interface. Our main contribution is a technique for effectively verifying parameterized ...
Parameterized verification through view abstraction
We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to ...
Monotonic Abstraction in Parameterized Verification
We present a tutorial on verification of safety properties for parameterized systems. Such a system consists of an arbitrary number of processes which are organized in a linear array. The aim is to prove correctness of the system regardless of the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© The Author(s) 2022.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 April 2022
Accepted: 13 January 2022
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 12 Nov 2024
Other Metrics
Citations
View Options
View options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in