{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T10:32:34Z","timestamp":1790937154848,"version":"4.1.0"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"VILLUM Foundation","doi-asserted-by":"crossref","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>We present the first specification and verification of an implementation of a causally-consistent distributed database that supports modular verification of full functional correctness properties of clients and servers. We specify and reason about the causally-consistent distributed database in Aneris, a higher-order distributed separation logic for an ML-like programming language with network primitives for programming distributed systems. We demonstrate that our specifications are useful, by proving the correctness of small, but tricky, synthetic examples involving causal dependency and by verifying a session manager library implemented on top of the distributed database. We use Aneris's facilities for modular specification and verification to obtain a highly modular development, where each component is verified in isolation, relying only on the specifications (not the implementations) of other components. We have used the Coq formalization of the Aneris logic to formalize all the results presented in the paper in the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3434323","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Distributed causal memory: modular specification and verification in higher-order distributed separation logic"],"prefix":"10.1145","volume":"5","author":[{"given":"L\u00e9on","family":"Gondelman","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6045-5232","authenticated-orcid":false,"given":"Simon Oddershede","family":"Gregersen","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2741-8119","authenticated-orcid":false,"given":"Abel","family":"Nieto","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_4"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463676.2465279"},{"key":"e_1_2_1_7_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2017. Lecture Notes on Iris: Higher-Order Concurrent Separation Log. ( 2017 ). http:\/\/irisproject.org\/tutorial-pdfs\/iris-lecture-notes.pdf"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2076450.2076465"},{"key":"e_1_2_1_9_1","volume-title":"Parkinson","author":"Bornat Richard","year":"2015","unstructured":"Richard Bornat, Jade Alglave, and Matthew J. Parkinson. 2015. New Lace and Arsenic: adventures in weak memory with a program logic. CoRR abs\/1512.01416 ( 2015 ). arXiv: 1512.01416 http:\/\/arxiv.org\/abs\/1512.01416"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009888"},{"key":"e_1_2_1_11_1","first-page":"152","article-title":"From Session Causality to Causal Consistency","author":"Brzezinski Jerzy","year":"2004","unstructured":"Jerzy Brzezinski, Cezary Sobaniec, and Dariusz Wawrzyniak. 2004. From Session Causality to Causal Consistency. In PDP. IEEE Computer Society, 152-158.","journal-title":"PDP. IEEE Computer Society"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_4"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1365815.1365816"},{"key":"e_1_2_1_16_1","unstructured":"Kristina Chodorow and Michael Dirolf. 2010. MongoDB-The Definitive Guide: Powerful and Scalable Data Storage. O'Reilly."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.14778\/1454159.1454167"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676984"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087801.3087802"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/564585.564601"},{"key":"e_1_2_1_24_1","volume-title":"Abel Nieto, Amin Timany, and Lars Birkedal.","author":"Gondelman L\u00e9on","year":"2020","unstructured":"L\u00e9on Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal. 2020. Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic-Technical Appendix. https:\/\/iris-project.org\/pdfs\/2021-popl-ccddb-appendix.pdf"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_2_1_26_1","volume-title":"Failure Recovery: When the Cure Is Worse Than the Disease. In 14th Workshop on Hot Topics in Operating Systems, HotOS XIV, Santa Ana Pueblo","author":"Guo Zhenyu","year":"2013","unstructured":"Zhenyu Guo, Sean McDirmid, Mao Yang, Li Zhuang, Pu Zhang, Yingwei Luo, Tom Bergan, Madan Musuvathi, Zheng Zhang, and Lidong Zhou. 2013. Failure Recovery: When the Cure Is Worse Than the Disease. In 14th Workshop on Hot Topics in Operating Systems, HotOS XIV, Santa Ana Pueblo, New Mexico, USA, May 13-15, 2013. https:\/\/www.usenix.org\/conference\/ hotos13\/session\/guo"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 ( 2018 ) e20. https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158115"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250755"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: a general extensible modal framework for interactive proofs in separation logic. PACMPL 2 ICFP ( 2018 ) 77 : 1-77 : 30. https:\/\/doi.org\/10.1145\/3236772 10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3326938.3326942"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385966"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57318-6_25"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043593"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS"},{"key":"e_1_2_1_46_1","volume-title":"29th International Conference on Concurrency Theory, CONCUR 2018","volume":"118","author":"Schewe Sven","year":"2018","unstructured":"Sven Schewe and Lijun Zhang (Eds.). 2018. 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China. LIPIcs, Vol. 118. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik. http:\/\/www.dagstuhl.de\/ dagpub\/978-3-95977-087-3"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926393"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213836.2213945"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_2_1_51_1","volume-title":"Tanenbaum and Maarten van Steen","author":"Andrew","year":"2007","unstructured":"Andrew S. Tanenbaum and Maarten van Steen. 2007. Distributed systems-principles and paradigms, 2nd Edition. Pearson Education.","edition":"2"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDIS.1994.331722"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3299869.3314049"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_1_57_1","volume-title":"Data Consistency in Transactional Storage Systems: a Centralised Approach. CoRR abs\/","author":"Xiong Shale","year":"1901","unstructured":"Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner. 2019. Data Consistency in Transactional Storage Systems: a Centralised Approach. CoRR abs\/ 1901.10615 ( 2019 ). arXiv: 1901.10615 http:\/\/arxiv.org\/abs\/ 1901.10615"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434323","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434323","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:25:57Z","timestamp":1781853957000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434323"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":57,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434323"],"URL":"https:\/\/doi.org\/10.1145\/3434323","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}