{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:08Z","timestamp":1775873408787,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,6,14]],"date-time":"2017-06-14T00:00:00Z","timestamp":1497398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-2-0032"],"award-info":[{"award-number":["FA8750-16-2-0032"]}],"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,6,14]]},"DOI":"10.1145\/3062341.3062353","type":"proceedings-article","created":{"date-parts":[[2017,6,14]],"date-time":"2017-06-14T10:01:04Z","timestamp":1497434464000},"page":"467-481","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":41,"title":["Synthesizing memory models from framework sketches and Litmus tests"],"prefix":"10.1145","author":[{"given":"James","family":"Bornholt","sequence":"first","affiliation":[{"name":"University of Washington, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,6,14]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0161-5"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-18941-3_3"},{"key":"e_1_3_2_2_4_1","volume-title":"The Phat Experiment. http: \/\/diy.inria.fr\/phat\/","author":"Alglave J.","year":"2010","unstructured":"J. Alglave and L. Maranget . The Phat Experiment. http: \/\/diy.inria.fr\/phat\/ , 2010 . J. Alglave and L. Maranget. The Phat Experiment. http: \/\/diy.inria.fr\/phat\/, 2010."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987389.1987395"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"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","volume-title":"July","author":"Alur R.","year":"2016","unstructured":"R. Alur and M. M. K. Martin . Personal communication , July 2016 . R. Alur and M. M. K. Martin. Personal communication, July 2016."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837666"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987389.1987393"},{"key":"e_1_3_2_2_16_1","volume-title":"Alpha Architecture Reference Manual","year":"2002","unstructured":"Compaq. Alpha Architecture Reference Manual . 4 th edition, 2002 . Compaq. Alpha Architecture Reference Manual. 4th edition, 2002.","edition":"4"},{"key":"e_1_3_2_2_17_1","volume-title":"KR","author":"Crawford J.","year":"1996","unstructured":"J. Crawford , M. Ginsberg , E. Luks , and A. Roy . Symmetrybreaking predicates for search problems . In KR , 1996 . J. Crawford, M. Ginsberg, E. Luks, and A. Roy. Symmetrybreaking predicates for search problems. In KR, 1996."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_25"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_3_2_2_22_1","unstructured":"IBM. Power ISA Version 2.06 Revision B. IBM 2010.  IBM. Power ISA Version 2.06 Revision B. IBM 2010."},{"key":"e_1_3_2_2_23_1","volume-title":"Intel 64 and IA-32 Architectures Software Developer\u2019s Manual","author":"Intel Corporation","year":"2015","unstructured":"Intel Corporation . Intel 64 and IA-32 Architectures Software Developer\u2019s Manual . Intel Corporation , 2015 . Revision 53. Intel Corporation. Intel 64 and IA-32 Architectures Software Developer\u2019s Manual. Intel Corporation, 2015. Revision 53."},{"key":"e_1_3_2_2_24_1","volume-title":"Software Abstractions: logic, language, and analysis","author":"Jackson D.","year":"2009","unstructured":"D. Jackson . Software Abstractions: logic, language, and analysis . MIT Press , 2 nd edition, 2009 . D. Jackson. Software Abstractions: logic, language, and analysis. MIT Press, 2nd edition, 2009.","edition":"2"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.38"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037723"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_26"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024842"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_2_2_32_1","volume-title":"Linux Plumbers Conference","author":"McKenney P. E.","year":"2016","unstructured":"P. E. McKenney . A Formal Model of Linux-Kernel Memory Ordering . Linux Plumbers Conference , 2016 . P. E. McKenney. A Formal Model of Linux-Kernel Memory Ordering. Linux Plumbers Conference, 2016."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2818754.2818829"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/215399.215413"},{"key":"e_1_3_2_2_37_1","unstructured":"Racket. The Racket programming language. http:\/\/racketlang.org.  Racket. The Racket programming language. http:\/\/racketlang.org."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763571"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806635"},{"key":"e_1_3_2_2_46_1","volume-title":"SPARC International","author":"Weaver D. L.","year":"1994","unstructured":"D. L. Weaver and T. Germond . The SPARC architecture manual (version 9) . SPARC International , 1994 . D. L. Weaver and T. Germond. The SPARC architecture manual (version 9). SPARC International, 1994."},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2004.1302944"},{"key":"e_1_3_2_2_49_1","first-page":"2","article-title":"Relaxed memory models must be rigorous","author":"Nardelli F. Zappa","year":"2009","unstructured":"F. Zappa Nardelli , P. Sewell , J. \u02d8 Sev\u02d8c\u00edk , S. Sarkar , S. Owens , L. Maranget , M. Batty , and J. Alglave . Relaxed memory models must be rigorous . In EC 2 , 2009 . F. Zappa Nardelli, P. Sewell, J. \u02d8Sev\u02d8c\u00edk, S. Sarkar, S. Owens, L. Maranget, M. Batty, and J. Alglave. Relaxed memory models must be rigorous. In EC 2, 2009.","journal-title":"EC"}],"event":{"name":"PLDI '17: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Barcelona Spain","acronym":"PLDI '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3062341.3062353","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3062341.3062353","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3062341.3062353","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:32Z","timestamp":1750203392000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3062341.3062353"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,14]]},"references-count":47,"alternative-id":["10.1145\/3062341.3062353","10.1145\/3062341"],"URL":"https:\/\/doi.org\/10.1145\/3062341.3062353","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3140587.3062353","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,6,14]]},"assertion":[{"value":"2017-06-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}