SHF: Small: Modular Automated Verification of Concurrent Data Structures

SHF：小型：并发数据结构的模块化自动验证

• 批准号: 2304758
• 负责人: Thomas Wies
• 金额: $ 60万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2304758&HistoricalAwards=false
• 关键词: SHF; Small; Modular; Automated; Verification

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.

并发搜索结构是数据结构和并行算法，可快速访问多层和分布式服务器上的键值对。并行算法在线程之间执行细粒度的同步，这使得它们难以正确设计。实际上，在实际实施和同行评审出版物专家提出的设计中都发现了错误。这些并发算法的快速发展和部署导致算法之间的裂痕可以通过最先进的技术与当今开发和使用的技术进行验证。该项目的新颖性是新的推理原则，并且随附的静态程序分析技术，用于验证将关闭此裂痕的并发搜索结构。该项目的影响是通过验证在现实世界应用中发现的高度复杂的并发数据结构来提高软件系统的可靠性。该项目的结果包括经过验证的并发搜索结构算法的模块化库。也就是说，用户将能够自由选择搜索结构（例如，链接列表，b-tree，hash表，日志结构合并-tree）和同步算法（例如，基于锁定，无锁或两者的混合物）。验证的代码将结果。最后，开发的程序逻辑和随附的静态分析适用于程序验证，超出并发搜索结构。研究基于两种关键成分。首先是可以通过模板算法来描述并发数据结构，该算法决定线程如何相互作用，但抽象从结构的混凝土内存布局中抽象。因此，相同的模板可以应用于哈希结构，b-树和列表等各种数据结构。一旦验证了模板算法，就可以在单个数据结构上实例化其证明。第二个成分（流程框架）对于验证模板算法至关重要。该流程框架提供了一种基于分离逻辑的抽象机制，该机制可以以局部方式对一般图形的全局电感不变性进行推理，同时从低级堆表示中抽象。该项目应对以下具体研究挑战：（i）如何自动为并发数据结构操作构建线性化证明，其线性化点取决于其他线程的未来干扰； （ii）如何自动推断出根据流框架表达的数据结构； （iii）如何为无锁以及基于锁的混合锁和无锁的数据结构构建新的模板算法。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的智力优点和更广泛影响的审查标准通过评估来获得支持的。