{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:09Z","timestamp":1775873409626,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T00:00:00Z","timestamp":1554336000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100011030","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["B620719"],"award-info":[{"award-number":["B620719"]}],"id":[{"id":"10.13039\/100011030","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,4,4]]},"DOI":"10.1145\/3297858.3304043","type":"proceedings-article","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T18:38:43Z","timestamp":1554403123000},"page":"257-270","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":47,"title":["A Formal Analysis of the NVIDIA PTX Memory Consistency Model"],"prefix":"10.1145","author":[{"given":"Daniel","family":"Lustig","sequence":"first","affiliation":[{"name":"NVIDIA, Santa Clara, CA, USA"}]},{"given":"Sameer","family":"Sahasrabuddhe","sequence":"additional","affiliation":[{"name":"NVIDIA, Santa Clara, CA, USA"}]},{"given":"Olivier","family":"Giroux","sequence":"additional","affiliation":[{"name":"NVIDIA, Santa Clara, CA, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,4,4]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2017. CppMem: Interactive C\/C++ Memory Model. http:\/\/svr-pes20-cppmem.cl.cam.ac.uk\/cppmem."},{"key":"e_1_3_2_1_2_1","unstructured":"2017. diy Release Seven.http:\/\/diy.inria.fr\/."},{"key":"e_1_3_2_1_3_1","unstructured":"2017. Lem a Tool for Lightweight Executable Mathematics.http:\/\/www.cl.cam.ac.uk\/~pes20\/lem."},{"key":"e_1_3_2_1_4_1","unstructured":"2017. The Coq Proof Assistant. https:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_5_1","unstructured":"2017. The HOL Interactive Theorem Prover. https:\/\/hol-theorem-prover.org."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694391"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_10_1","volume-title":"Integrating Model Checking and Theorem Proving for Relational Reasoning. International Conference on Relational Methods in Computer Science (RelMiCS).","author":"Arkoudas Konstantine","year":"2003","unstructured":"Konstantine Arkoudas, Sarfraz Khurshid, Darko Marinov, and Martin Rinard. 2003. Integrating Model Checking and Theorem Proving for Relational Reasoning. International Conference on Relational Methods in Computer Science (RelMiCS)."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2003476.2003493"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_3_2_1_19_1","volume-title":"Paul McKenney and others {sic}","author":"Boehm J.","year":"2018","unstructured":"Hans-J. Boehm, Olivier Giroux, Viktor Vafeiadis, and with in-put from Will Deacon, Doug Lea, Daniel Lustig, Paul McKenney and others {sic}. 2018. P0668R3: Revising the C++ memory model. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2018\/p0668r3.html.ISO\/JTC1\/SC22\/WG21(2018)."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/2584504"},{"key":"e_1_3_2_1_21_1","volume-title":"Mixed-size Concurrency: ARM, POWER, C\/C++11, and SC.","author":"Flur Shaked","year":"2017","unstructured":"Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E Gray, Ali Sezgin, Mark Batty, and Peter Sewell. 2017. Mixed-size Concurrency: ARM, POWER, C\/C++11, and SC. (2017)."},{"key":"e_1_3_2_1_22_1","unstructured":"HSA Foundation. 2017. Heterogeneous System Architecture. http:\/\/www.hsafoundation.com\/standards."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2021296.2021312"},{"key":"e_1_3_2_1_24_1","unstructured":"Khronos Group. 2017. OpenCL 2.2.https:\/\/www.khronos.org\/opencl."},{"key":"e_1_3_2_1_25_1","volume-title":"Unified Memory for CUDA Beginners.NVIDIA Developer Blog","author":"Harris Mark","year":"2017","unstructured":"Mark Harris. 2017. Unified Memory for CUDA Beginners.NVIDIA Developer Blog (2017). https:\/\/devblogs.nvidia.com\/unified-memory-cuda-beginners."},{"key":"e_1_3_2_1_26_1","volume-title":"Cooperative Groups: Flexible CUDA Thread Programming. NVIDIA Developer Blog","author":"Harris Mark","year":"2017","unstructured":"Mark Harris and Kyrylo Perelygin. 2017. Cooperative Groups: Flexible CUDA Thread Programming. NVIDIA Developer Blog (2017). https:\/\/devblogs.nvidia.com\/cooperative-groups."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541981"},{"key":"e_1_3_2_1_28_1","first-page":"2011","article-title":"Information technology -- Programming languages -- C++","volume":"14882","author":"International Organization for Standardization (ISO).","year":"2011","unstructured":"International Organization for Standardization (ISO). 2011. Information technology -- Programming languages -- C++, ISO\/IEC 14882:2011. Technical Report.","journal-title":"ISO\/IEC"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Ori Lahav Viktor Vafeiadis Jeehoon Kang Chung-Kil Hur and Derek Dreyer. 2017. Repairing Sequential Consistency in C\/C++11. (2017).","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.38"},{"key":"e_1_3_2_1_34_1","unstructured":"Daniel Lustig Sameer Sahasrabuddhe and Olivier Giroux. 2017. Supplemental material. https:\/\/github.com\/nvlabs\/ptxmemorymodel."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037723"},{"key":"e_1_3_2_1_36_1","volume-title":"Counterexamples and Proof Loop-hole for the C\/C++ to POWER and ARMv7 Trailing-sync Compiler Mappings. arXiv1611.01507v2 (Nov","author":"Manerkar Yatin A.","year":"2016","unstructured":"Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer,and Margaret Martonosi. 2016. Counterexamples and Proof Loop-hole for the C\/C++ to POWER and ARMv7 Trailing-sync Compiler Mappings. arXiv1611.01507v2 (Nov 2016)."},{"key":"e_1_3_2_1_37_1","volume-title":"Relational Constraint Solving in SMT. 26th International Conference on Automated Deduction (CADE).","author":"Meng Baoluo","year":"2017","unstructured":"Baoluo Meng, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. 2017. Relational Constraint Solving in SMT. 26th International Conference on Automated Deduction (CADE)."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544136"},{"key":"e_1_3_2_1_39_1","unstructured":"NVIDIA. 2017. CUDA C Programming Guide. https:\/\/docs.nvidia.com\/cuda\/cuda-c-programming-guide."},{"key":"e_1_3_2_1_40_1","unstructured":"NVIDIA. 2017. Parallel Thread Execution ISA Version 6.0. http:\/\/docs.nvidia.com\/cuda\/parallel-thread-execution\/index.html."},{"key":"e_1_3_2_1_42_1","unstructured":"Oracle. 2017. Java Language and Virtual Machine Specifications. https:\/\/docs.oracle.com\/javase\/specs\/."},{"key":"e_1_3_2_1_43_1","volume-title":"Languages & Applications Conference (OOPSLA)","author":"Ou Peizhao","year":"2018","unstructured":"Peizhao Ou and Brian Demsky. 2018. Towards Understanding the Costs of Avoiding Out-of-Thin-Air Results. Object-Oriented Programming, Systems, Languages & Applications Conference (OOPSLA) (2018)."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_1_45_1","volume-title":"Cookingthe Books: Formalizing JMM Implementation Recipes. 29th European Conference on Object-Oriented Programming (ECOOP)(2015)","author":"Petri Gustavo","year":"2015","unstructured":"Gustavo Petri, Jan Vitek, and Suresh Jagannathan. 2015. Cookingthe Books: Formalizing JMM Implementation Recipes. 29th European Conference on Object-Oriented Programming (ECOOP)(2015)."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830821"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3079856.3080206"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908114"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/2028905"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763571"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037719"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_29"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"}],"event":{"name":"ASPLOS '19: Architectural Support for Programming Languages and Operating Systems","location":"Providence RI USA","acronym":"ASPLOS '19","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-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3297858.3304043","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3297858.3304043","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3297858.3304043","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:14Z","timestamp":1750204394000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3297858.3304043"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,4]]},"references-count":50,"alternative-id":["10.1145\/3297858.3304043","10.1145\/3297858"],"URL":"https:\/\/doi.org\/10.1145\/3297858.3304043","relation":{},"subject":[],"published":{"date-parts":[[2019,4,4]]},"assertion":[{"value":"2019-04-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}