[HN Gopher] Snapshottable Stores
       ___________________________________________________________________
        
       Snapshottable Stores
        
       Author : matt_d
       Score  : 10 points
       Date   : 2024-09-04 21:18 UTC (1 hours ago)
        
 (HTM) web link (dl.acm.org)
 (TXT) w3m dump (dl.acm.org)
        
       | jauntywundrkind wrote:
       | This is the way.
       | 
       | We already have computing starting to log itself clearly via
       | OpenTelemtry. This feels like only a small jump, to recording
       | your processing just a little bit better.
       | 
       | There used to be a background rumbling about hardware
       | trasnsactional memory. But it never seemed like we needed
       | hardware, we always just needed better state snapshotting as we
       | go.
        
       | matt_d wrote:
       | 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."
       | 
       | Motivating example:
       | 
       | "Union-Find is a central data structure in several algorithms.
       | For example, it is at the core of ML type inference, which
       | proceeds by repeated unification between type variables. Union-
       | Find can also be used to track equalities between type
       | constructors, as introduced in the typing environment when type-
       | checking Guarded Algebraic Data Types (GADTs) for example.
       | 
       | When using a Union-Find data structure to implement a type
       | system, it is common to need backtracking, which requires the
       | inference state to be snapshottable. For example:
       | 
       | (1) A single unification between two types during ML type
       | inference translates into several unifications between type
       | variables, traversing the structure of the two types. If we
       | discover that the two types are in fact incompatible, we fail
       | with a type error. However, we may want to revert the
       | unifications that were already performed, so that the error
       | message shown to the user does not include confusing signs of
       | being halfway through the unification, or so that the interactive
       | toplevel session can continue in a clean environment.
       | 
       | (2) Production languages unfortunately have to consider
       | backtracking to implement certain less principled typing rules:
       | try A, and if it fails revert to a clean state and try B instead.
       | 
       | (3) GADT equations are only added to the typing environment in
       | the context of a given match clause, and must then be rolled back
       | before checking the other clauses.
       | 
       | We have encountered requirements (1) and (2) in the
       | implementation of the OCaml type-checker, and (1) and (3) in the
       | development of Inferno [Pottier, 2014], a prototype type-
       | inference library implemented in OCaml that aims to be efficient.
       | 
       | Now a question for the reader: how would you change the Union-
       | Find implementation above to support snapshots?"
        
       ___________________________________________________________________
       (page generated 2024-09-04 23:00 UTC)