{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,24]],"date-time":"2026-04-24T07:42:01Z","timestamp":1777016521154,"version":"3.51.4"},"reference-count":77,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1925605, 1815633, 1934388, 1840761, and 1339362"],"award-info":[{"award-number":["1925605, 1815633, 1934388, 1840761, and 1339362"]}],"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":[[2021,10,20]]},"abstract":"<jats:p>\n            Multicopy search structures such as log-structured merge (LSM) trees are optimized for high insert\/update\/delete (collectively known as upsert) performance. In such data structures, an upsert on key\n            <jats:italic>k<\/jats:italic>\n            , which adds (\n            <jats:italic>k<\/jats:italic>\n            ,\n            <jats:italic>v<\/jats:italic>\n            ) where\n            <jats:italic>v<\/jats:italic>\n            can be a value or a tombstone, is added to the root node even if\n            <jats:italic>k<\/jats:italic>\n            is already present in other nodes. Thus there may be multiple copies of\n            <jats:italic>k<\/jats:italic>\n            in the search structure. A search on\n            <jats:italic>k<\/jats:italic>\n            aims to return the value associated with the most recent upsert. We present a general framework for verifying linearizability of concurrent multicopy search structures that abstracts from the underlying representation of the data structure in memory, enabling proof-reuse across diverse implementations. Based on our framework, we propose template algorithms for (a) LSM structures forming arbitrary directed acyclic graphs and (b) differential file structures, and formally verify these templates in the concurrent separation logic Iris. We also instantiate the LSM template to obtain the first verified concurrent in-memory LSM tree implementation.\n          <\/jats:p>","DOI":"10.1145\/3485490","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Verifying concurrent multicopy search structures"],"prefix":"10.1145","volume":"5","author":[{"given":"Nisarg","family":"Patel","sequence":"first","affiliation":[{"name":"New York University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Siddharth","family":"Krishna","sequence":"additional","affiliation":[{"name":"Microsoft Research, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dennis","family":"Shasha","sequence":"additional","affiliation":[{"name":"New York University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[{"name":"New York University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_23"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_16"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770417"},{"key":"e_1_2_2_5_1","volume-title":"https:\/\/cassandra.apache.org\/ Last accessed on","author":"Foundation Apache Software","year":"2021"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2611462.2611471"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2016.11"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980024.2872406"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_17"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_8"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_28"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_41"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41527-2_12"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3196927"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.8"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429104"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3200691.3178503"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_11"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_25"},{"key":"e_1_2_2_23_1","unstructured":"Manuel Fahndrich and Rustan Leino. 2003. Heap Monotonic Typestate. In Proceedings of the first International Workshop on Alias Confinement and Ownership (IWACO) (proceedings of the first international workshop on alias confinement and ownership (iwaco) ed.). https:\/\/www.microsoft.com\/en-us\/research\/publication\/heap-monotonic-typestate\/  Manuel Fahndrich and Rustan Leino. 2003. Heap Monotonic Typestate. In Proceedings of the first International Workshop on Alias Confinement and Ownership (IWACO) (proceedings of the first international workshop on alias confinement and ownership (iwaco) ed.). https:\/\/www.microsoft.com\/en-us\/research\/publication\/heap-monotonic-typestate\/"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2018.23"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428196"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_2_27_1","volume-title":"ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. CoRR, abs\/2006.13635","author":"Frumin Dan","year":"2020"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887654.1887681"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.10.009"},{"key":"e_1_2_2_30_1","volume-title":"https:\/\/github.com\/google\/leveldb Last accessed on","author":"DB.","year":"2021"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_15"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_18"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/646752.704727"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_2_2_37_1","volume-title":"Leveled Compaction in Apache Cassandra. https:\/\/www.datastax.com\/blog\/2011\/10\/leveled-compaction-apache-cassandra Last accessed on","author":"Ellis Jonathan","year":"2021"},{"key":"e_1_2_2_38_1","volume-title":"Proceedings of the IFIP 9th World Computer Congress","author":"Jones Cliff B.","year":"1983"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158115"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_24"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_5"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_14"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009855"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.2200\/S01089ED1V01Y202104CSL013"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386029"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158125"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_12"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_37"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2013.6544834"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462189"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00778-019-00555-y"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835722"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050048"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485490"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_29"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132765"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815411"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213836.2213862"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737964"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_14"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/320473.320484"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.5555\/1884866.1884870"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/42201.42204"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026879"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2017.121"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429111"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_27"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314617"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.5555\/2813767.2813773"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.21"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29952-0_12"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485490","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485490","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485490","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485490"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":77,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485490"],"URL":"https:\/\/doi.org\/10.1145\/3485490","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}