Linearizability on hardware weak memory models

Abstract

Linearizability is a widely accepted notion of correctness for concurrent objects. Recent research has investigated redefining linearizability for particular hardware weak memory models, in particular for TSO. In this paper, we provide an overview of this research and show that such redefinitions of linearizability are not required: under an interpretation of specification behaviour which abstracts from weak memory effects, the standard definition of linearizability is sound and complete on all hardware weak memory models.We prove our result with respect to a definition of object refinement which takes a weak memory model as a parameter. The main consequence of our findings is that we can leverage the range of existing techniques and tools for standard linearizability when verifying concurrent objects running on hardware weak memory models.

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

References

  1. AFI+08

    Alglave J, Fox A, Ishtiaq S, Myreen MO, Sarkar S, Sewell P, Nardelli FZ (2008) The semantics of power and ARM multiprocessor machine code. In: Petersen L, Chakravarty MMT (eds) DAMP '09. ACM, pp 13–24

  2. AL91

    Abadi, M., Lamport, L.: The existence of refinement mappings. Theoret Comput Sci 82(2), 253–284 (1991)

    MathSciNet  Article  Google Scholar 

  3. AMT14

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

  4. Bac90

    Back, R.-J.R.: Refinement calculus, part II: parallel and reactive programs. Stepwise refinement of distributed systems models, formalisms, correctness, pp. 67–93. Springer, Berlin (1990)

    Google Scholar 

  5. BDM13

    Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) Programming languages and systems (ESOP 2013), pp. 533–553. Springer, Berlin (2013)

    Google Scholar 

  6. BGMY12

    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, Berlin (2012)

    Google Scholar 

  7. BMM11

    Bouajjani, A., Meyer, R., Möhlmann, E.: Deciding robustness against total store ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) Automata, languages and programming, pp. 428–440. Springer, Berlin (2011)

    Google Scholar 

  8. BOS+11

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

  9. BvW94

    Back, R.-J.R., von Wright, J.: Trace refinement of action systems. CONCUR '94, volume 836 of LNCS, pp. 367–384. Springer, Berlin (1994)

    Google Scholar 

  10. CL05

    Chase D, Lev Y (2005) Dynamic circular work-stealing deque. In: SPAA'05: proceedings of the 17th annual ACM symposium on parallelism in algorithms and architectures, New York, NY, USA. ACM Press, pp 21–28

  11. CS18

    Colvin, R.J., Smith, G.: A wide-spectrum language for verification of programs on weak memory models. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 240–257. Springer, Berlin (2018)

    Google Scholar 

  12. DD16

    Doherty, S., Derrick, J.: Linearizability and causality. SEFM 2016, volume 9763 of LNCS, pp. 45–60. Springer, Berlin (2016)

    Google Scholar 

  13. DDGS15

    Dongol B, Derrick J, Groves L, Smith G (2015) Defining correctness conditions for concurrent objects in multicore architectures. In: ECOOP '15, LIPIcs. Schloss Dagstuhl – Leibnis-Zentrum für Informatik, pp 470–494

  14. DDWD18

    Doherty S, Dongol B, Wehrheim H, Derrick J (2018) Making linearizability compositional for partially ordered executions. In: Furia CA, Winter K (eds) IFM 2018, vol 11023. LNCS. Springer, Cham, pp 110–129

  15. DG16

    Dongol, B., Groves, L.: Contextual trace refinement for concurrent objects: safety and progress. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016, pp. 261–278. Springer, Berlin (2016)

    Google Scholar 

  16. DJRA18

    Dongol, B., Jagadeesan, R., Riely, J., Armstrong, A.: On abstraction and compositionality for weak-memory linearisability. In: Dillig, I., Palsberg, J. (eds.) VMCAI'18. LNCS, vol. 10747, pp. 183–204. Springer, Berlin (2018)

    Google Scholar 

  17. DS15

    Derrick, J., Smith, G.: A framework for correctness criteria on weak memory models. In: Bjørner, N., de Boer, F.S. (eds.) FM 2015. LNCS, vol. 9109, pp. 178–194. Springer, Berlin (2015)

    Google Scholar 

  18. DSD14

    Derrick, J., Smith, G., Dongol, B., Verifying linearizability on TSO architectures. In: Albert E, Sekerinski E (eds) iFM, : volume 8739 of LNCS, pp. 341–356. Springer, Berlin (2014)

  19. DSGD14

    Derrick, J., Smith, G., Groves, L., Dongol, B.: Using coarse-grained abstractions to verify linearizability on TSO architectures. In: Yahav, E. (ed.) HVC 2014, pp. 1–16. Springer, Berlin (2014)

  20. DSGD17

    Derrick, J., Smith, G., Groves, L., Dongol, B.: A proof method for linearizability on TSO architectures. In: Hinchey, M., Bowen, J.P., Olderog, E.-R. (eds.) Provably correct systems, pp. 61–91. Springer, Berlin (2017)

    Google Scholar 

  21. DSW11

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

  22. FGP+16

    Flur S, Gray KE, Pulte C, Sarkar S, Sezgin A, Maranget L, Deacon W, Sewell P (2016) Modelling the ARMv8 architecture, operationally: concurrency and ISA. In: Bodik R, Majumdar R (eds) POPL 2016. ACM, pp 608–621

  23. FORY10

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

    MathSciNet  Article  Google Scholar 

  24. GMY12

    Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: Aguilera, M. (ed.) DISC 2012. LNCS, vol. 7611, pp. 31–45. Springer, Berlin (2012)

    Google Scholar 

  25. GY11

    Gotsman, A., Yang, H.: Liveness-preserving atomicity abstraction. ICALP 2011, volume 6756 of LNCS, pp. 453–465. Springer, Berlin (2011)

    Google Scholar 

  26. HS08

    Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann, Burlington (2008)

    Google Scholar 

  27. HW90

    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 

  28. LPCZN13

    Lê NM, Pop A, Cohen A, Zappa Nardelli F (2013) Correct and efficient work-stealing for weak memory models. In PPoPP’13, ACM, pp 69–80

  29. MHMS+12

    Mador-Haim, S., Maranget, L., Sarkar, S., Memarian, K., Alglave, J., Owens, S., Alur, R., Martin, M.M.K., Sewell, P., Williams, D.: An axiomatic memory model for POWER multiprocessors. CAV'12, pp. 495–512. Springer, Berlin (2012)

    Google Scholar 

  30. MS04

    Moir, M., Shavit, N.: Concurrent data structures. Handbook of data structures and applications 47(1–47), 30 (2004)

    MATH  Google Scholar 

  31. NMS16

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

  32. Owe10

    Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: D'Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 478–503. Springer, Berlin (2010)

    Google Scholar 

  33. SSA+11

    Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. SIGPLAN Not. 46(6), 175–186 (2011)

    Article  Google Scholar 

  34. SSO+10

    Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. Commun ACM 53(7), 89–97 (2010)

    Article  Google Scholar 

  35. SW17

    Smith, G., Winter, K.: Relating trace refinement and linearizability. Formal Asp Comput 29(6), 935–950 (2017)

    MathSciNet  Article  Google Scholar 

  36. SWC18

    Smith G, Winter K, Colvin RJ (2018) Correctness of concurrent objects under weak memory models. In Derrick J, Dongol B, Reeves S (eds) Refine 2018, volume 282 of EPTCS. Open Publishing Association, pp 53–67

  37. TMW13

    Travkin O., Mütze A,Wehrheim H (2013) SPIN as a linearizability checker under weak memory models. In Bertacco V, Legay A (eds) HVC2013, volume 8244 of LNCS. Springer, Berlin, pp 311–326

  38. TW14

    Travkin, O., Wehrheim, H.: Handling TSO in mechanized linearizability proofs. In: Yahav, E. (ed.) HVC2014. LNCS, vol. 8855, pp. 132–147. Springer, Berlin (2014)

    Google Scholar 

Download references

Acknowledgements

The authors would like to thank Lindsay Groves and the anonymous reviewers of this paper for their valuable feedback and advice. This work was supported by Australian Research Council Discovery Grant DP160102457.

Author information

Affiliations

Authors

Corresponding author

Correspondence to Graeme Smith.

Additional information

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Michael Butler

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Smith, G., Winter, K. & Colvin, R.J. Linearizability on hardware weak memory models. Form Asp Comp 32, 1–32 (2020). https://doi.org/10.1007/s00165-019-00499-8

Download citation

Keywords

  • Linearizability
  • Correctness
  • Concurrent objects