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 represent executions as Lamport histories: collections of events partially ordered under happens-before. We abstract away from implementation mechanics and reason only about the observable outcomes that a specification admits at each history. We show that a specification admits a coordination-free implementation if and only if observable outcomes evolve monotonically as the history is causally extended. This Coordination Criterion is stated entirely at the level of specifications, independent of 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 distributed protocols and impossibility results, CAP-style consistency tradeoffs, CALM-style coordination tests, and programming-language analyses. Each can be viewed as an instance of the same underlying semantic phenomenon.
翻译:在何种情况下,协调性是分布式规约的内在要求,而非特定协议或实现策略所强加的?我们使用最小假设给出了一个普适性答案。在异步消息传递模型中,我们将执行过程表示为Lamport历史:按"先发生于"关系偏序排列的事件集合。我们抽象掉实现机制,仅关注规约在每个历史状态下允许的可观测结果。我们证明:当且仅当可观测结果随历史的因果扩展而单调演化时,该规约才允许无协调实现。这一协调性准则完全在规约层面表述,独立于任何特定编程语言、对象实现或协议结构。它在可实现无协调的规约与必须协调的规约之间划定了清晰边界。该准则为一系列经典结果提供了统一解释,包括分布式协议与不可能性结论、CAP式一致性权衡、CALM式协调性检验以及编程语言分析。这些均可视为同一底层语义现象的不同实例。