The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Compositional Verification of Termination-Preserving Refinement of Concurrent Programs

Last modified: Tue Oct 21 13:56:33 2014 GMT.

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]

Copyright © 1996-2024 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page
colophon