Designing efficient concurrent objects often requires abandoning the standard
specification technique of linearizability in favor of more relaxed correctness
conditions. However, the variety of alternatives makes it difficult to choose
which condition to employ, and how to compose them when using objects specified
by different conditions.

In this work, we propose a uniform alternative in the form of Hoare logic,
which can explicitly capture-in the auxiliary state-the interference of
environment threads. We demonstrate the expressiveness of our method by
verifying a number of concurrent objects and their clients, which have so far
been specified only by non-standard conditions of concurrency-aware
linearizability, quiescent, and quantitative quiescent consistency.