Refinement Verification of Concurrent Programs and Its Applications
Hongjin Liang, Xinyu Feng, Zhong Shao · 2014
Many verification problems can be reduced to refinement verification, i.e., proving that a concrete program has no more behaviors than a more abstract program. This dissertation explores the applications of refinement verification of concurrent programs, and proposes compositional verification techniques that support these applications. It makes several contributions to understanding and verifying concurrent program refinement. First, it shows a Rely-Guarantee-based Simulation (RGSim) as a general proof technique for concurrent program refinement. The novel simulation relation is parameterized with the interference between threads and their parallel environments. It is compositional and supports modular verification. RGSim can incorporate the assumptions about environments made by specific refinement applications, thus is flexible and practical. We apply RGSim to reason about optimizations in parallel contexts. We also reduce the verification of concurrent garbage collectors (GCs) to refinement verification, and propose a general GC verification framework based on RGSim. Using the framework, we verify the Boehm et al. concurrent mark-sweep GC algorithm. Second, it shows a Hoare-style program logic for modular and effective verification of linearizability of concurrent objects, which is an important application of concurrent program refinement verification. Our logic with a lightweight instrumentation mechanism supports objects with non-fixed linearization points (LPs), including the most challenging ones that use the helping mechanism to achieve lock-freedom (as in HSY elimination-based stack), or have LPs depending on unpredictable future executions (as in the lazy set algorithm), or involve both features (as in the RDCSS algorithm). We generalize RGSim with the support for non-fixed LPs as the meta-theory of our logic, and show it implies a contextual refinement which is equivalent to linearizability. Using our logic we successfully verify 12 wellknown algorithms, two of which are used in the java.util.concurrent package. Finally, it shows a unified framework that characterizes the full correctness (i.e., linearizability and progress properties) of concurrent objects via contextual