Authors

Hongjin Liang
Jan Hoffmann
Xinyu Feng
Zhong Shao

Abstract

Implementations of concurrent objects should guarantee linearizability and a progress property such as wait-freedom, lock-freedom, obstruction-freedom, starvation-freedom, or deadlock-freedom. Conventional informal or semi-formal denitions of these progress properties describe conditions under which a method call is guaranteed to complete, but it is unclear how these denitions can be utilized to formally verify system software in a layered and modular way. In this paper, we propose a unified framework based on contextual refinements to show exactly how progress properties aect the behaviors of client programs. We give formal operational denitions of all common progress properties and prove that for linearizable objects, each progress property is equivalent to a specic type of contextual refinement that preserves termination. The equivalence ensures that verication of such a contextual refinement for a concurrent object guarantees both linearizability and the corresponding progress property. Contextual refinement also enables us to verify safety and liveness properties of client programs at a high abstraction level by soundly replacing concrete method implementations with abstract atomic operations.

Published

• In Proc. 24th International Conference on Concurrency Theory (CONCUR'13), Buenos Aires, Argentina, August 2013. Lecture Notes in Computer Science Vol. 8052, pages 227-241. © 2013 Springer-Verlag. [PDF]
• Technical Report [PDF]