{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:29:17Z","timestamp":1784255357167,"version":"3.55.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2318722"],"award-info":[{"award-number":["2318722"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2319168"],"award-info":[{"award-number":["2319168"]}],"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":[[2026,1,8]]},"abstract":"<jats:p>Nondeterminism makes parallel programs challenging to write and reason about. To avoid these challenges, researchers have developed techniques for internally deterministic parallel programming, in which the steps of a parallel computation proceed in a deterministic way. Internal determinism is useful because it lets a programmer reason about a program as if it executed in a sequential order. However, no verification framework exists to exploit this property and simplify formal reasoning about internally deterministic programs.<\/jats:p>\n                  <jats:p>To capture the essence of why internally deterministic programs should be easier to reason about, this paper defines a property called schedule-independent safety. A program satisfies schedule-independent safety, if, to show that the program is safe across all orderings, it suffices to show that one terminating execution of the program is safe. We then present a separation logic called Musketeer for proving that a program satisfies schedule-independent safety. Once a parallel program has been shown to satisfy schedule-independent safety, we can verify it with a new logic called Angelic, which allows one to dynamically select and verify just one sequential ordering of the program.<\/jats:p>\n                  <jats:p>Using Musketeer, we prove the soundness of MiniDet, an affine type system for enforcing internal determinism. MiniDet supports several core algorithmic primitives for internally deterministic programming that have been identified in the research literature, including a deterministic version of a concurrent hash set. Because any syntactically well-typed MiniDet program satisfies schedule-independent safety, we can apply Angelic to verify such programs.<\/jats:p>\n                  <jats:p>All results in this paper have been verified in Rocq using the Iris separation logic framework.<\/jats:p>","DOI":"10.1145\/3776668","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"748-776","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs"],"prefix":"10.1145","volume":"10","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, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2848-9808","authenticated-orcid":false,"given":"Sam","family":"Westrick","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5692-3347","authenticated-orcid":false,"given":"Joseph","family":"Tassarotti","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69562"},{"key":"e_1_3_2_3_1","volume-title":"9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010, October 4-6, 2010, Vancouver, BC, Canada, Proceedings","author":"Aviram Amittai","year":"2010","unstructured":"Amittai Aviram, Shu-Chun Weng, Sen Hu, and Bryan Ford. 2010. Efficient System-Enforced Deterministic Parallelism. In 9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010, October 4-6, 2010, Vancouver, BC, Canada, Proceedings, Remzi H. Arpaci-Dusseau and Brad Chen (Eds.). USENIX Association. http:\/\/www.usenix.org\/events\/osdi10\/tech\/full_papers\/Aviram.pdf"},{"key":"e_1_3_2_4_1","volume-title":"PPoPP 12","author":"Blelloch Guy E.","year":"2012","unstructured":"Guy E. Blelloch, Jeremy T. Fineman, Phillip B. Gibbons, and Julian Shun. 2012. Internally deterministic parallel algorithms can be fast. In PPoPP 12 (New Orleans, Louisiana, USA)."},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1006\/JPDC.1994.1038"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640097"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926447"},{"key":"e_1_3_2_8_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\/staff\/p.ohearn\/papers\/permissions_paper.pdf","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44681-8_76"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926354.1926358"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656437"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563298"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591289"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480885"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175734"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523727"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1248648.1248656"},{"key":"e_1_3_2_20_1","first-page":"3","article-title":"ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity","volume":"17","author":"Frumin Dan","year":"2021","unstructured":"Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2021. ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. Logical Methods in Computer Science 17, 3 (2021). https:\/\/arxiv.org\/abs\/2006.13635v3","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434291"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062354"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSTTCS.2008.1769"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254071"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863582"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/ISBN.978-3-85448-046-4_23"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2025.27"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009877"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2502323.2502326"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594312"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535842"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018827"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837635"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034675.2034685"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Alexandre Moine Sam Westrick and Joseph Tassarotti. 2025a. All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs (Artifact). doi:10.5281\/zenodo.17259376","DOI":"10.5281\/zenodo.17259376"},{"key":"e_1_3_2_39_1","unstructured":"Alexandre Moine Sam Westrick and Joseph Tassarotti. 2025b. All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs (Extended Version). (Nov. 2025). https:\/\/arxiv.org\/abs\/2511.23283"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61470-6_7"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462176"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004458"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2612669.2612687"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632851"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290372"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776668","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:45:32Z","timestamp":1784209532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776668"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776668"],"URL":"https:\/\/doi.org\/10.1145\/3776668","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}