zbMATH — the first resource for mathematics

Linearizability on hardware weak memory models. (English) Zbl 1451.68030
Summary: 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.
68M07 Mathematical problems of computer architecture
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Line-up; SPIN
Full Text: DOI
[1] 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] Abadi, M.; Lamport, L., The existence of refinement mappings, Theoret Comput Sci, 82, 2, 253-284 (1991) · Zbl 0728.68083
[3] 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] Back, R-JR, Refinement calculus, part II: parallel and reactive programs, Stepwise refinement of distributed systems models, formalisms, correctness, 67-93 (1990), Berlin: Springer, Berlin
[5] Bouajjani, A.; Derevenetc, E.; Meyer, R.; Felleisen, M.; Gardner, P., Checking and enforcing robustness against TSO, Programming languages and systems (ESOP 2013), 533-553 (2013), Berlin: Springer, Berlin · Zbl 1381.68039
[6] Burckhardt, S.; Gotsman, A.; Musuvathi, M.; Yang, H.; Seidl, H., Concurrent library correctness on the TSO memory model, ESOP 2012, 87-107 (2012), Berlin: Springer, Berlin · Zbl 1352.68049
[7] Bouajjani, A.; Meyer, R.; Möhlmann, E.; Aceto, L.; Henzinger, M.; Sgall, J., Deciding robustness against total store ordering, Automata, languages and programming, 428-440 (2011), Berlin: Springer, Berlin · Zbl 1333.68082
[8] Batty M, Owens S, Sarkar S, Sewell P, Weber T (2011) Mathematizing C++ concurrency. In: POPL. ACM, pp 55-66 · Zbl 1284.68165
[9] Back, R-JR; von Wright, J., Trace refinement of action systems, CONCUR ’94, volume 836 of LNCS, 367-384 (1994), Berlin: Springer, Berlin
[10] 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] Colvin, RJ; Smith, G.; Havelund, K.; Peleska, J.; Roscoe, B.; de Vink, E., A wide-spectrum language for verification of programs on weak memory models, FM 2018, 240-257 (2018), Berlin: Springer, Berlin
[12] Doherty, S.; Derrick, J., Linearizability and causality, SEFM 2016, volume 9763 of LNCS, 45-60 (2016), Berlin: Springer, Berlin
[13] 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] 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] Dongol, B.; Groves, L.; Ogata, K.; Lawford, M.; Liu, S., Contextual trace refinement for concurrent objects: safety and progress, ICFEM 2016, 261-278 (2016), Berlin: Springer, Berlin
[16] Dongol, B.; Jagadeesan, R.; Riely, J.; Armstrong, A.; Dillig, I.; Palsberg, J., On abstraction and compositionality for weak-memory linearisability, VMCAI’18, 183-204 (2018), Berlin: Springer, Berlin · Zbl 1446.68104
[17] Derrick, J.; Smith, G.; Bjørner, N.; de Boer, FS, A framework for correctness criteria on weak memory models, FM 2015, 178-194 (2015), Berlin: Springer, Berlin · Zbl 1427.68166
[18] 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) · Zbl 1432.68006
[19] 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] Derrick, J.; Smith, G.; Groves, L.; Dongol, B.; Hinchey, M.; Bowen, JP; Olderog, E-R, A proof method for linearizability on TSO architectures, Provably correct systems, 61-91 (2017), Berlin: Springer, Berlin
[21] 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] 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] Filipović, I.; O’Hearn, PW; Rinetzky, N.; Yang, H., Abstraction for concurrent objects, Theor Comput Sci, 411, 51-52, 4379-4398 (2010) · Zbl 1209.68156
[24] Gotsman, A.; Musuvathi, M.; Yang, H.; Aguilera, M., Show no weakness: sequentially consistent specifications of TSO libraries, DISC 2012, 31-45 (2012), Berlin: Springer, Berlin · Zbl 1377.68038
[25] Gotsman, A.; Yang, H., Liveness-preserving atomicity abstraction, ICALP 2011, volume 6756 of LNCS, 453-465 (2011), Berlin: Springer, Berlin · Zbl 1333.68198
[26] Herlihy, M.; Shavit, N., The art of multiprocessor programming (2008), Burlington: Morgan Kaufmann, Burlington
[27] Herlihy, M.; Wing, JM, Linearizability: a correctness condition for concurrent objects, ACM Trans Program Lang Syst, 12, 3, 463-492 (1990)
[28] 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] Mador-Haim, S.; Maranget, L.; Sarkar, S.; Memarian, K.; Alglave, J.; Owens, S.; Alur, R.; Martin, MMK; Sewell, P.; Williams, D., An axiomatic memory model for POWER multiprocessors, CAV’12, 495-512 (2012), Berlin: Springer, Berlin
[30] Moir, M.; Shavit, N., Concurrent data structures, Handbook of data structures and applications, 47, 1-47, 30 (2004)
[31] Nienhuis K, Memarian K, Sewell P (2016) An operational semantics for C/C++11 concurrency. In: OOPSLA. ACM, pp 111-128
[32] Owens, S.; D’Hondt, T., Reasoning about the implementation of concurrency abstractions on x86-TSO, ECOOP 2010, 478-503 (2010), Berlin: Springer, Berlin
[33] Sarkar, S.; Sewell, P.; Alglave, J.; Maranget, L.; Williams, D., Understanding POWER multiprocessors, SIGPLAN Not., 46, 6, 175-186 (2011)
[34] Sewell, P.; Sarkar, S.; Owens, S.; Nardelli, FZ; Myreen, MO, x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors, Commun ACM, 53, 7, 89-97 (2010)
[35] Smith, G.; Winter, K., Relating trace refinement and linearizability, Formal Asp Comput, 29, 6, 935-950 (2017) · Zbl 1377.68151
[36] 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] 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] Travkin, O.; Wehrheim, H.; Yahav, E., Handling TSO in mechanized linearizability proofs, HVC2014, 132-147 (2014), Berlin: Springer, Berlin
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.