{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:58:00Z","timestamp":1770289080193,"version":"3.49.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319737201","type":"print"},{"value":"9783319737218","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T00:00:00Z","timestamp":1514505600000},"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-73721-8_9","type":"book-chapter","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T04:13:05Z","timestamp":1514434385000},"page":"183-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["On abstraction and compositionality for weak-memory linearisability"],"prefix":"10.1007","author":[{"given":"Brijesh","family":"Dongol","sequence":"first","affiliation":[]},{"given":"Radha","family":"Jagadeesan","sequence":"additional","affiliation":[]},{"given":"James","family":"Riely","sequence":"additional","affiliation":[]},{"given":"Alasdair","family":"Armstrong","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,29]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/1787234.1787255","volume":"53","author":"SV Adve","year":"2010","unstructured":"Adve, S.V., Boehm, H.J.: Memory models: a case for rethinking parallel languages and hardware. Commun. ACM 53, 90\u2013101 (2010)","journal-title":"Commun. ACM"},{"issue":"12","key":"9_CR2","doi-asserted-by":"crossref","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. Computer 29(12), 66\u201376 (1996)","journal-title":"Computer"},{"issue":"2","key":"9_CR3","doi-asserted-by":"crossref","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":"9_CR4","doi-asserted-by":"crossref","unstructured":"Batty, M., Dodds, M., Gotsman, A.: Library abstraction for C\/C++ concurrency. In: POPL, pp. 235\u2013248. ACM (2013)","DOI":"10.1145\/2480359.2429099"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL, pp. 55\u201366. ACM (2011)","DOI":"10.1145\/1925844.1926394"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: Gupta, R., Amarasinghe, S.P. (eds.) PLDI, pp. 68\u201378. ACM (2008)","DOI":"10.1145\/1375581.1375591"},{"key":"9_CR7","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":"9_CR8","unstructured":"Deacon, W.: Arm64 cat file (2017). https:\/\/github.com\/herd\/herdtools7\/commit\/daa126680b6ecba97ba47b3e05bbaa51a89f27b7"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-60225-7_8","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"J Derrick","year":"2017","unstructured":"Derrick, J., Smith, G.: An observational approach to defining linearizability on weak memory models. In: Bouajjani, A., Silva, A. (eds.) FORTE 2017. LNCS, vol. 10321, pp. 108\u2013123. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-60225-7_8"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-319-10181-1_21","volume-title":"Integrated Formal Methods","author":"J Derrick","year":"2014","unstructured":"Derrick, J., Smith, G., Dongol, B.: Verifying linearizability on TSO architectures. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 341\u2013356. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10181-1_21"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-642-00590-9_26","volume-title":"Programming Languages and Systems","author":"M Dodds","year":"2009","unstructured":"Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 363\u2013377. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00590-9_26"},{"key":"9_CR12","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"},{"issue":"2","key":"9_CR13","doi-asserted-by":"crossref","first-page":"19","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 (2015)","journal-title":"ACM Comput. Surv."},{"key":"9_CR14","unstructured":"Dongol, B., Derrick, J., Smith, G., Groves, L.: Defining correctness conditions for concurrent objects in multicore architectures. In: Boyland, J.T. (ed.) ECOOP. LIPIcs, vol. 37, pp. 470\u2013494. Dagstuhl (2015)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-47846-3_17","volume-title":"Formal Methods and Software Engineering","author":"B Dongol","year":"2016","unstructured":"Dongol, B., Groves, L.: Contextual trace refinement for concurrent objects: safety and progress. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 261\u2013278. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47846-3_17"},{"issue":"51\u201352","key":"9_CR16","doi-asserted-by":"crossref","first-page":"4379","DOI":"10.1016\/j.tcs.2010.09.021","volume":"411","author":"I Filipovi\u0107","year":"2010","unstructured":"Filipovi\u0107, 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":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-642-22012-8_36","volume-title":"Automata, Languages and Programming","author":"A Gotsman","year":"2011","unstructured":"Gotsman, A., Yang, H.: Liveness-preserving atomicity abstraction. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 453\u2013465. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22012-8_36"},{"key":"9_CR18","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morg. Kauf. (2008)"},{"issue":"3","key":"9_CR19","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"MP Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-37036-6_27","volume-title":"Programming Languages and Systems","author":"R Jagadeesan","year":"2013","unstructured":"Jagadeesan, R., Petri, G., Pitcher, C., Riely, J.: Quarantining weakness - compositional reasoning under relaxed memory models (extended abstract). In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 492\u2013511. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_27"},{"issue":"7","key":"9_CR21","doi-asserted-by":"crossref","first-page":"779","DOI":"10.1109\/12.599898","volume":"46","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a correct multiprocess program execute correctly on a multiprocessor. IEEE Trans. Computers 46(7), 779\u2013782 (1979)","journal-title":"IEEE Trans. Computers"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-40184-8_17","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"H Liang","year":"2013","unstructured":"Liang, H., Hoffmann, J., Feng, X., Shao, Z.: Characterizing progress properties of concurrent objects via contextual refinements. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 227\u2013241. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_17"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL 2005, pp. 378\u2013391 (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., Sewell, P.: Simplifying arm concurrency: multicopy-atomic axiomatic and operational models for armv8. In: POPL (2018) (to appear)","DOI":"10.1145\/3158107"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding power multiprocessors. In: PLDI, pp. 175\u2013186. ACM (2011)","DOI":"10.1145\/1993498.1993520"},{"key":"9_CR26","unstructured":"Sevc\u00edk, J.: Program Transformations in Weak Memory Models. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh (2008)"},{"issue":"7","key":"9_CR27","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: A rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"issue":"3","key":"9_CR28","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1145\/1897852.1897873","volume":"54","author":"N Shavit","year":"2011","unstructured":"Shavit, N.: Data structures in the multicore age. Commun. ACM 54(3), 76\u201384 (2011)","journal-title":"Commun. ACM"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Smith, G., Winter, K.: Relating trace refinement and linearizability. Formal Aspects of Computing 1\u201316 (2017)","DOI":"10.1007\/s00165-017-0418-2"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73721-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T16:00:57Z","timestamp":1570550457000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73721-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,29]]},"ISBN":["9783319737201","9783319737218"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73721-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,29]]}}}