{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:38Z","timestamp":1772164058099,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":80,"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":[{"DOI":"10.13039\/100008885","name":"Lloyd's Register Foundation","doi-asserted-by":"publisher","award":["Research Fellowship (Mark Batty)"],"award-info":[{"award-number":["Research Fellowship (Mark Batty)"]}],"id":[{"id":"10.13039\/100008885","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000287","name":"Royal Academy of Engineering","doi-asserted-by":"publisher","award":["Research Fellowship (Mark Batty), Research Chair (George A. Constantinides)"],"award-info":[{"award-number":["Research Fellowship (Mark Batty), Research Chair (George A. Constantinides)"]}],"id":[{"id":"10.13039\/501100000287","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100002418","name":"Intel Corporation","doi-asserted-by":"publisher","award":["Gift"],"award-info":[{"award-number":["Gift"]}],"id":[{"id":"10.13039\/100002418","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/I020357\/1, EP\/K034448\/1, EP\/K015168\/1, Impact Acceleration Award"],"award-info":[{"award-number":["EP\/I020357\/1, EP\/K034448\/1, EP\/K015168\/1, Impact Acceleration Award"]}],"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":[[2017,1]]},"DOI":"10.1145\/3009837.3009838","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"190-204","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":75,"title":["Automatically comparing memory consistency models"],"prefix":"10.1145","author":[{"given":"John","family":"Wickerson","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Mark","family":"Batty","sequence":"additional","affiliation":[{"name":"University of Kent, UK"}]},{"given":"Tyler","family":"Sorensen","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"George A.","family":"Constantinides","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"Supplementary material for this paper is available in the ACM digital library and in the following GitHub repository.  Supplementary material for this paper is available in the ACM digital library and in the following GitHub repository."},{"key":"e_1_3_2_2_2_1","first-page":"12","article-title":"Rodin: an open toolset for modelling and reasoning in Event-B","author":"Abrial Jean-Raymond","year":"2010","unstructured":"Jean-Raymond Abrial , Michael Butler , Stefan Hallerstede , Thai Son Hoang , Farhad Mehta , and Laurent Voisin . \u201c Rodin: an open toolset for modelling and reasoning in Event-B \u201d. In: Int. J. Softw. Tools Technol. Transfer 12 ( 2010 ). Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. \u201cRodin: an open toolset for modelling and reasoning in Event-B\u201d. In: Int. J. Softw. Tools Technol. Transfer 12 (2010).","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/165231.165264"},{"key":"e_1_3_2_2_7_1","volume-title":"Techniques, &amp","author":"Aho Alfred V.","year":"2006","unstructured":"Alfred V. Aho , Monica S. Lam , Ravi Sethi , and Jeffrey D. Ullman . Compilers: Principles , Techniques, &amp ; Tools. Second edition. Addison-Wesley , 2006 . Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, & Tools. Second edition. Addison-Wesley, 2006."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0161-5"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694391"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_2_13_1","volume-title":"Int. Joint Conf. on Artificial Intelligence (IJCAI).","author":"Audemard Gilles","year":"2009","unstructured":"Gilles Audemard and Laurent Simon . \u201c Predicting Learnt Clauses Quality in Modern SAT Solvers \u201d. In: Int. Joint Conf. on Artificial Intelligence (IJCAI). 2009 . Gilles Audemard and Laurent Simon. \u201cPredicting Learnt Clauses Quality in Modern SAT Solvers\u201d. In: Int. Joint Conf. on Artificial Intelligence (IJCAI). 2009."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"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":"PicoSAT and PrecoSAT at SAT Race","author":"Biere Armin","year":"2010","unstructured":"Armin Biere . Lingeling, Plingeling , PicoSAT and PrecoSAT at SAT Race 2010 . Tech. rep. 10\/1. Institute for Formal Models and Verification, Johannes Kepler University , 2010. Armin Biere. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Tech. rep. 10\/1. Institute for Formal Models and Verification, Johannes Kepler University, 2010."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2003476.2003493"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_3_2_2_20_1","volume-title":"Synthesizing Memory Models from Litmus Tests. Tech. rep. UW-CSE-16-10-01","author":"Bornholt James","year":"2016","unstructured":"James Bornholt and Emina Torlak . Synthesizing Memory Models from Litmus Tests. Tech. rep. UW-CSE-16-10-01 . University of Washington , 2016 . James Bornholt and Emina Torlak. Synthesizing Memory Models from Litmus Tests. Tech. rep. UW-CSE-16-10-01. University of Washington, 2016."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11970-5_7"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854038.2854051"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/129082"},{"key":"e_1_3_2_2_24_1","unstructured":"Ashish Darbari Iain Singleton Michael Butler and John Colley. \u201cFormal Modelling Testing and Verification of HSA Memory Models using Event-B\u201d. Draft. 2016.  Ashish Darbari Iain Singleton Michael Butler and John Colley. \u201cFormal Modelling Testing and Verification of HSA Memory Models using Event-B\u201d. Draft. 2016."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_3_2_2_26_1","volume-title":"Theory and Applications of Satisfiability Testing (SAT).","author":"E\u00e9n Niklas","year":"2003","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson . \u201c An Extensible SATsolver \u201d. In: Theory and Applications of Satisfiability Testing (SAT). 2003 . Niklas E\u00e9n and Niklas S\u00f6rensson. \u201cAn Extensible SATsolver\u201d. In: Theory and Applications of Satisfiability Testing (SAT). 2003."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2014.6835930"},{"key":"e_1_3_2_2_30_1","volume-title":"Computer Architecture: A Quantitative Approach","author":"Hennessy John L.","year":"2012","unstructured":"John L. Hennessy and David A. Patterson . Computer Architecture: A Quantitative Approach . Fifth edition. Morgan Kaufmann , 2012 . John L. Hennessy and David A. Patterson. Computer Architecture: A Quantitative Approach. Fifth edition. Morgan Kaufmann, 2012."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1189736.1189737"},{"key":"e_1_3_2_2_32_1","volume-title":"Int. Conf. on Parallel and Distributed Computing Systems (PDCS).","author":"Higham Lisa","year":"1997","unstructured":"Lisa Higham , Jalal Kawash , and Nathaly Verwaal . \u201c Defining and Comparing Memory Consistency Models \u201d. In: Int. Conf. on Parallel and Distributed Computing Systems (PDCS). 1997 . Lisa Higham, Jalal Kawash, and Nathaly Verwaal. \u201cDefining and Comparing Memory Consistency Models\u201d. In: Int. Conf. on Parallel and Distributed Computing Systems (PDCS). 1997."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541981"},{"key":"e_1_3_2_2_35_1","volume-title":"HSA Platform System Architecture Specification. Version 1.0","author":"Foundation HSA","year":"2015","unstructured":"HSA Foundation . HSA Platform System Architecture Specification. Version 1.0 , 2015 . HSA Foundation. HSA Platform System Architecture Specification. Version 1.0, 2015."},{"key":"e_1_3_2_2_36_1","unstructured":"IBM. Power ISA (Version 2.06B). 2010.  IBM. Power ISA (Version 2.06B). 2010."},{"key":"e_1_3_2_2_37_1","volume-title":"Programming languages \u2013 C++. Draft N3092","author":"IEC.","year":"2010","unstructured":"ISO\/ IEC. Programming languages \u2013 C++. Draft N3092 , 2010 . ISO\/IEC. Programming languages \u2013 C++. Draft N3092, 2010."},{"key":"e_1_3_2_2_38_1","volume-title":"International standard 9899:2011","author":"IEC.","year":"2011","unstructured":"ISO\/ IEC. Programming languages \u2013 C . International standard 9899:2011 , 2011 . ISO\/IEC. Programming languages \u2013 C. International standard 9899:2011, 2011."},{"key":"e_1_3_2_2_39_1","volume-title":"Software Abstractions \u2013 Logic, Language, and Analysis. Revised edition","author":"Jackson Daniel","year":"2012","unstructured":"Daniel Jackson . Software Abstractions \u2013 Logic, Language, and Analysis. Revised edition . MIT Press , 2012 . Daniel Jackson. Software Abstractions \u2013 Logic, Language, and Analysis. Revised edition. MIT Press, 2012."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934536"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_2_42_1","volume-title":"The OpenCL Specification. Version 2.0","author":"Khronos Group","year":"2013","unstructured":"Khronos Group . The OpenCL Specification. Version 2.0 , 2013 . Khronos Group. The OpenCL Specification. Version 2.0, 2013."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_3_2_2_44_1","volume-title":"MPI-SWS","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. Tech. rep. MPI-SWS-2016-011 . MPI-SWS , 2016 . Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. Repairing Sequential Consistency in C\/C++11. Tech. rep. MPI-SWS-2016-011. MPI-SWS, 2016."},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.38"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2749469.2750378"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_26"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024842"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_3_2_2_51_1","unstructured":"Yatin A. Manerkar Caroline Trippel Daniel Lustig Michael Pellauer and Margaret Martonosi. \u201cCounterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings\u201d. 2016.  Yatin A. Manerkar Caroline Trippel Daniel Lustig Michael Pellauer and Margaret Martonosi. \u201cCounterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings\u201d. 2016."},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/2818754.2818829"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-2639-4_4"},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.003"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491967"},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/90417.90741"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983997"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_18"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_3_2_2_61_1","volume-title":"Parallel Thread Execution ISA, version 4.3","author":"NVIDIA.","year":"2015","unstructured":"NVIDIA. Parallel Thread Execution ISA, version 4.3 . 2015 . NVIDIA. Parallel Thread Execution ISA, version 4.3. 2015."},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694350"},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_3_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_3_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_3_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908114"},{"key":"e_1_3_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/2028905"},{"key":"e_1_3_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.2307\/2268577"},{"key":"e_1_3_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806635"},{"key":"e_1_3_2_2_76_1","unstructured":"Caroline Trippel Yatin A. Manerkar Daniel Lustig Michael Pellauer and Margaret Martonosi. \u201cExploring the Trisection of Software Hardware and ISA in Memory Model Design\u201d. Draft. 2016.  Caroline Trippel Yatin A. Manerkar Daniel Lustig Michael Pellauer and Margaret Martonosi. \u201cExploring the Trisection of Software Hardware and ISA in Memory Model Design\u201d. Draft. 2016."},{"key":"e_1_3_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_3_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/800135.804393"},{"key":"e_1_3_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993534"},{"key":"e_1_3_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_3"},{"key":"e_1_3_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926393"},{"key":"e_1_3_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814283"},{"key":"e_1_3_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2004.1302944"}],"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.3009838","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009838","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.3009838"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":80,"alternative-id":["10.1145\/3009837.3009838","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009838","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009838","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"}}]}}