{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:58Z","timestamp":1776305338546,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":56,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,4,4]],"date-time":"2017-04-04T00:00:00Z","timestamp":1491264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF- 1117147, CCF-1253700"],"award-info":[{"award-number":["CCF- 1117147, CCF-1253700"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR0011-13-3-0002 (through C-FAR, one of the six SRC STARnet Centers, sponsored by MARCO and DARPA)"],"award-info":[{"award-number":["HR0011-13-3-0002 (through C-FAR, one of the six SRC STARnet Centers, sponsored by MARCO and DARPA)"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,4,4]]},"DOI":"10.1145\/3037697.3037719","type":"proceedings-article","created":{"date-parts":[[2017,4,5]],"date-time":"2017-04-05T08:47:40Z","timestamp":1491382060000},"page":"119-133","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["TriCheck"],"prefix":"10.1145","author":[{"given":"Caroline","family":"Trippel","sequence":"first","affiliation":[{"name":"Princeton University, Princeton, NJ, USA"}]},{"given":"Yatin A.","family":"Manerkar","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, NJ, USA"}]},{"given":"Daniel","family":"Lustig","sequence":"additional","affiliation":[{"name":"NVIDIA, Santa Clara, CA, USA"}]},{"given":"Michael","family":"Pellauer","sequence":"additional","affiliation":[{"name":"NVIDIA, Westford, MA, USA"}]},{"given":"Margaret","family":"Martonosi","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, NJ, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,4,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Jade Alglave Luc Maranget and Michael Tautschnig. Herding cats: Modelling simulation testing and data mining for weak memory. ACM Transactions on Programming Languages and Systems (TOPLAS) 36(2):7:1--7:74 July 2014.  Jade Alglave Luc Maranget and Michael Tautschnig. Herding cats: Modelling simulation testing and data mining for weak memory. ACM Transactions on Programming Languages and Systems (TOPLAS) 36(2):7:1--7:74 July 2014.","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_3_1","unstructured":"ARM. ARM Cortex-A9 technical reference manual ARMv7-A 2008--2012. http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.ddi0388i\/DDI0388I_cortex_a9_r4p1_trm.pdf.  ARM. ARM Cortex-A9 technical reference manual ARMv7-A 2008--2012. http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.ddi0388i\/DDI0388I_cortex_a9_r4p1_trm.pdf."},{"key":"e_1_3_2_1_4_1","unstructured":"ARM. Cortex-A9 MPCore programmer advice notice read-after-read hazards. ARM Reference 761319. 2011. http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.uan0004a\/UAN0004A_a9_read_read.pdf.  ARM. Cortex-A9 MPCore programmer advice notice read-after-read hazards. ARM Reference 761319. 2011. http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.uan0004a\/UAN0004A_a9_read_read.pdf."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"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\/1555754.1555785"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065042"},{"key":"e_1_3_2_1_12_1","volume-title":"29th Conference on Programming Language Design and Implementation (PLDI)","author":"J.","year":"2008"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250662.1250697"},{"key":"e_1_3_2_1_14_1","volume-title":"USA","author":"Collier William W.","year":"1992"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2014.6835927"},{"key":"e_1_3_2_1_16_1","volume-title":"Stanford University","author":"Gharachorloo Kourosh","year":"1996"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325102"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2002.1106016"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/307338.300993"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2014.6835950"},{"key":"e_1_3_2_1_21_1","unstructured":"Martonosi Research Group. Check research tools and papers website 2017. http:\/\/check.cs.princeton.edu.  Martonosi Research Group. Check research tools and papers website 2017. http:\/\/check.cs.princeton.edu."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1028176.1006710"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541981"},{"key":"e_1_3_2_1_24_1","unstructured":"ISO\/IEC. Programming Languages -- C++ 2014.  ISO\/IEC. Programming Languages -- C++ 2014."},{"key":"e_1_3_2_1_25_1","volume-title":"MIT Press","author":"Jackson Daniel","year":"2012"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/139669.139676"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Ori Lahav Viktor Vafeiadis Jeehoon Kang Chung-Kil Hur and Derek Dreyer. Repairing sequential consistency in C\/C++11. MPI-SWS Tech. rep. MPI-SWS-2016-011 2016.  Ori Lahav Viktor Vafeiadis Jeehoon Kang Chung-Kil Hur and Derek Dreyer. Repairing sequential consistency in C\/C++11. MPI-SWS Tech. rep. MPI-SWS-2016-011 2016.","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2150976.2151006"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.38"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872399"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2749469.2750378"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037723"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830782"},{"key":"e_1_3_2_1_36_1","unstructured":"Yatin A. Manerkar Caroline Trippel Daniel Lustig Michael Pellauer and Margaret Martonosi. Counterexamples and proof loophole for the C\/C  Yatin A. Manerkar Caroline Trippel Daniel Lustig Michael Pellauer and Margaret Martonosi. Counterexamples and proof loophole for the C\/C"},{"key":"e_1_3_2_1_37_1","unstructured":"to POWER and armv7 trailing-sync compiler mappings. CoRR abs\/1611.01507 2016.  to POWER and armv7 trailing-sync compiler mappings. CoRR abs\/1611.01507 2016."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2001.991130"},{"key":"e_1_3_2_1_39_1","unstructured":"Paul E. McKenney and Raul Silvera. Example POWER implementation for C\/C++memory model 2011. http:\/\/www.rdrop.com\/users\/paulmck\/scalability\/paper\/N2745r.2011.03.04a.html.  Paul E. McKenney and Raul Silvera. Example POWER implementation for C\/C++memory model 2011. http:\/\/www.rdrop.com\/users\/paulmck\/scalability\/paper\/N2745r.2011.03.04a.html."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_1_43_1","volume-title":"29th European Conference on Object-Oriented Programming (ECOOP)","author":"Petri Gustavo","year":"2015"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/258492.258512"},{"key":"e_1_3_2_1_45_1","unstructured":"RISC-V Foundation. RISC-V port of Linux kernel 2016. https:\/\/github.com\/riscv\/riscv-linux\/blob\/master\/arch\/riscv\/include\/asm\/barrier.h.  RISC-V Foundation. RISC-V port of Linux kernel 2016. https:\/\/github.com\/riscv\/riscv-linux\/blob\/master\/arch\/riscv\/include\/asm\/barrier.h."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_1_48_1","unstructured":"Peter Sewell. C\/c++11 mappings to processors. 2016.  Peter Sewell. C\/c++11 mappings to processors. 2016."},{"key":"e_1_3_2_1_49_1","unstructured":"Peter Sewell et al. C\/C++11 mappings to processors 2016. https:\/\/www.cl.cam.ac.uk\/ pes20\/cpp\/cpp0xmappings.html.  Peter Sewell et al. C\/C++11 mappings to processors 2016. https:\/\/www.cl.cam.ac.uk\/ pes20\/cpp\/cpp0xmappings.html."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2012.6237045"},{"key":"e_1_3_2_1_51_1","volume-title":"USA","author":"International SPARC","year":"1994"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.461.0005"},{"key":"e_1_3_2_1_53_1","unstructured":"Linus Torvalds et al. Linux kernel 2016. https:\/\/github.com\/torvalds\/linux\/blob\/master\/arch\/alpha\/include\/asm\/barrier.h.  Linus Torvalds et al. Linux kernel 2016. https:\/\/github.com\/torvalds\/linux\/blob\/master\/arch\/alpha\/include\/asm\/barrier.h."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250662.1250696"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"}],"event":{"name":"ASPLOS '17: Architectural Support for Programming Languages and Operating Systems","location":"Xi'an China","acronym":"ASPLOS '17","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-Second International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3037697.3037719","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3037697.3037719","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3037697.3037719","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:50:27Z","timestamp":1750204227000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3037697.3037719"}},"subtitle":["Memory Model Verification at the Trisection of Software, Hardware, and ISA"],"short-title":[],"issued":{"date-parts":[[2017,4,4]]},"references-count":56,"alternative-id":["10.1145\/3037697.3037719","10.1145\/3037697"],"URL":"https:\/\/doi.org\/10.1145\/3037697.3037719","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093337.3037719","asserted-by":"object"},{"id-type":"doi","id":"10.1145\/3093336.3037719","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,4,4]]},"assertion":[{"value":"2017-04-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}