Characterizing Progress Properties of Concurrent Objects via Contextual Refinements
Last modified: Sat Nov 1 19:25:48 2014 GMT.
Authors
Hongjin LiangJan 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.
