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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
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
Abadi, M., Lamport, L.: The existence of refinement mappings. Theoret Comput Sci 82(2), 253–284 (1991)
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
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)
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)
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)
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)
Batty M, Owens S, Sarkar S, Sewell P, Weber T (2011) Mathematizing C++ concurrency. In: POPL. ACM, pp 55–66
Back, R.-J.R., von Wright, J.: Trace refinement of action systems. CONCUR '94, volume 836 of LNCS, pp. 367–384. Springer, Berlin (1994)
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
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)
Doherty, S., Derrick, J.: Linearizability and causality. SEFM 2016, volume 9763 of LNCS, pp. 45–60. Springer, Berlin (2016)
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
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
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)
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)
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)
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)
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)
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)
Derrick J, Schellhorn G, Wehrheim H (2011) Mechanically verified proof obligations for linearizability. ACM Trans Program Lang Syst 33(1):4:1–4:43
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
Filipović, I., O'Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor Comput Sci 411(51–52), 4379–4398 (2010)
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)
Gotsman, A., Yang, H.: Liveness-preserving atomicity abstraction. ICALP 2011, volume 6756 of LNCS, pp. 453–465. Springer, Berlin (2011)
Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann, Burlington (2008)
Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans Program Lang Syst 12(3), 463–492 (1990)
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
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)
Moir, M., Shavit, N.: Concurrent data structures. Handbook of data structures and applications 47(1–47), 30 (2004)
Nienhuis K, Memarian K, Sewell P (2016) An operational semantics for C/C++11 concurrency. In: OOPSLA. ACM, pp 111–128
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)
Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. SIGPLAN Not. 46(6), 175–186 (2011)
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)
Smith, G., Winter, K.: Relating trace refinement and linearizability. Formal Asp Comput 29(6), 935–950 (2017)
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
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
Travkin, O., Wehrheim, H.: Handling TSO in mechanized linearizability proofs. In: Yahav, E. (ed.) HVC2014. LNCS, vol. 8855, pp. 132–147. Springer, Berlin (2014)
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
Authors and Affiliations
Corresponding author
Additional information
Michael Butler
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
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
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-019-00499-8