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.
翻译:在何种情况下,协调性是分布式规范本身所固有的要求,而非由特定协议或实现策略所强加的?我们基于最小化假设给出了一个普适性答案。在异步消息传递模型中,我们证明:当且仅当规范在可观测结果集的适当序关系下关于历史扩展具有单调性时,该规范才允许无协调实现。这一协调性准则直接基于Lamport历史(在happens-before关系下的偏序执行轨迹)和规范定义的可观测结果进行表述,无需假设任何特定的编程语言、对象实现或协议结构。该准则清晰划分了可实现无协调执行的规范与必须进行协调的规范之间的严格边界。该准则为一系列经典结论提供了统一解释,包括CAP式不可能性、CALM式无协调性、共识与快照任务、事务隔离级别以及不变式汇合性——所有这些均为同一底层语义现象的具体实例。