{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T04:41:32Z","timestamp":1773895292310,"version":"3.50.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,8,5]]},"abstract":"<jats:p>\n            Consistency guarantees among concurrently executing transactions in local- and distributed systems, commonly referred to as isolation levels, have been formalized in a number of models. Thus far, no model can reason about executable implementations of databases or local transaction libraries providing weak isolation levels. Weak isolation levels are characterized by being highly concurrent and, unlike their stronger counterpart serializability, they are not equivalent to the consistency guarantees provided by a transaction library implemented using a global lock. Industrial-strength databases almost exclusively implement weak isolation levels as their default level. This calls for formalism as numerous bugs violating isolation have been detected in these databases.   In this paper, we formalize three weak isolation levels in separation logic, namely\n            <jats:italic toggle=\"yes\">read uncommitted<\/jats:italic>\n            ,\n            <jats:italic toggle=\"yes\">read committed<\/jats:italic>\n            , and\n            <jats:italic toggle=\"yes\">snapshot isolation<\/jats:italic>\n            . We define modular separation logic specifications that are independent of the underlying transaction library implementation. Historically, isolation levels have been specified using examples of executions between concurrent transactions that are not allowed to occur, and we demonstrate that our specifications correctly prohibit such examples. To show that our specifications are realizable, we formally verify that an executable implementation of a key-value database running the multi-version concurrency control algorithm from the original snapshot isolation paper satisfies our specification of snapshot isolation. Moreover, we prove implications between the specifications\u2014snapshot isolation implies read committed and read committed implies read uncommitted\u2014and thus the verification effort of the database serves as proof that all of our specifications are realizable. All results are mechanized in the Rocq proof assistant on top of the Iris separation logic framework.\n          <\/jats:p>","DOI":"10.1145\/3747515","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"306-340","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Reasoning about Weak Isolation Levels in Separation Logic"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-6587-5590","authenticated-orcid":false,"given":"Anders","family":"Alnor Mathiasen","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8262-6397","authenticated-orcid":false,"given":"L\u00e9on","family":"Gondelman","sequence":"additional","affiliation":[{"name":"Aalborg University, Aalborg, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-6141-5624","authenticated-orcid":false,"given":"L\u00e9on","family":"Ducruet","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/888672"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2000.839388"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/568271.223785"},{"key":"e_1_2_1_4_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2017. Lecture Notes on Iris: Higher-Order Concurrent Separation Log. http:\/\/iris-project.org\/tutorial-pdfs\/iris-lecture-notes.pdf"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485546"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591243"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_4"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.58"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3152396"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_2_1_12_1","volume-title":"15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)","author":"Chajed Tej","year":"2021","unstructured":"Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, and Nickolai Zeldovich. 2021. GoJournal: a verified, concurrent, crash-safe journaling system. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 423\u2013439. isbn:978-1-939133-22-9 https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/chajed"},{"key":"e_1_2_1_13_1","volume-title":"16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Chajed Tej","year":"2022","unstructured":"Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, and Nickolai Zeldovich. 2022. Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, Carlsbad, CA. 447\u2013463. isbn:978-1-939133-28-1 https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/chajed"},{"key":"e_1_2_1_14_1","volume-title":"17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23)","author":"Chang Yun-Sheng","year":"2023","unstructured":"Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. 2023. Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23). USENIX Association, Boston, MA. 871\u2013886. isbn:978-1-939133-34-2 https:\/\/www.usenix.org\/conference\/osdi23\/presentation\/chang"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491245"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087801.3087802"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1182635.1164189"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/38713.38742"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434323"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607859"},{"key":"e_1_2_1_21_1","unstructured":"Jepsen. 2025. Jepsen Analyses. https:\/\/jepsen.io\/analyses Accessed 2025-02-21"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158115"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582302.3582304"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57318-6_25"},{"key":"e_1_2_1_30_1","volume-title":"Sturgis","author":"Lampson Butler W.","year":"1981","unstructured":"Butler W. Lampson and Howard E. Sturgis. 1981. Crash Recovery in a Distributed Data Storage System. https:\/\/api.semanticscholar.org\/CorpusID:263889622"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527324"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689742"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","unstructured":"Alnor Alnor Mathiasen L\u00e9on Gondelman L\u00e9on Ducruet Amin Timany and Lars Birkedal. 2025. Reasoning about Weak Isolation Levels in Separation Logic \u2014 Artifact. https:\/\/doi.org\/10.5281\/zenodo.15626657 10.5281\/zenodo.15626657","DOI":"10.5281\/zenodo.15626657"},{"key":"e_1_2_1_34_1","unstructured":"MicrosoftSQL. 2025. MicrosoftSQL documentation. https:\/\/learn.microsoft.com\/en-us\/dotnet\/framework\/data\/adonet\/sql\/snapshot-isolation-in-sql-server Accessed 2025-06-02"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2023.22"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563351"},{"key":"e_1_2_1_37_1","unstructured":"Oracle. 2025. Oracle documentation. https:\/\/docs.oracle.com\/en\/database\/other-databases\/timesten\/22.1\/introduction\/transaction-isolation.html##GUID-7272EB20-51D6-412C-B25D-58986B3668C8 Accessed 2025-06-02"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_1_39_1","unstructured":"PostgeSQL. 2025. PostgeSQL documentation. https:\/\/www.postgresql.org\/docs\/7.2\/xact-read-committed.html Accessed 2025-06-02"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67220-1_4"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632851"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_2_1_46_1","volume-title":"Parametric Operational Semantics for Consistency Models","author":"Xiong Shale","unstructured":"Shale Xiong. 2020. Parametric Operational Semantics for Consistency Models. Imperial College London."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3552326.3567492"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747515","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:29Z","timestamp":1754412989000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747515"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":47,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747515"],"URL":"https:\/\/doi.org\/10.1145\/3747515","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}