{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:17Z","timestamp":1780994477174,"version":"3.54.1"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008394","name":"Natur og Univers, Det Frie Forskningsr\u00e5d","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100008394","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>Precise management of resources and the obligations they impose, such as the need to dispose of memory, close locks, and release file handles, is hard---especially in the presence of concurrency, when some resources are shared, and different threads operate on them concurrently. We present Iron, a novel higher-order concurrent separation logic that allows for precise reasoning about resources that are transferable among dynamically allocated threads. In particular, Iron can be used to show the correctness of challenging examples, where the reclamation of memory is delegated to a forked-off thread. We show soundness of Iron by means of a model of Iron, defined on top of the Iris base logic, and we use this model to prove that memory resources are accounted for precisely and not leaked. We have formalized all of the developments in the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3290378","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Iron: managing obligations in higher-order concurrent separation logic"],"prefix":"10.1145","volume":"3","author":[{"given":"Ale\u0161","family":"Bizjak","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Gratzer","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2017. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. http:\/\/iris- project. org\/tutorial- pdfs\/iris- lecture- notes.pdf .  Lars Birkedal and Ale\u0161 Bizjak. 2017. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. http:\/\/iris- project. org\/tutorial- pdfs\/iris- lecture- notes.pdf ."},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"John Boyland. 2003. Checking interference with fractional permissions. In SAS.   John Boyland. 2003. Checking interference with fractional permissions. In SAS.","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_2_3_1","volume-title":"Appel","author":"Cao Qinxiang","year":"2017"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Thomas Dinsdale-Young Mike Dodds Philippa Gardner Matthew J. Parkinson and Viktor Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP.   Thomas Dinsdale-Young Mike Dodds Philippa Gardner Matthew J. Parkinson and Viktor Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP.","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Manuel F\u00e4hndrich Mark Aiken Chris Hawblitzel Orion Hodson Galen Hunt James R. Larus and Steven Levi. 2006. Language support for fast and reliable message-based communication in singularity os. In EuroSys.  Manuel F\u00e4hndrich Mark Aiken Chris Hawblitzel Orion Hodson Galen Hunt James R. Larus and Steven Levi. 2006. Language support for fast and reliable message-based communication in singularity os. In EuroSys.","DOI":"10.1145\/1217935.1217953"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480922"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Xinyu Feng Rodrigo Ferreira and Zhong Shao. 2007. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP.   Xinyu Feng Rodrigo Ferreira and Zhong Shao. 2007. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP.","DOI":"10.1007\/978-3-540-71316-6_13"},{"key":"e_1_2_2_9_1","unstructured":"Ming Fu Yong Li Xinyu Feng Zhong Shao and Yu Zhang. 2010. Reasoning about optimistic concurrency using a program logic for history. In CONCUR.   Ming Fu Yong Li Xinyu Feng Zhong Shao and Yu Zhang. 2010. Reasoning about optimistic concurrency using a program logic for history. In CONCUR."},{"key":"e_1_2_2_10_1","unstructured":"Alexey Gotsman Josh Berdine Byron Cook Noam Rinetzky and Mooly Sagiv. 2007. Local reasoning about storable locks and threads. In APLAS.   Alexey Gotsman Josh Berdine Byron Cook Noam Rinetzky and Mooly Sagiv. 2007. Local reasoning about storable locks and threads. In APLAS."},{"key":"e_1_2_2_11_1","unstructured":"Aquinas Hobor Andrew W. Appel and Francesco Zappa Nardelli. 2008. Oracle semantics for concurrent separation logic. In ESOP.   Aquinas Hobor Andrew W. Appel and Francesco Zappa Nardelli. 2008. Oracle semantics for concurrent separation logic. In ESOP."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/373243.375719"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_14_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP","author":"Jung Ralf","year":"2018"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133911"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_22_1","unstructured":"John C. Reynolds. 2000. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science. 303\u2013321.  John C. Reynolds. 2000. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science. 303\u2013321."},{"key":"e_1_2_2_23_1","unstructured":"John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS.   John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_2_28_1","unstructured":"Viktor Vafeiadis and Matthew Parkinson. 2007. A marriage of rely\/guarantee and separation logic. In CONCUR.   Viktor Vafeiadis and Matthew Parkinson. 2007. A marriage of rely\/guarantee and separation logic. In CONCUR."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290378","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290378","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290378"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":28,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290378"],"URL":"https:\/\/doi.org\/10.1145\/3290378","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}