SHF: Small: Modular Automated Verification of Concurrent Data Structures

点击翻译按钮获取中文摘要

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.