Compositional Verification of Termination-Preserving Refinement of Concurrent Programs
Last modified: Tue Oct 21 13:56:33 2014 GMT.
AbstractMany verification problems can be reduced to refinement verification. However, existing work on verifying refinement of concurrent programs either fails to prove the preservation of termination, allowing a diverging program to trivially refine any programs, or is difficult to apply in compositional thread-local reasoning. In this paper, we first propose a new simulation technique, which establishes termination-preserving refinement and is a congruence with respect to parallel composition. Then we give a proof theory for the simulation, which is the first Hoare-style concurrent program logic supporting termination-preserving refinement proofs. We show two key applications of our logic, i.e., verifying linearizability and lock-freedom together for fine-grained concurrent objects, and verifying full correctness of optimizations of concurrent algorithms.
PublishedIn Proc. 23rd EACSL Annual Conference on Computer Science Logic and 29th Annual IEEE Symposium on Logic in Computer Science (CSL-LICS'14), Vienna, Austria, Paper No. 65, July 2014. ©2014 IEEE Computer Society.
Copyright © 1996-2021 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science