Verifying concurrent search structure templates
Verifying concurrent search structure templates
复制标题
DOI：
10.1145/3385412.3386029
复制
发表时间：
2020-06
期刊：
影响因子：
--
通讯作者：
Siddharth Krishna;Nisarg Patel-;D. Shasha
中科院分区：
文献类型：
--
作者：
Siddharth Krishna;Nisarg Patel-;D. Shasha
并发分离逻辑在并发数据结构的推理方面取得了巨大的成功。这种成功源于他们在多个层次上应用模块化，导致根据程序结构，程序状态和单个线程分解的证明。尽管有这些进步，但仍然很难在不同的数据结构实现中实现证明重用。对于大类的搜索结构，我们演示了如何可以实现进一步的证明模块化解耦线程安全的证明结构完整性的证明。我们的工作基于Shasha和Goodman的模板算法，这些算法决定了线程如何交互，但抽象于内存中节点的具体布局。基于最近提出的组合抽象和分离逻辑Iris的流程框架，我们展示了如何证明模板算法的正确性，以及如何实例化它们以获得多个经过验证的实现。我们证明了我们的方法，通过机械化的证明三个并发搜索结构模板，基于链接，放弃，锁耦合同步，并得出验证的实现基于B-树，哈希表和链表。这些案例研究包括现实世界文件系统和数据库中使用的算法，这些算法已经超出了之前自动化或机械化验证技术的能力。此外，我们的方法降低了证明的复杂性，并能够实现显着的证明重用。
Concurrent separation logics have had great success reasoning about concurrent data structures. This success stems from their application of modularity on multiple levels, leading to proofs that are decomposed according to program structure, program state, and individual threads. Despite these advances, it remains difficult to achieve proof reuse across different data structure implementations. For the large class of search structures, we demonstrate how one can achieve further proof modularity by decoupling the proof of thread safety from the proof of structural integrity. We base our work on the template algorithms of Shasha and Goodman that dictate how threads interact but abstract from the concrete layout of nodes in memory. Building on the recently proposed flow framework of compositional abstractions and the separation logic Iris, we show how to prove correctness of template algorithms, and how to instantiate them to obtain multiple verified implementations. We demonstrate our approach by mechanizing the proofs of three concurrent search structure templates, based on link, give-up, and lock-coupling synchronization, and deriving verified implementations based on B-trees, hash tables, and linked lists. These case studies include algorithms used in real-world file systems and databases, which have been beyond the capability of prior automated or mechanized verification techniques. In addition, our approach reduces proof complexity and is able to achieve significant proof reuse.