Formal Foundations of Continuous Graph Processing

TL;DR

This paper introduces CG Calculus, a formal semantic foundation for continuous graph processing systems, ensuring correctness and result determinism despite optimizations like temporal locality and incremental processing.

Contribution

It provides the first formal semantics for continuous graph processing, capturing essential behaviors and proving result determinism despite non-deterministic optimizations.

Findings

CG Calculus captures core behaviors of continuous graph processing.

Proves result determinism despite non-deterministic features.

Mechanized in Coq for formal verification.

Abstract

With the growing need for online and iterative graph processing, software systems that continuously process large-scale graphs become widely deployed. With optimizations inherent as part of their design, these systems are complex, and have unique features beyond conventional graph processing. This paper describes CG Calculus, the first semantic foundation for continuous graph processing. The calculus captures the essential behavior of both the backend graph processing engine and the frontend application, with a focus on two essential features: temporal locality optimization (TLO) and incremental operation processing (IOP). A key design insight is that the operations continuously applied to the graph can be captured by a semantics defined over the operation stream flowing through the graph nodes. CG Calculus is a systematic study on the correctness of building continuous graph processing systems and applications. The most important result is result determinism: despite significant non-deterministic executions introduced by TLO and IOP, the results produced by CG Calculus are the same as conventional graph processing without TLO or IOP. The metatheory of CG Calculus is mechanized in Coq.