Abstract
Correctness conditions like linearizability and opacity describe some form of atomicity imposed
on concurrent objects. In this paper, we propose a correctness condition (called causal atomicity)
for concurrent objects executing in a weak memory model, where the histories of the objects in
question are partially ordered. We establish compositionality and abstraction results for causal
atomicity and develop an associated refinement-based proof technique.