{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:13Z","timestamp":1775790673189,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T00:00:00Z","timestamp":1452470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"EC FET","award":["308830"],"award-info":[{"award-number":["308830"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,11]]},"DOI":"10.1145\/2837614.2837643","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T09:05:00Z","timestamp":1452157500000},"page":"649-662","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":70,"title":["Taming release-acquire consistency"],"prefix":"10.1145","author":[{"given":"Ori","family":"Lahav","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Nick","family":"Giannarakis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"LNCS","first-page":"367","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, TACAS","author":"Abdulla P. A.","year":"2015","unstructured":"P. A. Abdulla , S. Aronis , M. F. Atig , B. Jonsson , C. Leonardsson , and K. Sagonas . Stateless model checking for TSO and PSO . In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 , volume 9035 of LNCS , pages 353\u2013 367 . Springer, 2015. P. A. Abdulla, S. Aronis, M. F. Atig, B. Jonsson, C. Leonardsson, and K. Sagonas. Stateless model checking for TSO and PSO. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015, volume 9035 of LNCS, pages 353\u2013367. Springer, 2015."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_13"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2013.8"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_3_2_1_9_1","series-title":"LNCS","first-page":"440","volume-title":"Automata, Languages and Programming","author":"Bouajjani A.","unstructured":"A. Bouajjani , R. Meyer , and E. M\u00f6hlmann . Deciding robustness against total store ordering . In Automata, Languages and Programming , volume 6756 of LNCS , pages 428\u2013 440 . Springer, 2011. A. Bouajjani, R. Meyer, and E. M\u00f6hlmann. Deciding robustness against total store ordering. In Automata, Languages and Programming, volume 6756 of LNCS, pages 428\u2013440. Springer, 2011."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_3_2_1_11_1","first-page":"71","volume-title":"A Framework for Transactional Consistency Models with Atomic Visibility. In 26th International Conference on Concurrency Theory (CONCUR","volume":"42","author":"Cerone A.","year":"2015","unstructured":"A. Cerone , G. Bernardi , and A. Gotsman . A Framework for Transactional Consistency Models with Atomic Visibility. In 26th International Conference on Concurrency Theory (CONCUR 2015 ), volume 42 of LIPIcs, pages 58\u2013 71 . Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 2015. A. Cerone, G. Bernardi, and A. Gotsman. A Framework for Transactional Consistency Models with Atomic Visibility. In 26th International Conference on Concurrency Theory (CONCUR 2015), volume 42 of LIPIcs, pages 58\u201371. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 2015."},{"key":"e_1_3_2_1_12_1","series-title":"LNCS","first-page":"466","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Dan A.","unstructured":"A. Dan , Y. Meshman , M. Vechev , and E. Yahav . Effective abstractions for verification under relaxed memory models . In Verification, Model Checking, and Abstract Interpretation , volume 8931 of LNCS , pages 449\u2013 466 . Springer, 2015. A. Dan, Y. Meshman, M. Vechev, and E. Yahav. Effective abstractions for verification under relaxed memory models. In Verification, Model Checking, and Abstract Interpretation, volume 8931 of LNCS, pages 449\u2013466. Springer, 2015."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.159"},{"key":"e_1_3_2_1_14_1","volume-title":"Programming language C++","author":"IEC","year":"2011","unstructured":"ISO\/ IEC 14882:2011. Programming language C++ , 2011 . ISO\/IEC 14882:2011. Programming language C++, 2011."},{"key":"e_1_3_2_1_15_1","volume-title":"Programming language C","author":"IEC","year":"2011","unstructured":"ISO\/ IEC 9899:2011. Programming language C , 2011 . ISO\/IEC 9899:2011. Programming language C, 2011."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2601339"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993521"},{"key":"e_1_3_2_1_18_1","series-title":"LNCS","first-page":"323","volume-title":"Automata, Languages, and Programming, ICALP\u201915","author":"Lahav O.","unstructured":"O. Lahav and V. Vafeiadis . Owicki-gries reasoning for weak memory models . In Automata, Languages, and Programming, ICALP\u201915 , volume 9135 of LNCS , pages 311\u2013 323 . Springer, 2015. O. Lahav and V. Vafeiadis. Owicki-gries reasoning for weak memory models. In Automata, Languages, and Programming, ICALP\u201915, volume 9135 of LNCS, pages 311\u2013323. Springer, 2015."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_20_1","series-title":"LNCS","first-page":"226","volume-title":"Model Checking Software","author":"Linden A.","unstructured":"A. Linden and P. Wolper . An automata-based symbolic approach for verifying programs on relaxed memory models . In Model Checking Software , volume 6349 of LNCS , pages 212\u2013 226 . Springer, 2010. A. Linden and P. Wolper. An automata-based symbolic approach for verifying programs on relaxed memory models. In Model Checking Software, volume 6349 of LNCS, pages 212\u2013226. Springer, 2010."},{"key":"e_1_3_2_1_22_1","first-page":"26","volume-title":"First International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE","volume":"40","author":"Mansky W.","year":"2014","unstructured":"W. Mansky and E. L. Gunter . Verifying optimizations for concurrent programs . In First International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2014 , volume 40 of OASICS, pages 15\u2013 26 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. W. Mansky and E. L. Gunter. Verifying optimizations for concurrent programs. In First International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2014, volume 40 of OASICS, pages 15\u201326. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014."},{"key":"e_1_3_2_1_23_1","unstructured":"L. Maranget S. Sarkar and P. Sewell. A tutorial introduction to the ARM and POWER relaxed memory models. http:\/\/www.cl.cam.ac.uk\/\u02dcpes20\/ppc-supplemental\/test7.pdf 2012.  L. Maranget S. Sarkar and P. Sewell. A tutorial introduction to the ARM and POWER relaxed memory models. http:\/\/www.cl.cam.ac.uk\/\u02dcpes20\/ppc-supplemental\/test7.pdf 2012."},{"key":"e_1_3_2_1_24_1","first-page":"503","volume-title":"ECOOP 2010:  24th European Conference on Object-Oriented Programming","volume":"6183","author":"Owens S.","unstructured":"S. Owens . Reasoning about the implementation of concurrency abstractions on x86-TSO . In ECOOP 2010: 24th European Conference on Object-Oriented Programming , volume 6183 of LNCS, pages 478\u2013 503 . Springer, 2010. S. Owens. Reasoning about the implementation of concurrency abstractions on x86-TSO. In ECOOP 2010: 24th European Conference on Object-Oriented Programming, volume 6183 of LNCS, pages 478\u2013 503. Springer, 2010."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462196"},{"key":"e_1_3_2_1_27_1","series-title":"LNCS","first-page":"70","volume-title":"VSTTE","author":"Ridge T.","year":"2010","unstructured":"T. Ridge . A rely-guarantee proof system for x86-TSO . In VSTTE 2010 , volume 6217 of LNCS , pages 55\u2013 70 . Springer, 2010. T. Ridge. A rely-guarantee proof system for x86-TSO. In VSTTE 2010, volume 6217 of LNCS, pages 55\u201370. Springer, 2010."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_3_2_1_32_1","series-title":"LNCS","first-page":"761","volume-title":"ESOP","author":"Sieczkowski F.","year":"2015","unstructured":"F. Sieczkowski , K. Svendsen , L. Birkedal , and J. Pichon-Pharabod . A separation logic for fictional sequential consistency . In ESOP 2015 , volume 9032 of LNCS , pages 736\u2013 761 . Springer, 2015. F. Sieczkowski, K. Svendsen, L. Birkedal, and J. Pichon-Pharabod. A separation logic for fictional sequential consistency. In ESOP 2015, volume 9032 of LNCS, pages 736\u2013761. Springer, 2015."},{"key":"e_1_3_2_1_33_1","volume-title":"The SPARC Architecture Manual: Version 8","author":"SPARC International Inc.","year":"1992","unstructured":"SPARC International Inc. The SPARC Architecture Manual: Version 8 . Prentice-Hall, Inc. , 1992 . ISBN 0-13-825001-4. SPARC International Inc. The SPARC Architecture Manual: Version 8. Prentice-Hall, Inc., 1992. ISBN 0-13-825001-4."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017460.1017464"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737992"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_3_2_1_37_1","first-page":"162","volume-title":"18th International Conference on Static Analysis, SAS\u201911","volume":"6887","author":"Vafeiadis V.","unstructured":"V. Vafeiadis and F. Zappa Nardelli . Verifying fence elimination optimisations . In 18th International Conference on Static Analysis, SAS\u201911 , volume 6887 of LNCS, pages 146\u2013 162 . Springer, 2011. V. Vafeiadis and F. Zappa Nardelli. Verifying fence elimination optimisations. In 18th International Conference on Static Analysis, SAS\u201911, volume 6887 of LNCS, pages 146\u2013162. Springer, 2011."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2013.24"}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"St. Petersburg FL USA","acronym":"POPL '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837643","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837643","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:43:38Z","timestamp":1750211018000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837643"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":39,"alternative-id":["10.1145\/2837614.2837643","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837643","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837643","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}