{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:48:14Z","timestamp":1750308494888,"version":"3.41.0"},"reference-count":101,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>We present IrisFit, a Separation Logic with space credits for reasoning about heap space in a concurrent call-by-value language equipped with tracing garbage collection and shared mutable state.<\/jats:p>\n          <jats:p>We point out a fundamental difficulty in the analysis of the worst-case heap space complexity of concurrent programs in the presence of tracing garbage collection: If garbage collection phases and program steps can be arbitrarily interleaved, then there exist undesirable scenarios where a root held by a sleeping thread prevents a possibly large amount of memory from being freed.<\/jats:p>\n          <jats:p>To remedy this problem and eliminate such undesirable scenarios, we propose several language features, namely possibly-blocking memory allocation, polling points, and protected sections. Polling points are meant to be automatically inserted by the compiler; protected sections are delimited by the programmer and represent regions where no polling points must be inserted.<\/jats:p>\n          <jats:p>The heart of our contribution is IrisFit, a novel program logic that can establish worst-case heap space complexity bounds and whose reasoning rules can take advantage of the presence of protected sections. IrisFit is formalized inside the Coq proof assistant, on top of the Iris Separation Logic framework. We prove that IrisFit offers both a safety guarantee\u2014programs cannot crash and cannot exceed a heap space limit\u2014and a liveness guarantee\u2014provided enough polling points have been inserted, every memory allocation request is satisfied in bounded time. We illustrate the use of IrisFit via several case studies, including a version of Treiber\u2019s stack whose worst-case behavior relies on the presence of protected sections.<\/jats:p>","DOI":"10.1145\/3716312","type":"journal-article","created":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T16:53:41Z","timestamp":1739206421000},"page":"1-71","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Will It Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection"],"prefix":"10.1145","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2169-1977","authenticated-orcid":false,"given":"Alexandre","family":"Moine","sequence":"first","affiliation":[{"name":"New York University, New York, New York, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7764-4507","authenticated-orcid":false,"given":"Arthur","family":"Chargu\u00e9raud","sequence":"additional","affiliation":[{"name":"Inria, Strasbourg, France and Universit\u00e9 de Strasbourg, Strasbourg, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4069-1235","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2025,4,8]]},"reference":[{"key":"e_1_3_3_2_1","unstructured":"Ole Agesen. 1998. GC Points in a Threaded Environment. Technical Report SMLI TR-98-70. Sun Microsystems Inc. Retrieved from https:\/\/dl.acm.org\/doi\/10.5555\/974974"},{"key":"e_1_3_3_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3201897"},{"key":"e_1_3_3_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320418"},{"key":"e_1_3_3_5_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.442.0399"},{"key":"e_1_3_3_6_1","doi-asserted-by":"crossref","unstructured":"Andrew W. Appel. 1992. Compiling with Continuations. Cambridge University Press. Retrieved from https:\/\/www.cambridge.org\/9780521033114","DOI":"10.1017\/CBO9780511609619"},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.003"},{"key":"e_1_3_3_8_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/3-540-45927-8_4","volume-title":"European Symposium on Programming (ESOP)","volume":"2305","author":"Aspinall David","year":"2002","unstructured":"David Aspinall and Martin Hofmann. 2002. Another type system for in-place update. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science, Vol. 2305. Springer, 36\u201352. Retrieved from https:\/\/homepages.inf.ed.ac.uk\/da\/papers\/readonly\/readonly.pdf"},{"issue":"2","key":"e_1_3_3_9_1","first-page":"1","article-title":"Amortised resource analysis with separation logic","volume":"7","author":"Atkey Robert","year":"2011","unstructured":"Robert Atkey. 2011. Amortised resource analysis with separation logic. Logical Methods in Computer Science 7, 2:17 (2011), 1\u201333. Retrieved from https:\/\/lmcs.episciences.org\/685\/pdf","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_3_10_1","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions. Springer. Retrieved from https:\/\/www.labri.fr\/perso\/casteran\/CoqArt\/coqartF.pdf"},{"key":"e_1_3_3_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9496-y"},{"key":"e_1_3_3_12_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2023. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. Retrieved from https:\/\/iris-project.org\/tutorialpdfs\/iris-lecture-notes.pdf"},{"key":"e_1_3_3_13_1","first-page":"1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"5","author":"Birkedal Lars","year":"2021","unstructured":"Lars Birkedal, Thomas Dinsdale-Young, Arma\u00ebl Gu\u00e9neau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. 2021. Theorems for free from separation logic specifications. Proceedings of the ACM on Programming Languages 5, ICFP (2021), 1\u201329. DOI: 10.1145\/3473586"},{"key":"e_1_3_3_14_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093635499"},{"key":"e_1_3_3_15_1","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1996.0107"},{"key":"e_1_3_3_16_1","doi-asserted-by":"crossref","unstructured":"Richard Bornat Cristiano Calcagno Peter O\u2019Hearn and Matthew Parkinson. 2005. Permission accounting in separation logic. In Principles of Programming Languages (POPL) 259\u2013270. Retrieved from https:\/\/www.cs.ucl.ac.uk\/staff\/p.ohearn\/papers\/permissions_paper.pdf","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_3_3_17_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis Symposium (SAS)","volume":"2694","author":"Boyland John","year":"2003","unstructured":"John Boyland. 2003. Checking interference with fractional permissions. In Static Analysis Symposium (SAS), Lecture Notes in Computer Science, Vol. 2694. Springer, 55\u201372. DOI: 10.1007\/3-540-44898-5_4"},{"issue":"3","key":"e_1_3_3_18_1","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1145\/2984450.2984457","article-title":"Concurrent separation logic","volume":"3","author":"Brookes Stephen","year":"2016","unstructured":"Stephen Brookes and Peter W. O\u2019Hearn. 2016. Concurrent separation logic. SIGLOG News 3, 3 (2016), 47\u201365. Retrieved from https:\/\/siglog.hosting.acm.org\/wpcontent\/uploads\/2016\/07\/siglog_news_9.pdf","journal-title":"SIGLOG News"},{"key":"e_1_3_3_19_1","doi-asserted-by":"crossref","unstructured":"Quentin Carbonneaux Jan Hoffmann and Zhong Shao. 2015. Compositional certified resource bounds. In Programming Language Design and Implementation (PLDI) 467\u2013478. Retrieved from https:\/\/www.cs.yale.edu\/homes\/hoffmann\/papers\/amort_imp15.pdf","DOI":"10.1145\/2737924.2737955"},{"issue":"3","key":"e_1_3_3_20_1","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/s10817-017-9431-7","article-title":"Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits","volume":"62","author":"Chargu\u00e9raud Arthur","year":"2019","unstructured":"Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2019. Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Journal of Automated Reasoning 62, 3 (Mar. 2019), 331\u2013365. Retrieved from https:\/\/cambium.inria.fr\/~fpottier\/publis\/chargueraud-pottier-uf-sltc.pdf","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_3_3_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094852"},{"key":"e_1_3_3_22_1","first-page":"151","volume-title":"International Symposium on Memory Management","author":"Chin Wei-Ngan","year":"2008","unstructured":"Wei-Ngan Chin, Huu Hai Nguyen, Corneliu Popeea, and Shengchao Qin. 2008. Analysing memory resource bounds for low-level programs. In International Symposium on Memory Management, 151\u2013160. Retrieved from https:\/\/www7.in.tum.de\/~popeea\/research\/memory.ismm08.pdf"},{"key":"e_1_3_3_23_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/11547662_7","volume-title":"Static Analysis Symposium (SAS)","volume":"3672","author":"Chin Wei-Ngan","year":"2005","unstructured":"Wei-Ngan Chin, Huu Hai Nguyen, Shengchao Qin, and Martin C. Rinard. 2005. Memory usage verification for OO programs. In Static Analysis Symposium (SAS), Lecture Notes in Computer Science, Vol. 3672. Springer, 70\u201386. DOI: 10.1007\/11547662_7"},{"key":"e_1_3_3_24_1","doi-asserted-by":"crossref","unstructured":"William R. Cook. 2009. On understanding data abstraction revisited. In Object-Oriented Programming Systems Languages and Applications (OOPSLA) 557\u2013572. Retrieved from https:\/\/www.cs.utexas.edu\/~wcook\/Drafts\/2009\/essay.pdf","DOI":"10.1145\/1640089.1640133"},{"key":"e_1_3_3_25_1","doi-asserted-by":"crossref","unstructured":"Karl Crary and Stephanie Weirich. 2000. Resource bound certification. In Principles of Programming Languages (POPL) 184\u2013198. Retrieved from https:\/\/www.cs.cornell.edu\/talc\/papers\/resource_bound\/res.pdf","DOI":"10.1145\/325694.325716"},{"key":"e_1_3_3_26_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"European Conference on Object-Oriented Programming (ECOOP)","volume":"8586","author":"Pinto Pedro da Rocha","year":"2014","unstructured":"Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A logic for time and data abstraction. In European Conference on Object-Oriented Programming (ECOOP). Richard E. Jones (Ed.), Lecture Notes in Computer Science, Vol. 8586, Springer, 207\u2013231. Retrieved from https:\/\/vtss.doc.ic.ac.uk\/publications\/daRochaPinto2014TaDA.pdf"},{"key":"e_1_3_3_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165205"},{"issue":"2","key":"e_1_3_3_28_1","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","article-title":"The revised report on the syntactic theories of sequential control and state","volume":"103","author":"Felleisen Matthias","year":"1992","unstructured":"Matthias Felleisen and Robert Hieb. 1992. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science 103, 2 (1992), 235\u2013271. Retrieved from https:\/\/www2.ccs.neu.edu\/racket\/pubs\/tcs92-fh.pdf","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_3_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0211-0"},{"key":"e_1_3_3_30_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1007\/978-3-642-15375-4_27","volume-title":"International Conference on Concurrency Theory (CONCUR)","volume":"6269","author":"Fu Ming","year":"2010","unstructured":"Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang. 2010. Reasoning about optimistic concurrency using a program logic for history. In International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science, Vol. 6269. Springer, 388\u2013402. DOI: 10.1007\/978-3-642-15375-4_27"},{"key":"e_1_3_3_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544885.3544887"},{"key":"e_1_3_3_32_1","first-page":"204:1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"4","author":"G\u00f3mez-Londo\u00f1o Alejandro","year":"2020","unstructured":"Alejandro G\u00f3mez-Londo\u00f1o, Johannes \u00c5man Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, and Yong Kiam Tan. 2020. Do you have space for dessert? A verified space cost semantics for CakeML programs. Proceedings of the ACM on Programming Languages 4, OOPSLA (2020), 204:1\u2013204:29. DOI: 10.1145\/3428272"},{"key":"e_1_3_3_33_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/978-3-642-37036-6_15","volume-title":"European Symposium on Programming (ESOP)","volume":"7792","author":"Gotsman Alexey","year":"2013","unstructured":"Alexey Gotsman, Noam Rinetzky, and Hongseok Yang. 2013. Verifying concurrent memory reclamation algorithms with grace. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science, Vol. 7792. Springer, 249\u2013269. Retrieved from https:\/\/software.imdea.org\/~gotsman\/papers\/recycling-esop13.pdf"},{"key":"e_1_3_3_34_1","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/S0049-237X(08)70247-7","article-title":"Formalization of Boole\u2019s logic","volume":"85","author":"Hailperin Theodore","year":"1986","unstructured":"Theodore Hailperin. 1986. Formalization of Boole\u2019s logic. In Boole\u2019s Logic and Probability. Studies in Logic and the Foundations of Mathematics. J. Barwise, D. Kaplan, H. J. Keisler, P. Suppes, and A. S. Troelstra (Eds.), Vol. 85. Elsevier, 135\u2013172. Retrieved from https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0049237X08702477","journal-title":"Boole\u2019s Logic and Probability. Studies in Logic and the Foundations of Mathematics"},{"key":"e_1_3_3_35_1","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/3-540-45414-4_21","volume-title":"15th International Conference on Distributed Computing (DISC \u201901)","author":"Harris Timothy L.","year":"2001","unstructured":"Timothy L. Harris. 2001. A pragmatic implementation of non-blocking linked-lists. In 15th International Conference on Distributed Computing (DISC \u201901). Springer-Verlag, Berlin, 300\u2013314. DOI: 10.1007\/3-540-45414-4_21"},{"key":"e_1_3_3_36_1","doi-asserted-by":"crossref","unstructured":"Timothy L. Harris Keir Fraser and Ian A. Pratt. 2002. A practical multi-word compare-and-swap operation. In Distributed Computing. Dahlia Malkhi (Ed.) Springer Berlin 265\u2013279. Retrieved from https:\/\/www.cl.cam.ac.uk\/research\/srg\/netos\/papers\/2002-casn.pdf","DOI":"10.1007\/3-540-36108-1_18"},{"key":"e_1_3_3_37_1","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/978-3-642-04761-9_14","article-title":"Memory usage verification using hip\/sleek","volume":"5799","author":"He Guanhua","year":"2009","unstructured":"Guanhua He, Shengchao Qin, Chenguang Luo, and Wei-Ngan Chin. 2009. Memory usage verification using hip\/sleek. In Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, Vol. 5799. Springer, 166\u2013181. Retrieved from https:\/\/dro.dur.ac.uk\/6241\/","journal-title":"Automated Technology for Verification and Analysis (ATVA)"},{"key":"e_1_3_3_38_1","volume-title":"The Art of Multiprocessor Programming","author":"Herlihy Maurice","year":"2012","unstructured":"Maurice Herlihy and Nir Shavit. 2012. The Art of Multiprocessor Programming, Revised Reprint (1st. ed.). Morgan Kaufmann Publishers Inc., San Francisco, CA.","edition":"1"},{"key":"e_1_3_3_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"issue":"3","key":"e_1_3_3_40_1","first-page":"14:1","article-title":"Multivariate amortized resource analysis","volume":"34","author":"Hoffmann Jan","year":"2012","unstructured":"Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012. Multivariate amortized resource analysis. ACM Transactions on Programming Languages and Systems 34, 3 (2012), 14:1\u201314:62. Retrieved from https:\/\/www.cs.cmu.edu\/~janh\/assets\/pdf\/HoffmannAH10.pdf","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_3_41_1","doi-asserted-by":"crossref","first-page":"781","DOI":"10.1007\/978-3-642-31424-7_64","article-title":"Resource aware ML","volume":"7358","author":"Hoffmann Jan","year":"2012","unstructured":"Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012. Resource aware ML. In Computer Aided Verification (CAV), Lecture Notes in Computer Science, Vol. 7358. Springer, 781\u2013786. Retrieved from https:\/\/dx.doi.org\/10.1007\/978-3-642-31424-7_64","journal-title":"Computer Aided Verification (CAV)"},{"key":"e_1_3_3_42_1","doi-asserted-by":"crossref","unstructured":"Jan Hoffmann Ankush Das and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In Principles of Programming Languages (POPL) 359\u2013373. Retrieved from https:\/\/www.cs.cmu.edu\/~janh\/papers\/HoffmannDW17.pdf","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_3_3_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000487"},{"key":"e_1_3_3_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782641"},{"issue":"4","key":"e_1_3_3_45_1","first-page":"258","article-title":"A type system for bounded space and functional in-place update","volume":"7","author":"Hofmann Martin","year":"2000","unstructured":"Martin Hofmann. 2000. A type system for bounded space and functional in-place update. Nordic Journal of Computing 7, 4 (2000), 258\u2013289. Retrieved from https:\/\/www.dcs.ed.ac.uk\/home\/mxh\/nordic.ps.gz","journal-title":"Nordic Journal of Computing"},{"key":"e_1_3_3_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00009-9"},{"key":"e_1_3_3_47_1","doi-asserted-by":"crossref","unstructured":"Martin Hofmann and Steffen Jost. 2003. Static prediction of heap space usage for first-order functional programs. In Principles of Programming Languages (POPL) 185\u2013197. Retrieved from https:\/\/www2.tcs.ifi.lmu.de\/~jost\/research\/POPL_2003_Jost_Hofmann.pdf","DOI":"10.1145\/640128.604148"},{"key":"e_1_3_3_48_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/11693024_3","volume-title":"European Symposium on Programming (ESOP)","volume":"3924","author":"Hofmann Martin","year":"2006","unstructured":"Martin Hofmann and Steffen Jost. 2006. Type-based amortised heap-space analysis. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science, Vol. 3924. Springer, 22\u201337. Retrieved from https:\/\/www2.tcs.ifi.lmu.de\/~jost\/research\/hofmann_jost_esop06_postfinal.pdf"},{"key":"e_1_3_3_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_24"},{"key":"e_1_3_3_50_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"593","DOI":"10.1007\/978-3-642-37036-6_32","volume-title":"European Symposium on Programming (ESOP)","volume":"7792","author":"Hofmann Martin","year":"2013","unstructured":"Martin Hofmann and Dulma Rodriguez. 2013. Automatic type inference for amortised heap-space analysis. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science, Vol. 7792. Springer, 593\u2013613. DOI: 10.1007\/978-3-642-37036-6_32"},{"key":"e_1_3_3_51_1","doi-asserted-by":"crossref","unstructured":"Chung-Kil Hur Derek Dreyer and Viktor Vafeiadis. 2011. Separation logic in the presence of garbage collection. In Logic in Computer Science (LICS) 247\u2013256. Retrieved from https:\/\/people.mpi-sws.org\/~dreyer\/papers\/gcsl\/paper.pdf","DOI":"10.1109\/LICS.2011.46"},{"key":"e_1_3_3_52_1","unstructured":"Sadiq Jaffer. 2021. OCaml Compiler Pull Request 10462: Add [@poll error] Attribute. Retrieved from https:\/\/github.com\/ocaml\/ocaml\/pull\/10462"},{"key":"e_1_3_3_53_1","volume-title":"Garbage Collection\u2014Algorithms for Automatic Dynamic Memory Management","author":"Jones Richard E.","year":"1996","unstructured":"Richard E. Jones and Rafael Dueire Lins. 1996. Garbage Collection\u2014Algorithms for Automatic Dynamic Memory Management. Wiley."},{"key":"e_1_3_3_54_1","first-page":"828","volume-title":"Proceedings of the ACM on Programming Languages","volume":"7","author":"Jung Jaehwang","year":"2023","unstructured":"Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, and Jeehoon Kang. 2023. Modular verification of safe memory reclamation in concurrent separation logic. Proceedings of the ACM on Programming Languages 7, OOPSLA 2 (2023), 828\u2013856. DOI: 10.1145\/3622827"},{"key":"e_1_3_3_55_1","first-page":"66:1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"2","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018. RustBelt: Securing the foundations of the rust programming language. Proceedings of the ACM on Programming Languages 2, POPL (2018), 66:1\u201366:34. Retrieved from https:\/\/people.mpi-sws.org\/~dreyer\/papers\/rustbelt\/paper.pdf"},{"key":"e_1_3_3_56_1","doi-asserted-by":"crossref","first-page":"e20","DOI":"10.1017\/S0956796818000151","article-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic","volume":"28","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 (2018), e20. Retrieved from https:\/\/people.mpisws.org\/~dreyer\/papers\/iris-ground-up\/paper.pdf","journal-title":"Journal of Functional Programming"},{"key":"e_1_3_3_57_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung David Swasey Filip Sieczkowski Kasper Svendsen Aaron Turon Lars Birkedal and Derek Dreyer. 2015. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Principles of Programming Languages (POPL) 637\u2013650. Retrieved from https:\/\/plv.mpisws.org\/iris\/paper.pdf","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_3_3_58_1","first-page":"1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"5","author":"Kahn David M.","year":"2021","unstructured":"David M. Kahn and Jan Hoffmann. 2021. Automatic amortized resource analysis with the quantum physicist\u2019s method. Proceedings of the ACM on Programming Languages 5, ICFP (2021), 1\u201329. DOI: 10.1145\/3473581"},{"key":"e_1_3_3_59_1","first-page":"17:1","volume-title":"European Conference on Object-Oriented Programming (ECOOP)","author":"Kaiser Jan-Oliver","year":"2017","unstructured":"Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In European Conference on Object-Oriented Programming (ECOOP), 17:1\u201317:29. Retrieved from https:\/\/people.mpisws.org\/~dreyer\/papers\/iris-weak\/paper.pdf"},{"key":"e_1_3_3_60_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-3-642-37036-6_10","volume-title":"European Symposium on Programming (ESOP)","volume":"7792","author":"Kassios Ioannis T.","year":"2013","unstructured":"Ioannis T. Kassios and Eleftherios Kritikos. 2013. A discipline for program verification based on backpointers and its use in observational disjointness. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science, Vol. 7792. Springer, 149\u2013168. DOI: 10.1007\/978-3-642-37036-6_10"},{"key":"e_1_3_3_61_1","first-page":"77:1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"2","author":"Krebbers Robbert","year":"2018","unstructured":"Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Chargu\u00e9raud, and Derek Dreyer. 2018. MoSeL: A general, extensible modal framework for interactive proofs in separation logic. Proceedings of the ACM on Programming Languages 2, ICFP (2018), 77:1\u201377:30. DOI: 10.1145\/3236772"},{"key":"e_1_3_3_62_1","unstructured":"Rich Lander. 2015. Announcing .NET Framework 4.6. Retrieved from https:\/\/devblogs.microsoft.com\/dotnet\/announcing-net-framework-4-6\/"},{"issue":"4","key":"e_1_3_3_63_1","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","article-title":"The mechanical evaluation of expressions","volume":"6","author":"Landin Peter J.","year":"1964","unstructured":"Peter J. Landin. 1964. The mechanical evaluation of expressions. Computer Journal 6, 4 (Jan. 1964), 308\u2013320.","journal-title":"Computer Journal"},{"key":"e_1_3_3_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1693453.1693459"},{"key":"e_1_3_3_65_1","unstructured":"Xavier Leroy. 2024. The CompCert C Compiler. Retrieved from https:\/\/compcert.org\/"},{"key":"e_1_3_3_66_1","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2025. The OCaml Language (Language Extensions; Attributes). Retrieved from https:\/\/ocaml.org\/manual\/5.3\/attributes.html"},{"key":"e_1_3_3_67_1","first-page":"70","volume-title":"Symposium on Memory Management (ISMM)","author":"Lin Yi","year":"2015","unstructured":"Yi Lin, Kunshan Wang, Stephen M. Blackburn, Antony L. Hosking, and Michael Norrish. 2015. Stop and go: Understanding yieldpoint behavior. In Symposium on Memory Management (ISMM), 70\u201380. DOI: 10.1145\/2754169.2754187"},{"issue":"1","key":"e_1_3_3_68_1","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1016\/0001-8708(92)90011-9","article-title":"Sets with a negative number of elements","volume":"91","author":"Loeb Daniel","year":"1992","unstructured":"Daniel Loeb. 1992. Sets with a negative number of elements. Advances in Mathematics 91, 1 (1992), 64\u201374. Retrieved from https:\/\/www.sciencedirect.com\/science\/article\/pii\/0001870892900119","journal-title":"Advances in Mathematics"},{"key":"e_1_3_3_69_1","first-page":"275","volume-title":"Proceedings of the ACM on Programming Languages","volume":"7","author":"Lorenzen Anton","year":"2023","unstructured":"Anton Lorenzen, Daan Leijen, and Wouter Swierstra. 2023. FP2: Fully in-place functional programming. Proceedings of the ACM on Programming Languages 7, ICFP (Aug. 2023), 275\u2013304. DOI: 10.1145\/3607840"},{"key":"e_1_3_3_70_1","doi-asserted-by":"crossref","unstructured":"Anil Madhavapeddy and Yaron Minsky. 2022. Real World OCaml: Functional Programming for the Masses (2nd. ed.). Cambridge University Press. Retrieved from https:\/\/realworldocaml.org\/","DOI":"10.1017\/9781009129220"},{"key":"e_1_3_3_71_1","first-page":"718","volume-title":"Proceedings of the ACM on Programming Languages","volume":"6","author":"Madiot Jean-Marie","year":"2022","unstructured":"Jean-Marie Madiot and Fran\u00e7ois Pottier. 2022. A separation logic for heap space under garbage collection. Proceedings of the ACM on Programming Languages 6, POPL (Jan. 2022), 718\u2013747. Retrieved from https:\/\/cambium.inria.fr\/~fpottier\/publis\/madiot-pottier-diamonds-2022.pdf"},{"key":"e_1_3_3_72_1","first-page":"11","volume-title":"7th International Symposium on Memory Management (ISMM)","author":"Marlow Simon","year":"2008","unstructured":"Simon Marlow, Tim Harris, Roshan P. James, and Simon Peyton Jones. 2008. Parallel generational-copying garbage collection with a block-structured heap. In 7th International Symposium on Memory Management (ISMM). ACM, New York, NY, 11\u201320. DOI: 10.1145\/1375634.1375637"},{"key":"e_1_3_3_73_1","unstructured":"Paul McKenney Michael Wong Maged M. Michael Andrew Hunter Daisy Hollman J. F. Bastien Hans Boehm David Goldblatt Frank Birbacher Erik Rigtorp et al. 2023. Read-Copy Update (RCU). P2545R4. Retrieved from https:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2023\/p2545r4.pdf"},{"key":"e_1_3_3_74_1","unstructured":"Paul E. McKenney. 2004. Exploiting Deferred Destruction: An Analysis of Read-Copy-Update Techniques in Operating System Kernels. Ph.D. Dissertation. Oregon Health & Science University. Retrieved from https:\/\/www.rdrop.com\/~paulmck\/RCU\/RCUdissertation.2004.07.14e1.pdf"},{"key":"e_1_3_3_75_1","first-page":"31","volume-title":"Proceedings of the ACM on Programming Languages","volume":"3","author":"Meyer Roland","year":"2019","unstructured":"Roland Meyer and Sebastian Wolff. 2019. Decoupling lock-free data structures from memory reclamation for static analysis. Proceedings of the ACM on Programming Languages 3, POPL, Article 58 (Jan. 2019), 31 pages. DOI: 10.1145\/3290371"},{"key":"e_1_3_3_76_1","first-page":"73","volume-title":"14th Annual ACM Symposium on Parallel Algorithms and Architectures (SPAA)","author":"Michael Maged M.","year":"2002","unstructured":"Maged M. Michael. 2002. High performance dynamic lock-free hash tables and list-based sets. In 14th Annual ACM Symposium on Parallel Algorithms and Architectures (SPAA). ACM, New York, NY, 73\u201382. DOI: 10.1145\/564870.564881"},{"key":"e_1_3_3_77_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2004.8"},{"key":"e_1_3_3_78_1","unstructured":"Maged M. Michael. 2004. RC23089: ABA Prevention Using Single-Word Instructions. Technical Report. Retrieved from https:\/\/dominoweb.draco.res.ibm.com\/4813d7c4e4c6b1a085256e2b00539e0f.html"},{"key":"e_1_3_3_79_1","unstructured":"Maged M. Michael Michael Wong Paul McKenney Andrew Hunter Daisy Hollman J. F. Bastien Hans Boehm David Goldblatt Frank Birbacher and Mathias Stearn. 2023. Hazard Pointers for C++26. P2530R3. Retrieved from https:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2023\/p2530r3.pdf"},{"key":"e_1_3_3_80_1","unstructured":"Microsoft. 2024. Documentation of the GC Class of the .NET 8.0 Framework. Retrieved from https:\/\/learn.microsoft.com\/en-us\/dotnet\/api\/system.gc?view=net-8.0"},{"key":"e_1_3_3_81_1","unstructured":"Alexandre Moine. 2024. Formal Verification of Heap Space Bounds under Garbage Collection. Ph.D. Dissertation. Universit\u00e9 Paris Cit\u00e9. Retrieved from https:\/\/cambium.inria.fr\/~amoine\/phd.html"},{"key":"e_1_3_3_82_1","unstructured":"Alexandre Moine. 2025. Will It Fit? Verifying Heap Space Bounds for Concurrent Programs under Garbage Collection with Separation Logic (Artifact). Retrieved from https:\/\/archive.softwareheritage.org\/swh:1:snp:20f90f6c746ee641b3d8473340f68eae48c6bdd2;origin=https:\/\/github.com\/nobrakal\/irisfit"},{"key":"e_1_3_3_83_1","first-page":"718","volume-title":"Proceedings of the ACM on Programming Languages","volume":"7","author":"Moine Alexandre","year":"2023","unstructured":"Alexandre Moine, Arthur Chargu\u00e9raud, and Fran\u00e7ois Pottier. 2023. A high-level separation logic for heap space under garbage collection. Proceedings of the ACM on Programming Languages 7, POPL (Jan. 2023), 718\u2013747. DOI: 10.1145\/3571218"},{"key":"e_1_3_3_84_1","doi-asserted-by":"crossref","unstructured":"J. Gregory Morrisett Matthias Felleisen and Robert Harper. 1995. Abstract models of memory management. In Functional Programming Languages and Computer Architecture (FPCA) 66\u201377. Retrieved from https:\/\/www.cs.cmu.edu\/~rwh\/papers\/gc\/fpca95.pdf","DOI":"10.1145\/224164.224182"},{"key":"e_1_3_3_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_3_86_1","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"European Symposium on Programming (ESOP)","volume":"11423","author":"M\u00e9vel Glen","year":"2019","unstructured":"Glen M\u00e9vel, Jacques-Henri Jourdan, and Fran\u00e7ois Pottier. 2019. Time credits and time receipts in Iris. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science, Vol. 11423. Springer, 1\u201327. Retrieved from https:\/\/cambium.inria.fr\/~fpottier\/publis\/mevel-jourdan-pottier-timein-iris-2019.pdf"},{"key":"e_1_3_3_87_1","first-page":"543","article-title":"Automatic space bound analysis for functional programs with garbage collection","volume":"57","author":"Niu Yue","year":"2018","unstructured":"Yue Niu and Jan Hoffmann. 2018. Automatic space bound analysis for functional programs with garbage collection. In Logic for Programming Artificial Intelligence and Reasoning (LPAR). EPiC Series in Computing, Vol. 57, 543\u2013563. Retrieved from https:\/\/easychair.org\/publications\/paper\/dcnD","journal-title":"Logic for Programming Artificial Intelligence and Reasoning (LPAR)"},{"key":"e_1_3_3_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_3_3_89_1","first-page":"83:1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"3","author":"Paraskevopoulou Zoe","year":"2019","unstructured":"Zoe Paraskevopoulou and Andrew W. Appel. 2019. Closure conversion is safe for space. Proceedings of the ACM on Programming Languages 3, ICFP (2019), 83:1\u201383:29. DOI: 10.1145\/3341687"},{"key":"e_1_3_3_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190261"},{"key":"e_1_3_3_91_1","first-page":"95:1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"1","author":"Parkinson Matthew J.","year":"2017","unstructured":"Matthew J. Parkinson, Dimitrios Vytiniotis, Kapil Vaswani, Manuel Costa, Pantazis Deligiannis, Dylan McDermott, Aaron Blankstein, and Jonathan Balkind. 2017. Project Snowflake: Non-blocking safe manual memory management in .NET. Proceedings of the ACM on Programming Languages 1, OOPSLA (2017), 95:1\u201395:25. DOI: 10.1145\/3141879"},{"key":"e_1_3_3_92_1","first-page":"225","article-title":"Local reasoning about the presence of bugs: Incorrectness separation logic","volume":"12225","author":"Raad Azalea","year":"2020","unstructured":"Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O\u2019Hearn, and Jules Villard. 2020. Local reasoning about the presence of bugs: Incorrectness separation logic. In Computer Aided Verification (CAV), Lecture Notes in Computer Science, Vol. 12225. Springer, 225\u2013252. Retrieved from https:\/\/plv.mpi-sws.org\/ISL\/","journal-title":"Computer Aided Verification (CAV)"},{"key":"e_1_3_3_93_1","unstructured":"John C. Reynolds. 1975. User-Defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction. Technical Report 1278. Carnegie Mellon University. Retrieved from https:\/\/repository.cmu.edu\/compsci\/1278\/"},{"key":"e_1_3_3_94_1","doi-asserted-by":"crossref","unstructured":"John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science (LICS) 55\u201374. Retrieved from https:\/\/www.cs.cmu.edu\/~jcr\/seplogic.pdf","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_3_95_1","first-page":"113:1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"4","author":"Sivaramakrishnan K. C.","year":"2020","unstructured":"K. C. Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy. 2020. Retrofitting parallelism onto OCaml. Proceedings of the ACM on Programming Languages 4, ICFP (Aug. 2020), 113:1\u2013113:30. DOI: 10.1145\/3408995"},{"key":"e_1_3_3_96_1","first-page":"283","volume-title":"Proceedings of the ACM on Programming Languages","volume":"6","author":"Spies Simon","year":"2022","unstructured":"Simon Spies, Lennard G\u00e4her, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2022. Later credits: Resourceful reasoning for the later modality. Proceedings of the ACM on Programming Languages 6, ICFP (2022), 283\u2013311. DOI: 10.1145\/3547631"},{"key":"e_1_3_3_97_1","unstructured":"The Go Authors. 2019. Goroutine Preemption. Retrieved from https:\/\/go.dev\/src\/runtime\/preempt.go"},{"key":"e_1_3_3_98_1","first-page":"239","article-title":"Formal verification of a lock-free stack with hazard pointers","volume":"6916","author":"Tofan Bogdan","year":"2011","unstructured":"Bogdan Tofan, Gerhard Schellhorn, and Wolfgang Reif. 2011. Formal verification of a lock-free stack with hazard pointers. In Theoretical Aspects of Computing (ICTAC), Lecture Notes in Computer Science, Vol. 6916. Springer, 239\u2013255. Retrieved from https:\/\/opus.bibliothek.uni-augsburg.de\/opus4\/frontdoor\/index\/index\/docId\/55403","journal-title":"Theoretical Aspects of Computing (ICTAC)"},{"key":"e_1_3_3_99_1","unstructured":"R. Kent Treiber. 1986. Systems Programming: Coping with Parallelism. Retrieved from https:\/\/dominoweb.draco.res.ibm.com\/reports\/rj5118.pdf"},{"key":"e_1_3_3_100_1","doi-asserted-by":"crossref","unstructured":"Simon Friis Vindum and Lars Birkedal. 2021. Contextual refinement of the Michael-Scott queue. In Certified Programs and Proofs (CPP) 76\u201390. Retrieved from https:\/\/cs.au.dk\/~birke\/papers\/2021-ms-queue-final.pdf","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_3_3_101_1","unstructured":"Matt Warren. 2016. GC Pauses and Safe Points. Retrieved from https:\/\/mattwarren.org\/2016\/08\/08\/GC-Pauses-and-Safe-Points\/"},{"issue":"3","key":"e_1_3_3_102_1","doi-asserted-by":"crossref","first-page":"405","DOI":"10.2307\/1968168","article-title":"Characteristic functions and the algebra of logic","volume":"34","author":"Whitney Hassler","year":"1933","unstructured":"Hassler Whitney. 1933. Characteristic functions and the algebra of logic. Annals of Mathematics 34, 3 (1933), 405\u2013414. Retrieved from https:\/\/www.jstor.org\/stable\/1968168","journal-title":"Annals of Mathematics"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3716312","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3716312","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:42Z","timestamp":1750272222000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3716312"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,31]]},"references-count":101,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3716312"],"URL":"https:\/\/doi.org\/10.1145\/3716312","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2025,3,31]]},"assertion":[{"value":"2024-04-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-08","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}