Characterizing Progress Properties of Concurrent Objects via Contextual Refinements
Last modified: Sat Nov 1 19:25:48 2014 GMT.
AbstractImplementations 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.
Copyright © 1996-2023 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science