Peer-to-peer systems are the most resilient form of distributed computing, but the design of robust protocols for their coordination is difficult. This makes it hard to specify and reason about global behaviour of such systems. This paper presents swarm protocols to specify such systems from a global viewpoint. Swarm protocols are projected to machines, that is local specifications of peers. We take inspiration from behavioural types with a key difference: peers communicate through an event notification mechanism rather than through point-to-point message passing. Our goal is to adhere to the principles of local-first software where network devices collaborate on a common task while retaining full autonomy: every participating device can locally make progress at all times, not encumbered by unavailability of other devices or network connections. This coordination-free approach leads to inconsistencies that may emerge during computations. Our main result shows that under suitable well-formedness conditions for swarm protocols consistency is eventually recovered and the locally observable behaviour of conforming machines will eventually match the global specification. The model we propose elaborates on an existing industrial platform and provides the basis for tool support (sketched here and fully described in a companion artifact paper), wherefore we consider this work to be a viable step towards reasoning about local-first and peer-to-peer software systems.

翻译：点对点系统是分布式计算中最具弹性的形式，但设计用于协调的健壮协议十分困难。这导致难以规范和推理此类系统的全局行为。本文提出群协议（swarm protocols）以从全局视角规范此类系统。群协议可投影为机器规范，即对等节点的本地规范。我们借鉴行为类型学，但关键区别在于：对等节点通过事件通知机制而非点对点消息传递进行通信。我们的目标是遵循本地优先软件原则——网络设备在协作完成共同任务的同时保持完全自主性：每台参与设备始终能本地推进计算，不受其他设备或网络连接不可用的影响。这种无协调方法会导致计算中可能出现的非一致性问题。我们的主要结果表明：在群协议满足良好形成条件（well-formedness conditions）的情况下，非一致性最终可恢复，且符合规范的机器最终能展现与全局规范匹配的本地可观测行为。所提出的模型基于现有工业平台进行细化，并为工具支持奠定基础（本文概述其框架，配套论文详述工具实现），因此我们认为这项工作是向推理本地优先及点对点软件系统迈出的可行一步。