{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:35:50Z","timestamp":1774838150704,"version":"3.50.1"},"reference-count":87,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,5,10]],"date-time":"2017-05-10T00:00:00Z","timestamp":1494374400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"University of Washington, Samsung Research America, and Drexel University"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2017,9,30]]},"abstract":"<jats:p>Verifying invariants of fine-grained concurrent data structures is challenging, because interference from other threads may occur at any time. We propose a new way of proving invariants of fine-grained concurrent data structures: applying rely-guarantee reasoning to references in the concurrent setting. Rely-guarantee applied to references can verify bounds on thread interference without requiring a whole program to be verified.<\/jats:p>\n          <jats:p>\n            This article provides three new results. First, it provides a new approach to preserving invariants and restricting usage of concurrent data structures. Our approach targets a space between simple type systems and modern concurrent program logics, offering an intermediate point between unverified code and full verification. Furthermore, it avoids sealing concurrent data structure implementations and can interact safely with unverified imperative code. Second, we demonstrate the approach\u2019s broad applicability through a series of case studies, using two implementations: an axiomatic C\n            <jats:sc>oq<\/jats:sc>\n            domain-specific language and a library for Liquid Haskell. Third, these two implementations allow us to compare and contrast verifications by interactive proof (C\n            <jats:sc>oq<\/jats:sc>\n            ) and a weaker form that can be expressed using automatically-discharged dependent refinement types (Liquid Haskell).\n          <\/jats:p>","DOI":"10.1145\/3064850","type":"journal-article","created":{"date-parts":[[2017,5,10]],"date-time":"2017-05-10T18:08:53Z","timestamp":1494439733000},"page":"1-54","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types"],"prefix":"10.1145","volume":"39","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9012-4490","authenticated-orcid":false,"given":"Colin S.","family":"Gordon","sequence":"first","affiliation":[{"name":"Drexel University, Philadelphia, USA"}]},{"given":"Michael D.","family":"Ernst","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, USA"}]},{"given":"Dan","family":"Grossman","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, USA"}]},{"given":"Matthew J.","family":"Parkinson","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2017,5,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676972"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/103418.103458"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760273"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"e_1_2_1_6_1","volume-title":"Retrieved","author":"Capretta Venanzio","year":"2004","unstructured":"Venanzio Capretta. 2004. A Polymorphic Representation of Induction-Recursion. Retrieved September 12, 2012 from http:\/\/www.cs.ru.nl\/&sim;enanzio\/publications\/induction_recursion.pdf."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596565"},{"key":"e_1_2_1_9_1","volume-title":"Linear Programming","author":"Chvatal Vasek","unstructured":"Vasek Chvatal. 1983. Linear Programming. Macmillan."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_42"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1614191"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1884012"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Tayfun Elmas Shaz Qadeer Ali Sezgin Omer Subasi and Serdar Tasiran. 2010. Simplifying linearizability proofs with reduction and abstraction. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 10.1007\/978-3-642-12002-2_25","DOI":"10.1007\/978-3-642-12002-2_25"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480885"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480922"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/645393.651882"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349328"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887459.1887496"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462160"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384619"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/645958.676105"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11795490_3"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007944"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/114005.102808"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1734069"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384680"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_2_1_39_1","unstructured":"Ranjit Jhala. 2015. LiquidHaskell: Refinement Types for Haskell. Retrieved from http:\/\/www. degoesconsulting.com\/lambdaconf-2015\/#talk-6f64790e6c."},{"key":"e_1_2_1_40_1","unstructured":"Ranjit Jhala. 2016. Programming with Refinement Types. Retrieved from http:\/\/www.thestrangeloop.com\/2015\/programming-with-refinement-types.html."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032343"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254071"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542510"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_12"},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming (ECOOP\u201915)","author":"Kloos Johannes","year":"2015","unstructured":"Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis. 2015. Asynchronous liquid separation types. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP\u201915)."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429134"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451167"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2004.8"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_14"},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming (ECOOP\u201916)","author":"Milit\u00e3o Filipe","year":"2016","unstructured":"Filipe Milit\u00e3o, Jonathan Aldrich, and Lu\u00eds Caires. 2016. Composing interfering abstract protocols. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP\u201916)."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481872"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706331"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835722"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929553.1929565"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.16"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_29"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.5555\/2519342"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_59"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706316"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_14"},{"key":"e_1_2_1_73_1","volume-title":"Shared Boxes: Rely-Guarantee Reasoning in VeriFast. Technical Report CW622. KU Leuven.","author":"Smans Jan","year":"2014","unstructured":"Jan Smans, Dries Vanoverberghe, Dominique Devriese, Bart Jacobs, and Frank Piessens. 2014. Shared Boxes: Rely-Guarantee Reasoning in VeriFast. Technical Report CW622. KU Leuven."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094828"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1122992"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392200.2392220"},{"key":"e_1_2_1_83_1","unstructured":"Niki Vazou. 2016. LiquidHaskell: Verification of Haskell Programs with SMTs. Retrieved from http:\/\/cufp.org\/2016\/t6-niki-vazou-liquid-haskell-intro.html."},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784745"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_32"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287637"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869509"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3064850","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3064850","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:36:41Z","timestamp":1750217801000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3064850"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,10]]},"references-count":87,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,9,30]]}},"alternative-id":["10.1145\/3064850"],"URL":"https:\/\/doi.org\/10.1145\/3064850","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5,10]]},"assertion":[{"value":"2015-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-05-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}