SHF: Small: Modular Automated Verification of Concurrent Data Structures

并发搜索结构是提供对多核和分布式服务器上的键值对的快速访问的数据结构和并行算法。并行算法在线程之间执行细粒度的同步，这使得它们很难正确设计。事实上，无论是在实际实现中还是在同行评审出版物中专家提出的设计中，都发现了错误。这些并发算法的快速开发和部署导致了可以通过最先进的技术验证的算法与今天开发和使用的算法之间的裂痕。该项目的新颖性是新的推理原理和伴随的静态程序分析技术，用于验证并发搜索结构，从而弥合这一裂痕。该项目的影响是通过验证在现实世界应用程序中发现的高度复杂的并发数据结构来提高软件系统的可靠性。该项目的成果包括一个经过验证的并发搜索结构算法的模块化程序库。也就是说，用户将能够自由地选择搜索结构(例如，链表、B-树、哈希表、日志结构合并树)和同步算法(例如，基于锁的、无锁的、或两者的混合)。将产生已验证的代码。最后，所开发的程序逻辑和伴随的静态分析不仅适用于并发搜索结构，还广泛应用于程序验证。首先，并发数据结构可以由模板算法来描述，模板算法规定了线程如何交互，但从结构的具体内存布局中抽象出来。因此，相同的模板可以应用于不同的数据结构，例如散列结构、B树和列表。一旦验证了模板算法，就可以在单个数据结构上实例化其证明。第二个要素是流框架，它是验证模板算法的关键。流框架提供了一种基于分离逻辑的抽象机制，允许人们以局部方式推理一般图的全局归纳不变量，同时从低级堆表示中抽象出来。该项目解决了以下具体的研究挑战：(I)如何自动构建并发数据结构操作的线性化证明，其线性化点依赖于其他线程未来的干扰；(Ii)如何自动推断以流框架表示的数据结构不变量；以及(Iii)如何构建新的无锁以及基于锁和无锁的混合并发数据结构的模板算法。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Concurrent search structures are data structures and parallel algorithms that provide fast access to key-value pairs on multicore and distributed servers. The parallel algorithms perform fine-grained synchronization between threads, making them notoriously difficult to design correctly. Indeed, bugs have been found both in actual implementations and in the designs proposed by experts in peer-reviewed publications. The rapid development and deployment of these concurrent algorithms has resulted in a rift between the algorithms that can be verified by the state-of-the-art techniques and those being developed and used today. The project's novelties are new reasoning principles and accompanying static program analyses techniques for verifying concurrent search structures that will close this rift. The project's impacts are an increase in the reliability of software systems by verifying the highly complex concurrent data structures found in real world applications. The project's outcome includes a modular library of verified concurrent search structure algorithms. That is, a user will be able to freely choose both the search structure (e.g., linked list, B-tree, hash table, Log Structured Merge-tree) and the synchronization algorithm (e.g., lock-based, lock-free, or a mixture of the two). Verified code will result. Finally, the developed program logic and accompanying static analyses apply to program verification broadly, beyond concurrent search structures.The research rests on two key ingredients. The first is that concurrent data structures can be described by template algorithms that dictate how threads interact but abstract away from the structure's concrete memory layout. Thus, the same template can apply to diverse data structures such as hash structures, B-trees, and lists. Once a template algorithm is verified, its proof can be instantiated on individual data structures. The second ingredient, the flow framework, is crucial for verifying the template algorithms. The flow framework provides a separation logic-based abstraction mechanism that allows one to reason about global inductive invariants of general graphs in a local manner, while abstracting from low-level heap representations. The project addresses the following specific research challenges: (i) how to automatically construct linearizability proofs for concurrent data structure operations whose linearization points depend on future interferences by other threads; (ii) how to automatically infer data structure invariants that are expressed in terms of the flow framework; and (iii) how to construct new template algorithms for lock-free, as well as mixed lock-based and lock-free concurrent data structures.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.