Skip to main content
SpringerLink
Log in

Making Linearizability Compositional for Partially Ordered Executions

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2018)

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

Included in the following conference series:

Abstract

In the interleaving model of concurrency, where events are totally ordered, linearizability is compositional: the composition of two linearizable objects is guaranteed to be linearizable. However, linearizability is not compositional when events are only partially ordered, as in the weak-memory models that describe multicore memory systems. In this paper, we present a generalisation of linearizability for concurrent objects implemented in weak-memory models. We abstract from the details of specific memory models by defining our condition using Lamport’s execution structures. We apply our condition to the C11 memory model, providing a correctness condition for C11 objects. We develop a proof method for verifying objects implemented in C11 and related models. Our method is an adaptation of simulation-based methods, but in contrast to other such methods, it does not require that the implementation totally orders its events. We apply our proof technique and show correctness of the Treiber stack that blocks on empty, annotated with C11 release-acquire synchronisation.

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

Access this chapter

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

Institutional subscriptions

Notes

  1. 1.

    Example in Fig. 2 inspired by H.-J. Boehm talk at Dagstuhl, Nov. 2017.

  2. 2.

    In retrospect, the name “causal linearizability” is more fitting to this current paper.

  3. 3.

    Note that a successful CAS operation comprises both a read and a write access to Top, but we only require release synchronisation here. The corresponding acquire synchronisation is provided via the earlier read in the same operation. This synchronisation is propagated to the CAS by sequenced-before (aka program order), which, in C11, is included in happens-before (see Sect. 6 for details).

  4. 4.

    The original presentation allows infinite execution structures but requires that be well founded.

  5. 5.

    Note that we only assume completeness for the sake of simplicity here.

  6. 6.

    Thus, each low-level event can linearize at most one action of the specification.

References

  1. Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. Acta Inform. 54(8), 789–818 (2017)

    Article  MathSciNet  Google Scholar 

  2. Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: Context-bounded analysis for POWER. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 56–74. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_4

    Chapter  Google Scholar 

  3. Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. IEEE Comput. 29(12), 66–76 (1996)

    Article  Google Scholar 

  4. Ahamad, M., Neiger, G., Burns, J.E., Kohli, P., Hutto, P.W.: Causal memory: definitions, implementation, and programming. Distrib. Comput. 9(1), 37–49 (1995)

    Article  MathSciNet  Google Scholar 

  5. Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1–7:74 (2014)

    Article  Google Scholar 

  6. Batty, M., Dodds, M., Gotsman, A.: Library abstraction for C/C++ concurrency. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 235–248. ACM (2013)

    Google Scholar 

  7. Batty, M., Donaldson, A.F., Wickerson, J.: Overhauling SC atomics in C11 and OpenCL. In: POPL, pp. 634–648. ACM (2016)

    Google Scholar 

  8. Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 55–66. ACM (2011)

    Google Scholar 

  9. Bouajjani, A., Emmi, M., Enea, C., Mutluergil, S.O.: Proving linearizability using forward simulations. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 542–563. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_28

    Chapter  Google Scholar 

  10. Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 87–107. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28869-2_5

    Chapter  Google Scholar 

  11. Doherty, S., Derrick, J.: Linearizability and causality. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 45–60. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41591-8_4

    Chapter  Google Scholar 

  12. Doherty, S., Derrick, J., Dongol, B., Wehrheim, H.: Causal linearizability: compositionality for partially ordered executions. CoRR abs/1802.01866 (2018)

    Google Scholar 

  13. Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97–114. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30232-2_7

    Chapter  MATH  Google Scholar 

  14. Doko, M., Vafeiadis, V.: A program logic for C11 memory fences. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 413–430. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_20

    Chapter  Google Scholar 

  15. Doko, M., Vafeiadis, V.: Tackling real-life relaxed concurrency with FSL++. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 448–475. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54434-1_17

    Chapter  Google Scholar 

  16. Dongol, B., Derrick, J.: Verifying linearisability: a comparative survey. ACM Comput. Surv. 48(2), 19:1–19:43 (2015)

    Article  Google Scholar 

  17. Dongol, B., Derrick, J., Smith, G.: Reasoning algebraically about refinement on TSO architectures. In: Ciobanu, G., Méry, D. (eds.) ICTAC 2014. LNCS, vol. 8687, pp. 151–168. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10882-7_10

    Chapter  Google Scholar 

  18. Dongol, B., Jagadeesan, R., Riely, J., Armstrong, A.: On abstraction and compositionality for weak-memory linearisability. Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 10747, pp. 183–204. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73721-8_9

    Chapter  Google Scholar 

  19. Doolan, P., Smith, G., Zhang, C., Krishnan, P.: Improving the scalability of automatic linearizability checking in SPIN. In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 105–121. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68690-5_7

    Chapter  Google Scholar 

  20. Filipovic, I., O’Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51–52), 4379–4398 (2010)

    Article  MathSciNet  Google Scholar 

  21. Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 31–45. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33651-5_3

    Chapter  Google Scholar 

  22. He, M., Vafeiadis, V., Qin, S., Ferreira, J.F.: Reasoning about fences and relaxed atomics. In: PDP, pp. 520–527. IEEE Computer Society (2016)

    Google Scholar 

  23. Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, Burlington (2008)

    Google Scholar 

  24. Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM TOPLAS 12(3), 463–492 (1990)

    Article  Google Scholar 

  25. Kaiser, J., Dang, H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic for weak memory: reasoning about release-acquire consistency in iris. In: ECOOP. LIPIcs, vol. 74, pp. 17:1–17:29. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)

    Google Scholar 

  26. Kang, J., Hur, C., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: Castagna, G., Gordon, A.D. (eds.) POPL, pp. 175–189. ACM (2017)

    Google Scholar 

  27. Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C/C++ concurrency. PACMPL 2(POPL), 17:1–17:32 (2018)

    Google Scholar 

  28. Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: Bodík, R., Majumdar, R. (eds.) POPL, pp. 649–662. ACM (2016)

    Google Scholar 

  29. Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 311–323. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-47666-6_25

    Chapter  Google Scholar 

  30. Lahav, O., Vafeiadis, V., Kang, J., Hur, C., Dreyer, D.: Repairing sequential consistency in C/C++11. In: PLDI, pp. 618–632. ACM (2017)

    Google Scholar 

  31. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979)

    Article  Google Scholar 

  32. Lamport, L.: On interprocess communication. Part I: basic formalism. Distrib. Comput. 1(2), 77–85 (1986)

    Article  MathSciNet  Google Scholar 

  33. Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model checking linearizability via refinement. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 321–337. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-05089-3_21

    Chapter  Google Scholar 

  34. Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL, pp. 378–391. ACM (2005)

    Google Scholar 

  35. Nienhuis, K., Memarian, K., Sewell, P.: An operational semantics for C/C++11 concurrency. In: Visser, E., Smaragdakis, Y. (eds.) OOPSLA, pp. 111–128. ACM (2016)

    Google Scholar 

  36. Schellhorn, G., Derrick, J., Wehrheim, H.: A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Log. 15(4), 31:1–31:37 (2014)

    Article  MathSciNet  Google Scholar 

  37. Summers, A.J., Müller, P.: Automating deductive verification for weak-memory programs. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 190–209. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_11

    Chapter  Google Scholar 

  38. Svendsen, K., Pichon-Pharabod, J., Doko, M., Lahav, O., Vafeiadis, V.: A separation logic for a promising semantics. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 357–384. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_13

    Chapter  Google Scholar 

  39. Travkin, O., Wehrheim, H.: Handling TSO in mechanized linearizability proofs. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 132–147. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-13338-6_11

    Chapter  Google Scholar 

  40. Treiber, R.K.: Systems programming: coping with parallelism. Technical report, RJ 5118, IBM Almaden Res. Ctr. (1986)

    Google Scholar 

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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Sheffield, Sheffield, UK

    Simon Doherty & John Derrick

  2. University of Surrey, Guildford, UK

    Brijesh Dongol

  3. University of Paderborn, Paderborn, Germany

    Heike Wehrheim

Authors
  1. Simon Doherty
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Brijesh Dongol
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Heike Wehrheim
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. John Derrick
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Brijesh Dongol .

Editor information

Editors and Affiliations

  1. Università della Svizzera Italiana, Lugano, Switzerland

    Carlo A. Furia

  2. University of Queensland, Brisbane, Queensland, Australia

    Kirsten Winter

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Doherty, S., Dongol, B., Wehrheim, H., Derrick, J. (2018). Making Linearizability Compositional for Partially Ordered Executions. In: Furia, C., Winter, K. (eds) Integrated Formal Methods. IFM 2018. Lecture Notes in Computer Science(), vol 11023. Springer, Cham. https://doi.org/10.1007/978-3-319-98938-9_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-98938-9_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-98937-2

  • Online ISBN: 978-3-319-98938-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation