The CertiKOS project aims to develop a new ecosystem for specifying, programming, compiling, and composing large-scale certified heterogeneous systems. Since its inception, CertiKOS has applied ideas from game semantics and algebraic effects to support layered composition of deep specifications and certified abstraction layers. However, existing theory and tools for CertiKOS have only provided limited support for composing concurrent components. This talk will survey the challenges we encountered and then present a new general semantics for supporting horizontal and vertical composition of linearizable concurrent objects. We start by showcasing a common issue, which is independent of linearizability, in the construction of compositional models of concurrent computation: interaction with the neutral element for composition can lead to emergent behaviors, a hindrance to compositionality. Category theory provides a solution for the issue in the form of the Karoubi envelope. Surprisingly, this abstract construction is deeply related to linearizability and leads to a novel formulation of it. Notably, this new formulation neither relies on atomicity nor directly upon happens-before ordering and is only possible because of compositionality, revealing that linearizability and compositionality are intrinsically related to each other. We use this new, and compositional, understanding of linearizability to revisit much of the theory and practice of building certified concurrent abstraction layers.