Kahn Process Networks (KPNs) are a deterministic Model of Computation (MoC) for distributed systems. KPNs supports non-blocking writes and blocking reads, with the consequent assumption of unbounded buffers between processes. Variants such as Finite FIFO Platforms (FFP) have been developed, which enforce boundedness. One issue with existing models is that they mix process synchronisation with process execution. In this paper we address how these two facets may be decoupled. This paper explores a recent alternative called bittide, which decouples the execution of a process from the control needed for process synchronisation, and thus preserves determinism and boundedness while ensuring pipelined execution for better throughput. Our intuition is that such an approach could leverage not only determinism and buffer boundedness but may potentially offer better overall throughput. To understand the behavior of these systems we define a formal model -- a deterministic MoC called Logical Synchrony Networks (LSNs). LSNs describes a network of processes modelled as a graph, with edges representing invariant logical delays between a producer process and the corresponding consumer process. We show that this abstraction is satisfied by KPNs. Subsequently, we show that both FFPs and bittide faithfully implement this abstraction. Thus, we show for the first time that FFPs and bittide offer two alternative ways of implementing deterministic distributed systems with the latter being more performant.

翻译：卡恩过程网络（KPN）是一种用于分布式系统的确定性计算模型（MoC）。KPN支持非阻塞写入和阻塞读取，并因此假设进程间存在无界缓冲区。针对其衍生模型如有限FIFO平台（FFP），已实现了有界性约束。现有模型存在的一个问题是将进程同步与进程执行相耦合。本文探讨如何将这两个方面解耦，并研究一种称为bittide的新方案——该方案将进程执行与进程同步所需控制相分离，在保证确定性和有界性的同时，通过流水线执行提升吞吐量。我们的直觉表明，这种方法不仅能保持确定性和缓冲区有界性，还可能实现更优的整体吞吐量。为理解此类系统的行为，我们定义了一种形式化模型——确定性计算模型"逻辑同步网络（LSN）"。LSN将进程网络描述为图结构，边表示生产者进程与对应消费者进程之间的不变逻辑延迟。我们证明该抽象模型满足KPN的要求，并进一步证明FFP和bittide均忠实实现了这一抽象。由此，我们首次论证了FFP和bittide作为实现确定性分布式系统的两种替代方案，后者具有更优性能。