^{1 2}

Validating Traces of Distributed Programs Against Specifications††thanks: This work was partly supported by a grant from Oracle Corporation.

Horatiu Cirstea 11    Markus A. Kuppe 22    Benjamin Loillier 11    Stephan Merz 11

Abstract

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. 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 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 it is not necessary to provide values for all 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, how to interpret the verdict produced by TLC, and how to take into account the results of trace validation for implementation development.

1 Introduction

Distributed systems are at the heart of modern cloud services and they are known to be error-prone, due to phenomena such as delays or failures of nodes and communication networks. Applying formal methods in the design and development of these systems can help increase the confidence in their correctness and resilience. For example, the ² specification language and verification tools have been successfully used in industry ^{3 4} for designing distributed algorithms underlying modern cloud systems. and similar specification formalisms are most useful for describing and analyzing systems at high levels of abstraction, but do not provide support for checking that actual implementations of these systems are correct. Although supports a notion of refinement, formally proving a chain of refinements from a high-level design of a distributed algorithm to an actual implementation would be a daunting task, complicated by the fact that standard programming languages do not provide explicit control of the grain of atomicity of the running program. In this work, we present a lightweight approach to validating distributed programs against high-level specifications that relies on recording finite traces of program executions and leveraging the model checker TLC ⁵ for comparing those traces to the state machine described in the specification. Although this approach does not provide formal correctness guarantees, even when the specification has been extensively verified, we have found it very useful for discovering and analyzing discrepancies between the runs of distributed programs and their high-level specifications, including serious bugs that had gone undetected by more traditional quality assurance techniques.

The collection of program traces relies on an instrumentation of the program in order to record information on how program operations correspond to updates of the variables representing the state of the specification, and potentially indicating the corresponding transition in the specification. We have designed a Java library that facilitates this instrumentation and can be used to produce traces in JSON format. Because the traces record the evolution of the state of the specification, our approach is easiest to apply when the specification exists prior to building the implementation, the implementor is familar with it, and uses it as a blueprint when writing the code. However, we have also used the approach in order to “reverse engineer” a specification from an existing distributed program and better understand its operation. Trace validation can also help ensure that the specification and implementation remain in sync over time because it is easy to apply it again when the specification or the implementation changes.

The main problem when instrumenting a program is to identify suitable “linearization points” at which the program completes a step that corresponds to an atomic transition of the high-level state machine. Basic guiding principles are to log an event when shared state has been updated, such as when sending or receiving messages, performing operations on locks or on stable data storage. We discuss how to account for different grain of atomicity between the specification and the implementation based on feedback from trace validation. Because data representation generally differs between the specification and the actual program, it may be difficult or impractical to compute the value of a high-level variable (or its update) corresponding to the data manipulated by the implementation. We therefore allow traces to be incomplete and only record some information about the corresponding abstract state. We reduce the problem of trace validation to one of constrained model checking and show how TLC can reconstruct missing information. This leads to a tradeoff between the precision of information recorded in the trace (and potentially of the verdict of validation) and the amount of search that TLC must perform during model checking.

The paper is organized as follows: Section 2 provides some background on and introduces our running example, both in and as a Java program. Our approach to instrumentation is described in Section 3. In Section 4 we formalize the trace validation problem, describe how we realized the approach using TLC, and discuss our experience with it. Section 5 discusses related work, and Section 6 concludes the paper and presents some perspectives for future work.

2 Background

2.1 Specifications

² is a specification language based on Zermelo-Fraenkel set theory and linear-time temporal logic that has found wide use for writing high-level specifications of concurrent and distributed algorithms. It emphasizes the use of mathematical descriptions based on sets and functions for specifying data structures. is a state-based specification formalism: the state space of a system is represented using variables, and formulas are evaluated over behaviors, i.e., sequences of states that assign values to variables. Algorithms are described as state machines whose specifications are written in the canonical form

In this formula, Init is a state predicate describing the possible initial states of the system, Next represents the next-state relation, usually written as the disjunction of actions describing the possible state transitions, vars is a tuple containing all state variables that appear in the specification, and L is a temporal formula asserting liveness and fairness assumptions. A state predicate is a formula of first-order logic containing state variables, and it is evaluated over single states. A transition predicate (or, synonymously, action) is a first-order formula that may contain unprimed and primed occurrences of state variables. Such a formula is evaluated over a pair of states, with unprimed variables referring to the values before the transition and primed variables to the values after the transition. The formula [Next]_{vars} holds of any pair of states \langle s,t\rangle if either Next holds of \langle s,t\rangle (and therefore the pair represents an actual step of the system) or all variables in vars evaluate to the same values in the two states (and the pair represents a stuttering step). Systematically allowing for stuttering steps enables the implementation of a system specification by a lower-level specification to be represented as validity of implication between the formulas expressing the specifications. The complementary property L is used to express fairness assumptions and is at the basis of verifying liveness properties of algorithms. Since in this work we only analyze finite traces of programs, we ignore liveness properties and are interested in finite behaviors, i.e., sequences s_{0}\dots s_{n} of states such that Init holds of s_{0} and [Next]_{vars} holds for all pairs \langle s_{i},s_{i+1}\rangle for i\in 0\,..\,n-1.

Figure 1: Trace validation as a search for paths in the state space.

, Nov. 2011.