  Correctness conditions for concurrent objects describe how atomicity of an
abstract sequential object may be decomposed. Many different concurrent objects
and proof methods for them have been developed. However, arguments about
correctness are conducted with respect to an object in isolation. This is in
contrast to real-world practice, where concurrent objects are often implemented
as part of a programming language library (e.g., java.util.concurrent) and are
instantiated within a client program. A natural question to ask, then is: How
does a correctness condition for a concurrent object ensure correctness of a
client program that uses the concurrent object? This paper presents the main
issues that surround this question and provides some answers by linking
different correctness conditions with a form of trace refinement.
