Top

International Journal on Software Tools for Technology Transfer

Published in:

01-08-2016 | SPIN 2013

Model checking unbounded concurrent lists

Authors: Divjyot Sethi, Muralidhar Talupur, Sharad Malik

Published in: International Journal on Software Tools for Technology Transfer | Issue 4/2016

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We present a model checking-based method for verifying list-based concurrent set data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received significant attention from the verification community. These data structures are unbounded in two dimensions: the list size is unbounded and an unbounded number of threads access them. Thus, their model checking requires abstraction to a model bounded in both the dimensions. We first show how the unbounded number of threads can be model checked by reduction to a finite model, while assuming a bounded number of list nodes. In particular, we leverage the CMP (CoMPositional) method which abstracts the unbounded threads by keeping one thread as is (concrete) and abstracting all the other threads to a single environment thread. Next, the method proceeds as a series of iterations where in each iteration the abstraction is model checked and, if a spurious counterexample is observed, refined. This is accomplished by the user by inspecting the returned counterexamples. If the user determines the returned counterexample to be spurious, she adds constraints to the abstraction in the form of lemmas to refine it. Upon addition, these lemmas are also verified for correctness as part of the CMP method. Thus, since these lemmas are verified as well, we show how some of the lemmas required for refinement of this abstract model can be mined automatically using an assertion mining tool, Daikon. Next, we show how the CMP method approach can be extended to the list dimension as well, to fully verify the data structures in both the dimensions. While it is possible to show correctness of these data structures for an unbounded number of threads by keeping one concrete thread and abstracting others, this is not directly possible in the list dimension as the nodes pointed to by the threads change during list traversal. Our method addresses this challenge by constructing an abstraction for which the concrete nodes, i.e., the nodes pointed to by the threads, can change as the thread pointers move with program execution. Further, our method also allows for refinement of this abstraction to prove properties of interest. We show the soundness of our method and establish its utility by model checking challenging concurrent list-based data structure examples.

previous article Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic

next article Verifying a quantitative relaxation of linearizability via refinement

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Available only for authorised users

Note that the threads are symmetric in the sense that they run identical code. However, at runtime, individual threads may be in different states due to non-deterministic thread interleaving order.

In general, the abstractions are commutative. However, they are presented in the order of the thread abstraction first and then the list abstraction.

While this set of local fields is \(NULL\) for the Fine-grained list-based set data structure used as a running example, it is not \(NULL\) for other data structures verified in this paper.

This includes synchronization mechanisms; i.e., updates to the \(lock\) field.

Nodes which become a part of \(\widehat{nd}\) can, in practice, never become reachable from any thread pointer again. This is true for the list-based concurrent set data structures we have seen in [11] and is discussed in the “Appendix A.2”.

While we believe that the refinement approach presented in this paper is sound for any generic thread abstraction, its soundness is shown by assuming the data-type reduction abstraction in the thread dimension, for simplicity.

The refinement lemma is not explicitly added to assignKeys’; it is implicitly a part of Split and Join. This special treatment is given to it because, strictly speaking, it is a lemma across both, the list and the specification set \(S\).

We did some manual optimizations for the Optimistic algorithm to reduce the maximum number of list nodes in the abstraction, to reduce the runtime.

Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.: Thread quantification for concurrent shape analysis. In: Proceedings of CAV ’08, pp. 399–413. Springer, Berlin (2008)

Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’10, pp. 330–340. ACM, New York, NY, USA (2010)

Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Static Analysis, pp. 233–248. Springer, Berlin, Heidelberg (2007)

Cerný, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model checking of linearizability of concurrent list implementations. In: Proceedings of Computer Aided Verification, pp. 465–479 (2010)

Chou, C.T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Proceedings of FMCAD (2004)

Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set algorithm. In: Computer Aided Verification, pp. 475–488. Springer, Berlin, Heidelberg (2006)

Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Computer Aided Verification. pp. 160–171. Springer, Berlin, Heidelberg (1999)

Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: Proceedings of the 24th European Conference on Object-Oriented Programming. ECOOP’10, pp. 504–528. Springer, Berlin (2010)

Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Progr. 69(1–3), 35–45 (2007)MathSciNetCrossRefMATH

10.

Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. SIGPLAN Not. 42(6), 266–277 (2007)CrossRef

11.

Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco (2008)

12.

Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12, 463–492 (1990)CrossRef

13.

Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’11, pp. 271–282. ACM, New York (2011)

14.

Kristic, S.: Parameterized system verification with guard strengthening and parameter abstraction. In: Proceedings of 4th International Workshop on Automatic Verification of Finite State Systems (2005)

15.

Lahiri, S.K., Bryant, R.E.: Predicate abstraction with indexed predicates. ACM Trans. Comput. Logic (TOCL) 9(1) (2007)

16.

Lea, D.: The java.util.concurrent synchronizer framework. Sci. Comput. Program. 58, 293–309 (2005). http://dl.acm.org/citation.cfm?id=1127037.1127039

17.

Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model checking linearizability via refinement. In: Proceedings of FM ’09, pp. 321–337. Springer, Berlin (2009)

18.

McMillan, K.L.: Verification of infinite state systems by compositional model checking. In: Proceedings of CHARME ’99, pp. 219–234. Springer, London (1999)

19.

Michael, M.M., Scott, M.L.: Correction of a memory management method for lock-free data structures. No. TR-599. University of Rochester, Computer Science Department (1995)

20.

Noll, T., Rieger, S.: Verifying dynamic pointer-manipulating threads. In: Proceedings of the 15th International Symposium on Formal Methods, FM ’08, pp. 84–99. Springer, Berlin (2008)

21.

O’Leary, J., Talupur, M., Tuttle, M.: Protocol verification using flows: An industrial experience. In: Proeedings of Formal Methods in Computer-Aided Design, FMCAD 2009, pp. 172–179 (2009)

22.

Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants, TACAS 2001, pp. 82–97. Springer, London (2001)

23.

Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0, 1, infty)-counter abstraction. In: Proceedings of the 14th International Conference on Computer Aided Verification, CAV ’02, pp. 107–122. Springer London (2002)

24.

Reinders, J.: Intel Threading Building Blocks, 1st edn. O’Reilly & Associates Inc, Sebastopol (2007)

25.

Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’99, pp. 105–118. ACM, New York (1999)

26.

Sethi, D., Talupur, M., Schwartz-Narbonne, D., Malik, S.: Parameterized model checking of fine grained concurrency. In: Proceedings of 19th International SPIN Workshop on Model Checking of Software (2012)

27.

Talupur, M., Tuttle, M.: Going with the flow: Parameterized verification using message flows. In: Proceedings of Formal Methods in Computer-Aided Design, FMCAD ’08, pp. 1–8 (2008)

28.

Vafeiadis, V.: Shape-value abstraction for verifying linearizability, VMCAI ’09, pp. 335–348. Springer, Berlin (2009)

29.

Vafeiadis, V.: Automatically proving linearizability. In: Proceedings of Computer Aided Verification, pp. 450–464 (2010)

30.

Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: Proceedings of PPoPP ’06, pp. 129–136. ACM, New York (2006)

31.

Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: Proceedings of the 16th International SPIN Workshop on Model Checking Software, pp. 261–278. Springer, Berlin (2009)

32.

Yahav, E.: Verifying safety properties of concurrent java programs using 3-valued logic. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’01, pp. 27–40. ACM, New York (2001)

33.

Zhang, S.J.: Scalable automatic linearizability checking. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE ’11, pp. 1185–1187. ACM, New York (2011)

34.

Zhang, S.J., Liu, Y.: Model checking a lazy concurrent list-based set algorithm. In: Proceedings of the 2010 Fourth International Conference on Secure Software Integration and Reliability Improvement, SSIRI ’10, pp. 43–52. IEEE Computer Society, Washington DC (2010)

Title: Model checking unbounded concurrent lists
Authors: Divjyot Sethi
Muralidhar Talupur
Sharad Malik
Publication date: 01-08-2016
Publisher: Springer Berlin Heidelberg
Published in: International Journal on Software Tools for Technology Transfer / Issue 4/2016
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-015-0369-y

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 4/2016

Preface of the special issue on Model Checking of Software

Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic

Guard-based partial-order reduction

Efficient model-checking of weighted CTL with upper-bound constraints

Guided search for hybrid systems based on coarse-grained space abstractions

Verifying a quantitative relaxation of linearizability via refinement

Premium Partner