{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:54:27Z","timestamp":1790927667643,"version":"4.1.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100007601","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["683289"],"award-info":[{"award-number":["683289"]}],"id":[{"id":"10.13039\/501100007601","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":[[2020,1]]},"abstract":"<jats:p>\n                    The Rust programming language supports safe systems programming by means of a strong ownership-tracking type system. In their prior work on RustBelt, Jung et al. began the task of setting Rust\u2019s safety claims on a more rigorous formal foundation. Specifically, they used Iris, a Coq-based separation logic framework, to build a machine-checked proof of semantic soundness for a \u03bb-calculus model of Rust, as well as for a number of widely-used Rust libraries that internally employ unsafe language features. However, they also made the significant simplifying assumption that the language is sequentially consistent. In this paper, we adapt RustBelt to account for the relaxed-memory operations that concurrent Rust libraries actually use, in the process uncovering a data race in the Arc library. We focus on the most interesting technical problem: how to reason about\n                    <jats:italic>resource reclamation under relaxed memory<\/jats:italic>\n                    , using a logical construction we call\n                    <jats:italic>synchronized ghost state<\/jats:italic>\n                    .\n                  <\/jats:p>","DOI":"10.1145\/3371102","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T14:45:25Z","timestamp":1576853125000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":61,"title":["RustBelt meets relaxed memory"],"prefix":"10.1145","volume":"4","author":[{"given":"Hoang-Hai","family":"Dang","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jacques-Henri","family":"Jourdan","sequence":"additional","affiliation":[{"name":"LRI, France \/ CNRS, France \/ University of Paris-Saclay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan-Oliver","family":"Kaiser","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709094"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"Mark Batty Scott Owens Susmit Sarkar Peter Sewell and Tjark Weber. 2011. Mathematizing C++ concurrency. In POPL. 55\u201366.  Mark Batty Scott Owens Susmit Sarkar Peter Sewell and Tjark Weber. 2011. Mathematizing C++ concurrency. In POPL. 55\u201366.","DOI":"10.1145\/1925844.1926394"},{"key":"e_1_2_2_3_1","volume-title":"Boehm and Brian Demsky","author":"J.","year":"2014","unstructured":"Hans- J. Boehm and Brian Demsky . 2014 . Outlawing ghosts: Avoiding out-of-thin-air results. In MSPC. Hans-J. Boehm and Brian Demsky. 2014. Outlawing ghosts: Avoiding out-of-thin-air results. In MSPC."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1073970.1073974"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3539237"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293883.3295702"},{"key":"e_1_2_2_9_1","volume-title":"VMCAI (LNCS)","author":"Doko Marko","unstructured":"Marko Doko and Viktor Vafeiadis . 2016. A program logic for C11 memory fences . In VMCAI (LNCS) . Springer , 413\u2013430. Marko Doko and Viktor Vafeiadis. 2016. A program logic for C11 memory fences. In VMCAI (LNCS). Springer, 413\u2013430."},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Marko Doko and Viktor Vafeiadis. 2017. Tackling real-life relaxed concurrency with FSL++. In ESOP.  Marko Doko and Viktor Vafeiadis. 2017. Tackling real-life relaxed concurrency with FSL++. In ESOP.","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"e_1_2_2_11_1","unstructured":"Derek Dreyer. 2016. RustBelt project webpage. http:\/\/plv.mpi-sws.org\/rustbelt\/  Derek Dreyer. 2016. RustBelt project webpage. http:\/\/plv.mpi-sws.org\/rustbelt\/"},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Alexey Gotsman Josh Berdine Byron Cook Noam Rinetzky and Mooly Sagiv. 2007. Local reasoning for storable locks and threads. In APLAS. 19\u201337.  Alexey Gotsman Josh Berdine Byron Cook Noam Rinetzky and Mooly Sagiv. 2007. Local reasoning for storable locks and threads. In APLAS. 19\u201337.","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10766-017-0518-x"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Aquinas Hobor Andrew W. Appel and Francesco Zappa Nardelli. 2008. Oracle semantics for concurrent separation logic. In ESOP. 353\u2013367.  Aquinas Hobor Andrew W. Appel and Francesco Zappa Nardelli. 2008. Oracle semantics for concurrent separation logic. In ESOP. 353\u2013367.","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"e_1_2_2_15_1","unstructured":"Jacques-Henri Jourdan. 2018. Insufficient synchronization in Arc::get_mut. Rust issue #51780 https:\/\/github.com\/rustlang\/rust\/issues\/51780 .  Jacques-Henri Jourdan. 2018. Insufficient synchronization in Arc::get_mut. Rust issue #51780 https:\/\/github.com\/rustlang\/rust\/issues\/51780 ."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_18_1","first-page":"1","article-title":"Strong logic for weak memory: Reasoning about release-acquire consistency in Iris","volume":"17","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 ECOOP (LIPIcs). 17 : 1 \u2013 17 :29. 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 ECOOP (LIPIcs). 17:1\u201317:29.","journal-title":"ECOOP (LIPIcs)."},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"Jeehoon Kang Chung-Kil Hur Ori Lahav Viktor Vafeiadis and Derek Dreyer. 2017. A promising semantics for relaxedmemory concurrency. In POPL. ACM 175\u2013189.  Jeehoon Kang Chung-Kil Hur Ori Lahav Viktor Vafeiadis and Derek Dreyer. 2017. A promising semantics for relaxedmemory concurrency. In POPL. ACM 175\u2013189.","DOI":"10.1145\/3093333.3009850"},{"key":"e_1_2_2_20_1","unstructured":"Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. https:\/\/doc.rust-lang.org\/stable\/book\/2018-edition\/  Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. https:\/\/doc.rust-lang.org\/stable\/book\/2018-edition\/"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Ori Lahav Viktor Vafeiadis Jeehoon Kang Chung-Kil Hur and Derek Dreyer. 2017. Repairing sequential consistency in C\/C++11. In PLDI.  Ori Lahav Viktor Vafeiadis Jeehoon Kang Chung-Kil Hur and Derek Dreyer. 2017. Repairing sequential consistency in C\/C++11. In PLDI.","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_2_25_1","volume-title":"Operational aspects of C\/C++ concurrency. CoRR abs\/1606.01400","author":"Podkopaev Anton","year":"2016","unstructured":"Anton Podkopaev , Ilya Sergey , and Aleksandar Nanevski . 2016. Operational aspects of C\/C++ concurrency. CoRR abs\/1606.01400 ( 2016 ). arXiv: 1606.01400 http:\/\/arxiv.org\/abs\/1606.01400 Anton Podkopaev, Ilya Sergey, and Aleksandar Nanevski. 2016. Operational aspects of C\/C++ concurrency. CoRR abs\/1606.01400 (2016). arXiv: 1606.01400 http:\/\/arxiv.org\/abs\/1606.01400"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_13"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737992"},{"key":"e_1_2_2_29_1","volume-title":"Crossbeam: Support for concurrent and parallel programming.","author":"Turon Aaron","year":"2016","unstructured":"Aaron Turon . 2016 . Crossbeam: Support for concurrent and parallel programming. Available at https:\/\/github.com\/aturon\/ crossbeam . Aaron Turon. 2016. Crossbeam: Support for concurrent and parallel programming. Available at https:\/\/github.com\/aturon\/ crossbeam ."},{"key":"e_1_2_2_30_1","volume-title":"GPS: Navigating weak memory with ghosts, protocols, and separation. In OOPSLA. ACM, 691\u2013707.","author":"Turon Aaron","year":"2014","unstructured":"Aaron Turon , Viktor Vafeiadis , and Derek Dreyer . 2014 . GPS: Navigating weak memory with ghosts, protocols, and separation. In OOPSLA. ACM, 691\u2013707. Aaron Turon, Viktor Vafeiadis, and Derek Dreyer. 2014. GPS: Navigating weak memory with ghosts, protocols, and separation. In OOPSLA. ACM, 691\u2013707."},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","unstructured":"Viktor Vafeaidis and Chinmay Narayan. 2013. Relaxed separation logic: A program logic for C11 concurrency. In OOPSLA.  Viktor Vafeaidis and Chinmay Narayan. 2013. Relaxed separation logic: A program logic for C11 concurrency. In OOPSLA.","DOI":"10.1145\/2509136.2509532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371102","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371102","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:05:43Z","timestamp":1750259143000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371102"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":31,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371102"],"URL":"https:\/\/doi.org\/10.1145\/3371102","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}