Validating Traces of Distributed Programs Against TLA+ Specifications

TL;DR

This paper introduces a framework that verifies distributed program traces against TLA+ specifications by reducing the problem to model checking, enabling detection of implementation discrepancies with minimal trace data.

Contribution

The work presents a novel API and methodology for relating distributed program traces to TLA+ specifications using constrained model checking with TLC.

Findings

Successfully detected discrepancies in multiple distributed programs

Trace instrumentation reduces data to specification variables

Framework aids in verifying correctness of distributed implementations

Abstract

TLA+ is a formal language for specifying systems, including distributed algorithms, that is supported by powerful verification tools. In this work we present a framework for relating traces of distributed programs to high-level specifications written in TLA+. The problem is reduced to a constrained model checking problem, realized using the TLC model checker. Our framework consists of an API for instrumenting Java programs in order to record traces of executions, of a collection of TLA+ operators that are used for relating those traces to specifications, and of scripts for running the model checker. Crucially, traces only contain updates to specification variables rather than full values, and developers may choose to trace only certain variables. We have applied our approach to several distributed programs, detecting discrepancies between the specifications and the implementations in all cases. We discuss reasons for these discrepancies, best practices for instrumenting programs, and how to interpret the verdict produced by TLC.