https://dl.acm.org/doi/10.1145/3674637 skip to main content * ACM Digital Library home * ACM Association for Computing Machinery corporate logo * Advanced Search * Browse * About * + Sign in + Register * * Advanced Search * Journals * Magazines * Proceedings * Books * SIGs * Conferences * People * * More * Search ACM Digital Library[ ] SearchSearch Advanced Search Proceedings of the ACM on Programming Languages * Journal Home * Just Accepted * Latest Issue * * Archive * Authors + Author Guidelines + Calls for Papers + PACMPL Policies + ACM Author Policies + Author List * Editors + Editorial Board + Associate Editors Welcome Video * Reviewers * Open Access + PACMPL Open Access + ACM Open Access * Award Winners * About + About PACMPL + Announcements + Abstracting/Indexing + PACMPL Affiliations * Contact Us * More * Home * ACM Journals * Proceedings of the ACM on Programming Languages * Vol. 8, No. ICFP * Snapshottable Stores research-article Open access Share on * * * * * * Snapshottable Stores Authors: [default-pr]Clement Allain, [default-pr]Basile Clement, [contrib-99]Alexandre Moine, [default-pr]Gabriel SchererAuthors Info & Claims Proceedings of the ACM on Programming Languages, Volume 8, Issue ICFP Article No.: 248, Pages 338 - 369 https://doi.org/10.1145/3674637 Published: 15 August 2024 Publication History 0citation98Downloads Metrics Total Citations0 Total Downloads98 Last 12 Months98 Last 6 weeks98 Get Citation Alerts New Citation Alert added! This alert has been successfully added and will be sent to: You will be notified whenever a record that you have chosen has been cited. To manage your alert preferences, click on the button below. Manage my Alerts New Citation Alert! Please log in to your account PDFeReader * Contents Proceedings of the ACM on Programming Languages Volume 8, Issue ICFP PREVIOUS ARTICLE Example-Based Reasoning about the Realizability of Polymorphic Programs Previous NEXT ARTICLE Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl) Next + Abstract + References ACM Digital Library * + Information & Contributors + Bibliometrics & Citations + View Options + References + Media + Tables + Share Abstract We say that an imperative data structure is snapshottable or supports snapshots 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. Inspired by a data structure proposed in 1978 by Baker, we present a snapshottable 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. 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. The implementation, which is inspired by Baker's and the OCaml implementation of persistent arrays by Conchon and Filliatre, 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. References [1] Alberto Apostolico, Giuseppe F. Italiano, Giorgio Gambosi, and Maurizio Talamo. 1994. " The Set Union Problem with Unlimited Backtracking." SIAM Journal on Computing, 23, 1, 50-70. Digital Library Google Scholar [2] Phil Bagwell. 2001. Ideal Hash Trees. Tech. rep. EPFL. http:// infoscience.epfl.ch/record/64398. Google Scholar [3] Henry G. Baker. July 1978. "Shallow binding in Lisp 1.5." Communications of the ACM, 21, 7, ( July 1978 ), 565-569. Digital Library Google Scholar [4] Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Notzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. "cvc5: A Versatile and Industrial-Strength SMT Solver." In: Tools and Algorithms for the Construction and Analysis of Systems-28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I (Lecture Notes in Computer Science). Ed. by Dana Fisman and Grigore Rosu. Vol. 13243. Springer, 415-442. Digital Library Google Scholar [5] Michael A. Bender, Richard Cole, Erik D. Demaine, Martin Farach-Colton, and Jack Zito. Sept. 2002. " Two Simplified Algorithms for Maintaining Order in a List." In: Proceedings of the 10th Annual European Symposium on Algorithms (ESA 2002 ) (Lecture Notes in Computer Science). Vol. 2461. (Sept. 2002 ), 152-164. Crossref Google Scholar [6] Guillaume Bury, Basile Clement, 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/. Google Scholar [7] Lee Byron, Immutable.js library for JavaScript version 4.3.5, 2024. url: https://github.com/immutable-js/immutable-js/, swhid: < swh:1:rev:d7664bf9d3539da8ea095f2ed08bbe1cd0d46071> . Google Scholar [8] Yun-Sheng Chang, vMVCC 2023. url: https://github.com/mit-pdos/vmvcc/ blob/116f2a360d4390896cf042547caf757ab881e0 2a/wrbuf/wrbuf.go, swhid: < swh:1:dir:49034898d0dbbad741eadffa4501896fc17fb635> . Google Scholar [9] Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. July 2023. "Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. " In: OSDI. (July 2023 ). Google Scholar [10] Arthur Chargueraud. 2022. The CFML tool and library. http:// www.chargueraud.org/softs/cfml/. ( 2022 ). Google Scholar [11] Arthur Chargueraud and Francois Pottier. Mar. 2019. "Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. " Journal of Automated Reasoning, 62, 3, ( Mar. 2019 ), 331-365. http://cambium.inria.fr/ ~fpottier/publis/chargueraud-pottier-uf-sltc.pdf. Digital Library Google Scholar [12] Tyng-Ruey Chuang. 1994. "A randomized implementation of multiple functional arrays." In: ACM conference on LISP and functional programming, 173-184. Digital Library Google Scholar [13] Tyng-Ruey Chuang. 1992. " Fully persistent arrays for eficient incremental updates and voluminous reads." In: ESOP '92: 4th European symposium on programming, 110-129. Crossref Google Scholar [14] Basile Clement and Gabriel Scherer, Store 2023. url: https:// gitlab.com/basile.clement/store/-/ tree/37a14f 538e75eea3de930a 797623e7f 7f d036948, swhid: . Google Scholar [15] Sylvain Conchon and Jean-Christophe Filliatre. Oct. 2007. " A Persistent Union-Find Data Structure." In: ACM SIGPLAN Workshop on ML. ACM Press, Freiburg, Germany, (Oct. 2007 ), 37-45. http:// www.lri.f r/~f illiatr/f tp/publis/puf-wml07.pdf. Digital Library Google Scholar [16] Sylvain Conchon and Jean-Christophe Filliatre. Apr. 2008. " Semi-Persistent Data Structures." In: 17th European Symposium on Programming (ESOP'08). (Apr. 2008 ). http://www.lri.f r/~f illiatr/f tp/publis/spds-rr. pdf. Crossref Google Scholar [17] Erik Demaine, Stefan Langerman, and Eric Price. July 2008. "Confluently Persistent Tries for Eficient Version Control. " Algorithmica, 57, ( July 2008 ), 462-483. Crossref Google Scholar [18] Paul F. Dietz. 1989. " Fully persistent arrays." In: Algorithms and Data Structures, 67-74. Crossref Google Scholar [19] J. R. Driscoll, N. Sarnak, D. D. Sleator, and R. E. Tarjan. 1989. " Making data structures persistent. " Journal of Computer and System Sciences, 38, 1, 86-124. https://www.cs.cmu.edu/~sleator/papers/ another-persistence.pdf. Digital Library Google Scholar [20] John De Goes, zio-stm 2019. url: https://github.com/zio/zio/blob/ ecb38a3bf 15b085080f 9c092dbbd88091f 5ebb32/core/shared /src/main/ scala/zio/stm/TRef.scala, swhid: < swh:1:dir:0b66f 0e8e1427d8f 8cf d448843f 1b838765a17f 8> . Google Scholar [21] Tobias Gustafsson, Pyrsistent library for Python version 0.20.0, 2023. url: https://github.com/tobgu/pyrsistent, swhid: < swh:1:rev:827c5c8f 6135ee4977ea96e507367904689a2397> . Google Scholar [22] Tim Harris and Simon Marlow, ghc-stm 2004. url: https://github.com/ ghc/ghc/blob/f 2cc1107790d42f ee1a11d5b16bc282d31 ea6f 78/rts/STM.c, swhid: < swh:1:cnt:69b00f d127568d33f 0da7a8a9f 7c140de1bc129f > . Google Scholar [23] Barry Hayes. Oct. 1997. " Ephemerons: a new finalization mechanism." SIGPLAN Not., 32, 10, (Oct. 1997 ), 176-183. Digital Library Google Scholar [24] Hickey and contributors. 2024. Clojure Reference Manual on Transient Data Structures. https://clojure.org/ref erence/transients. ( 2024 ). Google Scholar [25] 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. " Journal of Functional Programming, 28, e20. https://people.mpi-sws.org/~dreyer/ papers/iris-ground-up/paper.pdf. Crossref Google Scholar [26] Vesa Karvonen, kcas 2024. url: https://github.com/ocaml-multicore/ kcas, swhid: < swh:1:dir:a85e74c5bd4e1af 9802e0a3f c23 7f 1531281ce31> . Google Scholar [27] Alexandre Moine, Arthur Chargueraud, and Francois Pottier. 2022. "Specification and verification of a transient stack." In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022 ). Association for Computing Machinery, Philadelphia, PA, USA, 82-99. isbn: 9781450391825. Digital Library Google Scholar [28] Melissa E. O'Neill and F. Warren Burton. Sept. 1997. "A new method for functional arrays. " J. Funct. Program., 7, 5, ( Sept. 1997 ), 487-513. Digital Library Google Scholar [29] Francois Pottier. Sept. 2014. " Hindley-Milner elaboration in applicative style." In: International Conference on Functional Programming (ICFP). (Sept. 2014 ). http://cambium.inria.f r/~f pottier/publis/f pottier-elaboration.pdf. Digital Library Google Scholar [30] Juan Pedro Bolivar Puente. Aug. 2017. " Persistence for the masses: RRB-vectors in a systems language. " Proc. ACM Program. Lang., 1, ICFP, ( Aug. 2017 ). Digital Library Google Scholar [31] Alex Reinking, Ningning Xie, Leonardo de Moura, and Daan Leijen. 2021. " Perceus: garbage free reference counting with reuse. " In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021 ). Virtual, Canada, 96-111. Digital Library Google Scholar [32] Gabriel Scherer. 2023. " Backtracking reference stores." In: JFLA. https://hal.science/hal-03936704. Google Scholar [33] Gabriel Scherer. 2024. Constrained generation of well-typed programs. Tech. rep. INRIA. https://inria.hal.science/hal-04607309. Google Scholar [34] 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-m utation, swhid: . Google Scholar [35] Jefery Westbrook and Robert E. Tarjan. 1989. " Amortized Analysis of Algorithms for Set Union with Backtracking." SIAM Journal on Computing, 18, 1, 1-11. Digital Library Google Scholar Index Terms 1. Snapshottable Stores 1. Software and its engineering 1. Software notations and tools 1. General programming languages 1. Language types 1. Functional languages 2. Theory of computation 1. Design and analysis of algorithms 1. Data structures design and analysis 2. Semantics and reasoning 1. Program reasoning 1. Program verification Recommendations * KVell: the design and implementation of a fast persistent key-value store SOSP '19: Proceedings of the 27th ACM Symposium on Operating Systems Principles Modern block-addressable NVMe SSDs provide much higher bandwidth and similar performance for random and sequential access. Persistent key-value stores (KVs) designed for earlier storage devices, using either Log-Structured Merge (LSM) or B trees, do not ... Read More * Can Applications Recover from fsync Failures? We analyze how file systems and modern data-intensive applications react to fsync failures. First, we characterize how three Linux file systems (ext4, XFS, Btrfs) behave in the presence of failures. We find commonalities across file systems (pages are ... Read More * Building Efficient Key-Value Stores via a Lightweight Compaction Tree Special Issue on MSST 2017 and Regular Papers Log-Structure Merge tree (LSM-tree) has been one of the mainstream indexes in key-value systems supporting a variety of write-intensive Internet applications in today's data centers. However, the performance of LSM-tree is seriously hampered by ... Read More Comments Please enable JavaScript to view thecomments powered by Disqus. Information & Contributors Information Published In cover image Proceedings of the ACM on Programming Languages Proceedings of the ACM on Programming Languages Volume 8, Issue ICFP August 2024 1031 pages EISSN:2475-1421 DOI:10.1145/3554318 * Editor: * Author PictureMichael Hicks Amazon, USA Issue's Table of Contents Copyright (c) 2024 Owner/Author. This work is licensed under a Creative Commons Attribution International 4.0 License. Publisher Association for Computing Machinery New York, NY, United States Publication History Published: 15 August 2024 Published in PACMPL Volume 8, Issue ICFP Permissions Request permissions for this article. Request Permissions Check for updates Author Tags 1. Backtracking 2. Persistence 3. Program verification 4. Semi-persistence Qualifiers * Research-article Contributors [loader-7e6] Other Metrics View Article Metrics Bibliometrics & Citations Bibliometrics Article Metrics * 0 Total Citations * 98 Total Downloads * Downloads (Last 12 months)98 * Downloads (Last 6 weeks)98 Reflects downloads up to 30 Aug 2024 Other Metrics View Author Metrics Citations View Options View options PDF View or Download as a PDF file. PDF eReader View online with eReader. eReader Get Access Login options Check if you have access through your login credentials or your institution to get full access on this article. Sign in Full Access Get this Article Media Figures Other Tables Share Share Share this Publication link Copy Link Copied! Copying failed. Share on social media XLinkedInRedditFacebookemail Affiliations [default-pr] Clement Allain Inria, Paris, France https://orcid.org/0009-0005-2972-5181 View Profile [default-pr] Basile Clement OCamlPro, Paris, France https://orcid.org/0000-0002-9126-0937 View Profile [contrib-99] Alexandre Moine Inria, Paris, France https://orcid.org/0000-0002-2169-1977 View Profile [default-pr] Gabriel Scherer Universite Paris Cite, Inria, CNRS, Paris, France https://orcid.org/0000-0003-1758-3938 View Profile Download PDF Go to Go to Show all references Request permissionsExpand All Collapse Expand Table Authors Info & Affiliations View Issue's Table of Contents Export Citations Select Citation format[BibTeX ] * Please download or close your previous search result export first before starting a new bulk export. Preview is not available. By clicking download,a status dialog will open to start the export process. The process may takea few minutes but once it finishes a file will be downloadable from your browser. You may continue to browse the DL while the export process is in progress. Download + Download citation + Copy citation Footer Categories * Journals * Magazines * Books * Proceedings * SIGs * Conferences * Collections * People About * About ACM Digital Library * ACM Digital Library Board * Subscription Information * Author Guidelines * Using ACM Digital Library * All Holdings within the ACM Digital Library * ACM Computing Classification System * Accessibility Statement Join * Join ACM * Join SIGs * Subscribe to Publications * Institutions and Libraries Connect * Contact us via email * ACM on Facebook * ACM DL on X * ACM on Linkedin * Send Feedback * Submit a Bug Report The ACM Digital Library is published by the Association for Computing Machinery. Copyright (c) 2024 ACM, Inc. * Terms of Usage * Privacy Policy * Code of Ethics ACM Digital Library home ACM Association for Computing Machinery corporate logo Your Search Results Download Request We are preparing your search results for download ... We will inform you here when the file is ready. Download now! Your Search Results Download Request Your file of search results citations is now ready. Download now! Your Search Results Download Request Your search export query has expired. Please try again.