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
- 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.
- Technical Report [PDF]