Authors
Hongjin Liang
Xinyu Feng
Zhong Shao
Abstract
Many 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.
Published
In
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.
- Conference version [PDF]
- Extended Technical Report [PDF]