{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:45:13Z","timestamp":1773193513004,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,3,9]],"date-time":"2020-03-09T00:00:00Z","timestamp":1583712000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,3,9]]},"DOI":"10.1145\/3373376.3378480","type":"proceedings-article","created":{"date-parts":[[2020,3,13]],"date-time":"2020-03-13T22:37:01Z","timestamp":1584139021000},"page":"1157-1171","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["HMC"],"prefix":"10.1145","author":[{"given":"Michalis","family":"Kokologiannakis","sequence":"first","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}]}],"member":"320","published-online":{"date-parts":[[2020,3,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3073408"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_8"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_3_2_1_6_1","volume-title":"CAV","author":"Albert Elvira","year":"2018"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"e_1_3_2_1_8_1","volume-title":"ASPLOS","author":"Alglave Jade","year":"2018"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_14"},{"key":"e_1_3_2_1_11_1","volume-title":"POPL","author":"Batty Mark","year":"2011"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062353"},{"key":"e_1_3_2_1_13_1","volume-title":"PLDI","author":"Burckhardt Sebastian","year":"2007"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290383"},{"key":"e_1_3_2_1_15_1","volume-title":"Proc. ACM Program. Lang., 2, POPL, Article 31","author":"Chalupa Marek","year":"2017"},{"key":"e_1_3_2_1_16_1","volume-title":"Choosing linux for medical devices. [Online","author":"Harold Ken","year":"2019"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_1_19_1","volume-title":"CAV","author":"Gavrilenko Natalia","year":"2019"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/271771.271800"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737975"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984025"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_1_26_1","volume-title":"Proc. ACM Program. Lang., 2, POPL, Article 17","author":"Kokologiannakis Michalis","year":"2017"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00514-6"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_1_30_1","article-title":"How to make a multiprocessor computer that correctly executes multiprocess programs","volume":"28","author":"Lamport Leslie","year":"1979","journal-title":"IEEE Trans. Computers"},{"key":"e_1_3_2_1_31_1","volume-title":"OSDI","author":"Musuvathi Madanlal","year":"2008"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_3_2_1_35_1","first-page":"1","article-title":"Simplifying ARM concurrency: Multicopy- atomic axiomatic and operational models for ARMv8","volume":"19","author":"Pulte Christopher","year":"2018","journal-title":"Proc. ACM Program. Lang., 2, POPL"},{"key":"e_1_3_2_1_36_1","volume-title":"PLDI","author":"Pulte Christopher","year":"2019"},{"key":"e_1_3_2_1_37_1","volume-title":"RISC-V, Power, and x86. [Online","year":"2019"},{"key":"e_1_3_2_1_38_1","volume-title":"CONCUR 2015 (LIPIcs).","volume":"42","author":"Rodr\u00edguez C\u00e9sar","year":"2015"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_1_40_1","volume-title":"The SPARC architecture manual (version 9)","author":"SPARC International Inc. 1994."},{"key":"e_1_3_2_1_41_1","volume-title":"Competition on software verification (SV-COMP). [Online","author":"SV-COMP.","year":"2019"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037719"},{"key":"e_1_3_2_1_43_1","unstructured":"Andrew Waterman and Krste Asanovi?. 2019. The RISC-V Instruction Set Manual Volume I: User-level ISA. https:\/\/content.riscv.org\/wpcontent\/ uploads\/2019\/06\/riscv-spec.pdf.  Andrew Waterman and Krste Asanovi?. 2019. The RISC-V Instruction Set Manual Volume I: User-level ISA. https:\/\/content.riscv.org\/wpcontent\/ uploads\/2019\/06\/riscv-spec.pdf."},{"key":"e_1_3_2_1_44_1","volume-title":"Constantinides","author":"Wickerson John","year":"2017"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737956"}],"event":{"name":"ASPLOS '20: Architectural Support for Programming Languages and Operating Systems","location":"Lausanne Switzerland","acronym":"ASPLOS '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGOPS ACM Special Interest Group on Operating Systems","SIGARCH ACM Special Interest Group on Computer Architecture","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373376.3378480","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373376.3378480","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:32:59Z","timestamp":1750199579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373376.3378480"}},"subtitle":["Model Checking for Hardware Memory Models"],"short-title":[],"issued":{"date-parts":[[2020,3,9]]},"references-count":45,"alternative-id":["10.1145\/3373376.3378480","10.1145\/3373376"],"URL":"https:\/\/doi.org\/10.1145\/3373376.3378480","relation":{},"subject":[],"published":{"date-parts":[[2020,3,9]]},"assertion":[{"value":"2020-03-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}