Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Free Termination Property of Queries Over Time

Conor Power, Paraschos Koutris, Joseph M Hellerstein

TL;DR

Addresses the problem of free termination in coordination-free distributed queries, complementing CALM's soundness with a completeness perspective. Develops a semiautomaton-based model to unify relational transducer reasoning with algebraic frameworks such as CRDTs and pre-semirings used in incremental view maintenance. Characterizes how algebraic properties—acyclicity, partial orders, join-semilattice structure, and group-like updates—govern the existence of free termination states and identifies threshold-like queries that enable termination. Also connects these ideas to distributed protocols (e.g., network flooding) and provides a linear-time procedure for deciding free termination states in finite state spaces, offering a finer granularity of coordination-freeness for specific query-input pairs.

Abstract

Building on prior work on distributed databases and the CALM Theorem, we define and study the question of free termination: in the absence of distributed coordination, what query properties allow nodes in a distributed (database) system to unilaterally terminate execution even though they may receive additional data or messages in the future? This completeness question is complementary to the soundness questions studied in the CALM literature. We also develop a new model based on semiautomata that allows us to bridge from the relational transducer model of the CALM papers to algebraic models that are popular among software engineers (e.g. CRDTs) and of increasing interest to database theory for datalog extensions and incremental view maintenance.

The Free Termination Property of Queries Over Time

TL;DR

Addresses the problem of free termination in coordination-free distributed queries, complementing CALM's soundness with a completeness perspective. Develops a semiautomaton-based model to unify relational transducer reasoning with algebraic frameworks such as CRDTs and pre-semirings used in incremental view maintenance. Characterizes how algebraic properties—acyclicity, partial orders, join-semilattice structure, and group-like updates—govern the existence of free termination states and identifies threshold-like queries that enable termination. Also connects these ideas to distributed protocols (e.g., network flooding) and provides a linear-time procedure for deciding free termination states in finite state spaces, offering a finer granularity of coordination-freeness for specific query-input pairs.

Abstract

Building on prior work on distributed databases and the CALM Theorem, we define and study the question of free termination: in the absence of distributed coordination, what query properties allow nodes in a distributed (database) system to unilaterally terminate execution even though they may receive additional data or messages in the future? This completeness question is complementary to the soundness questions studied in the CALM literature. We also develop a new model based on semiautomata that allows us to bridge from the relational transducer model of the CALM papers to algebraic models that are popular among software engineers (e.g. CRDTs) and of increasing interest to database theory for datalog extensions and incremental view maintenance.

Paper Structure

This paper contains 10 sections, 9 theorems, 2 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Motivating Examples
  3. Related Work
  4. Definitions of Free Termination
  5. Applications of Free Termination
  6. Algebraic Properties and Free Termination
  7. Partial Orders
  8. Group-Like Structures
  9. Free Termination in Distributed Systems
  10. Distributed Model

Key Result

Proposition 6

Let $\mathbb{S} = (D,L,U)$ and $U$ be acyclic. Then, the relation $s \sqsubseteq_U s' \Leftrightarrow s \twoheadrightarrow s'$ is a partial order for $D$. Moreover, $\mathbb{S}$ is inflationary w.r.t. $\sqsubseteq_U$.

Figures (2)

  • Figure 1: Four DFAs with labels $\{a,b,c\}$ showing four different categories of free termination. The doubly-lined states represent the accepting states of the DFA (query is true).
  • Figure 2: A state transition system for the set union state transition over the universe $\{a,b,c\}$. The green dotted line across the states indicates the threshold line for the query "the set contains an $a$". The doubly-lined states return True and single-lined states return False in the query.

Theorems & Definitions (20)

  • Definition 1: Semiautomaton
  • Definition 2: Transition Graph
  • Definition 3: Free Termination State
  • Example 4
  • Definition 5: Inflationary
  • Proposition 6
  • Example 7
  • Definition 8: Monotone Query
  • Proposition 9
  • Proposition 10
  • ...and 10 more