{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:52:58Z","timestamp":1787068378856,"version":"3.56.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1901381, CCF-2115104, CCF-2119352, CCF-2107241"],"award-info":[{"award-number":["CCF-1901381, CCF-2115104, CCF-2119352, CCF-2107241"]}],"id":[{"id":"10.13039\/100000001","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":[[2024,1,2]]},"abstract":"<jats:p>Disentanglement is a run-time property of parallel programs that facilitates task-local reasoning about the memory footprint of parallel tasks. In particular, it ensures that a task does not access any memory locations allocated by another concurrently executing task. Disentanglement can be exploited, for example, to implement a high-performance parallel memory manager, such as in the MPL (MaPLe) compiler for Parallel ML. Prior research on disentanglement has focused on the design of optimizations, either trusting the programmer to provide a disentangled program or relying on runtime instrumentation for detecting and managing entanglement. This paper provides the first static approach to verify that a program is disentangled: it contributes DisLog, a concurrent separation logic for disentanglement. DisLog enriches concurrent separation logic with the notions necessary for reasoning about the fork-join structure of parallel programs, allowing the verification that memory accesses are effectively disentangled. A large class of programs, including race-free programs, exhibit memory access patterns that are disentangled \"by construction\". To reason about these patterns, the paper distills from DisLog an almost standard concurrent separation logic, called DisLog+. In this high-level logic, no specific reasoning about memory accesses is needed: functional correctness proofs entail disentanglement. The paper illustrates the use of DisLog and DisLog+ on a range of case studies, including two different implementations of parallel deduplication via concurrent hashing. All our results are mechanized in the Coq proof assistant using Iris.<\/jats:p>","DOI":"10.1145\/3632853","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T15:48:51Z","timestamp":1704469731000},"page":"302-331","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["DisLog: A Separation Logic for Disentanglement"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2169-1977","authenticated-orcid":false,"given":"Alexandre","family":"Moine","sequence":"first","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2848-9808","authenticated-orcid":false,"given":"Sam","family":"Westrick","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8347-3529","authenticated-orcid":false,"given":"Stephanie","family":"Balzer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951946"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1839676.1839697"},{"key":"e_1_3_1_4_1","volume-title":"Compiling with Continuations","author":"Andrew W. Appel","year":"1992","unstructured":"Andrew W. Appel. 1992. Compiling with Continuations. Cambridge University Press. http:\/\/www.cambridge.org\/9780521033114"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434299"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591284"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110281"},{"key":"e_1_3_1_8_1","volume-title":"3rd USENIX Workshop on Hot Topics in Parallelism, HotPar\u201911","author":"Boehm Hans-Juergen","year":"2011","unstructured":"Hans-Juergen Boehm. 2011. How to Miscompile Programs with \"Benign\" Data Races. In 3rd USENIX Workshop on Hot Topics in Parallelism, HotPar\u201911, Berkeley, CA, USA, May 26-27, 2011."},{"key":"e_1_3_1_9_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. http:\/\/www.cs.ucl.ac.uk\/stafl7p.ohearn\/papers\/permissions_paper.pdf","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192421"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002240000120"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_27"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178487.3178494"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2385452"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360215"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00325-6"},{"key":"e_1_3_1_24_1","unstructured":"Iris Development Team. 2023. iris.base_logic.lib.gen_heap. https:\/\/plv.mpi-sws.org\/coqdoc\/iris\/iris.base_logic.lib.gen_heap.html."},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498662"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_27_1","first-page":"17:1","article-title":"Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris","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. https:\/\/people.mpi-sws.org\/~dreyer\/papers\/iris-weak\/paper.pdf","journal-title":"European Conference on Object-Oriented Programming (ECOOP)"},{"key":"e_1_3_1_28_1","volume-title":"The Art of Computer Programming, Volume 3: (2nd Ed.) Sorting and Searching","author":"Knuth Donald E.","year":"1998","unstructured":"Donald E. Knuth. 1998. The Art of Computer Programming, Volume 3: (2nd Ed.) Sorting and Searching. Addison Wesley Longman Publishing Co., Inc., USA."},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_23"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571218"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Alexandre Moine Sam Westrick and Stephanie Balzer. 2023b. DisLog: A Separation Logic for Disentanglement - Artifact. https:\/\/doi.org\/10.5281\/zenodo.8414566 10.5281\/zenodo.8414566 Last version available at: https:\/\/gitlab.inria.fr\/amoine\/dislog.","DOI":"10.5281\/zenodo.8414566"},{"key":"e_1_3_1_34_1","unstructured":"MPL Development Team. 2022. The MaPLe (MPL) compiler v0.3. https:\/\/github.com\/MPLLang\/mpl."},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408978"},{"key":"e_1_3_1_37_1","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/978-3-642-54833-8_16","volume-title":"Programming Languages and Systems","author":"Nanevski Aleksandar","year":"2014","unstructured":"Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germ\u00e1n Andr\u00e9s Delbianco. 2014. Communicating State Transition Systems for Fine-Grained Concurrent Resources. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 290\u2013310."},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951935"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"e_1_3_1_42_1","unstructured":"VerifyThis. 2022. Challenge 3 - The World\u2019s Simplest Lock-Free Hash Set. https:\/\/ethz.ch\/content\/dam\/ethz\/special-interest\/infk\/chair-program-method\/pm\/documents\/Verify%20This\/Challenges2022\/verifyThis2022-challenge3.pdf"},{"key":"e_1_3_1_43_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. https:\/\/cs.au.dk\/~birke\/papers\/2021-ms-queue-final.pdf","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_3_1_44_1","doi-asserted-by":"crossref","unstructured":"Philip Wadler. 2012. Propositions as Sessions. In ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM 273\u2013286. https:\/\/doi.org\/10.1145\/2364527.236456810.1145\/2364527.2364568","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_3_1_45_1","volume-title":"Efficient and Scalable Parallel Functional Programming Through Disentanglement","author":"Westrick Sam","year":"2022","unstructured":"Sam Westrick. 2022. Efficient and Scalable Parallel Functional Programming Through Disentanglement. Ph. D. Dissertation. Carnegie Mellon University. https:\/\/www.cs.cmu.edu\/~swestric\/22\/thesis.pdf"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547646"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371115"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632853","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632853","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632853","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:04:42Z","timestamp":1751645082000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632853"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":46,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632853"],"URL":"https:\/\/doi.org\/10.1145\/3632853","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}