{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:29:16Z","timestamp":1784255356890,"version":"3.55.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    We present DRFCaml, an extension of OCaml\u2019s type system that guarantees data race freedom for multithreaded OCaml programs while retaining backward compatibility with existing sequential OCaml code. We build on recent work of Lorenzen et al., who extend OCaml with\n                    <jats:italic toggle=\"yes\">modes<\/jats:italic>\n                    that keep track of locality, uniqueness, and affinity. We introduce two new mode axes,\n                    <jats:italic toggle=\"yes\">contention<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">portability<\/jats:italic>\n                    , which record whether data has been shared or can be shared between multiple threads. Although this basic type-and-mode system has limited expressive power by itself, it does let us express APIs for\n                    <jats:italic toggle=\"yes\">capsules<\/jats:italic>\n                    , regions of memory whose access is controlled by a unique ghost key, and\n                    <jats:italic toggle=\"yes\">reader-writer locks<\/jats:italic>\n                    , which allow a thread to safely acquire partial or full ownership of a key. We show that this allows complex data structures (which may involve aliasing and mutable state) to be safely shared between threads. We formalize the complete system and establish its soundness by building a semantic model of it in the Iris program logic on top of the Rocq proof assistant.\n                  <\/jats:p>","DOI":"10.1145\/3704859","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"656-686","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Data Race Freedom \u00e0 la Mode"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5951-4642","authenticated-orcid":false,"given":"A\u00efna Linn","family":"Georges","sequence":"first","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3193-6940","authenticated-orcid":false,"given":"Benjamin","family":"Peters","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9514-1360","authenticated-orcid":false,"given":"Laila","family":"Elbeheiry","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-7046-3035","authenticated-orcid":false,"given":"Leo","family":"White","sequence":"additional","affiliation":[{"name":"Jane Street, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4609-9101","authenticated-orcid":false,"given":"Stephen","family":"Dolan","sequence":"additional","affiliation":[{"name":"Jane Street, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7669-9781","authenticated-orcid":false,"given":"Richard A.","family":"Eisenberg","sequence":"additional","affiliation":[{"name":"Jane Street, New York, United States"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-6689-9463","authenticated-orcid":false,"given":"Chris","family":"Casinghino","sequence":"additional","affiliation":[{"name":"Jane Street, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4069-1235","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Javad Abdi Gilead Posluns Guozheng Zhang Boxuan Wang and Mark C. Jeffrey. 2024. When Is Parallelism Fearless and Zero-Cost with Rust?. In Symposium on Parallelism in Algorithms and Architectures. 27\u201340. https:\/\/doi.org\/10.1145\/3626183.3659966 10.1145\/3626183.3659966","DOI":"10.1145\/3626183.3659966"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622846"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_2"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622852"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133896"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Dawson Engler and Ken Ashcraft. 2003. RacerX: Effective static detection of race conditions and deadlocks. In Symposium on Operating Systems Principles (SOSP). 237\u2013252. https:\/\/doi.org\/10.1145\/1165389.945468 10.1145\/1165389.945468","DOI":"10.1145\/1165389.945468"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2301.02308"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49099-X_7"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"A\u00efna Linn Georges Benjamin Peters Laila Elbeheiry Leo White Stephen Dolan Richard A. Eisenberg Chris Casinghino Fran\u00e7ois Pottier and Derek Dreyer. 2024. Supplementary material for Data Race Freedom \u00e0 la Mode. Appendix and Rocq development: https:\/\/plv.mpi-sws.org\/drfcaml\/ Artifact on Zenodo: https:\/\/doi.org\/10.5281\/zenodo.13933463 10.5281\/zenodo.13933463","DOI":"10.5281\/zenodo.13933463"},{"key":"e_1_3_2_15_2","first-page":"62","volume-title":"Proceedings of the 17th Italian Conference on Theoretical Computer Science, Lecce, Italy, September 7-9, 2016 (CEUR Workshop Proceedings","author":"Giannini Paola","year":"2016","unstructured":"Paola Giannini, Marco Servetto, and Elena Zucca. 2016. Types for Immutability and Aliasing Control. In Proceedings of the 17th Italian Conference on Theoretical Computer Science, Lecce, Italy, September 7-9, 2016 (CEUR Workshop Proceedings, Vol. 1720), Vittorio Bil\u00f2 and Antonio Caruso (Eds.). CEUR-WS.org, 62\u201374. https:\/\/ceur-ws.org\/Vol-1720\/full5.pdf"},{"key":"e_1_3_2_16_2","doi-asserted-by":"crossref","unstructured":"Colin S. Gordon Matthew J. Parkinson Jared Parsons Aleks Bromfield and Joe Duffy. 2012. Uniqueness and reference immutability for safe parallelism. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). 21\u201340. https:\/\/www.cs.drexel.edu\/~csg63\/papers\/oopsla12.pdf","DOI":"10.1145\/2384616.2384619"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Philipp Haller and Alex Loiko. 2016. LaCasa: lightweight affinity and object capabilities in Scala. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages and Applications OOPSLA 2016. 272\u2013291. https:\/\/doi.org\/10.1145\/2983990.2984042 10.1145\/2983990.2984042","DOI":"10.1145\/2983990.2984042"},{"key":"e_1_3_2_18_2","volume-title":"Understanding and evolving the Rust programming language","author":"Jung Ralf","year":"2020","unstructured":"Ralf Jung. 2020. Understanding and evolving the Rust programming language. Ph. D. Dissertation. Saarland University, Saarbr\u00fccken, Germany. https:\/\/publikationen.sulb.uni-saarland.de\/handle\/20.500.11880\/29647"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_21_2","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"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3674642"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Mae Milano Joshua Turcotti and Andrew C. Myers. 2022. A flexible type system for fearless concurrency. In Programming Language Design and Implementation (PLDI). 458\u2013473. https:\/\/doi.org\/10.1145\/3519939.3523443 10.1145\/3519939.3523443","DOI":"10.1145\/3519939.3523443"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Mayur Naik Alex Aiken and John Whaley. 2006. Effective static race detection for Java. In Programming Language Design and Implementation (PLDI). 308\u2013319. https:\/\/doi.org\/10.1145\/1133981.1134018 10.1145\/1133981.1134018","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_3_2_25_2","unstructured":"Marco Servetto David J Pearce Lindsay Groves and Alex Potanin. 2013. Balloon types for safe parallelisation over arbitrary object graphs. In Workshop on Determinism and Correctness in Parallel Programming (WoDet) Vol. 107."},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3408995"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Jan Wen Voung Ranjit Jhala and Sorin Lerner. 2007. RELAY: static race detection on millions of lines of code. In Foundations of Software Engineering (FSE). 205\u2013214. https:\/\/doi.org\/10.1145\/1287624.1287654 10.1145\/1287624.1287654","DOI":"10.1145\/1287624.1287654"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649853"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3473597"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704859","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704859","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:37Z","timestamp":1770200197000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704859"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":31,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704859"],"URL":"https:\/\/doi.org\/10.1145\/3704859","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}