Logical Synchrony Networks: A Formal Model for Deterministic Distribution

Abstract

In the modelling of distributed systems, most Model of Computations (MoCs) rely on blocking communication to preserve determinism. A prominent example is Kahn Process Networks (KPNs), which supports non-blocking writes and blocking reads, and its implementable variant Finite FIFO Platforms (FFPs) which enforces boundedness using blocking writes. An issue with these models is that they mix process synchronisation with process execution, necessitating frequent blocking during synchronisation. This paper explores a recent alternative called bittide, which decouples the execution of a process from the synchronisation behaviour. Determinism and boundedness is preserved while enabling pipelined execution for better throughput. To understand the behaviour 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 the KPN model, and subsequently by both the concrete FFPs and bittide architectures. Thus, we show that FFPs and bittide offer two ways of implementing deterministic distributed systems, with the latter being more performant.

Keywords

• Distributed systems
• models of computation
• Kahn process networks
• bittide