{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T09:05:10Z","timestamp":1787043910312,"version":"3.56.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T00:00:00Z","timestamp":1723680000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,8,15]]},"abstract":"<jats:p>\n                    We say that an imperative data structure is\n                    <jats:italic toggle=\"yes\">snapshottable<\/jats:italic>\n                    or\n                    <jats:italic toggle=\"yes\">supports snapshots<\/jats:italic>\n                    if we can efficiently capture its current state, and restore a previously captured state to become the current state again. This is useful, for example, to implement backtracking search processes that update the data structure during search.\n                  <\/jats:p>\n                  <jats:p>\n                    Inspired by a data structure proposed in 1978 by Baker, we present a\n                    <jats:italic toggle=\"yes\">snapshottable<\/jats:italic>\n                    store, a bag of mutable references that supports snapshots. Instead of capturing and restoring an array, we can capture an arbitrary set of references (of any type) and restore all of them at once. This snapshottable store can be used as a building block to support snapshots for arbitrary data structures, by simply replacing all mutable references in the data structure by our store references. We present use-cases of a snapshottable store when implementing type-checkers and automated theorem provers.\n                  <\/jats:p>\n                  <jats:p>Our implementation is designed to provide a very low overhead over normal references, in the common case where the capture\/restore operations are infrequent. Read and write in store references are essentially as fast as in plain references in most situations, thanks to a key optimisation we call record elision. In comparison, the common approach of replacing references by integer indices into a persistent map incurs a logarithmic overhead on reads and writes, and sophisticated algorithms typically impose much larger constant factors.<\/jats:p>\n                  <jats:p>The implementation, which is inspired by Baker\u2019s and the OCaml implementation of persistent arrays by Conchon and Filli\u00e2tre, is both fairly short and very hard to understand: it relies on shared mutable state in subtle ways. We provide a mechanized proof of correctness of its core using the Iris framework for the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3674637","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"338-369","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Snapshottable Stores"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-2972-5181","authenticated-orcid":false,"given":"Cl\u00e9ment","family":"Allain","sequence":"first","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9126-0937","authenticated-orcid":false,"given":"Basile","family":"Cl\u00e9ment","sequence":"additional","affiliation":[{"name":"OCamlPro, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2169-1977","authenticated-orcid":false,"given":"Alexandre","family":"Moine","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1758-3938","authenticated-orcid":false,"given":"Gabriel","family":"Scherer","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Cit\u00e9, Inria, CNRS, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"Cl\u00e9ment Allain \u201cMechanization of the snapshottable store with record elision and without transactions \u201d part of The Zoo project 2024. url: https:\/\/github.com\/clef-men\/zoo\/blob\/icfp2024\/theories\/persistent\/pstore_2.v swhid: <swh:1:cnt:e637417fb4af3a462caa063a575e97905d32800b)."},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539789173597"},{"key":"e_1_3_1_4_1","volume-title":"Ideal Hash Trees","author":"Bagwell Phil","year":"2001","unstructured":"Phil Bagwell. 2001. Ideal Hash Trees. Tech. rep. EPFL. http:\/\/infoscience.epfl.ch\/record\/64398."},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359566"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_7_1","first-page":"152","article-title":"\u201cTwo Simplified Algorithms for Maintaining Order in a List.\u201d","volume":"2461","author":"Bender Michael A.","year":"2002","unstructured":"Michael A. Bender, Richard Cole, Erik D. Demaine, Martin Farach-Colton, and Jack Zito. Sept. 2002. \u201cTwo Simplified Algorithms for Maintaining Order in a List.\u201d In: Proceedings of the 10th Annual European Symposium on Algorithms (ESA 2002) (Lecture Notes in Computer Science). Vol. 2461. (Sept. 2002), 152-164.","journal-title":"Proceedings of the 10th Annual European Symposium on Algorithms (ESA 2002) (Lecture Notes in Computer Science)"},{"key":"e_1_3_1_8_1","unstructured":"Guillaume Bury Basile Cl\u00e9ment Albin Coquereau Sylvain Conchon Evelyne Contejean Steven de Olivera Hichem Rami Ait El Hara Mohamed Iguernlala Stephane Lescuyer Alain Mebsout Mattias Roux and Pierre Villemot. 2015. the Alt-Ergo SMT solver. (2015). https:\/\/alt-ergo.ocamlpro.com\/."},{"key":"e_1_3_1_9_1","unstructured":"Lee Byron Immutable.js library for JavaScript version 4.3.5 2024. url: https:\/\/github.com\/immutable-js\/immutable-js\/ swhid: (swh:1:rev:d7664bf9d3539da8ea095f2ed08bbe1cd0d4607l)."},{"key":"e_1_3_1_10_1","unstructured":"Yun-Sheng Chang vMVCC 2023. url: https:\/\/github.com\/mit-pdos\/vmvcc\/blob\/116f2a360d4390896cf042547caf757ab881e02a\/wrbuf\/wrbuf.go swhid: (swh:1:dir:49034898d0dbbad741eadffa4501896fc17fb635)."},{"key":"e_1_3_1_11_1","unstructured":"Yun-Sheng Chang Ralf Jung Upamanyu Sharma Joseph Tassarotti M. Frans Kaashoek and Nickolai Zeldovich. July 2023. \u201cVerifying vMVCC a high-performance transaction library using multi-version concurrency control.\u201d In: OSDI. (July 2023)."},{"key":"e_1_3_1_12_1","unstructured":"Arthur Chargu\u00e9raud. 2022. The CFML tool and library. http:\/\/www.chargueraud.org\/softs\/cfml\/. (2022)."},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9431-7"},{"key":"e_1_3_1_14_1","doi-asserted-by":"crossref","unstructured":"Tyng-Ruey Chuang. 1994. \u201cA randomized implementation of multiple functional arrays.\u201d In: ACM conference on LISP and functional programming 173-184.","DOI":"10.1145\/182590.156779"},{"key":"e_1_3_1_15_1","doi-asserted-by":"crossref","unstructured":"Tyng-Ruey Chuang. 1992. \u201cFully persistent arrays for efficient incremental updates and voluminous reads.\u201d In: ESOP \u201992: 4th European symposium on programming 110-129.","DOI":"10.1007\/3-540-55253-7_7"},{"key":"e_1_3_1_16_1","unstructured":"Basile Cl\u00e9ment and Gabriel Scherer Store 2023. url: https:\/\/gitlab.com\/basile.clement\/store\/-\/tree\/37a14f538e75eea3de930a797623e7f7fd036948 swhid: < swh:1:rev:37a14f538e75eea3de930a797623e7f7fd036948=."},{"key":"e_1_3_1_17_1","first-page":"37","volume-title":"ACM SIGPLAN Workshop on ML","author":"Conchon Sylvain","year":"2007","unstructured":"Sylvain Conchon and Jean-Christophe Filli\u00e2tre. Oct. 2007. \u201cA Persistent Union-Find Data Structure.\u201d In: ACM SIGPLAN Workshop on ML. ACM Press, Freiburg, Germany, (Oct. 2007), 37-45. http:\/\/www.lri.fr\/~filliatr\/ftp\/publis\/puf-wml07.pdf."},{"key":"e_1_3_1_18_1","unstructured":"Sylvain Conchon and Jean-Christophe Filli\u00e2tre. Apr. 2008. \u201cSemi-Persistent Data Structures.\u201d In: 17th European Symposium on Programming (ESOP\u201908). (Apr. 2008). http:\/\/www.lri.fr\/~filliatr\/ftp\/publis\/spds-rr.pdf."},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00453-008-9274-z"},{"key":"e_1_3_1_20_1","doi-asserted-by":"crossref","unstructured":"Paul F. Dietz. 1989. \u201cFully persistent arrays.\u201d In: Algorithms and Data Structures 67-74.","DOI":"10.1007\/3-540-51542-9_8"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90034-2"},{"key":"e_1_3_1_22_1","unstructured":"John De Goes zio-stm 2019. url: https:\/\/github.com\/zio\/zio\/blob\/ecb38a3bf15b085080f9c092dbbd88091f5ebb32\/core\/shared\/src\/main\/scala\/zio\/stm\/TRef.scala swhid: (swh:1:dir:0b66f0e8e1427d8f8cfd448843f1b838765a17f8)."},{"key":"e_1_3_1_23_1","unstructured":"Tobias Gustafsson Pyrsistent library for Python version 0.20.0 2023. url: https:\/\/github.com\/tobgu\/pyrsistent swhid: <swh:1:rev:827c5c8f6135ee4977ea96e507367904689a2397)."},{"key":"e_1_3_1_24_1","unstructured":"Tim Harris and Simon Marlow ghc-stm 2004. url: https:\/\/github.com\/ghc\/ghc\/blob\/f2cc1107790d42fee1a11d5b16bc282d31ea6f78\/rts\/STM.c swhid: (swh:1:cnt:69b00fd127568d33f0da7a8a9f7c140de1bc129f)."},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/263700.263733"},{"key":"e_1_3_1_26_1","unstructured":"Hickey and contributors. 2024. Clojure Reference Manual on Transient Data Structures. https:\/\/clojure.org\/reference\/transients. (2024)."},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_28_1","unstructured":"Vesa Karvonen kcas 2024. uri: https:\/\/github.com\/ocaml-multicore\/kcas swh\u00edd: (swh:1:dir:a85e74c5bd4e1af9802e0a3fc23 7f1531281ce31)."},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503677"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002852"},{"key":"e_1_3_1_31_1","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois Pottier. Sept. 2014. \u201cHindley-Milner elaboration in applicative style.\u201d In: International Conference on Functional Programming (ICFP). (Sept. 2014). http:\/\/cambium.inria.fr\/~fpottier\/publis\/fpottier-elaboration.pdf.","DOI":"10.1145\/2628136.2628145"},{"key":"e_1_3_1_32_1","volume-title":"JFLA 2021 - 32es Journ\u00e9es Francophones des Langages Applicatifs","author":"Pottier Fran\u00e7ois","year":"2021","unstructured":"Fran\u00e7ois Pottier. Feb. 2021. \u201cStrong Automated Testing of OCaml Libraries.\u201d In: JFLA 2021 - 32es Journ\u00e9es Francophones des Langages Applicatifs. Saint M\u00e9dard d\u2019Excideuil, France, (Feb. 2021). https:\/\/inria.hal.science\/hal-03049511."},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110260"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454032"},{"key":"e_1_3_1_35_1","unstructured":"Gabriel Scherer. 2023. \u201cBacktracking reference stores.\u201d In: JFLA. https:\/\/hal.science\/hal-03936704."},{"key":"e_1_3_1_36_1","volume-title":"Constrained generation of well-typed programs","author":"Scherer Gabriel","year":"2024","unstructured":"Gabriel Scherer. 2024. Constrained generation of well-typed programs. Tech. rep. INRIA. https:\/\/inria.hal.science\/hal-04607309."},{"key":"e_1_3_1_37_1","unstructured":"Bodil Stokke im crate in Rust: in-place mutation version 9.0.0 2018. url: https:\/\/docs.rs\/im\/latest\/im\/index.html#in-place-mutation swh\u00edd: <swh:1:rev:71331eadac64654bc56f598647ab544197cb1319)."},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1137\/0218001"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674637","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674637","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:50:32Z","timestamp":1770191432000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674637"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":37,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,15]]}},"alternative-id":["10.1145\/3674637"],"URL":"https:\/\/doi.org\/10.1145\/3674637","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,15]]},"assertion":[{"value":"2024-02-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}