{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:57:05Z","timestamp":1774025825554,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":58,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"EPSRC","award":["EP\/K008528\/1,EP\/M027317\/1"],"award-info":[{"award-number":["EP\/K008528\/1,EP\/M027317\/1"]}]},{"name":"ARM"},{"DOI":"10.13039\/100000865","name":"Bill and Melinda Gates Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000865","id-type":"DOI","asserted-by":"publisher"}]},{"name":"ANR","award":["WMC (ANR-11-JS02-011)"],"award-info":[{"award-number":["WMC (ANR-11-JS02-011)"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009839","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"429-442","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Mixed-size concurrency: ARM, POWER, C\/C++11, and SC"],"prefix":"10.1145","author":[{"given":"Shaked","family":"Flur","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Susmit","family":"Sarkar","sequence":"additional","affiliation":[{"name":"University of St. Andrews, UK"}]},{"given":"Christopher","family":"Pulte","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Kyndylan","family":"Nienhuis","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Luc","family":"Maranget","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"Kathryn E.","family":"Gray","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Ali","family":"Sezgin","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Mark","family":"Batty","sequence":"additional","affiliation":[{"name":"University of Kent, UK"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1978.1675013"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/17407.17406"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/5001.5007"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325102"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/129082"},{"key":"e_1_3_2_1_11_1","volume-title":"Springer US","author":"Sindhu Pradeep S.","year":"1992","unstructured":"Pradeep S. Sindhu , Jean-Marc Frailong , and Michel Cekleov . Formal Specification of Memory Models, pages 25\u201341 . Springer US , 1992 . Pradeep S. Sindhu, Jean-Marc Frailong, and Michel Cekleov. Formal Specification of Memory Models, pages 25\u201341. Springer US, 1992."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPP.1993.15"},{"key":"e_1_3_2_1_14_1","first-page":"52","volume-title":"Proceedings of the 1993 Symposium on Research on Integrated Systems","author":"Dill David L","unstructured":"David L Dill , Seungjoon Park , and Andreas G. Nowatzyk . Formal specification of abstract memory models . In Proceedings of the 1993 Symposium on Research on Integrated Systems , pages 38\u2013 52 . MIT Press, 1993. David L Dill, Seungjoon Park, and Andreas G. Nowatzyk. Formal specification of abstract memory models. In Proceedings of the 1993 Symposium on Research on Integrated Systems, pages 38\u201352. MIT Press, 1993."},{"key":"e_1_3_2_1_15_1","unstructured":"The SPARC Architecture Manual Version 9. SPARC Int. Inc. 1994.   The SPARC Architecture Manual Version 9. SPARC Int. Inc. 1994."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/181014.192323"},{"key":"e_1_3_2_1_17_1","first-page":"653","article-title":"Formalizing memory coherency models","volume":"1","author":"Bernab\u00e9u-Aub\u00e1n Jos\u00e9 M.","year":"1994","unstructured":"Jos\u00e9 M. Bernab\u00e9u-Aub\u00e1n and Vicente Cholvi-juan . Formalizing memory coherency models . Journal of Computing and Information , 1 : 653 \u2013 672 , 1994 . Jos\u00e9 M. Bernab\u00e9u-Aub\u00e1n and Vicente Cholvi-juan. Formalizing memory coherency models. Journal of Computing and Information, 1:653\u2013672, 1994.","journal-title":"Journal of Computing and Information"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/891506"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_3_2_1_20_1","volume-title":"Department of Computer Science","author":"Higham Lisa","year":"1998","unstructured":"Lisa Higham , Jalal Kawash , and Nathaly Verwaal . Weak memory consistency models. Part I: Definitions and comparisons. Technical report , Department of Computer Science , University of Calgary , 1998 . Lisa Higham, Jalal Kawash, and Nathaly Verwaal. Weak memory consistency models. Part I: Definitions and comparisons. Technical report, Department of Computer Science, University of Calgary, 1998."},{"key":"e_1_3_2_1_21_1","volume-title":"19th International Conference on Computer Design (ICCD 2001)","author":"Chatterjee Prosenjit","year":"2001","unstructured":"Prosenjit Chatterjee and Ganesh Gopalakrishnan . Towards a formal model of shared memory consistency for Intel Itaniumtm . In 19th International Conference on Computer Design (ICCD 2001) , September 2001 , Austin, TX, USA, pages 515\u2013518 , 2001. Prosenjit Chatterjee and Ganesh Gopalakrishnan. Towards a formal model of shared memory consistency for Intel Itaniumtm. In 19th International Conference on Computer Design (ICCD 2001), September 2001, Austin, TX, USA, pages 515\u2013518, 2001."},{"key":"e_1_3_2_1_22_1","volume-title":"A formal specification of Intel Itanium processor family memory ordering","year":"2002","unstructured":"Intel. A formal specification of Intel Itanium processor family memory ordering , 2002 . http:\/\/download.intel.com\/design\/ Itanium\/Downloads\/ 25142901.pdf. Intel. A formal specification of Intel Itanium processor family memory ordering, 2002. http:\/\/download.intel.com\/design\/ Itanium\/Downloads\/25142901.pdf."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2004.1302944"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11947950_7"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2006.26"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353522.1353528"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_3_2_1_36_1","volume-title":"A tutorial introduction to the ARM and POWER relaxed memory models. Draft available from http:\/\/www.cl.cam.ac.uk\/~pes20\/ ppc-supplemental\/test7.pdf","author":"Maranget Luc","year":"2012","unstructured":"Luc Maranget , Susmit Sarkar , and Peter Sewell . A tutorial introduction to the ARM and POWER relaxed memory models. Draft available from http:\/\/www.cl.cam.ac.uk\/~pes20\/ ppc-supplemental\/test7.pdf , 2012 . Luc Maranget, Susmit Sarkar, and Peter Sewell. A tutorial introduction to the ARM and POWER relaxed memory models. Draft available from http:\/\/www.cl.cam.ac.uk\/~pes20\/ ppc-supplemental\/test7.pdf, 2012."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_3_2_1_40_1","volume-title":"Taming weak memory models. CoRR, abs\/1606.05416","author":"Zhang Sizhuo","year":"2016","unstructured":"Sizhuo Zhang , Arvind, and Muralidaran Vijayaraghavan . Taming weak memory models. CoRR, abs\/1606.05416 , 2016 . Sizhuo Zhang, Arvind, and Muralidaran Vijayaraghavan. Taming weak memory models. CoRR, abs\/1606.05416, 2016."},{"key":"e_1_3_2_1_41_1","unstructured":"Linux kernel lockrefs. https:\/\/lwn.net\/Articles\/565734\/ http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/torvalds\/ linux.git\/tree\/lib\/lockref.c http:\/\/git.kernel.org\/cgit\/ linux\/kernel\/git\/torvalds\/linux.git\/tree\/include\/linux\/ lockref.h.  Linux kernel lockrefs. https:\/\/lwn.net\/Articles\/565734\/ http:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/torvalds\/ linux.git\/tree\/lib\/lockref.c http:\/\/git.kernel.org\/cgit\/ linux\/kernel\/git\/torvalds\/linux.git\/tree\/include\/linux\/ lockref.h."},{"key":"e_1_3_2_1_42_1","volume-title":"ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile)","author":"Ltd ARM","year":"2015","unstructured":"ARM Ltd . ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile) , 2015 . ARM DDI 0487A.h (ID 092915). ARM Ltd. ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile), 2015. ARM DDI 0487A.h (ID092915)."},{"key":"e_1_3_2_1_43_1","unstructured":"Power ISATM Version 2.07. IBM 2013.  Power ISATM Version 2.07. IBM 2013."},{"key":"e_1_3_2_1_44_1","first-page":"44","volume-title":"Proceedings of TACAS","author":"Alglave Jade","year":"2011","unstructured":"Jade Alglave , Luc Maranget , Susmit Sarkar , and Peter Sewell . Litmus : running tests against hardware . In Proceedings of TACAS 2011 , pages 41\u2013 44 . Springer-Verlag, 2011. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Litmus: running tests against hardware. In Proceedings of TACAS 2011, pages 41\u201344. Springer-Verlag, 2011."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_1_47_1","volume-title":"Counterexamples and proof loophole for the C\/C++ to POWER and ARMv7 trailing-sync compiler mappings. CoRR, abs\/1611.01507","author":"Manerkar Yatin A.","year":"2016","unstructured":"Yatin A. Manerkar , Caroline Trippel , Daniel Lustig , Michael Pellauer , and Margaret Martonosi . Counterexamples and proof loophole for the C\/C++ to POWER and ARMv7 trailing-sync compiler mappings. CoRR, abs\/1611.01507 , 2016 . Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. Counterexamples and proof loophole for the C\/C++ to POWER and ARMv7 trailing-sync compiler mappings. CoRR, abs\/1611.01507, 2016."},{"key":"e_1_3_2_1_48_1","volume-title":"Repairing sequential consistency in C\/C++11. Note,","author":"Lahav Ori","year":"2016","unstructured":"Ori Lahav , Viktor Vafeiadis , Jeehoon Kang , Chung-Kil Hur , and Derek Dreyer . Repairing sequential consistency in C\/C++11. Note, available at http:\/\/plv.mpi-sws.org\/scfix\/, 2016 . Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. Repairing sequential consistency in C\/C++11. Note, available at http:\/\/plv.mpi-sws.org\/scfix\/, 2016."},{"key":"e_1_3_2_1_49_1","volume-title":"December","author":"Sarkar Susmit","year":"2016","unstructured":"Susmit Sarkar and Peter Sewell . Corrigendum : C\/C++11 to POWER concurrency compilation scheme correctness proof. Note, available at http:\/\/www.cl.cam.ac.uk\/users\/pes20\/cppppc\/corrigendum. html , December 2016 . Susmit Sarkar and Peter Sewell. Corrigendum: C\/C++11 to POWER concurrency compilation scheme correctness proof. Note, available at http:\/\/www.cl.cam.ac.uk\/users\/pes20\/cppppc\/corrigendum. html, December 2016."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762206"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_3"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_3_2_1_54_1","unstructured":"Shaked Flur Susmit Sarkar Christopher Pulte Kyndylan Nienhuis Luc Maranget Kathryn E. Gray Ali Sezgin Mark Batty and Peter Sewell. Supplementary material. http:\/\/www.cl.cam.ac.uk\/ ~pes20\/popl17\/ Shaked Flur Susmit Sarkar Christopher Pulte Kyndylan Nienhuis Luc Maranget Kathryn E. Gray Ali Sezgin Mark Batty and Peter Sewell. Supplementary material. http:\/\/www.cl.cam.ac.uk\/ ~pes20\/popl17\/"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_3_2_1_56_1","volume-title":"Programming Languages \u2014 C++","author":"Becker P.","year":"2011","unstructured":"P. Becker , editor. Programming Languages \u2014 C++ . 2011 . ISO\/IEC 14882: 2011. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/ papers\/2011\/n3242.pdf. P. Becker, editor. Programming Languages \u2014 C++. 2011. ISO\/IEC 14882:2011. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/ papers\/2011\/n3242.pdf."},{"key":"e_1_3_2_1_58_1","unstructured":"P. E. McKenney and R. Silvera. Example POWER implementation for C\/C++ memory model. http:\/\/www.rdrop.com\/users\/paulmck\/ scalability\/paper\/N2745r.2011.03.04a.html 2011.  P. E. McKenney and R. Silvera. Example POWER implementation for C\/C++ memory model. http:\/\/www.rdrop.com\/users\/paulmck\/ scalability\/paper\/N2745r.2011.03.04a.html 2011."},{"key":"e_1_3_2_1_59_1","unstructured":"Jade Alglave and Luc Maranget. The diy tool. http:\/\/diy.inria. fr\/.  Jade Alglave and Luc Maranget. The diy tool. http:\/\/diy.inria. fr\/."},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429099"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_3_2_1_62_1","volume-title":"New lace and arsenic: adventures in weak memory with a program logic. CoRR, abs\/1512.01416","author":"Bornat Richard","year":"2015","unstructured":"Richard Bornat , Jade Alglave , and Matthew J. Parkinson . New lace and arsenic: adventures in weak memory with a program logic. CoRR, abs\/1512.01416 , 2015 . Richard Bornat, Jade Alglave, and Matthew J. Parkinson. New lace and arsenic: adventures in weak memory with a program logic. CoRR, abs\/1512.01416, 2015."}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009839","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009839","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:21Z","timestamp":1750203381000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009839"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":58,"alternative-id":["10.1145\/3009837.3009839","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009839","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009839","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}