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.
"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 Filliâtre, 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?"
this is a very nice result and promises to be very useful, if i am understanding it correctly. i was skeptical that they could find anything new to say in 02024 about such a well-studied problem, but the paper surprised me; they do. in fact there are many delightful things in this paper, starting with their clean and general abstract interface for union-find! (even though union-find is just their motivating example rather than anything central to the paper)
in essence, i think their proposal is to journal all the updates to your mutable store, in much the same way that transactional memory does, so that you can travel to any past or future state by replaying the journal of updates; if you change the past, you cause the timeline to diverge, but you don't lose the ability to travel back to the original timeline, because you can journal-replay your way back to the divergence point. unlike transactional memory, they don't do anything special on reads of mutable state, just writes. because they're testing on algorithms that mutate state sparingly, they get very good efficiency. moreover, their comparison is with the same algorithm using plain ocaml references, but ocaml's write barrier makes it expensive to mutate state anyway, so their efficiency looks even better
they avoid storing redundant journal entries between snapshots by using a generation counter that counts snapshots, so repeatedly mutating the same reference doesn't keep allocating memory; it just repeatedly checks the generation counter
i wonder to what extent you can combine their algorithm with umut acar's 'self-adjusting computation' to get a generic, efficient way of converting an imperative program into an incremental dataflow program?
perhaps inspired by union-find, their tree of store states is made out of only parent pointers, so you can walk up the tree (from a snapshot) to the root, but never back down. (a new child node is constructed for each parent when you do this.) this allows garbage collection to work on saved snapshots! however, a live snapshot can still keep alive an otherwise unreferenced mutable reference, even though there's no way for the user of the snapshottable store to access it
they credit fully fp-persistent shallow binding to henry baker. i don't think that's fair, much as i appreciate his work; baker himself credits shallow binding to maclisp, citing moon's maclisp reference manual, and the more capable version he describes to greenblatt's lispm, each from four years earlier. and i don't think moon or greenblatt would claim full credit for it either, nor would they claim it only dated from 01974; what was new in greenblatt's design was that it could handle lexical scoping and upward funargs, while older implementations of shallow binding could only handle dynamic scoping and downward funargs. this is the difference between 'persistence' and 'semi-persistence' in the terminology of allain et al., as they explain on page 4. to a great extent what baker was doing was explaining the technique rather than claiming credit for it
this reminds me of a section from the mother of all multics emacs papers (https://www.multicians.org/mepap.html), by bernie greenberg, about the first lisp emacs, which was written in maclisp
> The implementation of multiple buffers was viewed as a task of
multiplexing the extant function of the editor over several buffers.
The buffer being edited is defined by about two dozen Lisp variables
of the basic editor, identifying the current Editorline, its current
(open/closed) state, the first and last Editorlines of the buffer,
the list of marks, and so forth. Switching buffers (i.e., switching
the attention of the editor, as the user sees it) need consist only of
switching the values of all of these variables. Neither the interactive
driver nor the redisplay need be cognizant of the ex...
6 comments
[ 3.0 ms ] story [ 30.6 ms ] threadWe 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.
"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 Filliâtre, 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?"
in essence, i think their proposal is to journal all the updates to your mutable store, in much the same way that transactional memory does, so that you can travel to any past or future state by replaying the journal of updates; if you change the past, you cause the timeline to diverge, but you don't lose the ability to travel back to the original timeline, because you can journal-replay your way back to the divergence point. unlike transactional memory, they don't do anything special on reads of mutable state, just writes. because they're testing on algorithms that mutate state sparingly, they get very good efficiency. moreover, their comparison is with the same algorithm using plain ocaml references, but ocaml's write barrier makes it expensive to mutate state anyway, so their efficiency looks even better
they avoid storing redundant journal entries between snapshots by using a generation counter that counts snapshots, so repeatedly mutating the same reference doesn't keep allocating memory; it just repeatedly checks the generation counter
i wonder to what extent you can combine their algorithm with umut acar's 'self-adjusting computation' to get a generic, efficient way of converting an imperative program into an incremental dataflow program?
perhaps inspired by union-find, their tree of store states is made out of only parent pointers, so you can walk up the tree (from a snapshot) to the root, but never back down. (a new child node is constructed for each parent when you do this.) this allows garbage collection to work on saved snapshots! however, a live snapshot can still keep alive an otherwise unreferenced mutable reference, even though there's no way for the user of the snapshottable store to access it
they credit fully fp-persistent shallow binding to henry baker. i don't think that's fair, much as i appreciate his work; baker himself credits shallow binding to maclisp, citing moon's maclisp reference manual, and the more capable version he describes to greenblatt's lispm, each from four years earlier. and i don't think moon or greenblatt would claim full credit for it either, nor would they claim it only dated from 01974; what was new in greenblatt's design was that it could handle lexical scoping and upward funargs, while older implementations of shallow binding could only handle dynamic scoping and downward funargs. this is the difference between 'persistence' and 'semi-persistence' in the terminology of allain et al., as they explain on page 4. to a great extent what baker was doing was explaining the technique rather than claiming credit for it
this reminds me of a section from the mother of all multics emacs papers (https://www.multicians.org/mepap.html), by bernie greenberg, about the first lisp emacs, which was written in maclisp
> The implementation of multiple buffers was viewed as a task of multiplexing the extant function of the editor over several buffers. The buffer being edited is defined by about two dozen Lisp variables of the basic editor, identifying the current Editorline, its current (open/closed) state, the first and last Editorlines of the buffer, the list of marks, and so forth. Switching buffers (i.e., switching the attention of the editor, as the user sees it) need consist only of switching the values of all of these variables. Neither the interactive driver nor the redisplay need be cognizant of the ex...
* [talk overview](https://icfp24.sigplan.org/details/icfp-2024-papers/14/Snaps...)
* [youtube](https://www.youtube.com/watch?v=F70QZaMoYJQ&t=18605s)