{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:57:00Z","timestamp":1774025820081,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K008528\/1"],"award-info":[{"award-number":["EP\/K008528\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314624","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Promising-ARM\/RISC-V: a simpler and faster operational concurrency model"],"prefix":"10.1145","author":[{"given":"Christopher","family":"Pulte","sequence":"first","affiliation":[{"name":"Cambridge University, UK"}]},{"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[{"name":"Cambridge University, UK"}]},{"given":"Jeehoon","family":"Kang","sequence":"additional","affiliation":[{"name":"KAIST, South Korea"}]},{"given":"Sung-Hwan","family":"Lee","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]},{"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"2016. nidhugg. https:\/\/github.com\/nidhugg\/nidhugg .  2016. nidhugg. https:\/\/github.com\/nidhugg\/nidhugg ."},{"key":"e_1_3_2_2_2_1","unstructured":"2019. promising-arm-riscv. https:\/\/github.com\/promising-arm-riscv .  2019. promising-arm-riscv. https:\/\/github.com\/promising-arm-riscv ."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0275-0"},{"key":"e_1_3_2_2_4_1","volume-title":"TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II . 56\u201374","author":"Abdulla Parosh Aziz","year":"2017","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Ahmed Bouajjani , and Tuan Phong Ngo . 2017 . Context-bounded analysis for POWER. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference , TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II . 56\u201374 . Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. 2017. Context-bounded analysis for POWER. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II . 56\u201374."},{"key":"e_1_3_2_2_5_1","volume-title":"CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II . 134\u2013156","author":"Abdulla Parosh Aziz","year":"2016","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Bengt Jonsson , and Carl Leonardsson . 2016 . Stateless model checking for POWER. In Computer Aided Verification - 28th International Conference , CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II . 134\u2013156 . Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. 2016. Stateless model checking for POWER. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II . 134\u2013156."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_3_2_2_8_1","volume-title":"CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings . 141\u2013157","author":"Alglave Jade","year":"2013","unstructured":"Jade Alglave , Daniel Kroening , and Michael Tautschnig . 2013 . Partial orders for efficient bounded model checking of concurrent software. In Computer Aided Verification - 25th International Conference , CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings . 141\u2013157 . Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial orders for efficient bounded model checking of concurrent software. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings . 141\u2013157."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177156"},{"key":"e_1_3_2_2_10_1","volume-title":"TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings . 41\u201344","author":"Alglave Jade","year":"2011","unstructured":"Jade Alglave , Luc Maranget , Susmit Sarkar , and Peter Sewell . 2011 . Litmus: running tests against hardware. In Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference , TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings . 41\u201344 . Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2011. Litmus: running tests against hardware. In Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings . 41\u201344."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594347"},{"key":"e_1_3_2_2_12_1","unstructured":"ARM. 2018. ARM Architecture Reference Manual.  ARM. 2018. ARM Architecture Reference Manual."},{"key":"e_1_3_2_2_13_1","volume-title":"POPL","author":"Armstrong Alasdair","year":"2019","unstructured":"Alasdair Armstrong , Thomas Bauereiss , Brian Campbell , Alastair Reid , Kathryn E. Gray , Robert M. Norton , Prashanth Mundkur , Mark Wassell , Jon French , Christopher Pulte , Shaked Flur , Ian Stark , Neel Krishnaswami , and Peter Sewell . 2019. ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS. PACMPL 3 , POPL ( 2019 ), 71:1\u201371:31. https:\/\/dl.acm.org\/citation.cfm?id=3290384 Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. 2019. ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS. PACMPL 3, POPL (2019), 71:1\u201371:31. https:\/\/dl.acm.org\/citation.cfm?id=3290384"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2006.26"},{"key":"e_1_3_2_2_15_1","volume-title":"ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings . 283\u2013307","author":"Batty Mark","year":"2015","unstructured":"Mark Batty , Kayvan Memarian , Kyndylan Nienhuis , Jean PichonPharabod , and Peter Sewell . 2015 . The problem of programming language concurrency semantics. In Programming Languages and Systems - 24th European Symposium on Programming , ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings . 283\u2013307 . Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean PichonPharabod, and Peter Sewell. 2015. The problem of programming language concurrency semantics. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings . 283\u2013307."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_2_17_1","volume-title":"Watson IBM Research Center and R. K. Treiber","author":"Thomas","year":"1986","unstructured":"Thomas J. Watson IBM Research Center and R. K. Treiber . 1986 . Systems programming: coping with parallelism . International Business Machines Incorporated, Thomas J. Watson Research Center . https:\/\/books. google.co.uk\/books?id=YQg3HAAACAAJ Thomas J. Watson IBM Research Center and R. K. Treiber. 1986. Systems programming: coping with parallelism . International Business Machines Incorporated, Thomas J. Watson Research Center. https:\/\/books. google.co.uk\/books?id=YQg3HAAACAAJ"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353522.1353528"},{"key":"e_1_3_2_2_19_1","volume-title":"Technical Report RC18638: A formal specification of the PowerPC shared memory architecture . Technical Report.","author":"Corella F.","year":"1993","unstructured":"F. Corella , J. M. Stone , and C. M. Barton . 1993 . Technical Report RC18638: A formal specification of the PowerPC shared memory architecture . Technical Report. F. Corella, J. M. Stone, and C. M. Barton. 1993. Technical Report RC18638: A formal specification of the PowerPC shared memory architecture . Technical Report."},{"key":"e_1_3_2_2_20_1","unstructured":"Will Deacon. 2016. The ARMv8 Application Level Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/ aarch64.cat .  Will Deacon. 2016. The ARMv8 Application Level Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/ aarch64.cat ."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009839"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_3_2_2_25_1","unstructured":"David Howells Paul E. McKenney Will Deacon and Peter Zijlstra. 2018. Documentation\/memory-barriers.txt. https:\/\/www.kernel.org\/ doc\/Documentation\/memory-barriers.txt .  David Howells Paul E. McKenney Will Deacon and Peter Zijlstra. 2018. Documentation\/memory-barriers.txt. https:\/\/www.kernel.org\/ doc\/Documentation\/memory-barriers.txt ."},{"key":"e_1_3_2_2_26_1","volume-title":"Alloy: A Logical Modelling Language. In ZB 2003: Formal Specification and Development in Z and B, Third International Conference of B and Z Users, Turku, Finland, June 4-6, 2003, Proceedings . 1.","author":"Jackson Daniel","year":"2003","unstructured":"Daniel Jackson . 2003 . Alloy: A Logical Modelling Language. In ZB 2003: Formal Specification and Development in Z and B, Third International Conference of B and Z Users, Turku, Finland, June 4-6, 2003, Proceedings . 1. Daniel Jackson. 2003. Alloy: A Logical Modelling Language. In ZB 2003: Formal Specification and Development in Z and B, Third International Conference of B and Z Users, Turku, Finland, June 4-6, 2003, Proceedings . 1."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934536"},{"key":"e_1_3_2_2_28_1","unstructured":"Jeehoon Kang. 2018. crossbeam-rfcs. https:\/\/github.com\/jeehoonkang\/ crossbeam-rfcs\/blob\/deque-proof\/text\/2018-01-07-deque-proof.md .  Jeehoon Kang. 2018. crossbeam-rfcs. https:\/\/github.com\/jeehoonkang\/ crossbeam-rfcs\/blob\/deque-proof\/text\/2018-01-07-deque-proof.md ."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_2_30_1","volume-title":"POPL","author":"Kokologiannakis Michalis","year":"2018","unstructured":"Michalis Kokologiannakis , Ori Lahav , Konstantinos Sagonas , and Viktor Vafeiadis . 2018. Effective stateless model checking for C\/C++ concurrency. PACMPL 2 , POPL ( 2018 ), 17:1\u201317:32. Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2018. Effective stateless model checking for C\/C++ concurrency. PACMPL 2, POPL (2018), 17:1\u201317:32."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2442516.2442524"},{"key":"e_1_3_2_2_33_1","unstructured":"Linux contributors. 2014. Documentation\/locking\/spinlocks.txt. https: \/\/www.kernel.org\/doc\/Documentation\/locking\/spinlocks.txt .  Linux contributors. 2014. Documentation\/locking\/spinlocks.txt. https: \/\/www.kernel.org\/doc\/Documentation\/locking\/spinlocks.txt ."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_3_2_2_35_1","unstructured":"Luc Maranget Susmit Sarkar and Peter Sewell. 2012. A Tutorial Introduction to the ARM and POWER Relaxed Memory Models. http: \/\/www.cl.cam.ac.uk\/~pes20\/ppc-supplemental\/test7.pdf  Luc Maranget Susmit Sarkar and Peter Sewell. 2012. A Tutorial Introduction to the ARM and POWER Relaxed Memory Models. http: \/\/www.cl.cam.ac.uk\/~pes20\/ppc-supplemental\/test7.pdf"},{"key":"e_1_3_2_2_36_1","volume-title":"Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing","author":"Maged","year":"1996","unstructured":"Maged M. Michael and Michael L. Scott. 1996. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms . In Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing , Philadelphia, Pennsylvania, USA , May 23-26, 1996 . 267\u2013275. Maged M. Michael and Michael L. Scott. 1996. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, Philadelphia, Pennsylvania, USA, May 23-26, 1996 . 267\u2013275."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2806886"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_2_42_1","unstructured":"Andrew Waterman and Krste Asanovi\u0107. 2018. The RISC-V instruction set manual volume I: user-level ISA .  Andrew Waterman and Krste Asanovi\u0107. 2018. The RISC-V instruction set manual volume I: user-level ISA ."},{"key":"e_1_3_2_2_43_1","volume-title":"Taming weak memory models. CoRR abs\/1606.05416","author":"Zhang Sizhuo","year":"2016","unstructured":"Sizhuo Zhang , Arvind, and Muralidaran Vijayaraghavan . 2016. Taming weak memory models. CoRR abs\/1606.05416 ( 2016 ). arXiv: 1606.05416 http:\/\/arxiv.org\/abs\/1606.05416 Sizhuo Zhang, Arvind, and Muralidaran Vijayaraghavan. 2016. Taming weak memory models. CoRR abs\/1606.05416 (2016). arXiv: 1606.05416 http:\/\/arxiv.org\/abs\/1606.05416"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2017.29"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314624","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314624","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314624"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":44,"alternative-id":["10.1145\/3314221.3314624","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314624","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}