一句话：提出可快照存储，以近普通引用的开销支持任意可变引用集合的快照与恢复，并用Iris/Coq证明其核心正确性。
本文研究命令式数据结构如何高效地捕获和恢复当前状态，以支持回溯搜索等过程，应用于类型检查器和自动定理证明器。作者受 Baker（1978）与 Conchon–Filliâtre 持久数组启发，提出可快照存储：一个可变引用集合，支持捕获任意引用集合并一次性恢复；将数据结构中的普通可变引用替换为存储引用，即可为任意数据结构增加快照能力。其关键优化“记录省略”使常见情况下读写开销几乎等同普通引用，而持久映射索引方案则有对数开销。作者还给出基于 Coq/Iris 框架的核心正确性机器化证明。
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.
@article{AllainC0S24,
title = {Snapshottable Stores},
author = {Clément Allain and Basile Clément and Alexandre Moine and Gabriel Scherer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674637}
}