Coherent Causal Memory
Coherent Causal Memory (CCM) is causal memory in which prefixes of an execution can be mapped to global memory states in a consistent way. While CCM requires conflicting pairs of writes to be globally ordered, it allows writes to remain unordered with respect to both reads and non-conflicting writes. Nevertheless, it supports assertional, state-based program reasoning using generalized Owicki-Gries proof outlines (where assertions can be attached to any causal program edge). Indeed, the authors show that from a reasoning standpoint, CCM differs from Sequentially Consistent (SC) memory only in that ghost code added by the user is not allowed to introduce new write-write races.