Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Logical Synchrony Networks: A formal model for deterministic distribution

Logan Kenwright, Partha Roop, Nathan Allen, Sanjay Lall, Calin Cascaval, Tammo Spalink, Martin Izzard

TL;DR

This work introduces Logical Synchrony Networks (LSN), a deterministic MoC that decouples process execution from synchronization by enforcing invariant logical delays on edges. It demonstrates that classic Kahn Process Networks (KPN) are instances of LSN and presents two bounded, realizable realizations—Finite FIFO Platforms (FFP/LSFP) and Google's bittide—that support decoupled, pipelined execution while preserving determinism. LSFP provides a bounded-buffer, blocking-based realization, whereas bittide employs a clock-control system with elastic buffers to achieve higher throughput and more uniform latency. Across analytical mappings and comparative simulations, bittide shows superior average throughput and stable latency, suggesting two viable paths for scalable, deterministic distributed computation. Collectively, the work establishes a formal framework for deterministic distributed systems with bounded resources and guides practical design choices between hardware-assisted clock control and blocking buffer approaches.

Abstract

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.

Logical Synchrony Networks: A formal model for deterministic distribution

TL;DR

This work introduces Logical Synchrony Networks (LSN), a deterministic MoC that decouples process execution from synchronization by enforcing invariant logical delays on edges. It demonstrates that classic Kahn Process Networks (KPN) are instances of LSN and presents two bounded, realizable realizations—Finite FIFO Platforms (FFP/LSFP) and Google's bittide—that support decoupled, pipelined execution while preserving determinism. LSFP provides a bounded-buffer, blocking-based realization, whereas bittide employs a clock-control system with elastic buffers to achieve higher throughput and more uniform latency. Across analytical mappings and comparative simulations, bittide shows superior average throughput and stable latency, suggesting two viable paths for scalable, deterministic distributed computation. Collectively, the work establishes a formal framework for deterministic distributed systems with bounded resources and guides practical design choices between hardware-assisted clock control and blocking buffer approaches.

Abstract

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.
Paper Structure (17 sections, 5 theorems, 10 equations, 14 figures, 1 table)

This paper contains 17 sections, 5 theorems, 10 equations, 14 figures, 1 table.

Table of Contents

  1. Introduction
  2. Motivation
  3. The Bittide Approach
  4. Related Work
  5. Logical Synchrony Networks
  6. KPN as an instance of LSN
  7. Finite FIFO Platforms
  8. Efficient Fullness Checking
  9. Modified FFPs for enhanced throughput
  10. bittide
  11. Clock Control System
  12. Logical Delay Invariance
  13. Benefits of Elastic Buffers
  14. Throughput
  15. Physical Latency
  16. ...and 2 more sections

Key Result

Lemma 1

Consider any event $(M_i,n) \in V_{ext}$. The value of any edge (incoming/outgoing) is determinate.

Figures (14)

  • Figure 1: A simple FFP. Each machine has an execution time of 1 second and each link a delay of 2.0 seconds
  • Figure 2: The example from \ref{['fig:delay_1']}, with the initial marking changed to 3 tokens
  • Figure 3: A three-node *LSN
  • Figure 4: The execution trace of the three-machine *LSN (\ref{['fig:lsn_example']}), as measured by a global observer
  • Figure 5: $G_{ext}$ of the three-machine *LSN (\ref{['fig:lsn_example']}). Computation edges shown in black and communication edges coloured to differentiate source machine
  • ...and 9 more figures

Theorems & Definitions (12)

  • Definition 1
  • Example 1
  • Example 2
  • Definition 2
  • Definition 3
  • Lemma 1
  • Theorem 1
  • Definition 4
  • Lemma 2
  • Theorem 2
  • ...and 2 more