{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:39:46Z","timestamp":1773193186921,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,3,25]],"date-time":"2017-03-25T00:00:00Z","timestamp":1490400000000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CAREER-1253700, CCF-1117147"],"award-info":[{"award-number":["CAREER-1253700, CCF-1117147"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["HR0011-13-3-0002"],"award-info":[{"award-number":["HR0011-13-3-0002"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,3,25]]},"DOI":"10.1145\/2872362.2872399","type":"proceedings-article","created":{"date-parts":[[2016,3,28]],"date-time":"2016-03-28T09:24:30Z","timestamp":1459157070000},"page":"233-247","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":53,"title":["COATCheck"],"prefix":"10.1145","author":[{"given":"Daniel","family":"Lustig","sequence":"first","affiliation":[{"name":"Princeton University, Princeton, NJ, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geet","family":"Sethi","sequence":"additional","affiliation":[{"name":"Rutgers University, New Brunswick, NJ, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Margaret","family":"Martonosi","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, NJ, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abhishek","family":"Bhattacharjee","sequence":"additional","affiliation":[{"name":"Rutgers University, New Brunswick, NJ, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,3,25]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_3_2_1_2_1","volume-title":"A formal hierarchy of weak memory models. Formal Methods in System Design (FMSD), 41 (2): 178--210","author":"Alglave J.","year":"2012","unstructured":"J. Alglave. A formal hierarchy of weak memory models. Formal Methods in System Design (FMSD), 41 (2): 178--210, 2012."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694391"},{"key":"e_1_3_2_1_5_1","volume-title":"Publication number 25759. Revision: 3.79","author":"AMD.","year":"2009","unstructured":"AMD. Revision guide for AMD Athlon 64 and AMD Opteron processors. Publication number 25759. Revision: 3.79. 2009. URL http:\/\/support.amd.com\/TechDocs\/25759.pdf."},{"key":"e_1_3_2_1_6_1","volume-title":"publication number 41322. revision: 3.92","author":"AMD.","year":"2012","unstructured":"AMD. Revision guide for AMD family 10h processors. publication number 41322. revision: 3.92. 2012."},{"key":"e_1_3_2_1_7_1","unstructured":"AMD. AMD64 architecture programmer's manual. http:\/\/developer.amd.com\/resources\/documentation-articles\/developer-guides-manuals\/ 2013."},{"key":"e_1_3_2_1_8_1","volume-title":"Java memory model examples: Good, bad and ugly. ph1st International Workshop on Verification and Analysis of Multi-threaded Java-like Programs (VAMP)","author":"Aspinall D.","year":"2007","unstructured":"D. Aspinall and J. Sevcik. Java memory model examples: Good, bad and ugly. ph1st International Workshop on Verification and Analysis of Multi-threaded Java-like Programs (VAMP), 2007."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_3_2_1_11_1","volume-title":"HSA memory model. Hot Chips Tutorial","author":"Gaster Benedict R.","year":"2013","unstructured":"Benedict R. Gaster. HSA memory model. Hot Chips Tutorial, 2013. URL http:\/\/hsafoundation.com\/hot-chips-2013-hsa-foundation-presented-deeper-detail-hsa-hsail\/."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1736020.1736060"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_3_2_1_14_1","volume-title":"A machine program for theorem-proving. Communications of the ACM, 5 (7)","author":"Davis M.","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5 (7), 1962."},{"key":"e_1_3_2_1_15_1","volume-title":"International Conference on Parallel Processing (ICPP)","author":"Gharachorloo K.","year":"1991","unstructured":"K. Gharachorloo, A. Gupta, and J. Hennessy. Two techniques to enhance the performance of memory consistency models. International Conference on Parallel Processing (ICPP), 1991."},{"key":"e_1_3_2_1_16_1","volume-title":"Oct. 21","author":"Glew A.","year":"1997","unstructured":"A. Glew, G. Hinton, and H. Akkary. Method and apparatus for performing page table walks in a microprocessor capable of processing speculative instructions, Oct. 21 1997. URL https:\/\/www.google.com\/patents\/US5680565. US Patent 5,680,565."},{"key":"e_1_3_2_1_17_1","volume-title":"Intel 64 architecture memory ordering white paper","year":"2007","unstructured":"Intel. Intel 64 architecture memory ordering white paper. 2007. SKU 318147-001."},{"key":"e_1_3_2_1_18_1","volume-title":"Intel Core Duo processor and Intel Core Solo processor on 65 nm process specification update. Document number 309222. Revision number 20","year":"2009","unstructured":"Intel. Intel Core Duo processor and Intel Core Solo processor on 65 nm process specification update. Document number 309222. Revision number 20., 2009."},{"key":"e_1_3_2_1_19_1","volume-title":"Intel 64 and IA-32 architectures optimization reference manual","year":"2013","unstructured":"Intel. Intel 64 and IA-32 architectures optimization reference manual, 2013."},{"key":"e_1_3_2_1_20_1","volume-title":"Intel 64 and IA-32 architectures software developer's manual","year":"2013","unstructured":"Intel. Intel 64 and IA-32 architectures software developer's manual, 2013."},{"key":"e_1_3_2_1_21_1","volume-title":"Intel Xeon processor E5 product family specification update. Reference number 326510-018","year":"2015","unstructured":"Intel. Intel Xeon processor E5 product family specification update. Reference number 326510-018., 2015."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2749469.2749471"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_24_1","volume-title":"Correct and efficient bounded FIFO queues. ph25th Symposium on Computer Architecture and High-Performance Computing (SBAC-PAD)","author":"L\u00ea N. M.","year":"2013","unstructured":"N. M. L\u00ea, A. Guatto, A. Cohen, and A. Pop. Correct and efficient bounded FIFO queues. ph25th Symposium on Computer Architecture and High-Performance Computing (SBAC-PAD), 2013."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2442516.2442524"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.38"},{"key":"e_1_3_2_1_27_1","volume-title":"Verifying correct microarchitectural enforcement of memory consistency models","author":"Lustig D.","year":"2014","unstructured":"D. Lustig, M. Pellauer, and M. Martonosi. Verifying correct microarchitectural enforcement of memory consistency models. IEEE Micro Top Picks of 2014, 35 (3): 72--82, May 2015."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830782"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_2_1_31_1","volume-title":"November","author":"McKenney P. E.","year":"2014","unstructured":"P. E. McKenney, T. Riegel, J. Preshing, H. Boehm, C. Nelson, and O. Giroux. Towards implementation and use of memory_order_consume. ISO SC22 WG21 N4321, November 2014."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2012.32"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541942"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2014.6835965"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1002\/1096-9128(200005)12:6<445::AID-CPE484>3.0.CO;2-A"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2010.5416643"},{"key":"e_1_3_2_1_38_1","volume-title":"Specifying and dynamically verifying address translation-aware memory consistency. In ph15th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"Romanescu B. F.","year":"2010","unstructured":"B. F. Romanescu, A. R. Lebeck, and D. J. Sorin. Specifying and dynamically verifying address translation-aware memory consistency. In ph15th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2010."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2010.99"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/339647.339666"},{"key":"e_1_3_2_1_42_1","volume-title":"NVIDIA GPU Technology Conference","author":"Schroeder T. C.","year":"2011","unstructured":"T. C. Schroeder. Peer-to-peer & unified virtual addressing. NVIDIA GPU Technology Conference, 2011."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_1_44_1","volume-title":"The Coq proof assistant reference manual, version 8.0. LogiCal Project","author":"The Coq","year":"2004","unstructured":"The Coq development team. The Coq proof assistant reference manual, version 8.0. LogiCal Project, 2004. URL http:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_45_1","volume-title":"A don't (diy) tutorial, version 5.01","author":"The","year":"2012","unstructured":"The diy development team. A don't (diy) tutorial, version 5.01, 2012. http:\/\/diy.inria.fr\/doc\/index.html."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2011.65"}],"event":{"name":"ASPLOS '16: Architectural Support for Programming Languages and Operating Systems","location":"Atlanta Georgia USA","acronym":"ASPLOS '16","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-First International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2872362.2872399","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2872362.2872399","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2872362.2872399","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:40:52Z","timestamp":1763458852000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2872362.2872399"}},"subtitle":["Verifying Memory Ordering at the Hardware-OS Interface"],"short-title":[],"issued":{"date-parts":[[2016,3,25]]},"references-count":46,"alternative-id":["10.1145\/2872362.2872399","10.1145\/2872362"],"URL":"https:\/\/doi.org\/10.1145\/2872362.2872399","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2980024.2872399","asserted-by":"object"},{"id-type":"doi","id":"10.1145\/2954679.2872399","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,3,25]]},"assertion":[{"value":"2016-03-25","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}