Refinement Verification Of Concurrent Programs And Its Applications

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 dis-sertation 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 refine-ment.First, it shows a Rely-Guarantee-based Simulation (RGSim) as a general proof technique for concurrent program refinement. The novel simulation relation is param-eterized with the interference between threads and their parallel environments. It is compositional and supports modular verification. RGSim can incorporate the assump-tions 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 verifica-tion, 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 verifica-tion of linearizability of concurrent objects, which is an important application of con-current 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 execu-tions (as in the lazy set algorithm), or involve both features (as in the RDCSS algo-rithm). 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 lineariz-ability. Using our logic we successfully verify12well-known algorithms, two of which are 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 refinements. We prove that for linearizable objects, each progress property is equivalent to a certain form of termination-sensitive contextual refinement. The framework unifies lineariz-ability and all the five most common progress properties:wait-freedom, lock-freedom, obstruction-freedom, starvation-freedom, and deadlock-freedom. It enables modular verification of safety and liveness properties of client programs, and also makes it pos-sible to borrow ideas from existing proof methods for contextual refinements to verify linearizability and a progress property together.