Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Coordination Criterion

Joseph M. Hellerstein

TL;DR

This work introduces the Coordination Criterion, a semantic test that determines when coordination is intrinsic to implementing a distributed specification. By formulating specifications over Lamport histories with a Poss/Obs framework and an outcome order $\preceq$, it proves that coordination-free implementations exist iff observable outcomes are monotone under history extension, i.e., no future extension invalidates an already observed outcome. The criterion unifies classic results such as CAP, CALM, consensus, isolation levels, and invariant confluence by showing they all arise from the same monotonicity phenomenon. This semantic lens allows pre-design diagnosis of coordination requirements and explains why certain specifications inherently demand coordination while others can be implemented without it, independent of language, protocol, or concrete synchronization primitives.

Abstract

When is coordination intrinsically required by a distributed specification, rather than imposed by a particular protocol or implementation strategy? We give a general answer using minimal assumptions. In an asynchronous message-passing model, we show that a specification admits a coordination-free implementation if and only if it is monotone with respect to history extension under an appropriate order on observable outcomes. This Coordination Criterion is stated directly over Lamport histories -- partially ordered executions under happens-before -- and specification-defined observable outcomes, without assuming any particular programming language, object implementation, or protocol structure. It yields a sharp boundary between specifications that can be implemented without coordination and those for which coordination is unavoidable. The criterion provides a uniform explanation for a range of classical results, including CAP-style impossibility, CALM-style coordination-freedom, agreement and snapshot tasks, transactional isolation levels, and invariant confluence -- all instances of the same underlying semantic phenomenon.

The Coordination Criterion

TL;DR

This work introduces the Coordination Criterion, a semantic test that determines when coordination is intrinsic to implementing a distributed specification. By formulating specifications over Lamport histories with a Poss/Obs framework and an outcome order , it proves that coordination-free implementations exist iff observable outcomes are monotone under history extension, i.e., no future extension invalidates an already observed outcome. The criterion unifies classic results such as CAP, CALM, consensus, isolation levels, and invariant confluence by showing they all arise from the same monotonicity phenomenon. This semantic lens allows pre-design diagnosis of coordination requirements and explains why certain specifications inherently demand coordination while others can be implemented without it, independent of language, protocol, or concrete synchronization primitives.

Abstract

When is coordination intrinsically required by a distributed specification, rather than imposed by a particular protocol or implementation strategy? We give a general answer using minimal assumptions. In an asynchronous message-passing model, we show that a specification admits a coordination-free implementation if and only if it is monotone with respect to history extension under an appropriate order on observable outcomes. This Coordination Criterion is stated directly over Lamport histories -- partially ordered executions under happens-before -- and specification-defined observable outcomes, without assuming any particular programming language, object implementation, or protocol structure. It yields a sharp boundary between specifications that can be implemented without coordination and those for which coordination is unavoidable. The criterion provides a uniform explanation for a range of classical results, including CAP-style impossibility, CALM-style coordination-freedom, agreement and snapshot tasks, transactional isolation levels, and invariant confluence -- all instances of the same underlying semantic phenomenon.
Paper Structure (33 sections, 7 theorems, 10 equations)

This paper contains 33 sections, 7 theorems, 10 equations.

Table of Contents

  1. Introduction
  2. When Coordination is Intrinsic
  3. Computational Model
  4. Possibilities, Observations, Order, and Consistency
  5. Faithful Outcome Modeling
  6. Specifications and Coordination
  7. The Coordination Criterion
  8. Proof Sketch
  9. Applications of the Coordination Criterion
  10. Mutable Variables: Registers
  11. Replication, Partitions, and Waiting (CAP)
  12. Consensus and Agreement Protocols
  13. CALM
  14. Related Work
  15. Conclusion
  16. ...and 18 more sections

Key Result

Theorem 1

A distributed specification admits a coordination-free implementation iff it is monotone with respect to history extension under the chosen outcome order $\preceq$.

Theorems & Definitions (35)

  • Definition 1: History
  • Definition 2: Input history of an execution
  • Definition 3: History extension
  • Definition 4: Possibility Function
  • Example 1: Possibility vs. observability
  • Definition 5: Observability Function
  • Definition 6: Outcome Order
  • Definition 7: Consistency and Contradiction
  • Definition 8: Future-Consistent Outcome
  • Definition 9: Specification
  • ...and 25 more