A Formal Interface for Concurrent Search Structure Templates
摘要
Concurrent search structure templates simplify reasoning about concurrent data structures by dividing them into synchronization patterns and underlying sequential data structures, which can be designed and verified independently. Past work has used templates to decompose the verification of specific data structures and reuse some of their components, but has not given a general characterization of what makes a concurrency template or whether it can be applied to a given data structure. In this paper, we formally define the interface provided by search structure templates, and show that as long as a sequential data structure component and a concurrency template are proved to implement this interface, they can immediately compose into a verified concurrent data structure with no additional effort. Thus, from any m verified data structure components and n verified concurrency components, we obtain \(m \times n\) verified data structures. We validate our interface by verifying two data structure instances (linked list and binary search tree) and three concurrency templates (coarse-grained locking, lock coupling, and give-up), which can be freely plugged into a top-level verified data structure whose correctness proof is parameterized by the interface.