We present Linearizability Hoare Logic (LHL), the first \emph{mechanized}, \emph{sound} and \emph{complete} program logic for atomic, set, and interval linearizability. We achieve this by showing soundness and completeness of LHL w.r.t. to a more general criterion, \emph{compositional linearizability}, which subsumes all three criteria. We showcase the range of expressivity of LHL by verifying an exchanger with a set linearizable specification, the eimination-backoff stack built above the exchanger, a lock with an atomic linearized specification, and a write-snapshot object with an interval linearizable specification.

LHL exists within a compositional model for concurrent computation which enables us to use the compositionality features of compositional linearizability to compose verified components together into large systems with a high-level of abstraction for its subcomponents. As a showcase, we verify the elimination-backoff stack implementation modularly by verifying all of its sub-components against their linearized specifications and then linking them together using compositional linearizability.