Verifying concurrent multicopy search structures
Verifying concurrent multicopy search structures
复制标题
DOI：
10.1145/3485490
复制
发表时间：
2021-09
影响因子：
--
通讯作者：
Nisarg Patel-;Siddharth Krishna;D. Shasha;Thomas Wies
中科院分区：
文献类型：
--
作者：
Nisarg Patel-;Siddharth Krishna;D. Shasha;Thomas Wies
多副本搜索结构（如日志结构合并（LSM）树）针对高插入/更新/删除（统称为upsert）性能进行了优化。在这样的数据结构中，即使k已经存在于其他节点中，也会将添加（k，v）的密钥k上的upsert添加到根节点，其中v可以是值或墓碑。因此，在搜索结构中可能存在k的多个副本。对k的搜索旨在返回与最近的upsert相关联的值。我们提出了一个通用的框架，用于验证并行多副本搜索结构的线性化，从内存中的数据结构的底层表示抽象，使证明重用不同的实现。基于我们的框架，我们提出了（a）LSM结构形成任意有向无环图和（B）差分文件结构的模板算法，并在并发分离逻辑Iris中正式验证这些模板。我们还实例化的LSM模板，以获得第一个验证并发内存中的LSM树实现。
Multicopy search structures such as log-structured merge (LSM) trees are optimized for high insert/update/delete (collectively known as upsert) performance. In such data structures, an upsert on key k, which adds (k,v) where v can be a value or a tombstone, is added to the root node even if k is already present in other nodes. Thus there may be multiple copies of k in the search structure. A search on k aims to return the value associated with the most recent upsert. We present a general framework for verifying linearizability of concurrent multicopy search structures that abstracts from the underlying representation of the data structure in memory, enabling proof-reuse across diverse implementations. Based on our framework, we propose template algorithms for (a) LSM structures forming arbitrary directed acyclic graphs and (b) differential file structures, and formally verify these templates in the concurrent separation logic Iris. We also instantiate the LSM template to obtain the first verified concurrent in-memory LSM tree implementation.