Verifying Asynchronous EventDriven Programs Using Partial Abstract Transformers
Abstract
We address the problem of analyzing asynchronous eventdriven programs, in which concurrent agents communicate via unbounded message queues. The safety verification problem for such programs is undecidable. We present in this paper a technique that combines queuebounded exploration with a convergence test: if the sequence of certain abstractions of the reachable states, for increasing queue bounds k, converges, we can prove any property of the program that is preserved by the abstraction. If the abstract state space is finite, convergence is guaranteed; the challenge is to catch the point \(k_{\max }\) where it happens. We further demonstrate how simple invariants formulated over the concrete domain can be used to eliminate spurious abstract states, which otherwise prevent the sequence from converging. We have implemented our technique for the P programming language for eventdriven programs. We show experimentally that the sequence of abstractions often converges fully automatically, in hard cases with minimal designer support in the form of sequentially provable invariants, and that this happens for a value of \(k_{\max }\) small enough to allow the method to succeed in practice.
1 Introduction
Asynchronous eventdriven (AED) programming refers to a style of programming multiagent applications. The agents communicate shared work via messages. Each agent waits for a message to arrive, and then processes it, possibly sending messages to other agents, in order to collectively achieve a goal. This programming style is common for distributed systems as well as lowlevel designs such as device drivers [11]. Getting such applications right is an arduous task, due to the inherent concurrency: the programmer must defend against all possible interleavings of messages between agents. In response to this challenge, recent years have seen multiple approaches to verifying AEDlike programs, e.g. by delaying send actions, or temporarily bounding their number (to keep queue sizes small) [7, 10], or by reasoning about a small number of representative execution schedules, to avoid interleaving explosion [5].
In this paper we consider the P language for AED programming [11]. A P program consists of multiple state machines running in parallel. Each machine has a local store, and a message queue through which it receives events from other machines. P allows the programmer to formulate safety specifications via a statement that asserts some predicate over the local state of a single machine. Verifying such reachability properties of course requires reasoning over global system behavior and is, for unboundedqueue P programs, undecidable [8].
The unboundedness of the reachable state space does not prevent the use of testing tools that try to explore as much of the state space as possible [3, 6, 11, 13] in the quest for bugs. Somewhat inspired by this kind of approach, the goal of this paper is a verification technique that can (sometimes) prove a safety property, despite exploring only a finite fraction of that space. Our approach is as follows. Assuming that the machines’ queues are the only source of unboundedness, we consider a bound k on the queue size, and exhaustively compute the reachable states Open image in new window of the resulting finitestate problem, checking the local assertion \(\varPhi \) along the way. We then increase the queue bound until (an error is found, or) we reach some point Open image in new window of convergence: a point that allows us to conclude that increasing k further is not required to prove \(\varPhi \).
What kind of “convergence” are we targeting? We design a sequence Open image in new window of abstractions of each reachability set over a finite abstract state space. Due to the monotonicity of sequence Open image in new window , this ensures convergence, i.e. the existence of Open image in new window such that Open image in new window for all Open image in new window . Provided that an abstract state satisfies \(\varPhi \) exactly if all its concretizations do, we have: if all abstract states in Open image in new window comply with \(\varPhi \), then so do all reachable concrete states of P—we have proved the property.
We implement this strategy using an abstraction function Open image in new window with a finite codomain that leaves the local state of a machine unchanged and maintains the first occurrence of each event in the queue; repeat occurrences are dropped. This abstraction preserves properties over the local state and the head of the queue, i.e. the visible (to the machine) part of the state space, which is typically sufficient to express reachability properties.
The second major step in our approach is the detection of the point of convergence of Open image in new window : We show that, for the best abstract transformer Open image in new window [9, 27, see Sect. 4.2], if Open image in new window , then Open image in new window for all \(K \ge k\). In fact, we have a stronger result: under an easytoenforce condition, it suffices to consider abstract dequeue operations: all others, namely enqueue and local actions, never lead to abstract states in Open image in new window . The best abstract transformer for dequeue actions is efficiently implementable for a given P program.
It is of course possible that the convergence condition Open image in new window never holds (the problem is undecidable). This manifests in the presence of a spurious abstract state in the image produced by Open image in new window , i.e. one whose concretization does not contain any reachable state. Our third contribution is a technique to assist users in eliminating such states, enhancing the chances for convergence. We have observed that spurious abstract states are often due to violations of simple machine invariants: invariants that do not depend on the behavior of other machines. By their nature, they can be proved using a cheap sequential analysis.
We can eliminate an abstract state (e.g. produced by Open image in new window ) if all its concretizations violate a machine invariant. In this paper, we propose a domainspecific temporal logic to express invariants over machines with event queues and, more importantly, an algorithm that decides the above abstract queue invariant checking problem, by reducing it efficiently to a plain model checking problem. We have used this technique to ensure the convergence in “hard” cases that otherwise defy convergence of the abstract reachable states sequence.
We have implemented our technique for the P language and empirically evaluated it on an extensive set of benchmark programs. The experimental results support the following conclusions: (i) for our benchmark programs, the sequence of abstractions often converges fully automatically, in hard cases with minimal designer support in the form of separately dischargeable invariants; (ii) almost all examples converge at a small value of Open image in new window ; and (iii) the overhead our technique adds to the bounding technique is small: the bulk is spent on the exhaustive bounded exploration itself.
Proofs and other supporting material can be found in the Appendix of [23].
2 Overview
A critical property for P programs is (bounded) responsiveness: the receiving machine must have a handler (e.g. on, defer, ignore) for every event arriving at the queue head; otherwise the event will come as a “surprise” and crash the machine. To prove responsiveness for \( PiFl \), we have to demonstrate (among others) that in state Open image in new window , the Open image in new window event is never at the head of the Receiver’s queue. We cannot perform exhaustive model checking, since the set of reachable states is infinite. Instead, we will compute a conservative abstraction of this set that is precise enough to rule out Open image in new window events at the queue head in this state.
We now generate the sequence Open image in new window of abstractions of the reachable states sets Open image in new window for queue size bounds \(k=0,1,2,\ldots \), by computing each finite set Open image in new window , and then Open image in new window as Open image in new window . The obtained monotone sequence Open image in new window over a finite domain will eventually converge, but we must prove that it has. This is done by applying the best abstract transformer Open image in new window , restricted to dequeue operations (defined in Sect. 4.2), to the current set Open image in new window , and confirming that the result is contained in Open image in new window .
As it turns out, the confirmation fails for the \( PiFl \) program: \(k=5\) marks the first time set Open image in new window repeats, i.e. Open image in new window , so we are motivated to run the convergence test. Unfortunately we find a state Open image in new window , preventing convergence. Our approach now offers two remedies to this dilemma. One is to refine the queue abstraction. In our implementation, function Open image in new window is really Open image in new window , for a parameter p that denotes the size of the prefix of the queue that is kept unchanged by the abstraction. For example, for the queue from Eq. (1) we have Open image in new window , where \(\mid \) separates the prefix from the “infinite tail” of the abstract queue. This (straightforward) refinement maintains finiteness of the abstraction and increases precision, by revealing that the queue starts with three Open image in new window events. Rerunning the analysis for the \( PiFl \) program with \(p=4\), at \(k=5\) we find Open image in new window , and the proof is complete.
3 Queue(Un)Bounded Reachability Analysis
Communicating Queue Systems. We consider P programs consisting of a fixed and known number n of machines communicating via event passing through unbounded FIFO queues.^{1} For simplicity, we assume the machines are created at the start of the program; dynamic creation at a later time can be simulated by having the machine ignore all events until it receives a special creation event.

Open image in new window , denoting an action internal to Open image in new window (no other QA involved) that either dequeues an event (\( deq \)), or updates its local state (\( loc \)); or

Open image in new window , for Open image in new window , denoting a transmission, where Open image in new window (the sender) adds event Open image in new window to the end of the queue of Open image in new window (the receiver).
The individual QA of a CQS model machines of a P program; hence we refer to QA states as machine states. A transmit action is the only communication mechanism among the QA.

(internal) Open image in new window , and for all Open image in new window , Open image in new window ;
 (transmission) there exists Open image in new window and Open image in new window such that:
 1.
 2.
 3.
Open image in new window for all Open image in new window ; and
 4.
 1.
The execution model of a CQS is strictly interleaving. That is, in each step, one of the two above transitions (internal) or (transmission) is performed for a nondeterministically chosen machine i.
QueueBounded and QueueUnbounded Reachability. Given a CQS Open image in new window , a state Open image in new window , and a number k, the queuebounded reachability problem (for Open image in new window and k) determines whether Open image in new window is reachable under queue bound k, i.e. whether there exists a path Open image in new window such that Open image in new window , and for Open image in new window , all queues in state Open image in new window have at most k events. Queuebounded reachability for k is trivially decidable, by making enqueue actions for queues of size k blocking (the sender cannot continue), which results in a finite state space. We write Open image in new window .
Queuebounded reachability will be used in this paper as a tool for solving our actual problem of interest: Given a CQS Open image in new window and a state Open image in new window , the QueueUnBounded reachability Analysis (QUBA) problem determines whether Open image in new window is reachable, i.e. whether there exists a (queueunbounded) path from Open image in new window to Open image in new window . The QUBA problem is undecidable [8]. We write Open image in new window ( Open image in new window ) for the set of reachable states.
4 Convergence via Partial Abstract Transformers
In this section, we formalize our approach to detecting the convergence of a suitable sequence of observations about the states Open image in new window reachable under kbounded semantics. We define the observations as abstractions of those states, resulting in sets Open image in new window . We then investigate the convergence of the sequence Open image in new window .
4.1 List Abstractions of Queues
Our abstraction function applies to queues, as defined below. Its action on machine and system states then follows from the hierarchical design of a CQS. Let Open image in new window denote the number of events in Open image in new window , and Open image in new window the ith event in Open image in new window Open image in new window .
Definition 1
 1.
 2.For a nonempty queue Open image in new window ,
Intuitively, Open image in new window abstracts a queue by leaving its first p events unchanged (an idea also used in [16]). Starting from position p it keeps only the first occurrence of each event Open image in new window in the queue, if any; repeat occurrences are dropped.^{2} The preservation of existence and order of the first occurrences of all present events motivates the term list abstraction. An alternative is an abstraction that keeps only the set (not: list) of queue elements from position p, i.e. it ignores multiplicity and order. This is by definition less precise than the list abstraction and provided no efficiency advantages in our experiments. An abstraction that keeps only the queue head proved cheap but too imprecise.
The motivation for parameter p is that many protocols proceed in rounds of repeating communication patterns, involving a bounded number of message exchanges. If p exceeds that number, the list abstraction’s loss of information may be immaterial.
We write an abstract queue Open image in new window in the form Open image in new window s.t. \(p= pref \), and refer to \( pref \) as Open image in new window prefix (shared with Open image in new window ), and \( suff \) as Open image in new window suffix.
Example 2
The queues Open image in new window are Open image in new window equivalent: Open image in new window .
We extend Open image in new window to act on a machine state via Open image in new window , on a state via Open image in new window , and on a set of states pointwise via Open image in new window .
We say the abstraction function Open image in new window respects a property of a state if, for any two Open image in new window equivalent states (see Example 2), the property holds for both or for neither. Function Open image in new window respects properties that refer to the localstate part of a machine, and to the first \(p+1\) events of its queue (which are preserved by Open image in new window ). In addition, the property may look beyond the prefix and refer to the existence of events in the queue, but not their frequency or their order after the first occurrence.
The rich information preserved by the abstraction (despite being finitestate) especially pays off in connection with the defer feature in the P language, which allows machines to delay handling certain events at the head of a queue [11]. The machine identifies the first nondeferred event in the queue, a piece of information that is precisely preserved by the list abstraction (no matter what p).
Definition 3
As a special case, Open image in new window and so Open image in new window for the empty queue. We extend Open image in new window to act on abstract (machine or global) states in a way analogous to the extension of Open image in new window , by moving it inside to the queues occurring in those states.
4.2 Abstract Convergence Detection
The key of the algorithm is reflected in Lines 6–9 and is based on the following idea (all claims are proved as part of Theorem 4 below). If the computation of Open image in new window reveals no new abstract states in round k (Line 6; by monotonicity, “same size” implies “same sets”), we apply the best abstract transformer [9, 27] Open image in new window to Open image in new window : if the result is contained in Open image in new window , the abstract reachability sequence has converged. However, we can do better: we can restrict the successor function Open image in new window of the CQS to dequeue actions, denoted \( Im _{ deq }\) in Line 7. The ultimate reason is that firing a local or transmit action on two Open image in new window equivalent states r and s results again in Open image in new window equivalent states \(r'\) and \(s'\). This fact does not hold for dequeue actions: the successors \(r'\) and \(s'\) of dequeues depend on the abstracted parts of r and s, resp., which may differ and become “visible” during the dequeue (e.g. the event behind the queue head moves into the head position). Our main result therefore is: if Open image in new window and dequeue actions do not create new abstract states (Lines 7 and 8), sequence Open image in new window has converged:
Theorem 4
If Open image in new window and Open image in new window , then for any \(K \ge k\), Open image in new window .
If the sequence of reachable abstract states has converged, then all reachable concrete states (any k) belong to Open image in new window (for the current k). Since the abstraction function Open image in new window respects property \(\varPhi \), we know that if any reachable concrete state violated \(\varPhi \), so would any other concrete state that maps to the same abstraction. However, for each abstract state in Open image in new window , Line 4 has examined at least one state r in its concretization; a violation was not found. We conclude:
Corollary 5
Line 9 of Algorithm 1 correctly asserts that no reachable concrete state of the given CQS violates \(\varPhi \).
The corollary (along with the earlier statement about Lines 4–5) confirms the partial correctness of Algorithm 1. The procedure is, however, necessarily incomplete: if no error is detected and the convergence condition in Line 8 never holds, the for loop will run forever.
We conclude this part with two comments. First, note that we do not compute the sets Open image in new window as reachability fixpoints in the abstract domain (i.e. the domain of Open image in new window ). Instead, we compute the concrete reachability sets first, and then obtain the Open image in new window via projection (Line 1). The reason is that the projection gives us the exact set of abstractions of reachable concrete states, while an abstract fixpoint likely overapproximates (for instance, the best abstract transformer from Line 7 does) and loses precision. Note that a primary motivation for computing abstract fixpoints, namely that the concrete fixpoint may not be computable, does not apply here: the concrete domains are finite, for each k.
Second, we observe that this projection technique comes with a cost: sequence Open image in new window may stutter at intermediate moments: Open image in new window . The reason is that Open image in new window is not obtained as a functional image of Open image in new window , but by projection from Open image in new window . As a consequence, we cannot shortcut the convergence detection by just “waiting” for Open image in new window to stabilize, despite the finite domain.
4.3 Computing Partial Best Abstract Transformers
The first case for Open image in new window applies if there are no occurrences of Open image in new window in the suffix after the dequeue. The remaining cases enumerate possible positions of the first occurrence of Open image in new window (boxed, for readability) in the suffix after the dequeue. The cost of this enumeration is linear in the length of the suffix of the abstract queue.
Since our list abstraction maintains the first occurrence of each event, the semantics of defer (see the Discussion in Sect. 4.1) can be implemented abstractly without loss of information (not shown above, for simplicity).
5 Abstract Queue Invariant Checking
The abstract transformer function in Sect. 4 is used to decide whether sequence Open image in new window has converged. Being an overapproximation, the function may generate spurious states: they are not reachable, i.e. no concretization of them is. Unfortunate for us, spurious abstract states always prevent convergence.
A key empirical observation is that concretizations of spurious abstract states often violate simple machine invariants, which can be proved from the perspective of a single machine, while collapsing all other machines into a nondeterministically behaving environment. Consider our example from Sect. 2 for \(p=0\). It fails to converge since Line 7 generates an abstract state \(\bar{s}\) that features a Open image in new window event followed by a Open image in new window event in the Open image in new window queue. A lightweight static analysis proves that the Open image in new window machine permits no path from the Open image in new window to the Open image in new window statement. Since every concretization of \(\bar{s}\) features a Open image in new window followed by a Open image in new window event, the abstract state \(\bar{s}\) is spurious and can be eliminated.
Our tool assists users in discovering candidate machine invariants, by facilitating the inspection of states in Open image in new window (which foil the test in Line 8). We discharge such invariants separately, via a simple sequential modelcheck or static analysis. In the section we focus on the more interesting question of how to use them. Formally, suppose the P program comes with a queue invariant I, i.e. an invariant property of concrete queues. The abstract invariant checking problem is to decide, for a given abstract queue Open image in new window , whether every concretization of Open image in new window violates I; in this case, and this case only, an abstract state containing Open image in new window can be eliminated. In the following we define a language QuTL for specifying concrete queue invariants (5.1), and then show how checking an abstract queue against a QuTL invariant can be efficiently solved as a model checking problem (5.2).
5.1 Queue Temporal Logic (QuTL)
Our logic to express invariant properties of queues is a form of firstorder lineartime temporal logic. This choice is motivated by the logic’s ability to constrain the order (via temporal operators) and multiplicity of queue events, the latter via relational operators that express conditions on the number of event occurrences.
Definition 6

\( false \) and \( true \).

E, for a queue relational expression E.

Open image in new window , Open image in new window , Open image in new window , for a QuTL formula \(\phi \).
The set QuTL is the Boolean closure of the above set of formulas.
Definition 7
(Concrete semantics of QuTL). Concrete queue Open image in new window satisfies QuTL formula \(\phi \), written Open image in new window , depending on the form of \(\phi \) as follows.

for Open image in new window iff Open image in new window and Open image in new window .

for a queue relational expression E, Open image in new window iff \(V(E) = true \).

Open image in new window iff Open image in new window and Open image in new window .

Open image in new window iff there exists \(i \in \mathbb N\) such that Open image in new window and Open image in new window .

Open image in new window iff for all \(i \in \mathbb N\) such that Open image in new window , Open image in new window .
Satisfaction of Boolean combinations is defined as usual, e.g. Open image in new window iff Open image in new window . No other pair Open image in new window satisfies Open image in new window .
For instance, formula Open image in new window is true exactly for queues containing at most 3 Open image in new window , and formula Open image in new window is true of Open image in new window iff Open image in new window is empty or its final event (!) is Open image in new window . See App. B of [23] for more examples.
Algorithmically checking whether a concrete queue Open image in new window satisfies a QuTL formula \(\phi \) is straightforward, since Open image in new window is of fixed size and straightline. The situation is different with abstract queues. Our motivation here is to declare that an abstract queue Open image in new window violates a formula \(\phi \) if all its concretizations (Definition 3) do: under this condition, if \(\phi \) is an invariant, we know Open image in new window is not reachable. Equivalently:
Definition 8
5.2 Abstract QuTL Model Checking
A QuTL constraint is a QuTL formula without Boolean connectives. We first describe how to model check against QuTL constraints, and come back to Boolean connectives at the end of Sect. 5.2.
Model checking an abstract queue Open image in new window against a QuTL constraint \(\phi \), i.e. checking whether some concretization of Open image in new window satisfies \(\phi \), can be reduced to a standard model checking problem over a labeled transition system (LTS) Open image in new window with states Open image in new window , transitions Open image in new window , and a labeling function Open image in new window . The LTS characterizes the concretization Open image in new window of Open image in new window , as illustrated in Fig. 2 using an example: the concretizations of Open image in new window are formed from the regularexpression traces generated by paths of Open image in new window LTS that end in the doublecircled green state.
The straightforward construction of the LTS Open image in new window is formalized in App. A.2 of [23]. Its size is linear in Open image in new window .
We call a path through Open image in new window complete if it ends in the rightmost state \(s_z\) of Open image in new window (green in Fig. 2). The labeling function extends to paths via Open image in new window . This gives rise to the following characterization of Open image in new window :
Lemma 9
We say path Open image in new window satisfies \(\phi \), written Open image in new window , if there exists Open image in new window s.t. Open image in new window .
Corollary 10
Let Open image in new window and M as in Lemma 9, and \(\phi \) a QuTL constraint. Then the following are equivalent.
 1.
 2.
There exists a complete path Open image in new window from \(s_0\) in Open image in new window such that Open image in new window .
Given an abstract queue Open image in new window , its LTS Open image in new window , and a QuTL constraint \(\phi \), our abstract queue model checking algorithm is based on Corollary 10: we need to find a complete path from \(s_0\) in Open image in new window that satisfies \(\phi \). This is similar to standard model checking against existential temporal logics like ECTL, with two particularities:
First, paths must be complete. This poses no difficulty, as completeness is suffixclosed: a path ends in \(s_z\) iff any suffix does. This implies that temporal reductions on QuTL constraints work like in standard temporal logics. For example: there exists a complete path Open image in new window from \(s_0\) in Open image in new window such that Open image in new window iff there exists a complete path Open image in new window from some successor \(s_1\) of \(s_0\) such that Open image in new window .

this is true iff Open image in new window , as is immediate from the Open image in new window case in Definition 7.
 Open image in new window ): this is true iff

the number of states reachable from s labeled e is greater than c, or

there exists a state reachable from s labeled with e that has a selfloop.
The other relational expressions Open image in new window are checked similarly. \(\square \)

Results: \( \#M \): #P machines; \( Loc \): #lines of code; Open image in new window : property holds; p: minimum unabstracted prefix for required convergence; \(k_{\max }\): point of convergence or exposed bugs (– means divergence); Time: runtime (sec); Mem.: memory usage (Mb.).
6 Empirical Evaluation
We implemented the proposed approaches in C# atop the bounded model checker PTester [11], an analysis tool for P programs. PTester employs a bounded exploration strategy similar to Zing [4]. We denote by Pat the implementation of Algorithm 1, and by Open image in new window the version with queue invariants (“Pat+ Invariants”). A detailed introduction to tool design and implementation is available online [22].

Q1. Is Pat effective: does it converge for many programs? for what values of k?

Q2. What is the impact of the QuTL invariant checking?

1–5: protocols implemented in P: the German Cache Coherence protocol with different number of clients (1–2) [11], a buggy version of a token ring protocol [11], and a fixed version (3–4), and a failure detector protocol from [25] (5).

6–7: two device drivers where OSR is used for testing USB devices [10].

8–14: miscellaneous: 8–10 [25], 11 [15], 12 is the example from Sect. 2, 13–14 are the buggy and fixed versions of an Elevator controller [11].
We conduct two types of experiments: (i) we run Pat on each benchmark to empirically answer Q1; (ii) we run Open image in new window on the examples which fail to verify in (i) to answer Q2. All experiments are performed on a 2.80 GHz Intel(R) Core(TM) i77600 machine with 8 GB memory, running 64bit Windows 10. The timeout is set to 3600 s (1h); the memory limit to 4 GB.
Results. Table 1 shows that Pat converges on almost all safe examples (and successfully exposes the bugs for unsafe ones). Second, in most cases, the \(k_{\max }\) where convergence was detected is small, 5 or less. This is what enables the use of this technique in practice: the exploration space grows fast with k, so early convergence is critical. Note that \(k_{\max }\) is guaranteed to be the smallest value for which the respective example converges. If convergent, the verification succeeded fully automatically: the queue abstraction prefix parameter p is incremented in a loop whenever the current value of p caused a spurious abstract state.
The German protocol does not converge in reasonable time. In this case, we request minimal manual assistance from the designer. Our tool inspects spurious abstract states, compares them to actually reached abstract states, and suggests candidate invariants to exclude them. We describe the process of invariant discovery, and why and how they are easy to prove, in [22].
Program  p  \(k_{\max }\)  Time  Mem.  Invariant 

German1  0  4  15.65  45.65  Server: \(\#{ req\_excl } \le 1 \wedge \#{req\_share} \le 1\) 
German2  0  4  629.43  284.75  Client: \(\#{ ask\_excl } \le 1 \wedge \#{ ask\_share } \le 1\) 
The invariant states that there is always at most one exclusive request and at most one shared request in the Server or Client machine’s queue.
Performance Evaluation. We finally consider the following question: To perform full verification, how much overhead does Pat incur compared to PTester? We iteratively run PTester with a queue bound from 1 up to \(k_{\max }\) (from Table 1).
The figure on the right compares the running times of Pat and PTester. We observe that the difference is small, in all cases, suggesting that turning PTester into a full verifier comes with little extra cost. Therefore, as for improving Pat’s scalability, the focus should be on the efficiency of the Open image in new window computation (Line 3 in Algorithm 1). Techniques that lend themselves here are partial order reduction [2, 28] or symmetry reduction [29]. Note that our proposed approach is orthogonal to how these sets are computed.
7 Related Work
Automatic verification for asynchronous eventdriven programs communicating via unbounded FIFO queues is undecidable [8], even when the agents are finitestate machines. To sidestep the undecidability, various remedies are proposed. One is to underapproximate program behaviors using various bounding techniques; examples include depth [17] and contextbounded analysis [19, 20, 26], delaybounding [13], bounded asynchrony [15], preemptionbounding [24], and phasebounded analysis [3, 6]. It has been shown that most of these bounding techniques admit a decidable model checking problem [19, 20, 26] and thus have been successfully used in practice for finding bugs.
Gall et al. proposed an abstract interpretation of FIFO queues in terms of regular languages [16]. While our works share some basic insights about taming queues, the differences are fundamental: our abstract domain is finite, guaranteeing convergence of our sequence. In [16] the abstract domain is infinite; they propose a widening operator for fixpoint computation. More critically, we use the abstract domain only for convergence detection; the set of reachable states returned is in the end exact. As a result, we can prove and refute properties but may not terminate; [16] is inexact and cannot refute but always returns.
Several partial verification approaches for asynchronous messagepassing programs have been presented recently [5, 7, 10]. In [5], Bakst et al. propose canonical sequentialization, which avoids exploring all interleavings by sequentializing concurrent programs. Desai et al. [10] propose an alternative way, namely by prioritizing receive actions over send actions. The approach is complete in the sense that it is able to construct almostsynchronous invariants that cover all reachable local states and hence suffice to prove local assertions. Similarly, Bouajjani et al. [7] propose an iterative analysis that bounds send actions in each interaction phase. It approaches the completeness by checking a program’s synchronizability under the bounds. Similar to our work, the above three works are sound but incomplete. An experimental comparison against the techniques reported in [7, 10] fails due to the unavailability of a tool that implements them. While tools implementing these techniques are not available [7, 10], a comparison based on what is reported in the papers suggests that our approach is competitive in both performance and precision.
Our approach can be categorized as a cutoff detection technique [1, 12, 14, 28]. Cutoffs are, however, typically determined statically, often leaving them too large for practical verification. Aiming at minimal cutoffs, our work is closer in nature to earlier dynamic strategies [18, 21], which targeted different forms of concurrent programs. The generator technique proposed in [21] is unlikely to work for P programs, due to the large local state space of machines.
8 Conclusion
We have presented a method to verify safety properties of asynchronous eventdriven programs of agents communicating via unbounded queues. Our approach is sound but incomplete: it can both prove (or, by encountering bugs, disprove) such properties but may not terminate. We empirically evaluate our method on a collection of P programs. Our experimental results showcase our method can successfully prove the correctness of programs; such proof is achieved with little extra resource costs compared to plain state exploration. Future work includes an extension to P programs with other sources of unboundedness than the queue length (e.g. messages with integer payloads).
Footnotes
 1.
The P language permits unbounded machine creation, a feature that we do not allow here and that is not used in any of the benchmarks we are aware of.
 2.
Note that the head of the queue is always preserved by Open image in new window , even for \(p=0\).
Notes
Acknowledgments
We thank Dr. Vijay D’Silva (Google, Inc.), for enlightening discussions about partial abstract transformers.
References
 1.Abdulla, A.P., Haziza, F., Holík, L.: All for the price of few (parameterized verification through view abstraction). In: VMCAI, pp. 476–495 (2013)Google Scholar
 2.Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: POPL, pp. 373–384 (2014)Google Scholar
 3.Abdulla, P.A., Atig, M.F., Cederberg, J.: Analysis of message passing programs using SMTsolvers. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 272–286. Springer, Cham (2013). https://doi.org/10.1007/9783319024448_20CrossRefzbMATHGoogle Scholar
 4.Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: a model checker for concurrent software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 484–487. Springer, Heidelberg (2004). https://doi.org/10.1007/9783540278139_42CrossRefGoogle Scholar
 5.Bakst, A., Gleissenthall, K.v., Kici, R.G., Jhala, R.: Verifying distributed programs via canonical sequentialization. PACMPL 1(OOPSLA), 110:1–110:27 (2017)Google Scholar
 6.Bouajjani, A., Emmi, M.: Bounded phase analysis of messagepassing programs. Int. J. Softw. Tools Technol. Transf. 16(2), 127–146 (2014)CrossRefGoogle Scholar
 7.Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 372–391. Springer, Cham (2018). https://doi.org/10.1007/9783319961422_23CrossRefGoogle Scholar
 8.Brand, D., Zafiropulo, P.: On communicating finitestate machines. J. ACM 30(2), 323–342 (1983)MathSciNetCrossRefGoogle Scholar
 9.Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282 (1979)Google Scholar
 10.Desai, A., Garg, P., Madhusudan, P.: Natural proofs for asynchronous programs using almostsynchronous reductions. In: OOPSLA, pp. 709–725 (2014)Google Scholar
 11.Desai, A., Gupta, V., Jackson, E., Qadeer, S., Rajamani, S., Zufferey, D.: P: safe asynchronous eventdriven programming. In: PLDI, pp. 321–332 (2013)Google Scholar
 12.Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 236–254. Springer, Heidelberg (2000). https://doi.org/10.1007/10721959_19CrossRefGoogle Scholar
 13.Emmi, M., Qadeer, S., Rakamarić, Z.: Delaybounded scheduling. In: POPL, pp. 411–422 (2011)Google Scholar
 14.Farzan, A., Kincaid, Z., Podelski, A.: Proof spaces for unbounded parallelism. In: POPL, pp. 407–420 (2015)Google Scholar
 15.Fisher, J., Henzinger, T.A., Mateescu, M., Piterman, N.: Bounded asynchrony: concurrency for modeling cellcell interactions. In: Fisher, J. (ed.) FMSB 2008. LNCS, vol. 5054, pp. 17–32. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540684138_2CrossRefGoogle Scholar
 16.Le Gall, T., Jeannet, B., Jéron, T.: Verification of communication protocols using abstract interpretation of FIFO queues. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 204–219. Springer, Heidelberg (2006). https://doi.org/10.1007/11784180_17CrossRefGoogle Scholar
 17.Godefroid, P.: Model checking for programming languages using VeriSoft. In: POPL, pp. 174–186 (1997)Google Scholar
 18.Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645–659. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642142956_55CrossRefGoogle Scholar
 19.La Torre, S., Parthasarathy, M., Parlato, G.: Analyzing recursive programs using a fixedpoint calculus. In: PLDI, pp. 211–222 (2009)Google Scholar
 20.Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. Form. Methods Syst. Des. 35(1), 73–97 (2009)CrossRefGoogle Scholar
 21.Liu, P., Wahl, T.: CUBA: interprocedural contextunbounded analysis of concurrent programs. In: PLDI, pp. 105–119 (2018)Google Scholar
 22.Liu, P., Wahl, T., Lal, A.: (2019). www.khoury.northeastern.edu/home/lpzun/quba
 23.Liu, P., Wahl, T., Lal, A.: Verifying asynchronous eventdriven programs using partial abstract transformers (extended manuscript). CoRR abs/1905.09996 (2019)Google Scholar
 24.Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI, pp. 446–455 (2007)Google Scholar
 25.PGitHub: The P programming langugage (2019). https://github.com/porg/P
 26.Qadeer, S., Rehof, J.: Contextbounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005). https://doi.org/10.1007/9783540319801_7CrossRefzbMATHGoogle Scholar
 27.Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252–266. Springer, Heidelberg (2004). https://doi.org/10.1007/9783540246220_21CrossRefzbMATHGoogle Scholar
 28.Sousa, M., Rodríguez, C., D’Silva, V., Kroening, D.: Abstract interpretation with unfoldings. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 197–216. Springer, Cham (2017). https://doi.org/10.1007/9783319633909_11CrossRefGoogle Scholar
 29.Wahl, T., Donaldson, A.: Replication and abstraction: symmetry in automated formal verification. Symmetry 2(2), 799–847 (2010)MathSciNetCrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.