[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

An integrated specification and verification technique for highly concurrent data structures

  • TACAS 2013
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

A Correction to this article was published on 31 May 2021

This article has been updated

Abstract

We present a technique for automatically verifying safety properties of concurrent programs, in particular programs that rely on subtle dependencies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded number of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state automata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verification, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have implemented our method and used it to verify programs, some of which have not been verified by any other automatic method before.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14

Similar content being viewed by others

Change history

Notes

  1. When the observers in Figs. 6, 7, 8, 10 and 9 are used to specify a stack (respectively, a queue), each occurrence of in(.) should be replaced by push(.) (respectively, enq(.)) and each occurrence of out(.) should be replaced by pop(.) (respectively, deq(.))

References

  1. Abdulla, P., Jonsson, B., Nilsson, M., d’Orso, J., Saksena, M.: Regular model checking for LTL(MSO). STTT 14(2), 223–241 (2012)

    Article  Google Scholar 

  2. Abdulla, P.A., Haziza, F., Holík, L.: All for the price of few. In: VMCAI, pp. 476–495. Springer, Berlin (2013)

  3. Abdulla, P.A., Haziza, F., Holík, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In: TACAS, vol. 7795, LNCS, pp. 324–338. Springer, Berlin (2013)

  4. Amit, D., Rinetzky, N., Reps, T., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Proc. of CAV’07. LNCS, vol. 4590, pp. 477–490. Springer, Berlin (2007)

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

  6. Bingham, J., Rakamaric, Z.: A logic and decision procedure for predicate abstraction of heap-manipulating programs. In: Proc. of VMCAI’06. LNCS, vol. 3855, pp. 207–221. Springer, Berlin (2006)

  7. Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: Proceedings of PLDI’10, pp. 330–340. ACM, New York (2010)

  8. Cerný, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model checking of linearizability of concurrent list implementations. In: Proc. of CAV’10, LNCS, vol. 6174, pp. 465–479. Springer, Berlin (2010)

  9. Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set algorithm. In: Proceedings of CAV’06. LNCS, vol. 4144, pp. 475–488. Springer, Berlin (2006)

  10. Dill, D.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite-State Systems, vol. 407. LNCS. Springer, Berlin (1989)

  11. Doherty, S., Detlefs, D., Groves, L., Flood, C., Luchangco, V., Martin, P., Moir, M., Shavit, N., Jr. G.S.: Dcas is not a silver bullet for nonblocking algorithm design. In: Proceedings of SPAA’04, pp. 216–224. ACM, New York (2004)

  12. Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: Proceedings of FORTE’04. LNCS, vol. 3235, pp. 97–114. Springer, Berlin (2004)

  13. Elmas, T., Qadeer, S., Sezgin, A., Subasi, O., Tasiran, S.: Simplifying linearizability proofs with reduction and abstraction. In: Proceedings of TACAS’10, vol. 6015. LNCS, pp. 296–311. Springer, Berlin (2010)

  14. Emmi, M., Jhala, R., Kohler, E., Majumdar, R.: Verifying reference counting implementations. In: Proceedings of TACAS’09. LNCS, vol. 5505, pp. 352–367. Springer, Berlin (2009)

  15. Flanagan, C., Freund, S.: Atomizer: a dynamic atomicity checker for multithreaded programs. Sci. Comput. Program. 71(2), 89–109 (2008)

    Article  MathSciNet  Google Scholar 

  16. Habermehl, P., Holík, L., Rogalewicz, A., Šimáček, J., Vojnar, T.: Forest automata for verification of heap manipulation. In: Formal Methods in System Design, pp. 1–24 (2012)

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

    Article  Google Scholar 

  18. IBM. System/370 principles of operation (1983)

  19. Kidd, N., Reps, T., Dolby, J., Vaziri, M.: Finding concurrency-related bugs using random isolation. STTT 13(6), 495–518 (2011)

    Article  Google Scholar 

  20. Michael, M., Scott, M.: Correction of a memory management method for lock-free data structures. Technical Report TR599, University of Rochester, Rochester (1995)

  21. Michael, M., Scott, M.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of 15th ACM Symposium on Principles of Distributed Computing, pp. 267–275 (1996)

  22. Michael, M.M.: Safe memory reclamation for dynamic lock-free objects using atomic reads and writes. In: Proceedings of the Twenty-First Annual Symposium on Principles of Distributed Computing, PODC ’02, pp. 21–30. ACM, New York (2002)

  23. Naik, M., Aiken, A., Whaley, J.: Effective static race detection for java. In: Proceedings of PLDI’06, pp. 308–319. ACM, New York (2006)

  24. Naik, M., Park, C.-S., Sen, K., Gay, D.: Effective static deadlock detection. In: Proceedings of ICSE, pp. 386–396. IEEE, New York (2009)

  25. Segalov, M., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.: Abstract transformers for thread correlation analysis. In: APLAS, LNCS, pp. 30–46. Springer, Berlin (2009)

  26. Shacham, O.: Verifying atomicity of composed concurrent operations. PhD thesis, Department of Computer Science, Tel Aviv University (2012)

  27. Treiber, R.: Systems programming: coping with parallelism. Technical Report RJ5118, IBM Almaden Res. Ctr. (1986)

  28. Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Proceedings of VMCAI, vol. 5403. LNCS, pp. 335–348. Springer, Berlin (2009)

  29. Vafeiadis, V.: Automatically proving linearizability. In: CAV, vol. 6174. Lecture Notes in Computer Science, pp. 450–464. Springer, Berlin (2010)

  30. Vafeiadis, V.: Rgsep action inference. In: Proceedings of VMCAI’10, vol. 5944. LNCS, pp. 345–361. Springer, Berlin (2010)

  31. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of LICS’86, pp. 332–344 (1986)

  32. Vechev, M., Yahav, E.: Deriving linearizable fine-grained concurrent objects. In: Proceedings of PLDI’08, pp. 125–135. ACM, New York (2008)

  33. Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: Proceedings of SPIN’09, vol. 5578. LNCS, pp. 261–278. Springer, Berlin (2009)

  34. Wang, L., Stoller, S.: Static analysis of atomicity for programs with non-blocking synchronization. In: Proceedings of PPOPP’05, pp. 61–71. ACM, New York (2005)

  35. Wolper, P.: Expressing interesting properties of programs in propositional temporal logic (extended abstract). In: Proceedings of POPL’86, pp. 184–193 (1986)

  36. Yahav, E., Sagiv, S.: Automatically verifying concurrent queue algorithms. Electr. Notes Theor. Comput. Sci. 89(3) (2003)

Download references

Author information

Authors and Affiliations

  1. Uppsala University, Uppsala, Sweden

    Parosh Aziz Abdulla, Frédéric Haziza, Lukáš Holík & Bengt Jonsson

  2. Brno University of Technology, Brno, Czech Republic

    Lukáš Holík

  3. Linköping University, Linköping, Sweden

    Ahmed Rezine

Authors
  1. Parosh Aziz Abdulla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frédéric Haziza
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lukáš Holík
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Bengt Jonsson
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Ahmed Rezine
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ahmed Rezine.

Additional information

F. Haziza and L. Holik were in part supported by the Uppsala Programming for Multicore Architectures Research Center (UPMARC). L. Holik was in part supported by the Czech Science Foundation (project 13-37876P), the internal projects of Brno University of Technology FIT-S-12-1 and FIT-S-14-2486. A. Rezine was in part supported by the CENIIT research organization at Linköping (project 12.04).

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Abdulla, P.A., Haziza, F., Holík, L. et al. An integrated specification and verification technique for highly concurrent data structures. Int J Softw Tools Technol Transfer 19, 549–563 (2017). https://doi.org/10.1007/s10009-016-0415-4

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-016-0415-4

Keywords

Search

Navigation