Complete CALM: A Coordination Criterion for Specifications
Provides a unified theoretical foundation for coordination-free distributed systems, subsuming CALM, CRDTs, I-confluence, and HATs, enabling verification of proper coordination.
The paper generalizes the CALM theorem from relational transducers to arbitrary concurrent specifications, proving that a specification admits a coordination-free implementation if and only if its outcomes are monotone. This yields a Complete CAP companion: a specification admits a consistent, available, partition-tolerant implementation iff it is distributed-monotone.
The CALM theorem connects coordination-freedom to monotonicity, but is tied to relational transducers and set-inclusion growth. We generalize it to arbitrary concurrent specifications. A specification maps execution histories to outcome sets under a declared refinement order; we prove it admits coordination-free implementation if and only if its outcomes are monotone (\emph{Complete CALM}). The criterion subsumes CALM, CRDTs, I-confluence, and HATs as instances, enables verification of proper coordination, and yields a \emph{Complete CAP} companion: a specification admits a consistent, available, partition-tolerant implementation if and only if it is distributed-monotone.