Skip to main content
SpringerLink
Log in
Book cover

Concurrency, Security, and Puzzles pp 162–184Cite as

Analysing Lock-Free Linearizable Datatypes Using CSP

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10160))

Abstract

We consider how we can use the process algebra CSP and the model checker FDR in order to obtain assurance about the correctness of concurrent datatypes. In particular, we perform a formal analysis of a concurrent queue based on a linked list of nodes. We model the queue in CSP and analyse it using FDR. We capture two important properties using CSP, namely linearizability and lock-freedom.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    http://docs.oracle.com/javase/7/docs/api/java/util/concurrent/atomic/AtomicReference.html.

  2. 2.

    The Scala code ignores the possibility of new nodes not being available, but we will need to consider this possibility in our CSP models.

  3. 3.

    The CSP script is available from http://www.cs.ox.ac.uk/people/gavin.lowe/LockFreeQueue/LockFreeQueueLin.csp.

References

  1. Alur, R., McMillan, K., Peled, D.: Model-checking of correctness conditions for concurrent objects. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS 1996 (1996)

    Google Scholar 

  2. 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 2010), pp. 330–340 (2010)

    Google Scholar 

  3. Černý, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model checking of linearizability of concurrent list implementations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 465–479. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_41

    Chapter  Google Scholar 

  4. Chen, K.: Analysing concurrent datatypes in CSP. Master’s thesis. University of Oxford (2015)

    Google Scholar 

  5. Colvin, R., Dohery, S., Groves, L.: Verifying concurrent data structures by simulation. Electron. Notes Theor. Comput. Sci. 137, 93–110 (2005)

    Article  MATH  Google Scholar 

  6. Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanically verified proof obligations for linearizability. ACM Trans. Programm. Lang. Syst. 33(1), 4:1–4:43 (2011)

    Article  Google Scholar 

  7. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: Failures Divergences Refinement (FDR) Version 3 (2013)

    Google Scholar 

  8. Gibson-Robinson, T., Lowe, G.: Symmetry reduction in CSP model checking. Submitted for publication (2016)

    Google Scholar 

  9. Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming, 1st edn. Morgan Kaufmann, San Francisco (2012)

    Google Scholar 

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

    Article  Google Scholar 

  11. Janssen, R.: Verification of concurrent datatypes using CSP. Master’s thesis. University of Oxford (2015)

    Google Scholar 

  12. Liu, Y., Chen, W., Liu, Y.A., Sun, J., Zhang, S.J., Dong, J.S.: Verifying linearizability via optimized refinement checking. IEEE Trans. Softw. Eng. 39(7), 1018–1039 (2013)

    Article  Google Scholar 

  13. Lowe, G.: Implementing generalised alt – a case study in validated design using CSP. In: Communicating Process Architectures, pp. 1–34 (2011)

    Google Scholar 

  14. Mazur, T., Lowe, G.: Counter abstraction in the CSP/FDR setting. In: Proceedings of the Seventh International Workshop on Automated Verification of Critical Systems (AVoCS 2007). Electronic Notes on Theoretical Computer Science, vol. 250, pp. 171–186 (2007)

    Google Scholar 

  15. Mazur, T., Lowe, G.: CSP-based counter abstraction for systems with node identifiers. Sci. Comput. Program. 81, 3–52 (2014)

    Article  Google Scholar 

  16. Michael, M., Scott, M.: 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)

    Google Scholar 

  17. Michael, M.M.: Safe memory reclamation for dynamic lock-free objects using atomic reads and writes. In: Proceedings of Principles of Distributed Computing (PODC 2002) (2002)

    Google Scholar 

  18. Pnueli, A., Jessie, X., Zuck, L.D.: Liveness with (0, 1, \(\infty \))-counter abstraction. In: Proceedings of the 14th International Conference on Computer Aided Verification (CAV 2002), pp. 107–122 (2002)

    Google Scholar 

  19. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River (1998)

    Google Scholar 

  20. Roscoe, A.W.: Understanding Concurrent Systems. Springer, London (2010)

    Book  MATH  Google Scholar 

  21. Roscoe, A.W., Broadfoot, P.J.: Proving security protocols with model checkers by data independence techniques. J. Comput. Secur. 7(2,3), 147–190 (1999)

    Article  Google Scholar 

  22. Roscoe, A.W., Gibson-Robinson, T.: The relationship between CSP. FDR and Büchi automata, Draft paper (2016)

    Google Scholar 

  23. Roscoe, A.W., Hopkins, D.: SVA, a tool for analysing shared-variable programs. In: Proceedings of AVoCS 2007, pp. 177–183 (2007)

    Google Scholar 

  24. Shalev, O., Shavit, N.: Split-ordered lists: lock-free extensible hash tables. J. ACM 53(3), 379–405 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  25. Sundell, H., Tsigas, P.: Lock-free deques and doubly linked lists. J. Parallel Distrib. Comput. 68(7), 1008–1020 (2008)

    Article  MATH  Google Scholar 

  26. Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450–464. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_40

    Chapter  Google Scholar 

  27. Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: Păsăreanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 261–278. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02652-2_21

    Chapter  Google Scholar 

  28. Welch, P., Martin, J.: A CSP model for Java multithreading. In: Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems, pp. 114–122. IEEE (2000)

    Google Scholar 

Download references

Acknowledgements

This work has benefited from my working with Bill Roscoe for over 25 years. It would have been impossible without his contributions to CSP and FDR. Many of the techniques used in this paper are based on his ideas.

I would like to thank Tom Gibson-Robinson for useful discussions on this work, in particular concerning our joint work on adding symmetry reduction to FDR, and for producing the CSP model that allowed comparison with the work of [12]. I would also like to thank Ke Chen and Ruben Janssen for more general discussions concerning CSP model checking of concurrent datatypes.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Oxford, UK

    Gavin Lowe

Authors
  1. Gavin Lowe
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gavin Lowe .

Editor information

Editors and Affiliations

  1. University of Oxford, Oxford, United Kingdom

    Thomas Gibson-Robinson

  2. University of Oxford, Oxford, United Kingdom

    Philippa Hopcroft

  3. University of Warwick, Coventry, United Kingdom

    Ranko Lazić

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Lowe, G. (2017). Analysing Lock-Free Linearizable Datatypes Using CSP. In: Gibson-Robinson, T., Hopcroft, P., Lazić, R. (eds) Concurrency, Security, and Puzzles. Lecture Notes in Computer Science(), vol 10160. Springer, Cham. https://doi.org/10.1007/978-3-319-51046-0_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-51046-0_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-51045-3

  • Online ISBN: 978-3-319-51046-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation