Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems

Abstract

Forms of synchrony can greatly simplify modeling, design, and verification of distributed systems. Thus, recent advances in clock synchronization protocols and their adoption hold promise for system design. However, these protocols synchronize the distributed clocks only within a certain tolerance, and there are transient phases while synchronization is still being achieved. Abstractions used for modeling and verification of such systems should accurately capture these imperfections that cause the system to only be “almost synchronized.” In this paper, we present approximate synchrony, a sound and tunable abstraction for verification of almost-synchronous systems. We show how approximate synchrony can be used for verification of both time synchronization protocols and applications running on top of them. We provide an algorithmic approach for constructing this abstraction for symmetric, almost-synchronous systems, a subclass of almost-synchronous systems. Moreover, we show how approximate synchrony also provides a useful strategy to guide state-space exploration. We have implemented approximate synchrony as a part of a model checker and used it to verify models of the Best Master Clock (BMC) algorithm, the core component of the IEEE 1588 precision time protocol, as well as the time-synchronized channel hopping protocol that is part of the IEEE 802.15.4e standard.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Forms of synchrony can greatly simplify modeling, design, and verification of distributed systems. Traditionally, a common sense of time is established using time-synchronization (clock-synchronization) protocols or systems such as the global positioning system (GPS), network time protocol (NTP), and the IEEE 1588 [20] precision time protocol (PTP). These protocols, however, synchronize the distributed clocks only within a certain bound. In other words, at any time point, clocks of different nodes can have differing values, but time synchronization ensures that those values are within a specified offset of each other, i.e., they are almost synchronized.

Distributed protocols running on top of time-synchronized nodes are designed under the assumption that while processes at different nodes make independent progress, no process falls very far behind any other. Figure 1 provides examples of such real world systems. For example, Google Spanner [8] is a distributed fault tolerant system that provides consistency guarantees when run on top of nodes that are synchronized using GPS and atomic clocks, wireless sensor networks [27, 28] use time synchronized channel hopping (TSCH) [1] as a standard for time synchronization of sensor nodes in the network, and IEEE 1588 precision time protocol (PTP) [20] has been adopted in industrial automation, scientific measurement [22], and telecommunication networks. Correctness of these protocols depends on having some synchrony between different processes or nodes.

Fig. 1.

Almost-synchronous systems comprise an application protocol running on top of a time-synchronization layer.

When modeling and verifying systems that are almost-synchronous it is important to compose them using the right concurrency model. One requires a model that lies somewhere between completely synchronous (lock-step progress) and completely asynchronous (unbounded delay). Various such concurrency models have been proposed in the literature, including quasi-synchrony [7, 18] and bounded-asynchrony [16]. However, we discuss in Sect. 7, these models permit behaviors that are typically disallowed in almost-synchronous systems. Alternatively, one can use formalisms for hybrid or timed systems that explicitly model clocks (e.g., [2, 3]), but the associated methods (e.g., [17, 21]) tend to be less efficient for systems with a huge discrete state space, which is typical for distributed software systems.

In this paper, we introduce symmetric, almost-synchronous (SAS) systems, a class of distributed systems in which processes have symmetric timing behavior. In our experience, protocols at both the application layer and the time-synchronization layer can be modeled as SAS systems. Additionally, we introduce the notion of approximate synchrony ( AS ) as a concurrency model for almost-synchronous systems, which also enables one to compute a sound discrete abstraction of a SAS system. Intuitively, a system is approximately-synchronous if the number of steps taken by any two processes do not differ by more than a specified bound, denoted $\varDelta$. The presence of the parameter $\varDelta$ makes approximate synchrony a tunable abstraction method. We demonstrate three different uses of the approximate synchrony abstraction:

• 1. Verifying Time-Synchronized Systems: Suppose that the system to be verified runs on top of a layer that guarantees time synchronization throughout its execution. In this case, we show that there is a sound value of $\varDelta$ which can be computed using a closed form equation as described in Sect. 3.2.

• 2. Verifying Systems with Recurrent Logical Behavior: Suppose the system to be verified does not rely on time synchronization, but its traces contain recurrent logical conditions — a set of global states that are visited repeatedly during the protocol’s operation. We show that an iterative approach based on model checking can identify such recurrent behavior and extract a value of $\varDelta$ that can be used to compute a sound discrete abstraction for model checking (see Sect. 4). Protocols verifiable with this approach include some at the time-synchronization layer, such as IEEE 1588 [20].

• 3. Prioritizing State-Space Exploration: The approximate synchrony abstraction can also be used as a search prioritization technique for model checking. We show in Sect. 6 that in most cases it is more efficient to search behaviors for smaller value of $\varDelta$ (“more synchronous” behaviors) first for finding bugs.

We present two practical case studies: (i) a time-synchronized channel hopping (TSCH) protocol that is part of the IEEE802.15.4e [1] standard, and (ii) the best master clock (BMC) algorithm of the IEEE 1588 precision time protocol. The former is system where the nodes are time-synchronized, while the latter is the case of a system with recurrent logical behavior. Our results show that approximate synchrony can reduce the state space to be explored by orders of magnitude while modeling relevant timing semantics of these protocols, allowing one to verify properties that cannot be verified otherwise. Moreover, we were able to find a so-called “rogue frame” scenario that the IEEE 1588 standards committee had long debated without resolution (see our companion paper written for the IEEE 1588 community [6] for details).

Our abstraction technique can be used with any finite-state model checker. In this paper we implement it on top of the Zing model checker [4], due to its ability to control the model checker’s search using an external scheduler that enforces the approximate synchrony condition.

To summarize, this paper makes the following contributions:

• The formalism of symmetric, almost synchronous (SAS) systems and its use in modeling an important class of distributed systems (Sect. 2);

• A tunable abstraction technique, termed approximate synchrony (Sects. 2 and 3);

• Automatic procedures to derive values of $\varDelta$ for sound verification (Sects. 3 and 4);

• An implementation of approximate synchrony in an explicit-state model checker (Sect. 5), and

• The use of approximate synchrony for verification and systematic testing of two real-world protocols, the BMC algorithm (a key component of the IEEE 1588 standard), and the time synchronized channel hopping protocol (Sect. 6).

2 Formal Model and Approach

In this section, we define clock synchronization precisely and formalize the notion of symmetric almost-synchronous (SAS) systems, the class of distributed systems we are concerned with in this paper.

2.1 Clocks and Synchronization

Each node in the distributed system has an associated (local) physical clock $\chi$, which takes a non-negative real value. For purposes of modeling and analysis, we will also assume the presence of an ideal (global) reference clock, denoted t. The notation $\chi (t)$ denotes the value of $\chi$ when the reference clock has value t. Given this notation, we describe the following two basic concepts:

• 1. Clock Skew: The skew between two clocks $\chi _i$ and $\chi _j$ at time t (according to the reference clock) is the difference in their values $|\chi _i(t) - \chi _j(t)|$.

• 2. Clock Drift: The drift in the rate of a clock $\chi$ is the difference per unit time of the value of $\chi$ from the ideal reference clock t.

Time synchronization ensures that the skew between any two physical clocks in the network is bounded. The formal definition is as below.

Definition 1

A distributed system is time-synchronized (or clock-synchronized) if there exists a parameter $\beta$ such that for every pair of nodes i and j and for any t,

$$\begin{aligned} |\chi _i(t) - \chi _j(t)| \le \beta \end{aligned}$$

(1)

For ease of exposition, we will not explicitly model the details of dynamics of physical clocks or the updates to them. We will instead abstract the clock dynamics as comprising arbitrary updates to $\chi _i$ variables subject to additional constraints on them such as Eq. 1 (wherever such assumptions are imposed).

Example 1

The IEEE 1588 precision time protocol [20] can be implemented so as to bound the physical clock skew to the order of sub-nanoseconds [22], and the typical clock drift to at most $10^{-4}$ [20].

2.2 Symmetric, Almost-Synchronous Systems

We model the distributed system as a collection of processes, where processes are used to model both the behavior of nodes as well as of communication channels. There can be one or more processes executing at a node.

Formally, the system is modeled as the tuple ${\mathcal {M}}_C= (\mathcal {S}, \delta , \mathcal {I}, \textsc {id}, \mathbf {\chi }, \mathbf {\tau })$ where

• $\mathcal {S}$ is the set of discrete states of the system,

• $\delta \subseteq \mathcal {S}\times \mathcal {S}$ is the transition relation for the system,

• $\mathcal {I}\subseteq \mathcal {S}$ is the set of initial states,

• $\textsc {id}= \{1,2,\ldots ,K\}$ is the set of process identifiers,

• $\mathbf {\chi }= (\chi _1, \chi _2, \ldots , \chi _{K})$ is a vector of local clocks, and

• $\mathbf {\tau }= (\tau _1, \tau _2, \ldots , \tau _{K})$ is a vector of process timetables. The timetable of the ith process, $\tau _i$, is an infinite vector $(\tau _i^1, \tau _i^2, \tau _i^3, \ldots )$ specifying the time instants according to local clock $\chi _i$ when process i executes (steps). In other words, process i makes its jth step when $\chi _i = \tau _i^j$.

For convenience, we will denote the ith process by $\mathcal {P}_i$. Since in practice the dynamics of physical clocks can be fairly intricate, we choose not to model these details — instead, we assume that the value of a physical clock $\chi _i$ can vary arbitarily subject to additional constraints (e.g., Eq. 1).

The kth nominal step size of process $\mathcal {P}_i$ is the intended interval between the ($k-1$)th and kth steps of $\mathcal {P}_i$, viz., $\tau _i^{k} - \tau _i^{k-1}$. The actual step size of the process is the actual time elapsed between the ($k-1$)th and kth step, according to the ideal reference clock t. In general, the latter differs from the former due to clock drift, scheduling jitter, etc.

Motivated by our case studies with the IEEE 1588 and 802.15.4e standards, we impose two restrictions on the class of systems considered in this paper:

• 1. Common Timetable: For any two processes $\mathcal {P}_i$ and $\mathcal {P}_j$, $\tau _i = \tau _j$. Note that this does not mean that the process step synchronously, since their local clocks may report different values at the same time t. However, if the system is time synchronized, then the processes step “almost synchronously.”

• 2. Bounded Process Step Size: For any process $\mathcal {P}_i$, its actual step size lies in an interval $[\sigma ^l, \sigma ^u]$. This interval is the same for all processes. This restriction arises in practice from the bounded drift of physical clocks.

A set of processes obeying the above restrictions is termed a symmetric, almost-synchronous (SAS) system. The adjective “symmetric” refers only to the timing behavior — note that the logical behavior of different processes can be very different. Note also that SAS systems may or may not be running on top of a time synchronization layer, i.e., SAS systems and time-synchronized systems are orthogonal concepts.

Example 2

The IEEE 1588 protocol can be modeled as a SAS system. All processes intend to step at regular intervals called the announce time interval. The specification [20] states the nominal step size for all processess as 1 second; thus the timetable is the sequence $(0,1,2,3,\ldots )$. However, due to the drift of clocks and other non-idealities such as jitter due to OS scheduling, the step size in typical IEEE 1588 implementations can vary by $\pm 10^{-3}$. From this, the actual step size of processes can be derived to lie in the interval [0.999, 1.001].

Traces and Segments. A timed trace (or simply trace) of the SAS system ${\mathcal {M}}_C$ is a timestamped record of the execution of the system according to the global (ideal) time reference t. Formally, a timed trace is a sequence $h_0, h_1, h_2, \ldots$ where each element $h_j$ is a triple $(s_j, \mathbf {\chi }_j, t_j)$ where $s_j \in \mathcal {S}$ is a discrete (global) state at time $t = t_j$ and $\mathbf {\chi }_j = (\chi _{1,j}, \chi _{2,j}, \ldots , \chi _{K,j})$ is the vector of clock values at time $t_j$. For all j, at least one process makes a step at time $t_j$, so there exists at least one i and a corresponding $m_i \in \{0,1,2,\ldots \}$ such that $\chi _{i,j}(t_j) = \tau _i^{m_i}$. Moreover, processes step according to their timetables; thus, if any $\mathcal {P}_i$ makes its $m_i$th and $l_i$th steps at times $t_j$ and $t_k$ respectively, for $m_i < l_i$, then $\chi _{i,j}(t_j) = \tau _i^{m_i} < \tau _i^{l_i} = \chi _{i,k}(t_k)$. Also, by the bounded process step size restriction, if any $\mathcal {P}_i$ makes its $m_i$th and $m_i+1$th steps at times $t_j$ and $t_k$ respectively (for all $m_i$), $|t_k - t_j| \in [\sigma ^l, \sigma ^u]$. Finally, $s_{0} \in \mathcal {I}$ and $\delta (s_j, s_{j+1})$ holds for all $j \ge 0$ with the transition into $s_j$ occuring at time $t = t_j$.A trace segment is a (contiguous) subsequence $h_j, h_{j+1}, \ldots , h_l$ of a trace of ${\mathcal {M}}_C$.

2.3 Verification Problem and Approach

The central problem considered in this paper is as follows:

Problem 1

Given an SAS system ${\mathcal {M}}_C$ modeled as above, and a linear temporal logic (LTL) property $\varPhi$ with propositions over the discrete states of ${\mathcal {M}}_C$, verify whether ${\mathcal {M}}_C$ satisfies $\varPhi$.

One way to model ${\mathcal {M}}_C$ would be as a hybrid system (due to the continuous dynamics of physical clocks), but this approach does not scale well due to the extremely large discrete state space. Instead, we provide a sound discrete abstraction ${\mathcal {M}}_A$ of ${\mathcal {M}}_C$ that preserves the relevant timing semantics of the ‘almost-synchronous’ systems. (Soundness is formalized in Sect. 3).

There are two phases in our approach:

• 1. Compute Abstraction Parameter: Using parameters of ${\mathcal {M}}_C$ (relating to clock dynamics), we compute a parameter $\varDelta$ characterizing the “approximate synchrony” condition, and use $\varDelta$ to generate a sound abstract model ${\mathcal {M}}_A$.

• 2. Model Checking: We verify the temporal logic property $\varPhi$ on the abstract model using finite-state model checking.

The key to this strategy is the first step, which is the focus of the following sections.

3 Approximate Synchrony

We now formalize the concept of approximate synchrony (AS) and explain how it can be used to generate a discrete abstraction of almost-synchronous distributed systems. Approximate synchrony applies to both (segments of) traces and to systems.

Definition 2

(Approximate Synchrony for Traces) A trace (segment) of a SAS system ${\mathcal {M}}_C$ is said to satisfy approximate synchrony (is approximately-synchronous) with parameter $\varDelta$ if, for any two processes $\mathcal {P}_i$ and $\mathcal {P}_j$ in ${\mathcal {M}}_C$, the number of steps $N_i$ and $N_j$ taken by the two processes in that trace (segment) satisfies the following condition:

$$ | N_i - N_j | \le \varDelta $$

Although this definition is in terms of traces of SAS systems, we believe the notion of approximate synchrony is more generally applicable to other distributed systems also. An early version of this definition appeared in [10].

The definition extends to a SAS system in the standard way:

Definition 3

(Approximate Synchrony for Systems) A SAS system ${\mathcal {M}}_C$ satisfies approximate synchrony (is approximately-synchronous) with parameter $\varDelta$ if all traces of that system satisfy approximate synchrony with parameter $\varDelta$.

We refer to the condition in Definition 3 above as the approximate synchrony (AS) condition with parameter $\varDelta$, denoted ${\text {AS}}(\varDelta )$. For example, in Fig. 2, executing step 5 of process P1 before step 3 of process P2 violates the approximate synchrony condition for $\varDelta = 2$. Note that $\varDelta$ quantifies the “approximation” in approximate synchrony. For example, for a (perfectly) synchronous system $\varDelta = 0$, since processes step at the same time instants. For a fully asynchronous system, $\varDelta = \infty$, since one process can get arbitrarily ahead of another.

3.1 Discrete Approximate Synchrony Abstraction

We now present a discrete abstraction of a SAS system. The key modification is to (i) remove the physical clocks and timetables, and (ii) include instead an explicit scheduler that constrains execution of processes so as to satisfy the approximate synchrony condition ${\text {AS}}(\varDelta )$.

Fig. 2.

${\text {AS}}(\varDelta )$ violated for $\varDelta = 2$

Formally, given a SAS system ${\mathcal {M}}_C= (\mathcal {S}, \delta , \mathcal {I}, \textsc {id}, \mathbf {\chi }, \mathbf {\tau })$, we construct an $\varDelta$-abstract model ${\mathcal {M}}_A$ as the tuple $(\mathcal {S}, \delta ^a, \mathcal {I}, \textsc {id}, \rho _{\varDelta })$ where $\rho _{\varDelta }$ is a scheduler process that performs an asynchronous composition of the processes $\mathcal {P}_1, \mathcal {P}_2, \ldots , \mathcal {P}_{K}$ while enforcing ${\text {AS}}(\varDelta )$. Conceptually, the scheduler $\rho _{\varDelta }$ maintains state counts $N_i$ of the numbers of steps taken by each process $\hat{\mathcal {P}}_i$ from the initial state.¹ A configuration of ${\mathcal {M}}_A$ is a pair $(s, N)$ where $s\in \mathcal {S}$ and $N\in \mathbb Z^{K}$ is the vector of step counts of the processes. The abstract model ${\mathcal {M}}_A$ changes its configuration according to its transition function $\delta ^a$ where $\delta ^a((s, N), (s', N'))$ iff (i) $\delta (s, s')$ and (ii) $N'_i = N_i + 1$ if $\rho _{\varDelta }$ permits $\mathcal {P}_i$ to make a step and $N'_i = N_i$ otherwise.

In an initial state, all processes $\mathcal {P}_i$ are enabled to make a step. At each step of $\delta ^a$, $\rho _{\varDelta }$ enforces the approximate synchrony condition by only enabling $\mathcal {P}_i$ to step iff that step does not violate ${\text {AS}}(\varDelta )$. Behaviors of ${\mathcal {M}}_A$ are untimed traces, i.e., sequences of discrete (global) states $s_0, s_1, s_2, \ldots$ where $s_j \in \mathcal {S}$, $s_0$ is an initial (global) state, and each transition from $s_j$ to $s_{j+1}$ is consistent with $\delta ^a$ defined above.

Note that approximate synchrony is a tunable timing abstraction. Larger the value of $\varDelta$, more conservative the abstraction. The key question is: for a given system, what value of $\varDelta$ constitutes a sound timing abstraction, and how do we automatically compute it? Recall that one model is a sound abstraction of another if and only if every execution trace of the latter (concrete model ${\mathcal {M}}_C$) is also an execution trace of the former (abstract model ${\mathcal {M}}_A$). In our setting, the $\varDelta$-abstract and concrete models both capture the protocol logic in an identical manner, and differ only in their timing semantics. The concrete model explicitly models the physical clocks of each process as real-valued variables as described in Sect. 2. The executions of this model can be represented as timed traces (sequences of timestamped states). On the other hand, in the $\varDelta$-abstract model, processes are interleaved asynchronously while respecting the approximate synchrony condition stated in Definition 3. An execution of the $\varDelta$-abstract model is an untimed trace (sequences of states). We equate timed and untimed traces using the “untiming” transformation proposed by Alur and Dill [3] — i.e., the traces must be identical with respect to the discrete states.

3.2 Computing $\varDelta$ for Time-Synchronized Systems

We now address the question of computing a value of $\varDelta$ such that the resulting ${\mathcal {M}}_A$ is a sound abstraction of the original SAS system ${\mathcal {M}}_C$. We consider here the case when ${\mathcal {M}}_C$ is a system running on a layer that guarantees time synchronization (Eq. 1) from the initial state. A second case, when nodes are not time-synchronized and approximate synchrony only holds for segments of the traces of a system, is handled in Sect. 4.

Consider a SAS system in which the physical clocks are always synchronized to within $\beta$, i.e., Eq. 1 holds for all time t and $\beta$ is a tight bound computed based on the system configuration. Intuitively, if $\beta > 0$, then $\varDelta \ge 1$ since two processes are not guaranteed to step at the same time instants, and so the number of steps of two processes can be off by at least one. The main result of this section is that SAS systems that are time-synchronized are also approximately-synchronous, and the value of $\varDelta$ is given by the following theorem.

Theorem 1

Any SAS system ${\mathcal {M}}_C$ satisfying Eq. 1 is approximately-synchronous with parameter $\varDelta = \left\lceil \frac{\beta }{\sigma ^l} \right\rceil$. (Proof in [12])

Suppose the abstract model ${\mathcal {M}}_A$ is constructed as described in Sect. 3.1 with $\varDelta$ as given in Theorem 1 and $\sigma ^l$ is the lower bound of the step size defined in Sect. 2.2. Then as a corollary, we can conclude that ${\mathcal {M}}_A$ is a sound abstraction of ${\mathcal {M}}_C$: every trace of ${\mathcal {M}}_C$ satisfies ${\text {AS}}(\varDelta )$ and hence is a trace of ${\mathcal {M}}_A$ after untiming.

Example 3

The Time-Synchronized Channel Hopping (TSCH) [1] protocol is being adopted as a part of the low power Medium Access Control standard IEEE802.15.4e. It can be modeled as a SAS system since it has a time-slotted architecture where processes share the same timetable for making steps. The TSCH protocol has two components: one that operates at the application layer, and one that provides time synchronization, with the former relying upon the latter. We verify the application layer of TSCH that assumes that nodes in the system are always time-synchronized within a bound called the “guard time” which corresponds to $\beta$. Moreover, in practice, $\beta$ is much smaller than $\sigma ^l$ and thus $\varDelta$ is typically 1 for implementations of the TSCH.

4 Systems with Recurrent Logical Conditions

We now consider the case of a SAS system that does not execute on top of a layer that guarantees time synchronization (i.e., Eq. 1 may not hold). We identify behavior of certain SAS systems, called recurrent logical conditions, that can be exploited for abstraction and verification. Specifically, even though ${\text {AS}}(\varDelta )$ may not hold for the system for any finite $\varDelta$, it may still hold for segments of every trace of the system.

Definition 4

(Recurrent Logical Condition) For a SAS system ${\mathcal {M}}_C$, a recurrent logical condition is a predicate $logicConv$ on the state of ${\mathcal {M}}_C$ such that ${\mathcal {M}}_C$ satisfies the LTL property $\mathbf{{G}}\; \mathbf{{F}}\; logicConv$.

Our verification approach is based on finding a finite $\varDelta$ such that, for every trace of ${\mathcal {M}}_C$, segments of the trace between states satisfying $logicConv$ satisfy ${\text {AS}}(\varDelta )$. This property of system traces can then be exploited for efficient model checking.

We begin with an example of a recurrent logical condition case in the context of the IEEE 1588 protocol (Sect. 4.1). We then present our verification approach based on inferring $\varDelta$ for trace segments via iterative use of model checking (Sect. 4.2).

4.1 Example: IEEE 1588 Protocol

The IEEE 1588 standard [20], also known as the precision time protocol (PTP), enables precise synchronization of clocks over a network. The protocol consists of two parts: the best master clock (BMC) algorithm and a time synchronization phase. The BMC algorithm is a distributed algorithm whose purpose is two-fold: (i) to elect a unique grandmaster clock that is the best clock in the network, and (ii) to find a unique spanning tree in the network with the grandmaster clock at the root of the tree. The combination of a grandmaster clock and a spanning tree constitutes the global stable configuration known as logical convergence that corresponds to the recurrent logical condition. The second phase, the time synchronization phase, uses this stable configuration to synchronize or correct the physical clocks (more details in  [20]).

Fig. 3.

Phases of the IEEE 1588 time-synchronization protocol

Figure 3 gives an overview of the phases of the IEEE 1588 protocol execution. The distributed system starts executing the first phase (e.g., the BMC algorithm) from an initial configuration. Initially, the clocks are not guaranteed to be synchronized to within a bound $\beta$. However, once logical convergence occurs, the clocks are synchronized shortly thereafter. Once the clocks have been synchronized, it is possible for a failure at a node or link to break clock synchronization. The BMC algorithm operates continually, with the goal of ensuring that, if time synchronization is broken, the clocks will be re-synchronized. Thus, a typical 1588 protocol execution is structured as a (potentially infinite) repetition of the two phases: logical convergence, followed by clock synchronization. We exploit this recurrent structure to show in Sect. 4.2 that we can compute a value of $\varDelta$ obeyed by segments of any trace of the system. The approach operates by iterative model checking of a specially-crafted temporal logic formula.

Note that the time taken by the protocol to logically converge depends on various factors including network topology and clock drift. In Sect. 6, we demonstrate empirically that the value of $\varDelta$ depends on the number of steps (length of the segment) taken by BMCA to converge which in turn depends on factors mentioned above.

4.2 Iterative Algorithm to Compute $\varDelta$-Abstraction for Verification

Given a SAS system ${\mathcal {M}}_C$ whose traces have a recurrent structure, and an LTL property $\varPhi$, we present the following approach to verify whether ${\mathcal {M}}_C$ satisfies $\varPhi$:

• 1. Define recurrent condition: Guess a recurrent logical condition, $logicConv$, on the global state of ${\mathcal {M}}_C$.

• 2. Compute $N_{\min }$ : Guess an initial value of $\varDelta$, and compute, from parameters $\sigma ^l, \sigma ^u$ of the processes in ${\mathcal {M}}_C$, a number $N_{\min }$ such that the ${\text {AS}}(\varDelta )$ condition is satisfied on all trace segments where no process makes $N_{\min }$ or more steps. We describe the computation of $N_{\min }$ in more detail below.

• 3. Verify if $\varDelta$ is sound: Verify using model checking on ${\mathcal {M}}_A$ that, every trace segment that starts in an initial state or a state satisfying $logicConv$ and ends in another state in $logicConv$ satisfies ${\text {AS}}(\varDelta )$. This is done by checking that no process makes $N_{\min }$ or more steps in any such segment. Note that verifying ${\mathcal {M}}_A$ in place of ${\mathcal {M}}_C$ is sound as ${\text {AS}}(\varDelta )$ is obeyed for up to $N_{\min }$ steps from any state. Further details, including the LTL property checked, are provided below.

• 4. Verify ${\mathcal {M}}_C$ using $\varDelta$ : If the verification in the preceding step succeeds, then a model checker can verify $\varPhi$ on a discrete abstraction ${\widehat{\mathcal {M}}_A}$ of ${\mathcal {M}}_C$, which, similar to ${\mathcal {M}}_A$, is obtained by dropping physical clocks and timetables, and enforcing the ${\text {AS}}(\varDelta )$ condition to segments between visits to $logicConv$. Formally, ${\widehat{\mathcal {M}}_A}= (\mathcal {S}, \widehat{\delta ^a}, \mathcal {I}, \textsc {id}, \rho _{\varDelta })$ where $\widehat{\delta ^a}$ differs from $\delta ^a$ only in that for a configuration $(s, N)$, $N'_i = 0$ for all i if $s' \in logicConv$ (otherwise it is identical to $\delta ^a$). However, if the verification in Step 3 fails, we go back to Step 2 and increment $\varDelta$ and repeat the process to compute a sound value of $\varDelta$.

Fig. 4.

Iterative algorithm for computing $\varDelta$ exploiting logical convergence

Figure 4 depicts this iterative approach for the specific case of the BMC algorithm. We now elaborate on Steps 2 and 3 of the approach.

Step 2: Computing $N_{\min }$ for a Given $\varDelta$ . Recall from Sect. 2.2 that the actual step size of a process lies in the interval $[\sigma ^l, \sigma ^u]$. Let $\mathcal {P}_f$ be the fastest process (the one that makes the most steps from the initial state) and $\mathcal {P}_s$ be the slowest (the fewest steps). Denote the corresponding number of steps by $N_f$ and $N_s$ respectively. Then the approximate synchrony condition in Definition 3 is always satisfied if $N_f - N_s \le \varDelta$. We wish to find the smallest number of steps taken by the fastest process when ${\text {AS}}(\varDelta )$ is violated. We denote this value as $N_{\min }$, and obtain it by formulating and solving a linear program.

Suppose first that $\mathcal {P}_s$ and $\mathcal {P}_f$ begin stepping at the same time t. Then, since the time between steps of $\mathcal {P}_f$ is at least $\sigma ^l$ and that between steps of $\mathcal {P}_s$ is at most $\sigma ^u$, the total elapsed must be at least $\sigma _l N_f$ and at most $\sigma ^u N_s$, yielding the inequality $\sigma ^l N_f \le \sigma ^u N_s$.

However, processes need not begin making steps simultaneously. Since each process must make its first step at least $\sigma ^u$ seconds into its execution, the maximum initial offset between processes is $\sigma ^u$. The smallest value of $N_f$ occurs when the fast process starts $\sigma ^u$ time units after the slowest one, yielding the inequality:

$$ \sigma ^l N_f + \sigma ^u \le \sigma ^u N_s $$

We can now set up the following integer linear program (ILP) to solve for $N_{\min }$:

$$\begin{aligned} \min&\; N_f \; \; s.t.&\\ N_f \ge N_s, \; \; \;&\; \; \; N_f - N_s > \varDelta , \; \; \; \; \sigma ^l N_f + \sigma ^u \le \sigma ^u N_s, \; \; \; \; \; N_f, N_s \ge 1 \end{aligned}$$

$N_{\min }$ is the optimal value of this ILP. In effect, it gives the fewest steps any process can take (smallest $N_f$) to violate the approximate synchrony condition ${\text {AS}}(\varDelta )$.

Example 4

For the IEEE 1588 protocol, as described in Sect. 2.2, the actual process step sizes lie in [0.999, 1.001]. Setting $\varDelta = 1$, solving the above ILP yields $N_{\min }= 1502$.

Step 3: Temporal Logic Property. Once $N_{\min }$ is computed, we verify on the discrete abstraction ${\mathcal {M}}_A$ whether, from any state satisfying $\mathcal {I}\vee logicConv$, the model reaches a state satisfying $logicConv$ in less than $N_{\min }$ steps. This also verifies that all traces in the BMC algorithm satisfy the recurrent $logicConv$ property and the segments between $logicConv$ satisfy ${\text {AS}}(\varDelta )$. We perform this by invoking a model checker to verify the following LTL property, which references the variables $N_i$ recording the number of steps of process $\mathcal {P}_i$:

$$\begin{aligned} (\mathcal {I}\vee logicConv) \implies \mathbf{{F}}\, \bigl [ logicConv\wedge \bigl ( \bigwedge _i (0 < N_i < N_{\min })\bigr ) \bigr ] \end{aligned}$$

(2)

We show in Sect. 5 how to implement the above check without explicitly including the $N_i$ variables in the system state. Note that it suffices to verify the above property on the discrete abstraction ${\mathcal {M}}_A$ constrained by the scheduler $\rho _{\varDelta }$ because we explore no more than $N_{\min }$ steps of any process and so ${\mathcal {M}}_A$ is a sound abstraction. The overall soundness result is formalized below.

Theorem 2

If the abstract model ${\mathcal {M}}_A$ satisfies Property 2, then all traces of the concrete model ${\mathcal {M}}_C$ are traces of the model ${\widehat{\mathcal {M}}_A}$ (after untiming) (Proof in [12])

In Sect. 6, we report on our experiments verifying properties of the BMC algorithm by model checking the discrete abstract model ${\widehat{\mathcal {M}}_A}$ as described above.

5 Model Checking with Approximate Synchrony

We implemented approximate synchrony within zing [4], an explicit state model checker. zing performs a “constrained” asynchronous composition of processes, using an external scheduler to guide the interleaving. Approximate synchrony is enforced by an external scheduler that explores only those traces satisfying ${\text {AS}}(\varDelta )$ by scheduling, in each state, only those processes whose steps will not violate ${\text {AS}}(\varDelta )$.

Section 4 described an iterative approach to verify whether a $\varDelta$-abstract model of a protocol is sound. The soundness proof depends on verifying Property 2. A naïve approach for checking this property would be to include a local variable $N_i$ in each process as part of the process state to keep track of the number of steps executed by each process, causing state space explosion. Instead, we store the values of $N_i$ for each i external to the system state, as a part of the model checker explorer.

Fig. 5.

Algorithm for Verification of Property 2

The algorithm in Fig. 5 performs systematic bounded depth first search for a state $s_{initial}$, belonging to the set of all possible initial states. To check whether all traces of length $N_{\min }$ satisfy eventual logical convergence under ${\text {AS}}(\varDelta )$ constraint, we enforce two bounds: first, the final depth bound is $(N_{\min }+\varDelta )$ and second, in each state a process is enabled only if executing that process does not violate ${\text {AS}}(\varDelta )$. If a state satisfies $logicConv$ then we terminate the search along that path.

The BoundedDFS function is called recursively on each successor state and it explore only those traces that satisfy ${\text {AS}}(\varDelta )$. If the steps executed by a process is $N_{min}$ then the $logicConv$ monitor is invoked to assert if $s' \models logicConv$ (i.e. we have reached logical convergence state) and if the assertion fails we increment the value of $\varDelta$ as described in Sect. 4.2. $N_{\min }$ and $\varDelta$ values are derived as explained in Sect. 4.2.

StateTable is a map from reachable state to the tuple of steps with which it was last explored. $steps'$ is the vector of number of steps executed by each process and is stored as a list of integers. #Processes(s) returns the number of enabled processes in the state s. IncElement(i, t) increments the $i^{th}$ element of tuple t and returns the updated tuple. CheckASCond$(steps')$ checks the following condition that $\forall s_1, s_2 \in steps' \, \, | s_1 - s_2 | \le \varDelta$.

To avoid re-exploring a state which may not lead to new states, we do not re-explore a state if it is revisited with $steps'$ greater than what it was last visited with. The operator $\ge _{ pt }$ does a pointwise comparison of the integer tuples. We show in the following section that we are able to obtain significant state space reduction using this implementation.

6 Evaluation

In this section, we present our empirical evaluation of the approximate synchrony abstraction, guided by the following goals:

• Verify two real-world standards protocols: (1) the best master clock algorithm in IEEE 1588 and (2) the time synchronized channel hopping protocol in IEEE 802.15.4e.

• Evaluate if we can verify properties that cannot be verified with full asynchrony (either by reducing state space or by capturing relevant timing constraints).

• Evaluate approximate synchrony as an iterative bounding technique for finding bugs efficiently in almost-synchronous systems.

6.1 Modeling and Experimental Setup

We model the system in P [11], a domain-specific language for writing event-driven protocols. A protocol model in P is a collection of state machines interacting with each other via asynchronous events or messages. The P compiler generates a model for systematic exploration by Zing [4]. P also provides ways of writing LTL properties as monitors that are synchronously composed with the model. Both the case studies, the BMC algorithm and the TSCH protocol, are modeled using P. Each node in the protocol is modeled as a separate P state machine. Faults and message losses in the protocol are modeled as non-deterministic choices.

Table 1. Temporal properties verified for the case studies

All experiments were performed on a 64-bit Windows server with Intel Xeon ES-2440, 2.40GHz (12 cores/24 threads) and 160 GB of memory. Zing can exploit parallelism as its iterative depth-first search algorithm is completely parallelized. All timing results reported in this section are when Zing is run with 24 threads. We use the number of states explored and the time taken to explore them as the comparison metric.

6.2 Verification and Testing Using Approximate Synchrony

We applied approximate synchrony in three different contexts: (1) Time synchronized Channel Hopping protocol (time synchronized system) (2) Best Master Clock Algorithm in IEEE 1588 (exploiting recurrent logical condition) (3) Approximate Synchrony as a bounding technique for finding bugs.

Verification of the TSCH Protocol. Time Synchronized Channel Hopping (TSCH) is a Medium Access Control scheme that enables low power operations in wireless sensor network using time-synchronization. It makes an assumptions that the clocks are always time-synchronized within a bound, referred to as the ‘guard’ time in the standard. The low power operation of the system depends on the sensor nodes being able to maintain synchronization (desynchronization property in Table 1). A central server broadcasts the global schedule that instructs each sensor node when to perform operations. Whether the system satisfies the desynchronization property depends on this global schedule, and the standard provides no recommendation on these schedules.

We modeled the TSCH as a SAS system and used Theorem 1 to calculate the value of $\varDelta$ ². We verified the desynchronization property (Table 1) in the presence of failures like message loss, interference in wireless network, etc. For the experiments we considered three schedules (1) round-robin: nodes are scheduled in a round robin fashion, (2) shared with random back-off: all the schedule slots are shared and conflict is resolved using random back-off (3) Priority Scheduler: nodes are assigned fixed priority and conflict is resolved based on the priority.

We were able to verify if the property was satisfied for a given topology under the global schedule, and generated a counterexample otherwise (Table 2) which helped the TSCH system developers in choosing the right schedules for low power operation. Using sound approximate synchrony abstraction (with $\varDelta = 1$), we could accurately capture the “almost synchronous” behavior of the TSCH system.

Table 2. Verification results using Approximate Synchrony.

Verification of BMC Algorithm. The BMC algorithm is a core component of the IEEE 1588 precision time protocol. It is a distributed fault tolerant protocol where nodes in the system perform operations periodically to converge on a unique hierarchical tree structure, referred to as the logical convergence state in Sect. 4. Note that the convergence property for BMCA holds only in the presence of almost synchrony — it does not guarantee convergence in the presence of unbounded process delay or message delay. Hence, it is essential to verify BMC using the right form of synchrony.

We generated various verification instances by changing the configuration parameters such as number of nodes, clock characteristics, and the network topology. The results in Table 2 for the BMC algorithm are for 5 and 7 nodes in the network with linear, star, ring, and random topologies. The $\varDelta$ value used for verification of each of these configurations was derived by using the iterative approach described in Sect. 4.2. The results demonstrate that the value of $\varDelta$ required to construct the sound abstraction varies depending on network topology, and clock dynamics. Table 2 shows the total number of states explored and time taken by the model checker for proving the safety and convergence property (Table 1) using the sound $\varDelta$-abstract model. Approximate synchrony abstraction is orders of magnitude faster as it explores the reduced state-space. BMCA algorithm satisfies safety invariant even in the presence of complete asynchrony. For demonstrating the efficiency of using approximate synchrony we also conducted the experiments with complete asynchronous composition, exploring all possible interleaving (for safety properties). The complete asynchronous model is simple to implement but fails to prove the properties for most of the topologies.

An upshot of our approach is that we are the first to prove that the BMC algorithm in IEEE 1588 achieves logical convergence to a unique stable state for some interesting configurations. This was possible because of the sound and tunable approximate synchrony abstraction. Although experiments with 5/7 nodes may seem small, networks of this size do occur in practice, e.g., in industrial automation where one has small teams of networked robots on a factory floor.

Endlessly Circulating (Rogue) Frames in IEEE 1588: The possibility of an endlessly circulating frame in a 1588 network has been debated for a while in the standards committee. Using formal model of BMC algorithm under approximate synchrony, we were able to reproduce a scenario were rogue frame could occur. Existence of a rogue frame can lead to network congestion or cause the BMC algorithm to never converge. The counter example was cross-validated using simulation and is described in detail in [6]. It was well received by the IEEE 1588 standards committee.

Table 3. Iterative Approximate Synchrony with bound $\varDelta$ for finding bugs faster.

Approximate Synchrony as a Search Prioritization Technique. Approximate synchrony can also be used as a bounding technique to prioritize search. We collected buggy models during the process of modeling the BMC algorithm and used them as benchmarks, along with buggy instance of the Perlman’s Spanning Tree Protocol [24] (SPT). We used AS as an iterative bounding technique, starting with $\varDelta = 0$ and incrementing $\varDelta$ after each iteration. For $\varDelta =0$, the model checker explores only synchronous system behaviors. Increasing the value could be considered as adding bounded asynchronous behaviors incrementally. Table 3 shows comparison between iterative AS, non-iterative AS with fixed value of $\varDelta$ taken from Table 2 and iterative depth bounding with random search. Number of states explored and the corresponding time taken for finding the bug is used as the comparison metric. Results demonstrate that most of the bugs are found at small values of $\varDelta$ (hence iterative search is beneficial for finding bugs). Some bugs like the rogue frame error, that occur only when there is asynchrony were found with minimal asynchrony in the system ($\varDelta = 1$). These results confirm that prioritizing search based on approximate synchrony is beneficial in finding bugs. Other bounding techniques such as delay bounding [15] and context bounding [23] can be combined with approximate synchrony but this is left for future work.

7 Related Work

The concept of partial synchrony has been well-studied in the theory of distributed systems [13, 14, 25]. There are many ways to model partial synchrony depending on the type of system and the end goal (e.g., formal verification). Approximate synchrony is one such approach, which we contrast against the most closely-related work below.

Hybrid/Timed Modeling: The choice of modeling formalism greatly influences the verification approach. A time-synchronized system can be modeled as a hybrid system [2]. However, it is important to note that, unlike traditional hybrid systems examples from the domain of control, the discrete part of the state space for these protocols is very large. Due to this we observed that leading hybrid systems verification tools, such as SpaceEx [17], cannot explore the entire state space.

There has been work on modeling timed protocols using real-time formalisms such as timed automata [3], where the derivatives of all continuous-time variables are equal to one. While tools based on the theory of timed automata do not explicitly support modeling and verification of multi-rate timed systems [21], there do exist techniques for approximating multirate clocks. For instance, Huang et al. [19] propose the use of integer clocks on top of UPPAAL models. Daws and Yovine [9] show how multirate timed systems can be over-approximated into timed automata. Vaandrager and Groot [29] models a clock that can proceed with different rate by defining a clock model consisting of one location and one self transition. Such models only approximately represent multirate time systems. By contrast, our approach algorithmically constructs abstractions that can be refined to be more precise by tuning the value of $\varDelta$, and results in an sound untimed model that can be directly checked by a finite-state model checker.

Synchrony and Asynchrony: There have been numerous efforts devoted towards mixing synchronous and asynchronous modeling. Multiclock Esterel [26] and communicating reactive processes (CRP) [5] extend the synchronous language Esterel to support a mix of synchronous and asynchronous processes. Bounded asynchrony is another such modeling technique with applications to biological systems [16]. It can be used to model systems in which processes can have different but constant rates, and can be interleaved asynchronously (with possible stuttering) before they all synchronize at the end of a global “period.” Approximate synchrony has no such synchronizing global period. The quasi-synchronous (QS) [7, 18] approach is designed for communicating processes that are periodic and have almost the same period. QS [18] is defined as “Between any two successive activations of one period process, the process on any other process is activated either 0, 1, or at most 2 times”. As a consequence, in both quasi-synchrony and bounded asynchrony, the difference of the absolute number of activations of two different processes can grow unboundedly. In contrast, the definition of AS does not allow this difference to grow unbounded.

8 Conclusion

This paper has introduced two new concepts: a class of distributed systems termed as symmetric, almost-synchronous (SAS) systems, and approximate synchrony, an abstraction method for such systems. We evaluated applicability of approximate synchrony for verification in two different contexts: (i) application-layer protocols running on top of time-synchronized systems (TSCH), and (ii) systems that do not rely on time synchronization but exhibit recurrent logical behavior (BMC algorithm). We also described an interesting search prioritization technique based on approximate synchrony with the key insight that, prioritizing synchronous behaviors can help in finding bugs faster.

In this paper, we focus on verifying protocols that fit the SAS formalism defined in Sect. 2.2. While other protocols whose behavior and correctness relies on using values of timestamps do not natively fit into the SAS formalism, they can be abstracted using the suitable methods (e.g., using a state variable to model a local timer for a process whose value is incremented on each step of that process — with approximate synchrony the timer values across different processes will not differ by more than $\varDelta$). Evaluating such abstractions for protocols like Google Spanner and others that use timestamps would be an interesting next step.