{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T16:51:52Z","timestamp":1725987112809},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319989372"},{"type":"electronic","value":"9783319989389"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-98938-9_7","type":"book-chapter","created":{"date-parts":[[2018,8,8]],"date-time":"2018-08-08T15:08:34Z","timestamp":1533740914000},"page":"110-129","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Making Linearizability Compositional for\u00a0Partially Ordered Executions"],"prefix":"10.1007","author":[{"given":"Simon","family":"Doherty","sequence":"first","affiliation":[]},{"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[]},{"given":"John","family":"Derrick","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,9]]},"reference":[{"issue":"8","key":"7_CR1","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/s00236-016-0275-0","volume":"54","author":"PA Abdulla","year":"2017","unstructured":"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\u2013818 (2017)","journal-title":"Acta Inform."},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-662-54580-5_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2017","unstructured":"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\u201374. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_4"},{"issue":"12","key":"7_CR3","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"SV Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. IEEE Comput. 29(12), 66\u201376 (1996)","journal-title":"IEEE Comput."},{"issue":"1","key":"7_CR4","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/BF01784241","volume":"9","author":"M Ahamad","year":"1995","unstructured":"Ahamad, M., Neiger, G., Burns, J.E., Kohli, P., Hutto, P.W.: Causal memory: definitions, implementation, and programming. Distrib. Comput. 9(1), 37\u201349 (1995)","journal-title":"Distrib. Comput."},{"issue":"2","key":"7_CR5","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"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\u20137:74 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Batty, M., Dodds, M., Gotsman, A.: Library abstraction for C\/C++ concurrency. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 235\u2013248. ACM (2013)","DOI":"10.1145\/2480359.2429099"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Batty, M., Donaldson, A.F., Wickerson, J.: Overhauling SC atomics in C11 and OpenCL. In: POPL, pp. 634\u2013648. ACM (2016)","DOI":"10.1145\/2837614.2837637"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 55\u201366. ACM (2011)","DOI":"10.1145\/1925844.1926394"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"542","DOI":"10.1007\/978-3-319-63390-9_28","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2017","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Mutluergil, S.O.: Proving linearizability using forward simulations. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 542\u2013563. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_28"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-28869-2_5","volume-title":"Programming Languages and Systems","author":"S Burckhardt","year":"2012","unstructured":"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\u2013107. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_5"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-41591-8_4","volume-title":"Software Engineering and Formal Methods","author":"S Doherty","year":"2016","unstructured":"Doherty, S., Derrick, J.: Linearizability and causality. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 45\u201360. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_4"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Doherty, S., Derrick, J., Dongol, B., Wehrheim, H.: Causal linearizability: compositionality for partially ordered executions. CoRR abs\/1802.01866 (2018)","DOI":"10.1007\/978-3-319-98938-9_7"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30232-2_7","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"S Doherty","year":"2004","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a\u00a0practical lock-free queue algorithm. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97\u2013114. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30232-2_7"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-662-49122-5_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Doko","year":"2016","unstructured":"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\u2013430. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_20"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/978-3-662-54434-1_17","volume-title":"Programming Languages and Systems","author":"M Doko","year":"2017","unstructured":"Doko, M., Vafeiadis, V.: Tackling real-life relaxed concurrency with FSL++. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 448\u2013475. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_17"},{"issue":"2","key":"7_CR16","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/2796550","volume":"48","author":"B Dongol","year":"2015","unstructured":"Dongol, B., Derrick, J.: Verifying linearisability: a comparative survey. ACM Comput. Surv. 48(2), 19:1\u201319:43 (2015)","journal-title":"ACM Comput. Surv."},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-319-10882-7_10","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2014","author":"B Dongol","year":"2014","unstructured":"Dongol, B., Derrick, J., Smith, G.: Reasoning algebraically about refinement on TSO architectures. In: Ciobanu, G., M\u00e9ry, D. (eds.) ICTAC 2014. LNCS, vol. 8687, pp. 151\u2013168. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10882-7_10"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-319-73721-8_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Dongol","year":"2018","unstructured":"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\u2013204. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_9"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-319-68690-5_7","volume-title":"Formal Methods and Software Engineering","author":"P Doolan","year":"2017","unstructured":"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\u2013121. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68690-5_7"},{"issue":"51\u201352","key":"7_CR20","doi-asserted-by":"publisher","first-page":"4379","DOI":"10.1016\/j.tcs.2010.09.021","volume":"411","author":"I Filipovic","year":"2010","unstructured":"Filipovic, I., O\u2019Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51\u201352), 4379\u20134398 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-33651-5_3","volume-title":"Distributed Computing","author":"A Gotsman","year":"2012","unstructured":"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\u201345. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33651-5_3"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"He, M., Vafeiadis, V., Qin, S., Ferreira, J.F.: Reasoning about fences and relaxed atomics. In: PDP, pp. 520\u2013527. IEEE Computer Society (2016)","DOI":"10.1109\/PDP.2016.103"},{"key":"7_CR23","volume-title":"The Art of Multiprocessor Programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, Burlington (2008)"},{"issue":"3","key":"7_CR24","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM TOPLAS 12(3), 463\u2013492 (1990)","journal-title":"ACM TOPLAS"},{"key":"7_CR25","unstructured":"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\u201317:29. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"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\u2013189. ACM (2017)","DOI":"10.1145\/3009837.3009850"},{"issue":"POPL","key":"7_CR27","first-page":"17:1","volume":"2","author":"M Kokologiannakis","year":"2018","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. PACMPL 2(POPL), 17:1\u201317:32 (2018)","journal-title":"PACMPL"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: Bod\u00edk, R., Majumdar, R. (eds.) POPL, pp. 649\u2013662. ACM (2016)","DOI":"10.1145\/2837614.2837643"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-662-47666-6_25","volume-title":"Automata, Languages, and Programming","author":"O Lahav","year":"2015","unstructured":"Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 311\u2013323. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_25"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C., Dreyer, D.: Repairing sequential consistency in C\/C++11. In: PLDI, pp. 618\u2013632. ACM (2017)","DOI":"10.1145\/3140587.3062352"},{"issue":"9","key":"7_CR31","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"7_CR32","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF01786227","volume":"1","author":"L Lamport","year":"1986","unstructured":"Lamport, L.: On interprocess communication. Part I: basic formalism. Distrib. Comput. 1(2), 77\u201385 (1986)","journal-title":"Distrib. Comput."},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-05089-3_21","volume-title":"FM 2009: Formal Methods","author":"Y Liu","year":"2009","unstructured":"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\u2013337. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_21"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL, pp. 378\u2013391. ACM (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Nienhuis, K., Memarian, K., Sewell, P.: An operational semantics for C\/C++11 concurrency. In: Visser, E., Smaragdakis, Y. (eds.) OOPSLA, pp. 111\u2013128. ACM (2016)","DOI":"10.1145\/3022671.2983997"},{"issue":"4","key":"7_CR36","doi-asserted-by":"publisher","first-page":"31:1","DOI":"10.1145\/2629496","volume":"15","author":"G Schellhorn","year":"2014","unstructured":"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\u201331:37 (2014)","journal-title":"ACM Trans. Comput. Log."},{"key":"7_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-89960-2_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"AJ Summers","year":"2018","unstructured":"Summers, A.J., M\u00fcller, P.: Automating deductive verification for weak-memory programs. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 190\u2013209. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_11"},{"key":"7_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-89884-1_13","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2018","unstructured":"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\u2013384. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_13"},{"key":"7_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-319-13338-6_11","volume-title":"Hardware and Software: Verification and Testing","author":"O Travkin","year":"2014","unstructured":"Travkin, O., Wehrheim, H.: Handling TSO in mechanized linearizability proofs. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 132\u2013147. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_11"},{"key":"7_CR40","unstructured":"Treiber, R.K.: Systems programming: coping with parallelism. Technical report, RJ 5118, IBM Almaden Res. Ctr. (1986)"},{"key":"7_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Computer Aided Verification","author":"V Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450\u2013464. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_40"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98938-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T01:01:30Z","timestamp":1571706090000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98938-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319989372","9783319989389"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98938-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}