In this paper, we propose a new approach for the analysis and verification of asynchronous message-passing programs with unbounded FIFO buffers, which provides a decision procedure for checking state reachability for a wide class of programs, and which is also applicable for bounded-analysis in the general case.

We first define a bounding concept for prioritizing the enumeration of program behaviors. This concept is guided by our conviction that the behaviors of well designed programs can be seen as successions of *bounded interaction phases*, each of them being a sequence of send actions (by different processes), followed by a sequence of receive actions (again by different processes) corresponding to send actions belonging to the same interaction phase. For instance, interaction phases corresponding to *rendezvous communications* are formed of a single send action followed immediately by its corresponding receive. More complex interactions are the result of exchanges of messages between processes. For instance two processes can send messages to each other, and therefore their interaction starts with two send actions (in any order), followed by the two corresponding receive actions (again in any order). This exchange schema can be generalized to any number of processes. We say that an interaction phase is k*-bounded*, for a given k > 0, if its number of send actions is less than or equal to k. For instance rendezvous interactions are precisely 1-bounded phases. In general, we call k*exchange* any k-bounded interaction phase. Given k > 0, we consider that a computation is k*-synchronous* if it is a succession of k-exchanges. It can be seen that, in k-synchronous computations the sum of the sizes of all messages buffers is bounded by k. However, as it will be explained later, boundedness of the messages buffers does not guarantee that there is a k such that all computations are k-synchronous.

Then, we introduce a new bounded analysis which for a given k, considers only computations that are *equivalent* to k-synchronous computations. The equivalence relation on computations is based on a notion of *trace* corresponding to a *happens-before* relation capturing the program order (the order of actions in the code of a process) and the precedence order between sends and their corresponding receives. Two computations are equivalent if they have the same trace, i.e., they differ only in the order of causally independent actions. We show that this analysis is PSPACE-complete when processes have a finite number of states.

An important feature of our bounding concept is that it is possible to decide its completeness for systems composed of finite-state processes, but with unbounded message buffers: For any given k, it is possible to decide whether every computation of the program (under the asynchronous semantics) is equivalent to (i.e., has the same trace as) a k-synchronous computation of that program. When this holds, we say that the program is k*-synchronizable*1. Knowing that a program is k-synchronizable allows to conclude that an invariant holds for all computations of the program if no invariant violations have been found by its k-bounded exchange analysis. Notice that k-synchronizability of a program *does not* imply that all its behaviours use bounded buffers. Consider for instance a program with two processes, a producer that consists of a loop of sends, and a consumer that consists of a loop of receives. Although there are computations where the entry buffer of the consumer is arbitrarily large, the program is 1-synchronizable because all its computations are equivalent to computations where each message sent by the producer is immediately received by the consumer.

Importantly, we show that checking k-synchronizability of a program, with possibly infinite-state processes, can be reduced in linear time to checking state reachability under the k-synchronous semantics (i.e., without considering all the program computations). Therefore, for finite-state processes, checking ksynchronizability is PSPACE and it is possible to decide invariant properties without dealing with unbounded message buffers when the programs are ksynchronizable (the overall complexity being PSPACE).

Then, a method for verifying asynchronous message passing programs can be defined, based on iterating k-bounded analyses with increasing value of k, starting from k = 1. If for some k, a violation (i.e., reachability of an error state) is detected, then the iteration stops and the conclusion is that the program is not correct. On the other hand, if for some k, the program is shown to be k-synchronizable and no violations have been found, then again the iteration terminates and the conclusion is that the program is correct.

However, it is possible that the program is *not* k-synchronizable for any k. In this case, if the program is correct then the iteration above will not terminate. Thus, an important issue is to determine whether a program is *synchronizable*, i.e., *there exists a* k *such that the program is* k*-synchronizable*. This problem is hard, and we believe that it is undecidable, but we do not have a formal proof.

We have applied our theory to a set of nontrivial examples, two of them being presented in Sect. 2. All the examples are synchronizable, which confirms our conviction that non-synchronizability should correspond to an ill-designed system (and therefore it should be reported as an anomaly).

An extended version of this paper with missing proofs can be found at [9].

1 A different notion of synchronizability has been defined in [4] (see Sect. 8).

# **2 Motivating Examples**

We provide in this section examples illustrating the relevance and the applicability of our approach. Figure 1 shows a *commit protocol* allowing a client to update a memory that is replicated in two processes, called *nodes*. The access to the nodes is controlled by a manager. Figure 2 shows an execution of this protocol. This system is 1-synchronizable, i.e., every execution is equivalent to one where only rendezvous communication is used. Intuitively, this holds because mutually interacting components are never in the situation where messages sent from one to the other are crossing messages sent in the other direction (i.e., the components are "talking" to each other at the same time). For instance, the execution in Fig. 2 is 1-synchronizable because its *conflict graph* (shown in the same figure) is acyclic. Nodes in the conflict graph are matching send-receive pairs (numbered from 1 to 6 in the figure), and edges correspond to the program order between actions in these pairs. The label of an edge records whether the actions related by program order are sends or receives, e.g., the edge from 1 to 2 labeled by RS represents the fact that the receive of the send-receive pair 1

**Fig. 1.**  Each process is defined as a labeled transition system. Transitions are labeled by send and receive actions, e.g., send(c, m, update) is a send from the client c to the manager m with payload update. Similarly, rec(c, OK) denotes process c receiving a message OK.

**Fig. 2.** An execution of the distributed commit protocol and its conflict graph.

is before the send of the send-receive pair 2, in program order. For the moment, these labels should be ignored, their relevance will be discussed in Sect. 5. The conflict graph being acyclic means that matching pairs of send-receive actions are "serializable", which implies that this execution is equivalent to one where every send is immediately followed by the matching receive (as in rendezvous communication).

Although the message buffers are bounded in all the computations of the commit protocol, this is not true for every 1-synchronizable system. There are asynchronous computations where buffers have an arbitrarily big size, which are equivalent to synchronous computations. This is illustrated by a (family of) computations shown in Fig. 4a of the system modeling an elevator described in Fig. 3 (a simplified version of the system described in [14]). This system consists of three processes: User models the user of the elevator, Elevator models the elevator's controller, and Door models the elevator's door which reacts to commands received from the controller. The execution in Fig. 4a models an interaction where the user sends an unbounded number of requests for closing the door, which generates an unbounded number of messages in the entry buffer of Elevator. These computations are 1-synchronizable since they are equivalent to a 1-synchronous computation where Elevator receives immediately every message sent by User. This is witnessed by the acyclicity of the conflict graph of this computation (shown on the right of the same figure). It can be checked that the elevator system without the dashed edge is a 1-synchronous system.

Consider now a slightly different version of the elevator system where the transition from Stopping2 to Opening2 is moved to target Opening1 instead (see the dashed transition in Fig. 3). It can be seen that this version reaches exactly the same set of configurations (tuples of process local states) as the previous one. Indeed, modifying that transition enables Elevator to send a message open to Door, but the latter can only be at StopDoor, OpenDoor, or ResetDoor at this point, and therefore it can (maybe after sending doorStopped and doorOpened) receive at state ResetDoor the message open. However, receiving this message doesn't change Door's state, and the set of reachable configurations of the system remains the same. This version of the system is not 1-synchronizable as it is shown in Fig. 4b: once the doorStopped message sent by Door is received by Elevator2, these two processes can send messages to each other at the same time (the two send actions happen before the corresponding receives). This mutual interaction consisting of 2 parallel send actions is called a 2*-exchange* and it is witnessed by the cycle of size 2 in the execution's conflict graph (shown on the right of Fig. 4b). In general, it can be shown that every execution of this version of the elevator system has a conflict graph with cycles of size at most 2, which implies that it is 2-synchronizable (by the results in Sect. 5).

2 Door sends the message from state StopDoor, and Elevator is at state Stopping2 before receiving the message.

# **3 Message Passing Systems**

We define a message passing system as the composition of a set of processes that exchange messages, which can be stored in FIFO buffers before being received (we assume one buffer per process, storing incoming messages from all the other processes). Each process is described as a state machine that evolves by executing send or receive actions. An execution of such a system can be represented abstractly using a partially-ordered set of events, called a *trace*. The partial order in a trace represents the causal relation between events. We show that these systems satisfy *causal delivery*, i.e., the order in which messages are received by a process is consistent with the causal relation between the corresponding sendings.

**Fig. 3.** A system modeling an elevator.

We fix sets P and V of process ids and message payloads, and sets S = {send(p, q, v) : p, q ∈ P, v ∈ V} and R = {rec(q, v) : q ∈ P, v ∈ V} of *send actions* and *receive actions*. Each send send(p, q, v) combines two process ids p, q denoting the sender and the receiver of the message, respectively, and a message payload v. Receive actions specify the process q receiving the message, and the message payload v. The process executing an action a ∈ S ∪ R is denoted proc(a), i.e., proc(a) = p for all a = send(p, q, v) or a = rec(p, v), and the destination q of a send s = send(p, q, v) ∈ S is denoted dest(s). The set of send, resp., receive, actions a of process p, i.e., with proc(a) = p, is denoted by S*p*, resp., R*p*.

A *message passing system* is a tuple S = ((L*p*, δ*p*, l0 *p*) | p ∈ P) where L*p* is the set of local states of process p, δ*p* ⊆ L × (S*p* ∪ R*p*) × L is a transition relation describing the evolution of process p, and l 0 *p* is the initial state of process p. Examples of message passing systems can be found in Figs. 1 and 3.

We fix a set M of message identifiers, and the sets S*id* = {s*i* : s ∈ S, i ∈ M} and R*id* = {r*i* : r ∈ R, i ∈ M} of indexed actions. Message identifiers are used to pair send and receive actions. We denote the message id of an indexed send/receive action a by msg(a). Indexed send and receive actions s ∈ S*id* and r ∈ R*id* are *matching*, written s −r, when msg(s) = msg(r).

A configuration c = *l*, *b* is a vector *l* of local states along with a vector *b* of message buffers (sequences of message payloads tagged with message identifiers). The transition relation *a* −→ (with label a ∈ S*id* ∪ R*id*) between configurations is defined as expected. Every send action enqueues the message into the destination's buffer, and every receive dequeues a message from the buffer. An execution of a system S under the asynchronous semantics is a sequence of indexed actions which corresponds to applying a sequence of transitions from the initial configuration (where processes are in their initial states and the buffers are empty). Let asEx(S) denote the set of these executions. Given an execution e, a send action s in e is called an *unmatched send* when e contains no receive action r such that s −r. An execution e is called *matched* when it contains no unmatched send.

**Traces.** Executions are represented using traces which are sets of indexed actions together with a *program order* relating every two actions of the same process and a *source* relation relating a send with the matching receive (if any).

**Fig. 4.** Executions of the elevator.

Formally, a *trace* is a tuple t = (A, po, src) where A ⊆ S*id* ∪ R*id*, po ⊆ A2 defines a total order between actions of the same process, and src ⊆ S*id* ×R*id* is a relation s.t. src(a, a ) iff a −a . The *trace* tr(e) of an execution e is (A, po, src) where A is the set of all actions in e, po(a, a ) iff proc(a) = proc(a ) and a occurs before a in e, and src(a, a ) iff a −a . Examples of traces can be found in Figs. 2 and 4. The union of po and src is acyclic. Let asTr(S) = {tr(e) : e ∈ asEx(S)} be the set of traces of S under the asynchronous semantics.

Traces abstract away the order of non-causally related actions, e.g., two sends of different processes that could be executed in any order. Two executions have the same trace when they only differ in the order between such actions. Formally, given an execution e = e1 ·a·a ·e2 with tr(e)=(A, po, src), where e1, e2 ∈ (S*id*∪ R*id*)∗ and a, a ∈ S*id*∪R*id*, we say that e = e1·a ·a·e2 is derived from e by a *valid swap* iff (a, a ) ∈ po∪src. A permutation e of an execution e is *conflict-preserving* when e can be derived from e through a sequence of valid swaps. For simplicity, whenever we use the term permutation we mean conflict-preserving permutation. For instance, a permutation of send1(p1, q, ) send2(p2, q, ) rec1(q, ) rec2(q, ) is send1(p1, q, ) rec1(q, ) send2(p2, q, ) rec2(q, ) and a permutation of the execution send1(p1, q1, ) send2(p2, q2, ) rec2(q2, ) rec1(q1, ) is send1(p1, q1, ) rec1(q1, ) send2(p2, q2, ) rec2(q2, ).

Note that the set of executions having the same trace are permutations of one another. Also, a system S cannot distinguish between permutations of executions or equivalently, executions having the same trace.

**Causal Delivery.** The asynchronous semantics ensures a property known as *causal delivery*, which intuitively, says that the order in which messages are received by a process q is consistent with the "causal" relation between them. Two messages are causally related if for instance, they were sent by the same process p or one of the messages was sent by a process p after the other one was received by the same process p. This property is ensured by the fact that the message buffers have a FIFO semantics and a sent message is instantaneously enqueued in the destination's buffer. For instance, the trace (execution) on the left of Fig. 5 satisfies causal delivery. In particular, the messages v1 and v3 are causally related, and they are received in the same order by q2. On the right of Fig. 5, we give a trace where the messages v1 and v3 are causally related, but received in a different order by q2, thus violating causal delivery. This trace is not valid because the message v1 would be enqueued in the buffer of q2 before send(p, q1, v2) is executed and thus, before send(q1, q2, v3) as well.

**Fig. 5.**

**Fig. 6.** An execution of the 1-synchronous semantics.

Formally, for a trace t = (A, po, src), the transitive closure of po∪src, denoted by *t*, is called the *causal relation* of t. For instance, for the trace t on the left of Fig. 5, we have that send(p, q2, v1) *t* send(q1, q2, v3). A trace t satisfies *causal delivery* if for every two send actions s1 and s2 in A,

$$\begin{aligned} (s\_1 \curvearrowright\_t s\_2 \land \mathsf{dest}(s\_1) = \mathsf{dest}(s\_2)) & \implies (\exists r\_2 \in A. \ s\_2 \mapsto r\_2) \lor \\ (\exists r\_1, r\_2 \in A. \ s\_1 \mapsto r\_1 \land s\_2 \mapsto r\_2 \land (r\_2, r\_1) \notin po) \end{aligned}$$

It can be easily proved that every trace t ∈ asTr(S) satisfies causal delivery.

### **4 Synchronizability**

We define a property of message passing systems called k*-synchronizability* as the equality between the set of traces generated by the asynchronous semantics and the set of traces generated by a particular semantics called k*-synchronous*.

The k-synchronous semantics uses an extended version of the standard rendez-vous primitive where more than one process is allowed to send a message and a process can send multiple messages, but all these messages must be received before being allowed to send more messages. This primitive is called k*-exchange* if the number of sent messages is at most k. For instance, the execution send1(p1, p2, ) send2(p2, p1, ) rec1(p2, ) rec2(p1, ) is an instance of a 2-exchange. To ensure that the k-synchronous semantics is prefix-closed (if it admits an execution, then it admits all its prefixes), we allow messages to be dropped during a k-exchange transition. For instance, the prefix of the previous execution without the last receive (rec2(p1, )) is also an instance of a 2-exchange. The presence of unmatched send actions must be constrained in order to ensure that the set of executions admitted by the k-synchronous semantics satisfies causal delivery. Consider for instance, the sequence of 1-exchanges in Fig. 6, a 1-exchange with one unmatched send, followed by two 1-exchanges with matching pairs of send/receives. The receive action (rec(q2, v3)) pictured as an empty box needs to be disabled in order to exclude violations of causal delivery. To this, the semantics tracks for each process p a set of processes B(p) from which it is forbidden to receive messages. For the sequence of 1-exchanges in Fig. 6, the unmatched send(p, q2, v1) disables any receive by q2 of a message sent by p (otherwise, it will be even a violation of the FIFO semantics of q2's buffer). Therefore, the first 1-exchange results in B(q2) = {p}. The second 1-exchange (the message from p to q1) forbids q2 to receive any message from q1. Otherwise, this message will be necessarily causally related to v1, and receiving it will lead to a violation of causal delivery.  The synchronous semantics. Above,  is a vector where all the components are -, and *e* −→ is the transition relation of the asynchronous semantics.

Formally, a configuration c = (*l*, B) in the synchronous semantics is a vector *l* of local states together with a function B : P → 2P. The transition relation ⇒*k* is defined in Fig. 7. A k-exchange transition corresponds to a sequence of transitions of the asynchronous semantics starting from a configuration with empty buffers. The sequence of transitions is constrained to be a sequence of at most k sends followed by a sequence of receives. The receives are enabled depending on previous unmatched sends as explained above, using the function B. The semantics defined by ⇒*k* is called the k-synchronous semantics.

Executions and traces are defined as in the case of the asynchronous semantics, using ⇒*k* for some fixed k instead of →. The set of executions, resp., traces, of S under the k-synchronous semantics is denoted by sEx*k*(S), resp., sTr*k*(S). The executions in sEx*k*(S) and the traces in sTr*k*(S) are called k-synchronous.

An execution e such that tr(e) is k-synchronous is called k-synchronizable. We omit k when it is not important. The set of executions generated by a system S under the k-synchronous semantics is prefix-closed. Therefore, the set of its k-synchronizable executions is prefix-closed as well. Also, k-synchronizable and k-synchronous executions are undistinguishable up to permutations.

**Definition 1.** *A message passing system* S *is called* k-synchronizable *when* asTr(S) = sTr*k*(S)*.*

It can be easily proved that k-synchronizable systems reach exactly the same set of local state vectors under the asynchronous and the k-synchronous semantics. Therefore, any assertion checking or invariant checking problem for a k-synchronizable system S can be solved by considering the k-synchronous semantics instead of the asynchronous one. This holds even for the problem of detecting deadlocks. Therefore, all these problems become decidable for finitestate k-synchronizable systems, whereas they are undecidable in the general case (because of the FIFO message buffers).

### **5 Characterizing Synchronous Traces**

**Fig. 8.** A trace and its conflict graph.

We give a characterization of the traces generated by the k-synchronous semantics that uses a notion of *conflictgraph* similar to the one used in conflict serializability [27]. The nodes of the conflict graph correspond to pairs of matching actions (a send and a receive) or to unmatched sends, and the edges represent the program order relation between the actions represented by these nodes.

For instance, an execution with an acyclic conflict graph, e.g., the execution in Fig. 2, is "equivalent" to an execution where every receive immediately follows the matching send. Therefore, it is an execution of the 1 synchronous semantics. For arbitrary values of k, the conflict graph may contain cycles, but of a particular form. For instance, traces of the 2-synchronous semantics may

contain a cycle of size 2 like the one in Fig. 4(b). More generally, we show that the conflict graph of a k-synchronous trace cannot contain cycles of size strictly bigger than k. However, this class of cycles is not sufficient to precisely characterize the k-synchronous traces. Consider for instance the trace on top of Fig. 8. Its conflict-graph contains a cycle of size 4 (shown on the bottom), but the trace is not 4-synchronous. The reason is that the messages tagged by 1 and 4 must be sent during the same exchange transition, but receiving message 4 needs that the message 3 is sent after 2 is received. Therefore, it is not possible to schedule all the send actions before all the receives. Such scenarios correspond to cycles in the conflict graph where at least one receive is before a send in the program order (witnessed by the edge labeled by RS). We show that excluding such cycles, in addition to cycles of size strictly bigger than k, is a precise characterization of k-synchronous traces.

The *conflict-graph* of a trace t = (A, po, src) is the labeled directed graph CG*t* = V,E, *E* where: (1) the set of nodes V includes one node for each pair of matching send and receive actions, and each unmatched send action in t, and (2) the set of edges E is defined by: (v, v ) ∈ E iff there exist actions a ∈ act(v) and a ∈ act(v ) such that (a, a ) ∈ po (where act(v) is the set of actions of trace t corresponding to the graph node v). The label of the edge (v, v ) records whether a and a are send or receive actions, i.e., for all X, Y ∈ {S, R}, XY ∈ (v, v ) iff a ∈ X*id* and a ∈ Y*id*.

A direct consequence of previous results on conflict serializability [27] is that a trace is 1-synchronous whenever its conflict-graph is acyclic. A cycle of a conflict graph CG*t* is called *bad* when it contains an edge labeled by RS. Otherwise, it is called *good*. The following result is a characterization of k-synchronous traces.

**Theorem 1.** *A trace* t *satisfying causal delivery is* k*-synchronous iff every cycle in its conflict-graph is good and of size at most* k*.*

Theorem 1 can be used to define a runtime monitoring algorithm for ksynchronizability checking. The monitor records the conflict-graph of the trace produced by the system and checks whether it contains some bad cycle, or a cycle of size bigger than k. While this approach requires dealing with unbounded message buffers, the next section shows that this is not necessary. Synchronizability violations, if any, can be exposed by executing the system under the *synchronous* semantics.

# **6 Checking Synchronizability**

We show that checking k-synchronizability can be reduced to a reachability problem under the k*-synchronous* semantics (where message buffers are bounded). This reduction holds for arbitrary, possibly infinite-state, systems. More precisely, since the set of (asynchronous) executions of a system is prefix-closed, if a system S admits a synchronizability violation, then it also admits a *borderline* violation, for which every strict prefix is synchronizable. We show that every *borderline* violation can be "simulated"3 by the synchronous semantics of an instrumentation of S where the receipt of exactly one message is delayed (during every execution). We describe a monitor that observes executions of the instrumentation (under the synchronous semantics) and identifies synchronizability violations (there exists a run of this monitor that goes to an error state whenever such a violation exists).

### **6.1 Borderline Synchronizability Violations**

For a system S, a violation e to k-synchronizability is called *borderline* when every strict prefix of e is k-synchronizable. Figure 9(a) gives an example of a borderline violation to 1-synchronizability (it is the same execution as in Fig. 4(b)).

We show that every borderline violation e ends with a receive action and this action is included in every cycle of CG*tr*(*e*) that is bad or exceeds the bound k. Given a cycle c = v, v1,...,v*n*, v of a conflict graph CG*t*, the node v is called a *critical* node of c when (v, v1) is an SX edge with X ∈ {S, R} and (v*n*, v) is an Y R edge with Y ∈ {S, R}.

**Lemma 1.** *Let* e *be a borderline violation to* k*-synchronizability of a system* S*. Then,* e = e · r *for some* e ∈ (S*id* ∪ R*id*)∗ *and* r ∈ R*id. Moreover, the node* v *of* CG*tr*(*e*) *representing* r *(and the corresponding send) is a critical node of every cycle of* CG*tr*(*e*) *which is bad or of size bigger than* k*.*

### **6.2 Simulating Borderline Violations on the Synchronous Semantics**

Let S be a system obtained from S by "delaying" the reception of exactly one nondeterministically chosen message: S contains an additional process π and exactly one message sent by a process in S is non-deterministically redirected

3 We refer to the standard notion of (stuttering) simulation where one system mimics the transitions of the other system.

**Fig. 9.** A borderline violation to 1-synchronizability.

to π4, which sends it to the original destination at a later time5. We show that the synchronous semantics of S "simulates" a permutation of every borderline violation of S. Figure 9(b) shows the synchronous execution of S that corresponds to the borderline violation in Fig. 9(a). It is essentially the same except for delaying the reception of doorOpened by sending it to π who relays it to the elevator at a later time.

The following result shows that the k-synchronous semantics of S "simulates" all the borderline violations of S, modulo permutations.

**Lemma 2.** *Let* e = e1 · send*i*(p, q, v) · e2 · rec*i*(q, v) *be a borderline violation to* k*-synchronizability of* S*. Then,* sEx*k*(S ) *contains an execution* e *of the form:*

$$e' = e'\_1 \cdot \text{send}\_i(p, \pi, (q, v)) \cdot \text{rec}\_i(\pi, (q, v)) \cdot e'\_2 \cdot \text{send}\_j(\pi, q, v) \cdot \text{rec}\_j(q, v)$$

*such that* e 1 · send*i*(p, q, v) · e 2 *is a permutation of* e1 · send*i*(p, q, v) · e2*.*

Checking k-synchronizability for S on the system S would require that every (synchronous) execution of S can be transformed to an execution of S by applying an homomorphism σ where the send/receive pair with destination π is replaced with the original send action and the send/receive pair initiated by π is replaced with the original receive action (all the other actions are left unchanged). However, this is not true in general. For instance, S may admit an execution send*i*(p, π,(q, v))·rec*i*(π,(q, v))·send*j* (p, q, v )·rec*j* (q, v )·send*i*- (π, q, v)· rec*i*- (q, v) where a message sent after the one redirected to π is received earlier, and the two messages were sent by the same process p. This execution is possible under the 1-synchronous semantics of S . Applying the homomorphism σ, we get the execution send*i*(p, q, v) · send*j* (p, q, v ) · rec*j* (q, v ) · rec*i*(q, v) which violates causal delivery and therefore, it is not admitted by the asynchronous semantics

4 Meaning that every transition labeled by a send action send(p, q, v) is doubled by a transition labeled by send(p, π, (q, v)), and such a send to π is enabled only once throughout the entire execution.

5 The process π stores the message (q, v) it receives in its state and has one transition where it can send v to the original destination q.

of S. Our solution to this problem is to define a monitor M*causal* , i.e., a process which reads every transition label in the execution and advances its local state, which excludes such executions of S when run under the synchronous semantics, i.e., it blocks the system S whenever applying some transition would lead to an execution which, modulo the homomorphism σ, is a violation of causal delivery. This monitor is based on the same principles that we used to exclude violations of causal delivery in the synchronous semantics in the presence of unmatched sends (the component B from a synchronous configuration).

### **6.3 Detecting Synchronizability Violations**

We complete the reduction of checking k-synchronizability to a reachability problem under the k-synchronous semantics by describing a monitor M*viol*(k), which observes executions in the k-synchronous semantics of S ||M*causal* and checks whether they represent violations to k-synchronizability; M*viol*(k) goes to an error state whenever such a violation exists.

Essentially, M*viol*(k) observes the sequence of k-exchanges in an execution and tracks a conflict graph cycle, if any, interpreting send*i*(p, π,(q, v)) · rec*i*(π,(q, v)) as in the original system S, i.e., as send*i*(p, q, v), and send*i*(π, q, v)· rec*i*(q, v) as rec*i*(q, v). By Lemma 2, every cycle that is a witness for *non* ksynchronizability includes the node representing the pair send*i*(p, q, v), rec*i*(q, v). Moreover, the successor of this node in the cycle represents an action that is executed by p and the predecessor an action executed by q. Therefore, the monitor searches for a conflict-graph path from a node representing an action of p to a node representing an action of q. Whenever it finds such a path it goes to an error state.

Figure 10 lists the definition of M*viol*(k) as an abstract state machine. By the construction of S , we assume w.l.o.g., that both the send to π and the send from π are executed in isolation as an instance of 1-exchange. When observing the send to π, the monitor updates the variable conflict, which in general stores the process executing the last action in the cycle, to p. Also, a variable count, which becomes 0 when the cycle has strictly more than k nodes, is initialized to k. Then, for every k-exchange transition in the execution, M*viol*(k) non-deterministically picks pairs of matching send/receive or unmatched sends to continue the conflict-graph path, knowing that the last node represents an action of the process stored in conflict. The rules for choosing pairs of matching send/receive to advance the conflict-graph path are pictured on the right of Fig. 10 (advancing the conflict-graph path with an unmatched send doesn't modify the value of conflict, it just decrements the value of count). There are two cases depending on whether the last node in the path conflicts with the send or the receive of the considered pair. One of the two processes involved in this pair of send/receive equals the current value of conflict. Therefore, conflict can either remain unchanged or change to the value of the other process. The variable lastIsRec records whether the current conflict-graph path ends in a conflict due to a receive action. If it is the case, and the next conflict is between

**Fig. 10.** The monitor M*viol* (k). B is the set of Booleans and N is the set of natural numbers. Initially, conflict is ⊥, while lastIsRec and sawRS are false.

this receive and a send, then sawRS is set to true to record the fact that the path contains an RS labeled edge (leading to a potential bad cycle).

When π sends its message to q, the monitor checks whether the conflict-graph path it discovered ends in a node representing an action of q. If this is the case, this path together with the node representing the delayed send forms a cycle. Then, if sawRS is true, then the cycle is bad and if count reached the value 0, then the cycle contains more than k nodes. In both cases, the current execution is a violation to k-synchronizability.

The set of executions in the k-synchronous semantics of S composed with M*causal* and M*viol*(k), in which the latter goes to an error state, is denoted by S *k* ||M*causal* || ¬M*viol*(k).

**Theorem 2.** *For a given* k*, a system* S *is* k*-synchronizable iff the set of executions* S *k* ||M*causal* || ¬M*viol*(k) *is empty.*

Given a system S, an integer k, and a local state l, *the reachability problem under the* k*-synchronous semantics* asks whether there exists a k-synchronous execution of S reaching a configuration (*l*, B) with l = *lp* for some p ∈ P. Theorem 2 shows that checking k-synchronizability can be reduced to a reachability problem under the k-synchronous semantics. This reduction holds for arbitrary (infinite-state) systems, which implies that k-synchronizability can be checked using the existing assertion checking technology. Moreover, for finite-state systems, where each process has a finite number of local states (message buffers can still be unbounded), it implies that checking this property is PSPACE-complete. **Theorem 3.** *For a finite-state system* S*, the reachability problem under the* k*synchronous semantics and the problem of checking* k*-synchronizability of* S *are decidable and PSPACE-complete.*

# **7 Experimental Evaluation**

**Fig. 11.** Experimental results.

As a proof of concept, we have applied our procedure for checking k-synchronizability to a set of examples extracted from the distribution of the P language6. Two-phase commit and Elevator are presented in Sect. 2, German is a model of the cachecoherence protocol with the same name, OSR is a model of a device driver, and

Replication Storage is a model of a protocol ensuring eventual consistency of a replicated register. These examples cover common message communication patterns that occur in different domains: distributed systems (Two-phase commit, Replication storage), device drivers (Elevator, OSR), cache-coherence protocols (German). We have rewritten these examples in the Promela language and used the Spin model checker7 for discharging the reachability queries. For a given program, its k-synchronous semantics and the monitors defined in Sect. 6 are implemented as ghost code. Finding a conflict-graph cycle which witnesses non k-synchronizability corresponds to violating an assertion.

The experimental data is listed in Fig. 11: Proc, resp., Loc, is the number of processes, resp., the number of lines of code (loc) of the original program, k is the *minimal* integer for which the program is k-synchronizable, and Time gives the number of minutes needed for this check. The ghost code required to check k-synchronizability takes 250 lines of code in average.

# **8 Related Work**

Automatic verification of asynchronous message passing systems is undecidable in general [10]. A number of decidable subclasses has been proposed. The class of systems, called *synchronizable* as well, in [4], requires that a system generates the same sequence of send actions when executed under the asynchronous semantics as when executed under a synchronous semantics based on rendezvous communication. These systems are all 1-synchronizable, but the inclusion is strict (the 1-synchronous semantics allows unmatched sends). The techniques proposed in [4] to check that a system is synchronizable according to their definition cannot be extended to k-synchronizable systems. Other classes of systems that are 1-synchronizable have been proposed in the context of session types,

6 Available at https://github.com/p-org.

7 Available at http://spinroot.com.

e.g., [12,20,21,26]. A sound but incomplete proof method for distributed algorithms that is based on a similar idea of avoiding reasoning about all program computations is introduced in [3]. Our class of synchronizable systems differs also from classes of communicating systems that restrict the type of communication, e.g., lossy-communication [2], half-duplex communication [11], or the topology of the interaction, e.g., tree-based communication in concurrent pushdowns [19,23].

The question of deciding if all computations of a communicating system are equivalent (in the language theoretic sense) to computations with bounded buffers has been studied in, e.g., [17], where this problem is proved to be undecidable. The link between that problem and our synchronizability problem is not (yet) clear, mainly because non synchronizable computations may use bounded buffers.

Our work proposes a solution to the question of defining adequate (in terms of coverage and complexity) parametrized bounded analyses for message passing programs, providing the analogous of concepts such as context-bounding or delay-bounding defined for shared-memory concurrent programs. Bounded analyses for concurrent systems was initiated by the work on bounded-context switch analysis [25,28,29]. For shared-memory programs, this work has been extended to unbounded threads or larger classes of behaviors, e.g., [8,15,22,24]. Few bounded analyses incomparable to ours have been proposed for message passing systems, e.g., [6,23]. Contrary to our work, these works on bounded analyses in general do not propose decision procedures for checking if the analysis is complete (covers all reachable states). The only exception is [24], which concerns shared-memory.

Partial-order reduction techniques, e.g., [1,16], allow to define equivalence classes on behaviors, based on notions of action independence and explore (ideally) only one representative of each class. This has lead to efficient algorithmic techniques for enhanced model-checking of concurrent shared-memory programs that consider only a subset of relevant action interleavings. In the worst case, these techniques will still need to explore all of the interleavings. Moreover, these techniques are not guaranteed to terminate when the buffers are unbounded.

The work in [13] defines a particular class of schedulers, that roughly, prioritize receive actions over send actions, which is complete in the sense that it allows to construct the whole set of reachable states. Defining an analysis based on this class of schedulers has the same drawback as partial-order reductions, in the worst case, it needs to explore all interleavings, and termination is not guaranteed.

The approach in this work is related to robustness checking [5,7]. The general paradigm is to decide that a program has the same behaviors under two semantics, one being weaker than the other, by showing a polynomial reduction to a state reachability problem under the stronger semantics. For instance, in our case, the class of message passing programs with unbounded FIFO channels is Turing powerful, but still, surprisingly, k-synchronizability of these programs is decidable and PSPACE-complete. The results in [5,7] cannot be applied in our context: the class of programs and their semantics are different, and the corresponding robustness checking algorithms are based on distinct concepts and techniques.

# **References**

**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.

# **Constrained Dynamic Partial Order Reduction**

Elvira Albert1 , Miguel G´omez-Zamalloa1(B) , Miguel Isabel1 , and Albert Rubio2

> 1 Complutense University of Madrid, Madrid, Spain<EMAIL_ADDRESS>2 Universitat Polit`ecnica de Catalunya, Barcelona, Spain

**Abstract.** The cornerstone of dynamic partial order reduction (DPOR) is the notion of *independence* that is used to decide whether each pair of concurrent events *p* and *t* are in a race and thus both *p* · *t* and *t* · *p* must be explored. We present *constrained* dynamic partial order reduction (CDPOR), an extension of the DPOR framework which is able to avoid redundant explorations based on the notion of *conditional independence*—the execution of *p* and *t* commutes only when certain *independence constraint*s (ICs) are satisfied. ICs can be declared by the programmer, but importantly, we present a novel SMT-based approach to automatically synthesize ICs in a static pre-analysis. A unique feature of our approach is that we have succeeded to exploit ICs within the state-of-the-art DPOR algorithm, achieving *exponential* reductions over existing implementations.

# **1 Introduction**

Partial Order Reduction (POR) is based on the idea that two interleavings can be considered equivalent if one can be obtained from the other by swapping adjacent, non-conflicting *independent* execution steps. Such equivalence class is called a Mazurkiewicz trace, and POR guarantees that it is sufficient to explore one interleaving per equivalence class. Early POR algorithms [8,10,20] relied on static over-approximations to detect possible *future* conflicts. The Dynamic-POR (DPOR) algorithm, introduced by Godefroid [9] in 2005, was a breakthrough in the area because it does not need to look at the future. It keeps track of the independence races witnessed along its execution and uses them to decide the required exploration dynamically, without the need of static approximation. DPOR is nowadays considered one of the most scalable techniques for

This work was funded partially by the Spanish MECD Salvador de Madariaga Mobility Grants PRX17/00297 and PRX17/00303, the Spanish MINECO projects TIN2015-69175-C4-2-R and TIN2015-69175-C4-3-R, and by the CM project S2013/ICE-3006.

c The Author(s) 2018

H. Chockler and G. Weissenbacher (Eds.): CAV 2018, LNCS 10982, pp. 392–410, 2018. https://doi.org/10.1007/978-3-319-96142-2\_24

software verification. The key of DPOR algorithms is in the dynamic construction of two types of sets at each scheduling point: the *sleep set* that contains processes whose exploration has been proved to be redundant (and hence should not be selected), and the *backtrack set* that contains the processes that have not been proved independent with previously explored steps (and hence need to be explored). Source-DPOR (SDPOR) [1,2] improves the precision to compute backtrack sets (named *source* sets), proving optimality of the resulting algorithm for *any* number of processes w.r.t. an *unconditional independence* relation.

*Challenge.* When considering (S)DPOR with unconditional independence, if a pair of events is not independent in all possible executions, they are treated as potentially dependent and their interleavings explored. Unnecessary exploration can be avoided using conditional independence. E.g., two processes executing respectively the atomic instructions if(z ≥ 0) z = x; and x = x + 1; would be considered dependent even if z ≤ −1—this is indeed an *independence constraint* (IC) for these two instructions. Conditional independence was early introduced in the context of POR [11,15]. The first algorithm that has used notions of conditional independence within the state-of-the-art DPOR algorithm is Context-Sensitive DPOR (CSDPOR) [3]. However, CSDPOR does not use ICs (it rather checks state equivalence dynamically during the exploration) and exploits conditional (context-sensitive) independence only *partially* to extend the sleep sets. Our challenge is twofold: (i) extend the DPOR framework to exploit ICs during the exploration in order to both reduce the backtrack sets and expand the sleep sets as much as possible, (ii) statically synthesize ICs in an automatic pre-analysis.

*Contributions.* The main contributions of this work can be summarized as:

### **2 Background**

In this section we introduce some notations, the basic notions on the POR theory and the state-of-the-art DPOR algorithm that we will extend in Sect. 3.

Our work is formalized for a general model of concurrent systems, in which a program is composed of *atomic blocks* of code. An atomic block can contain just one (global) statement that affects the global state, a sequence of local statements (that only read and write the local state of the process) followed by a global statement, or a block of code with possibly several global statements but whose execution cannot interleave with other processes because it has been implemented as atomic (e.g., using locks, semaphores, etc.). Each atomic block in the program is given a unique block identifier. We use *spawn*(*P*[*ini*]) to create a new process. Depending on the programming language, P can be the name of a method and [ini] initial values for the parameters, or P can be the identifier of the initial block to execute and [ini] the initialization instructions, etc., in every case with mechanisms to continue the execution from one block to the following one. Notice that the use of atomic blocks in our formalization generalizes the particular case of considering atomicity at the level of single instructions.

As previous work on DPOR [1–3], we assume the state space does not contain cycles, executions have finite unbounded length and processes are deterministic (i.e., at a given time there is at most one event a process can execute). Let Σ be the set of states of the system. There is a unique initial state s0 ∈ Σ. The execution of a process p is represented as a partial function executep : Σ → Σ that moves the system from one state to a subsequent state. Each application of the function executep represents the execution of an *atomic block* of the code that p is running, denoted as *event* (or execution step) of process p. An *execution sequence* E (also called *derivation*) of a system is a finite sequence of events of its processes starting from s0, and it is uniquely characterized by the sequence of processes that perform steps of E. For instance, p · q · q denotes the execution sequence that first performs one step in p, followed by two steps in q. We use to denote the empty sequence. The state of the system after E is denoted by s[E]. The set of processes enabled in state s (i.e., that can perform an execution step from s) is denoted by *enabled*(*s*).

### **2.1 Basics of Partial Order Reduction**

An *event* e of the form (p, i) denotes the i-th occurrence of process p in an execution sequence, and ˆe denotes the process p of event e, which is extended to sequences of events in the natural way. We write ¯e to refer to the identifier of the atomic block of code the event e is executing. The set of events in execution sequence E is denoted by dom(E). We use e <E e to denote that event e occurs before event e in E, s.t. <E establishes a total order between events in E, and E ≤ E to denote that sequence E is a prefix of sequence E . Let dom[E](w) denote the set of events in execution sequence E.w that are in sequence w, i.e., dom(E.w)\dom(E). If w is a single process p, we use next[E](p) to denote the single event in dom[E](p). If P is a set of processes, next[E](P) denotes the set of next[E](p) for all p ∈ P. The core concept in POR is that of the *happens-before* partial order among the events in execution sequence E, denoted by →E. This relation defines a subset of the <E total order, such that any two sequences with the same happens-before order are equivalent. Any linearization E of →E on dom(E) is an execution sequence with exactly the same happens-before relation →E as →E. Thus, →E induces a set of equivalent execution sequences, all with the same happens-before relation. We use E E to denote that E and E are linearizations of the same happens-before relation. The happens-before partial order has traditionally been defined in terms of a *dependency* relation between

### **Algorithm 1.** (Source+Context-sensitive)+Constrained DPOR algorithm

```
1: procedure explore(E)
2: if (∃p ∈ (enabled(s[E])\sleep(E))) then
3: back(E) := {p};
4: while (∃p ∈ (back(E)\sleep(E))) do
5: let n = next[E](p);
6: for all (e ∈ dom(E) such that e -
                                      E.p n) do
7: let E-
                = pre(E,e);
8: let u = dep(E, e, n);
9: if (¬(U⇒(Ie, ¯ n¯ , e, n, s[E-
                              .uˆ])) then
10: updateBack(E,E-

                            , e, p);
11: if C(s[E-
                    .uˆ]) for some C ∈ Ie, ¯ n¯ then
12: add ˆu.p.eˆ to sleep(E-

                                );
13: else
14: updateSleepCS(E,E-

                                , e, p);
15: sleep(E.p) := {x | x ∈ sleep(E), E |= p  x}
16: ∪ {x | p.x ∈ sleep(E)}
17: ∪ {x | x ∈ sleep(E), |x| = 1, m = next[E](x), U⇒(In, ¯ m¯ , n, m, s[E]
                                                                    ))};
18: explore(E.p);
19: sleep(E) := sleep(E) ∪ {p};
```
the execution steps associated to those events [10]. Intuitively, two steps p and q are *dependent* if there is at least one execution sequence E for which they do not commute, either because (i) one *enable*s the other (i.e., the execution of p leads to introducing q, or viceversa), or because (ii) s[E.p.q] = s[E.q.p]. We define dep(E, e, n) as the subsequence containing all events e in E that occur after e and happen-before n in E.p (i.e., e<Ee and e →E.pn). The unconditional dependency relation is used for defining the concept of a *race* between two events. Event e is said to be in race with event e in execution E, if the events belong to different processes, e happens-before e in E (e →E e ), and the two events are "concurrent", i.e. there exists an equivalent execution sequence E E where the two events are adjacent. We write e -E e to denote that e is in race with e and that the race can be reversed (i.e., the events can be executed in reverse order). POR algorithms use this relation to reduce the number of equivalent execution sequences explored, with SDPOR ensuring that only one execution sequence in each equivalence class is explored.

#### **2.2 State-of-the-Art DPOR with Unconditional Independence**

Algorithm 1 shows the state-of-the-art DPOR algorithm –based on the SDPOR algorithm of [1,2],1 which in turn is based on the original DPOR algorithm of [9]. We refer to this algorithm as DPOR in what follows. The context-sensitive extension of CSDPOR [3] (lines 14 and 16) and our extension highlighted in blue

1 The extension to support *wake-up trees* [2] is deliberately not included to simplify the presentation.

(lines 8–10, 11–13 and 17) should be ignored by now and will be described in Sect. 3.

The algorithm carries out a depth-first exploration of the execution tree using POR receiving as parameter a derivation E (initially empty). Essentially, it dynamically finds reversible races and is able to backtrack at the appropriate scheduling points to reverse them. For this purpose, it keeps two sets at every prefix E of E: back(E ) with the set of processes that must be explored from E , and, sleep(E ) with the set of sequences of processes that previous executions have determined do not need to be explored from E . Note that in the original DPOR the sleep set contained only single processes, but in later improvements sequences of processes are added, so our description considers this general case. The algorithm starts by selecting any process p that is enabled by the state reached after executing E and is not already in sleep(E). If it does not find any such process p, it stops. Otherwise, after setting back(E) = {p} to start the search, it explores every element in back(E) that is not in sleep(E). The backtrack set of E might grow as the loop progresses (due to later executions of line 10). For each such p, DPOR performs two phases: race detection (lines 6, 7 and 10) and state exploration (lines 15, 18 and 19). The race detection starts by finding all events e in dom(E) such that e -E.p n, where n is the event being selected (see line 5). For each such e, it sets E to pre(E,e), i.e., to be the prefix of E up to, but not including e. Procedure updateBack modifies back(E ) in order to ensure that the race between e and n is reversed. The source-set extension of [1,2] detects cases where there is no need to modify back(E ) –this is done within procedure updateBack whose code is not shown because it is not affected by our extension. After this, the algorithm continues with the state exploration phase for E.p, by retaining in its sleep set any element x in sleep(E) whose events in E.p are independent of the next event of p in E (denoted as E |= p x), i.e., any x such that next[E](p) would not happen-before any event in dom(E.p.x)\dom(E.p). Then, the algorithm explores E.p, and finally it adds p to sleep(E) to ensure that, when backtracking on E, p is not selected until a dependent event with it is selected. All versions of the DPOR algorithm (except [3]) rely on the unconditional (or context-insensitive) dependency relation. This relation has to be over-approximated, usually by requiring that global variables accessed by one execution step are not modified by the other.

*Example 1.* Consider the example in Fig. 1 with 3 processes p, q, r containing a single atomic block. Since all processes have a single event, by abuse of notation, we refer to events by their process name throughout all examples in the paper. Relying on the usual over-approximation of dependency all three pairs of events are dependent. Therefore, starting with one instance per process, the algorithm has to explore 6 execution sequences, each with a different happens-before relation. The tree, including the dotted and dashed fragments, shows the exploration from the initial state z = −2, x = −2. The value of variable z is shown in brackets at each state. Essentially, in all states of the form E.e, the algorithm always finds a reversible race between the next event of the current selected process (p, q or r) and e, and adds it to back(E). Also, when backtracking on E, none of the elements in sleep(E) is propagated down, since all events are considered dependent. In the best case, considering an exact (yet unconditional) dependency relation which realizes that events p and r are independent, the algorithm will make the following reductions. In state 6, p and r will not be in race and hence p will not be added to back(q). This avoids exploring the sequence p.r from 5. When backtracking on state 0 with r, where sleep() = {p, q}, p will be propagated down to sleep(r) since |= r p, hence avoiding the exploration of p.q from 8. Thus, the algorithm will explore 4 sequences.

**Fig. 1.** Left: code of working example (up) and ICs (down). Right: execution tree starting from *z* = −2*, x* = −2. Full tree computed by SDPOR, dotted fragment not computed by CSDPOR, and, dashed+dotted fragment not computed by CDPOR.

# **3 DPOR with Conditional Independence**

Our aim in CDPOR is twofold: (1) provide techniques to both infer and soundly check conditional independence, and (2) be able to exploit them at *all* points of the DPOR algorithm where dependencies are used. Section 3.1 reviews the notions of conditional independence and ICs, and introduces a first type of check where ICs can be directly used in the DPOR algorithm. Section 3.2 illustrates why ICs cannot be used at the remaining independence check points in the algorithm, and introduces sufficient conditions to soundly exploit them at those points. Finally, Sect. 3.3 presents the CDPOR algorithm that includes all types of checks.

### **3.1 Using Precomputed ICs Directly Within DPOR**

Conditional independence consists in checking independence at the given state.

**Definition 1 (conditional independence).** *Two events* α *and* β *are* independent *in state* S*, written* indep(α, β, S) *if (i1) none of them* enables *the other from* S*; and, (i2) if they are both enabled in* S*, then* S α·β −→ S *and* S β·α −→ S *.*

The use of conditional independence in the POR theory was firstly studied in [15], and it has been partially applied within the DPOR algorithm in CSDPOR [3]. Function *updateSleepCS* at line 14 and the modification of *sleep* at 16 encapsulate this partial application of CSDPOR (the code of *updateSleepCS* is not shown because it is not affected by our extension). Intuitively, *updateSleepCS* works as follows: when a reversible race is found in the current sequence being explored, it builds an *alternative* sequence which corresponds to the reverse race, and then checks whether the states reached after running the two sequences are the same. If they are, it adds the alternative sequence to the corresponding *sleep* set so that this sequence is not fully explored when backtracking. Therefore, sleep sets can contain *sequences* of events which can be propagated down via the rule of line 16 (i.e., if the event being explored is the head of a sequence in the sleep set, then the tail of the sequence is propagated down). In essence, the technique to check (i2) in Definition 1 in CSDPOR consists in checking state equivalence with an alternative sequence in the current state (hence it is conditional) and, if the check succeeds, it is exploited in the *sleep* set only (and not in the *backtrack* set).

*Example 2.* Let us explain the intuition behind the reductions that CSDPOR is able to achieve w.r.t. unconditional independence-based DPOR on the example. In state 1, when the algorithm selects q and detects the reversible race between q and p, it computes the alternative sequence q.p and realizes that s[p.q] = s[q.p], and hence adds p.q to sleep(). Similarly, in state 2, it computes p.r.q and realizes that s[p.q.r] = s[p.r.q] adding r.q to sleep(p). Besides these two alternative sequences, it computes two more. Overall, CSDPOR explores 2 complete sequences (p.q.r and q.r.p) and 13 states (the 9 states shown, plus 4 additional states to compute the alternative sequences).

Instead of computing state equivalence to check (i2) as in [3], our approach assumes precomputed *independence constraints* (ICs) for all pairs of atomic blocks in the program. ICs will be evaluated at the appropriate state to determine the independence between pairs of concurrent events executing such atomic blocks.

**Definition 2 (ICs).** *Consider two events* α *and* β *that execute, respectively, the atomic blocks* α¯ *and* β¯*. The* independence constraints Iα, ¯ β¯ *are a set of boolean expressions (constraints) on the variables accessed by* α *and* β *(including local and global variables) s.t., if some constraint* C *in* Iα, ¯ β¯ *holds in state* S*, written* C(S)*, then condition (i2) of* indep(α, β, S) *holds.*

Our first contribution is in lines 11–13 where ICs are used within DPOR as follows. Before executing *updateSleepCS* at line 14, we check if some constraint in Ie, ¯ n¯ holds in the state s[E-.uˆ], by building the sequence E .uˆ, where u = dep(E, e, n). Only if our check fails we proceed to execute *updateSleepCS*. The advantages of our check w.r.t. *updateSleepCS* are: (1) the alternative execution sequence built by *updateSleepCS* is strictly longer than ours and hence more states will be explored, and (2) *updateSleepCS* must check state equivalence while we evaluate boolean expressions. Yet, because our IC is an approximation, if we fail to prove independence we can still use *updateSleepCS*.

*Example 3.* Consider the ICs in Fig. 1 (down left), which provide the constraints ensuring the independence of each pair of atomic blocks, and whose synthesis is explained in Sect. 4.1. In the exploration of the example, when the algorithm detects the reversible race between q and p in state 1, instead of computing q.p and then comparing s[p.q] = s[q.p] as in CSDPOR, we would just check the constraint in Ip, ¯ q¯ at state , i.e., in z = −2 (line 11), and since it succeeds, q.p is added to sleep(). The same happens at states 2, again at 1 (when backtracking with r), and 5. This way we avoid the exploration of the additional 4 states due to the computation of the alternative sequences in Example 2 (namely q.p, r.p and r.q from state 0, and r.q from 1). The algorithm is however still exploring many redundant derivations, namely states 4, 5, 6, 7 and 8.

### **3.2 Transitive Uniformity: How to Further Exploit ICs Within DPOR**

The challenge now is to use ICs, and therefore conditional independence, at the remaining dependency checks performed by the DPOR algorithm, and most importantly, for the race detection (line 6). In the example, that would avoid the addition of q and r to back() and r to back(p), and hence would make the algorithm only explore the sequence p.q.r. Although that can be done in our example, it is unsound in general as the following counter-example illustrates.

*Example 4.* Consider the same example but starting from the initial state z = −1, x = −2. During the exploration of the first sequence p.q.r, the algorithm will not find any race since p and q are independent in z = −1, q and r are independent in z = x = −1, and, p and r are always independent. Therefore, no more sequences than p.q.r with final result z = 0 will be explored. There is however a non-equivalent sequence, r.q.p, which leads to a different final state z = −1.

The problem of using conditional independence within the POR theory was already identified by Katz and Peled [15]. Essentially, the main idea of POR is that the different linearizations of a partial order yield equivalent executions that can be obtained by swapping adjacent independent events. However, this is no longer true with conditional dependency. In Example 4, using conditional independence, the partial order of the explored derivation p.q.r would be empty, which means there would be 6 possible linearizations. However r.q.p is not equivalent to p.q.r since q and p are dependent in s[r], i.e., when z = 0. An extra condition, called *uniformity*, is proposed in [15] to allow using conditional independence within the POR theory. Intuitively, *uniform independence* adds a condition to Definition 1 to ensure that independence holds at all successor states for those events that are enabled and are *uniformly independent* with the two events whose independence is being proved. While this notion can be checked *a posteriori* in a given exploration, it is unclear how it could be applied in a dynamic setting where decisions are made *a priori*. Here we propose a weaker notion of uniformity, called *transitive uniformity*, for which we have been able to prove that the *dynamic*-POR framework is sound. The difference with [15] is that our extra condition ensures that independence holds at all successor states for *all* events that are enabled, which is thus a superset of the events considered in [15]. We notice that the general happens-before definition of [1,2] does not capture our transitive uniform conditional independence below (namely property seven of [1,2] does not hold), hence CDPOR cannot be seen as an instance of SDPOR but rather as an extension.

**Definition 3.** *The* transitive uniform *conditional independence relation, written unif*(α, β, S)*, fulfills (i1) and (i2) and, (i3) unif*(α, β, Sγ) *holds for all* γ /∈ {α, β} *enabled in* S*, where* Sγ *is defined by* S γ −→ Sγ*.*

During the exploration of the sequence p.q.r in Example 4, the algorithm will now find a reversible race between p and q, since the independence is not transitively uniform in z = −1, x = −2. Namely, *(i3)* does not hold since r is enabled and we have x = −1 and z = 0 in s[r], which implies ¬*unif*(p, q, s[r]) (*(i2)* does not hold).

We now introduce sufficient conditions for transitive uniformity that can be precomputed statically, and efficiently checked, in our dynamic algorithm. Condition *(i1)* is computed dynamically as usual during the exploration simply storing enabling dependencies. Condition *(i2)* is provided by the ICs. Our sufficient conditions to ensure *(i3)* are as follows. For each atomic block b, we precompute *statically* (before executing DPOR) the set W(b) of the global variables that can be modified by the full execution of b, i.e., by an instruction in b or by any other block called from, or enabled by, b (transitively). To this end, we do a simple analysis which consists in: (1) First we build the call graph for the program to establish the calling relationships between the blocks in the program. Note that when we find a process creation instruction spawn(P[ini]) we have a calling relationship between the block in which the spawn instruction appears and P. (2) We obtain (by a fixed point computation) the largest relation fulfilling that g belongs to W(b) if either g is *modified* by an instruction in b or g belongs to W(c) for some block c called from b. This computation can be done with different levels of precision, and it is well-studied in the static analysis field [18]. We let *G*(C) be the set of global variables evaluated on constraint C in I.

**Definition 4 (sufficient condition for transitive uniformity,** U⇒**).** *Let* E *be a sequence,* I *a set of constraints,* α *and* β *be two events enabled in* s[E]*, and* T = next[E](enabled(s[E])) \ {α, β}*, we define* U⇒(I, α, β, s[E]) ≡ ∃C ∈ I : C(s[E]) ∧ ((*G*(C) ∩ - t∈T W(t ¯)) = ∅)*.*

Intuitively, our sufficient condition ensures transitive uniformity by checking that the global variables involved in the constraint C of the IC used to ensure the uniformity condition are not modified by other enabled events in the state.

**Theorem 1.** *Given a sequence* E *and two events* α *and* β *enabled in* s[E]*, we have that* U⇒(Iα, ¯ β¯, α, β, s[E]) ⇒ *unif*(α, β, s[E])*.*

### **3.3 The Constrained DPOR Algorithm**

The code highlighted in blue in Algorithm 1 provides the extension to apply conditional independence within DPOR. In addition to the pruning explained in Sect. 3.1, it achieves two further types of pruning:

It is important to note also that the inferred conditional independencies are recorded in the happens-before relation to be later re-used for subsequent computations of the and dep definitions.

*Example 5.* Let us describe the exploration for the example in Fig. 1 using our CDPOR. At state 1, the algorithm checks whether p and q are in race. U⇒(Ip, ¯ q¯, p, q, S) does not hold in z = −2 since, although (z ≤ −1) ∈ Ip, ¯ q¯ holds, we have that *G*(z ≤ −1)∩W(r) = {z} = ∅. Process q is hence added to back(). On the other hand, since (z ≤ −1) ∈ Ip, ¯ q¯ holds in z = −2 (line 11), q.p is added to sleep() (line 12). At state 2 the algorithm checks the possible race between q and r after executing p. This time the transitive uniformity of the independence of q and r holds since (z ≤ −2) ∈ Iq,¯ r¯ holds, and there are no enabled events out of {q, r}. Our algorithm therefore avoids the addition of r to back(p) (pruning 1 above). The algorithm also checks the possible race between p and r in z = −2. Again, true ∈ Ip, ¯ r¯ holds and is uniform since *G*(true) = ∅ (pruning 1). The algorithm finishes the exploration of sequence p.q.r and then backtracks with q at state 0. At state 5 the algorithm selects process r (p is in the sleep set of 5 since it is propagated down from the q.p in sleep()). It then checks the possible race between q and r, which is again discarded (pruning 1), since transitive uniformity of the independence of q and r can be proved: we have that (z ≤ −2) ∈ Iq,¯ r¯ holds in z = −2 and W(p) ∩ G(z ≤ −2) = ∅, where p is the only enabled event out of {q, r} and W(p) = {x}. This avoids adding r to back(). Finally, at state 5, p is propagated down in the new sleep set (pruning 2), since as before true ∈ Ip, ¯ r¯ ensures transitive uniformity. The exploration therefore finishes at state 6.

Overall, on our working example, CDPOR has been able to explore only one complete sequence p.q.r and the partial sequence q.r (a total of 6 states). The latter one could be avoided if a more precise sufficient condition for uniformity is provided which, in particular, is able to detect that the independence of p and q in is transitive uniform, i.e., it still holds after r (even if r writes variable z). **Theorem 2 (soundness).** *For each Mazurkiewicz trace* T *defined by the happens before relation, Explore(*, ∅*) in Algorithm 1 explores a complete execution sequence* T *that reaches the same final state as* T*.*

# **4 Automatic Generation of ICs Using SMT**

Generating ICs amounts to proving (conditional) program equivalence w.r.t. the global memory. While the problem is very hard in general, proving equivalence of smaller blocks of code becomes more tractable. This section introduces a novel SMT-based approach to synthesize ICs between pairs of atomic blocks of code. Our ICs can be used within any transformation or analysis tool –beyond DPOR– which can gain accuracy or efficiency by knowing that fragments of code (conditionally) commute. Section 4.1 first describes the inference for basic blocks; Sect. 4.2 extends it to handle process creation and Sect. 4.3 outlines other extensions, like loops, method invocations and data structures.

### **4.1 The Basic Inference**

In this section we consider blocks of code containing conditional statements and assignments using linear integer arithmetic (LIA) expressions. The first step to carry out the inference is to transform q and r into two respective *deterministic* Transition Systems (TSs), Tq and Tr (note that q and r are assumed to be deterministic), and compose them in both reverse orders Tq·r and Tr·q. Consider r and q in Fig. 1 whose associated TSs are (primed variables represent the final value of the variables):

$$\begin{array}{ll} T\_q: z \ge 0 \to z' = x; & T\_r: true \to x' = x+1, z' = z+1; \\ z < 0 \to z' = z; \end{array}$$

The code to be analyzed is the composition of Tq and Tr in both orders:

$$\begin{array}{llll} T\_{q\cdot r} \colon & z \ge 0 \to x' = x + 1, z' = x + 1; & T\_{r\cdot q} \colon & z \ge -1 \to x' = x + 1, z' = x + 1; \\ & z < 0 \to x' = x + 1, z' = z + 1; & & z < -1 \to x' = x + 1, z' = z + 1; \end{array}$$

In what follows we denote by Ta·b the deterministic TS obtained from the concatenation of the blocks a and b, such that all variables are assigned in one instruction using parallel assignment. We let A |G be the restriction to the global memory of the assignments in A (i.e., ignoring the effect on local variables). The following definition provides an SMT formula over LIA (a boolean formula where the atoms are equalities and inequalities over linear integer arithmetic expressions) which encodes the independence between the two blocks.

**Definition 5 (IC generation).** *Let us consider two atomic blocks* q *and* r *and a global memory* G *and let* Ci → Ai *(resp.* C j → A j *) be the transitions in* Tq·r *(resp.* Tr·q*). We obtain* Fq,r *as the SMT formula:* i,j (Ci ∧ C j ∧ Ai |G= A j |G)*.* Intuitively, the SMT encoding in the above definition has as solutions all those states where both a condition Ci of a transition in Tq·r and C j of a transition in Tr·q hold (and hence are compatible) and the final global state after executing all instructions in the two transitions (denoted Ai and A j ) remains the same.

Next, we generate the constraints of the independence condition Iq,r by obtaining a compact representation of all models over linear arithmetic atoms (computed by an *allSAT* SMT solver) satisfying Fq,r. In particular, we add a constraint in Iq,r for every obtained model.

*Example 6.* In the example, we have the TS with conditions and assignments:

$$\begin{array}{c|c} T\_{q \cdot r} \colon C\_1 \colon z \ge 0 \quad A\_1 \colon x' = x + 1, z' = x + 1\\ C\_2 \colon z < 0 \quad A\_2 \colon x' = x + 1, z' = z + 1 \end{array} \Big| \begin{array}{c} T\_{r \cdot q} \colon C\_1' \colon z \ge -1 \quad A\_1' \colon x' = x + 1, z' = x + 1\\ C\_2' \colon z < -1 \quad A\_2' \colon x' = x + 1, z' = z + 1 \end{array}$$

and we obtain a set with three constraints Iq,r = {(z ≥ 0),(z = x),(z < −1)} by computing all models satisfying the following resulting formula:

$$\begin{aligned} &(z \ge 0 \land z \ge -1 \land x + 1 = x + 1 \land x + 1 = x + 1) \lor \\ &(z \ge 0 \land z < -1 \land x + 1 = x + 1 \land x + 1 = z + 1) \lor \\ &(z < 0 \land z \ge -1 \land x + 1 = x + 1 \land z + 1 = x + 1) \lor \\ &(z < 0 \land z < -1 \land x + 1 = x + 1 \land z + 1 = z + 1) \end{aligned}$$

The second conjunction is unsatisfiable since there is no model with both C1 and C 2. On the other hand, the equalities of the first and the last conjunctions always hold, which give us the constraints z ≥ 0 and z ≤ −2. Finally, all equalities hold when x = z, which give us the third constraint as a result for our SMT encoding.

Note that, as in this case Fq,r describes not only a sufficient but also a necessary condition for independence, the obtained constraints IC are also a sufficient and necessary conditions for independence. This allows removing line 14 in the algorithm, since the context-sensitive check will fail if line 11 does. However, the next extensions do not ensure that the generated ICs are necessary conditions.

### **4.2 IC for Blocks with Process Creation**

Consider the following two methods whose body constitutes an atomic block (e.g., the lock is taken at the method start and released at the return). They are inspired by a highly concurrent computation for the Fibonacci used in the experiments. Variables nr and r are global to all processes:

We now want to infer Ifib(v),fib(v1), Ifib(v),res(v1), Ires(v),res(v1). The first step is to obtain, for each block r, a *TS with uninterpreted functions*, denoted T Su r , in which transitions are of the form C → (A, S) where A are the parallel assignments as in Sect. 4.1, and S is a multiset containing calls to fresh *uninterpreted* functions associated to the processes spawned within the transition (i.e., a process creation spawn(P) is associated to an uninterpreted function spawn P).

$$\begin{array}{l} T\_{\mathsf{lib}}^{u} \colon v \le 1 \to (skip, \{spawn.res(v)\})\\ v > 1 \to (skip, \{spawn.fib(v-1), spawn.fib(v-2)\})\\ T\_{\mathsf{res}}^{u} \colon nr \ge 0 \to (nr'=0, r'=v, \{\})\\ nr < 0 \to (nr'=1, r'=0, \{spawn.res(r+v)\}) \end{array}$$

The following definition extends Definition 5 to handle process creation. Intuitively, it associates a fresh variable to each different element in the multisets (mapping P below) and enforces equality among the multisets.

**Definition 6 (IC generation with process creation).** *Let us consider* T Su r·q *and* T Su q·r*. We define* P = {∪s | s ∈ S, with C → (A, S) ∈ T Su r·q ∪ T Su q·r}*. Let* P *be a mapping from the elements in* P *to fresh variables, and* P (S) *be the replacement of the elements in the multiset* S *applying the mapping* P *. Let* Ci → (Ai, Si) *(resp.* C j → (A j , S j )*) be the transitions in* T Su q·r *(resp.* T Su r·q*). We obtain* Fq,r *as the SMT formula:* i,j (Ci∧C j ∧Ai |G= A j |G ∧P (Si) ≡ P (S j ))*.*

For simplicity and efficiency, we consider that ≡ corresponds to the syntactic equality of the multisets. However, in order to improve the precision of the encoding we apply P to Si and Sj replacing two process creations by the same variable if they are equal modulo associativity and commutativity (AC) of arithmetic operators and after substituting the equalities already imposed by Ai |G= A j (see example below). A more precise treatment can be achieved by using equality with uninterpreted functions (EUF) to compare the multisets of processes.

*Example 7.* Let us show how we apply the above definition to infer Ires(v),res(v1). We first build Tres(v)·res(v1) from Tres(v) by composing it with itself:

$$\begin{aligned} nr &\le 0 \to \left(nr'=0, r'=v\_1, \{spawn.res(r+v)\}\right) \\ nr &> 0 \to \left(nr'=1, r'=0, \{spawn.res(v+v\_1)\}\right) \end{aligned}$$

and Tres(v1)·res(v) which is like the one above but exchanging v and v1. Next, we define P = {spawn res(r + v) → x1, spawn res(v + v1) → x2, spawn res(r + v1) → x3, spawn res(v1+v) → x4} and apply it with the improvement described above

$$\begin{aligned} \left(nr &\le 0 \land nr \le 0 \land 0 = 0 \land v = v\_1 \land \{x\_1\} = \{x\_1\}\right) \lor \\ \left(nr &\le 0 \land nr > 0 \land 0 = 1 \land v\_1 = 0 \land \{x\_1\} = \{x\_4\}\right) \lor \\ \left(nr &> 0 \land nr \le 0 \land 1 = 0 \land 0 = v \land \{x\_2\} = \{x\_3\}\right) \lor \\ \left(nr &> 0 \land nr > 0 \land 1 = 1 \land 0 = 0 \land \{x\_2\} = \{x\_2\}\right) \end{aligned}$$

Note that the second and the third conjunction are unfeasible and hence can be removed from the formula. In the first one spawn res(r + v1) is replaced by x1 (instead of x3) since we can substitute v1 by v as v = v1 is imposed in the conjunction and in the fourth one spawn res(v1 + v) is replaced by x2 (instead of x4) since it is equal modulo AC to spawn res(v + v1). Then we finally have

$$(nr \le 0 \land nr \le 0 \land 0 = 0 \land v = v\_1) \quad \lor \quad (nr > 0 \land nr > 0 \land 1 = 1 \land 0 = 0)$$

As before, Ires(v),res(v1) = {(nr > 0),(v = v1)} is then obtained by computing all satisfying models. In the same way we obtain Ifib(v),res(v1) = Ifib(v),fib(v1) = {true}. The following theorem states the soundness of the inference of ICs, that holds by construction of the SMT formula.

**Theorem 3 (soundness of independence conditions).** *Given the assumptions in Definition 6, if* ∃C ∈ Ir,q *s.t.* C(S) *holds, then* S r·q −→ S *and* S q·r −→ S *.*

We will also get a necessary condition in those instances where the use of syntactic equality modulo AC on the multisets of created processes (as described above) is not loosing precision. This can be checked when building the encoding.

### **4.3 Other Extensions**

We abstract loops from the code of the blocks so that we can handle them as uninterpreted functions similarly to Definition 6. Basically, for each loop, we generate as many uninterpreted functions as variables it modifies (excluding local variables of the loop) plus one to express all processes created inside the loop. The functions have as arguments the variables accessed by the loop (again excluding local variables). This transformation allows us to represent that each variable might be affected by the execution of the loop over some parameters, and then check in the reverse trace whether we get to the loop over the same parameters.

**Definition 7 (loop extraction for IC generation).** *Let us consider a loop* L *that accesses* x1,...,xn *variables and modifies* y1,...,ym *variables (excluding local loop variables) and let* l1,...,lm+1 *be fresh function symbol names. We replace* L *by the following code:*

$$\begin{aligned} x'\_1 &= x\_1; \dots; \ x'\_n = x\_n; \ y\_1 = l\_1(x'\_1, \dots, x'\_n); \dots; \ y\_m = l\_m(x'\_1, \dots, x'\_n);\\ sspan(f\_{m+1}(x'\_1, \dots, x'\_n)); \quad (only \; if \; there \; are \; square \; operations \; inside \; the \; loop) \end{aligned}$$

Existing dependency analysis can be used to infer the subset of x1,...,xn that affects each yi, achieving more precision with a small pre-computation overhead.

The treatment of method invocations (or function calls) to be executed atomically within the considered blocks can be done analogously to loops by introducing one fresh function for every (non-local) variable that is modified within the method call and one more for the result. The parameters of these new functions are the original ones plus one for each accessed (non-local) variable. After the transformations for both loops and calls described above, we have TSs with function calls that are treated as uninterpreted functions in a similar way to Definition 6. However these functions can now occur in the conditions and the assignments of the TS. To handle them, we use again a mapping P to remove all function calls from the TS and replace them by fresh integer variables. After that the encoding is like in Definition 6, and we obtain an SMT formula over LIA, which is again sent to the allSAT SMT solver. Once we have obtained the models we replace back the introduced fresh variables by the function calls using the mapping P. Several simplifications on equalities involving function calls can be done before and after invoking the solver to improve the result. As a final remark, data structures like lists or maps have been handled by expressing their uses as function calls, hence obtaining constraints that include conditions on them.

# **5 Experiments**

In this section we report on experimental results that compare the performance of three DPOR algorithms: SDPOR [1,2], CSDPOR [3] and our proposal CDPOR. We have implemented and experimentally evaluated our method within the SYCO tool [3], a systematic testing tool for message-passing concurrent programs. SYCO can be used online through its web interface available at http:// costa.fdi.ucm.es/syco. To generate the ICs, SYCO calls a new feature of the VeryMax program analyzer [6] which uses Barcelogic [5] as SMT solver. As benchmarks, we have borrowed the examples from [3] (available online from the previous url) that were used to compare SDPOR with CSDPOR. They are classical concurrent applications: several concurrent sorting algorithms (QS, MS, PS), concurrent Fibonacci Fib, distributed workers Pi, a concurrent registration system Reg and database DBP, and a consumer producer interaction BB. These benchmarks feature the typical concurrent programming methodology in which computations are split into smaller atomic subcomputations which concurrently interleave their executions, and which work on the same shared data. Therefore, the concurrent processes are highly interfering, and both inferring ICs and applying DPOR algorithms on them becomes challenging.

We have executed each benchmark with size increasing input parameters. A timeout of 60 s is used and, when reached, we write >X to indicate that for the corresponding measure we encountered X units up to that point (i.e., it is at least X). Table 1 shows the results of the executions for 6 different inputs. Column T r shows the number of traces, S the number of states that the algorithms explore, and T the time in *sec* it takes to compute them. For CDPOR, we also show the time Tsmt of inferring the ICs (since the inference is performed once for all executions, it is only shown in the first row). Times are obtained on an Intel(R) Core(TM) i7 CPU at 2.5 GHz with 8 GB of RAM (Linux Kernel 5.4.0). Columns G**s** and G**cs** show the time speedup of CDPOR over SDPOR and CSDPOR, respectively, computed by dividing each respective T by the time T of CDPOR. Column G**smt** shows the time speedup over CSDPOR including Tsmt in the time of CDPOR. We can see from the speedups that the gains of CDPOR increase exponentially in all examples with the size of the input. When compared with CSDPOR, we achieve reductions up to 4 orders of magnitude for the largest inputs on which CSDPOR terminates (e.g., Pi, QS). It is important to highlight that the number of non-unitary sequences stored in sleep sets is 0 in every benchmark except in BB for which it remains quite low (namely for BB(11) the peak is 22).

W.r.t. SDPOR, we achieve reductions of 4 orders of magnitude even for smaller inputs for which SDPOR terminates (e.g., PS). Note that since most examples reach the timeout, the gains are at least the ones we show, thus the

**Table 1.** Experimental evaluation

concrete numbers shown should not be taken into account. In some examples (e.g., BB, MS), though the gains are linear for the small inputs, when the size of the problem increases both SDPOR and CSDPOR time out, while CDPOR can still handle them efficiently.

Similar reductions are obtained for number of states explored. In this case, the system times out when it has memory problems, and the computation stops progressing (hence the number of explored states does not increase with the input any more). As regards the time to infer the annotations Tsmt, we observe that in most cases it is negligible compared to the exploration time of the other methods. QS is the only example that needs some seconds to be solved and this is due to the presence of several nested conditional statements combined with the use of built-in functions for lists, which makes the generated SMT encoding harder for the solver and the subsequent simplification step. Note that the inference is a pre-process which does not add complexity to the actual DPOR algorithm.

# **6 Related Work and Conclusions**

The notion of conditional independence in the context of POR was first introduced in [11,15]. Also [12] provides a similar strengthened dependency definition. CSDPOR was the first approach to exploit this notion within the state-of-the-art DPOR algorithm. We advance this line of research by fully integrating conditional independence within the DPOR framework by using *independence constraints* (ICs) together with the notion of *transitive uniform* conditional independence –which ensures the ICs hold along the whole execution sequence. Both ICs and transitive uniformity can be approximated statically and checked dynamically, making them effectively applicable within the dynamic framework. The work in [14,21] generated for the first time ICs for processes with a single instruction following some predefined patterns. This is a problem strictly simpler than our inference of ICs both in the type of IC generated (restricted to the patterns) and on the single-instruction blocks they consider. Furthermore, our approach using an AllSAT SMT solver is different from the CEGAR approach in [4]. The ICs are used in [14,21] for SMT-based bounded model checking, an approach to model checking fundamentally different from our stateless model checking setting. As a consequence ICs are used in a different way, in our case with no bounds on number of processes, nor derivation lengths, but requiring a uniformity condition on independence in order to ensure soundness. Maximal causality reduction [13] is technically quite different from CDPOR as it integrates SMT solving within the dynamic algorithm.

Finally, data-centric DPOR (DCDPOR) [7] presents a new DPOR algorithm based on a different notion of dependency according to which the equivalence classes of derivations are based on the pairs read-write of variables. Consider the following three simple processes {p, q, r} and the initial state x = 0:

p: write(x = 5), q: write(x = 5), r: read(x). In DCDPOR, we have only three different observation functions: (r, x) (reading the initial value), (r, p) (reading the value that p writes), (r, q) (reading the value that q writes). Therefore, this notion of relational independence is finer grained than the traditional one in DPOR. However, DCDPOR does not consider conditional dependency, i.e., it does not realize that (r, p) and (r, q) are equivalent, and hence only two explorations are required (and explored by CDPOR). The example in conclusion, our approach and DCDPOR can complement each other: our approach would benefit from using a dependency based on the read-write pairs as proposed in DCDPOR, and DCDPOR would benefit from using conditional independence as proposed in our work. It remains as future work to study this integration. Related to DCDPOR, [16] extends optimal DPOR with observers. For the previous example, [16] needs to explore five executions: r.p.q and r.q.p, are equivalent because p and q do not have any observer. Another improvement orthogonal to ours is to inspect dependencies over chains of events, as in [17,19].

# **References**

**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.

CPS, Hardware, Industrial Applications

# **Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System**

Mark Tullsen1(B), Lee Pike2, Nathan Collins1, and Aaron Tomb1

1 Galois, Inc., Portland, OR, USA<EMAIL_ADDRESS>2 Groq, Inc., Palo Alto, USA<EMAIL_ADDRESS>
**Abstract.** Vehicle-to-Vehicle (V2V) communications is a "connected vehicles" standard that will likely be mandated in the U.S. within the coming decade. V2V, in which automobiles broadcast to one another, promises improved safety by providing collision warnings, but it also poses a security risk. At the heart of V2V is the communication messaging system, specified in SAE J2735 using the Abstract Syntax Notation One (ASN.1) data-description language. Motivated by numerous previous ASN.1 related vulnerabilities, we present the formal verification of an ASN.1 encode/decode pair. We describe how we generate the implementation in C using our ASN.1 compiler. We define *self-consistency* for encode/decode pairs that approximates functional correctness without requiring a formal specification of ASN.1. We then verify self-consistency and memory safety using symbolic simulation via the *Software Analysis Workbench*.

**Keywords:** Automated verification · ASN.1 · Vehicle-to-Vehicle LLVM · Symbolic execution · SMT solver

# **1 Introduction**

At one time, automobiles were mostly mechanical systems. Today, a modern automobile is a complex distributed computing system. A luxury car might contain tens of millions of lines of code executing on 50–70 microcontrollers, also known as *electronic control units* (ECUs). A midrange vehicle might contain at least 25 ECUs, and that number continues to grow. In addition, various radios such as Bluetooth, Wifi, and cellular provide remote interfaces to an automobile.

With all that code and remotely-accessible interfaces, it is no surprise that software vulnerabilities can be exploited to gain unauthorized access to a vehicle. Indeed, in a study by Checkoway *et al.* on a typical midrange vehicle, for every remote interface, they found some software vulnerability that provided an attacker access to the vehicle's internal systems [4]. Furthermore, in each case,

This work was performed while Dr. Pike was at Galois, Inc.

c The Author(s) 2018

H. Chockler and G. Weissenbacher (Eds.): CAV 2018, LNCS 10982, pp. 413–429, 2018. https://doi.org/10.1007/978-3-319-96142-2\_25

once the interface is exploited, the attackers could parlay the exploit to make arbitrary modifications to other ECUs in the vehicle. Such modifications could include disabling lane assist, locking/unlocking doors, and disabling the brakes. Regardless of the interface exploited, full control can be gained.

Meanwhile, the U.S. Government is proposing a new automotive standard for vehicle-to-vehicle (V2V) communications. The idea is for automobiles to have dedicated short-range radios that broadcast a *Basic Safety Message* (BSM) e.g., vehicle velocity, trajectory, brake status, etc.—to other nearby vehicles (within approximately 300 m). V2V is a crash prevention technology that can be used to warn drivers of unsafe situations—such as a stopped vehicle in the roadway. Other potential warning scenarios include left-turn warnings when lineof-sight is blocked, blind spot/lane change warnings, and do-not-pass warnings. In addition to warning drivers, such messages could have even more impact for autonomous or vehicle-assisted driving. The U.S. Government estimates that if applied to the full national fleet, approximately one-half million crashes and 1,000 deaths could be prevented annually [15]. We provide a more detailed overview of V2V in Sect. 2.

While V2V communications promise to make vehicles safer, they also provide an additional security threat vector by introducing an additional radio and more software on the vehicle.

This paper presents initial steps in ensuring that V2V communications are implemented securely. We mean "secure" in the sense of having no flaws that could be a vulnerability; confidentiality and authentication are provided in other software layers and are not in scope here. Specifically, we focus on the security of encoding and decoding the BSM. The BSM is defined using ASN.1, a data description language in widespread use. It is not an exaggeration to say that ASN.1 is the backbone of digital communications; ASN.1 is used to specify everything from the X.400 email protocol to voice over IP (VoIP) to cellular telephony. While ASN.1 is pervasive, it is a complex language that has been amended substantially over the past few decades. Over 100 security vulnerabilities have been reported for ASN.1 implementations in MITRE's Common Vulnerability Enumeration (CVE) [14]. We introduce ASN.1 and its security vulnerabilities in Sect. 3.

This paper presents the first work in formally verifying a subsystem of V2V. Moreover, despite the pervasiveness and security-critical nature of ASN.1, it is the first work we are aware of in which any ASN.1 encoder (that translate ASN.1 messages into a byte stream) and decoder (that recovers an ASN.1 message from a byte stream) has been formally verified. The only previous work in this direction is by Barlas *et al.*, who developed a translator from ASN.1 into CafeOBJ, an algebraic specification and verification system [1]. Their motivation was to allow reasoning about broader network properties, of which an ASN.1 specification may be one part, their work does not address ASN.1 encoding or decoding and appears to be preliminary.

The encode/decode pair is first generated by Galois' ASN.1 compiler, part of the *High-Assurance ASN.1 Workbench* (HAAW). The resulting encode/decode pair is verified using Galois' open source *Software Analysis Workbench* (SAW), a state-of-the-art symbolic analysis engine [6]. Both tools are further described in Sect. 4.

In Sect. 5 we state the properties verified: we introduce the notion of selfconsistency for encode/decode verification, which approximates functional correctness without requiring a formal specification of ASN.1 itself. Then we describe our approach to verifying the self consistency and memory safety of the C implementation of the encode/decode pair in Sect. 6 using compositional symbolic simulation as implemented in SAW. In Sect. 7 we put our results into context.

# **2 Vehicle-to-Vehicle Communications**

As noted in the introduction, V2V is a short-range broadcast technology with the purpose of making driving safer by providing early warnings. In the V2V system, the BSM is the key message broadcasted, up to a frequency of 10 Hz (it can be perhaps lower due to congestion control). The BSM must be compatible between all vehicles, so it is standardized under SAE J2735 [7].

The BSM is divided into Part I and Part II, and both are defined with ASN.1. Part I is called the *BSM Core Data* and is part of every message broadcast. Part I includes positional data (latitude, longitude, and elevation), speed, heading, and acceleration. Additionally it includes various vehicle state information including transmission status (e.g., neutral, park, forward, reverse), the steering wheel angle, braking system status (e.g., Are the brakes applied? Are anti-lock brakes available/engaged?, etc.), and vehicle size. Our verification, described in Sect. 6, is over Part I.

Part II is optional and extensible. Part II could include, for example, regionally-relevant data. It can also include additional vehicle safety data, including, for example, which of the vehicle's exterior lights are on. It may include information about whether a vehicle is a special vehicle or performing a critical mission, such as a police car in an active pursuit or an ambulance with a critical patient. It can include weather data, and obstacle detection.

### **3 ASN.1**

*Abstract Syntax Notation One* (ASN.1) is a standardized data description language in widespread usage. Our focus in this section is to give a sense of what ASN.1 is as well as its complexity. We particularly focus on aspects that have led to security vulnerabilities.

### **3.1 The ASN.1 Data Description Language and Encoding Schemes**

ASN.1 was first standardized in 1984, with many revisions since. ASN.1 is a data description language for specifying messages; although it can express relations between request and response messages, it was not designed to specify stateful protocols. While ASN.1 is "just" a data description language, it is quite large and complex. Indeed, merely parsing ASN.1 specifications is difficult. Dubuisson notes that the grammar of ASN.1 (1997 standard) results in nearly 400 shift/reduce errors and over 1,300 reduce/reduce errors in a LALR(1) parser generator, while a LL(k) parser generator results in over 200 production rules beginning with the same lexical token [8]. There is a by-hand transformation of the grammar into an LL(1)-compliant grammar, albeit no formal proof of their equivalence [9].

Not only is the syntax of ASN.1 complex, but so is its semantics. ASN.1 contains a rich datatype language. There are at least 26 base types, including arbitrary integers, arbitrary-precision reals, and 13 kinds of string types. Compound datatypes include sum types (e.g., CHOICE and SET), records with subtyping (e.g., SEQUENCE), and recursive types. There is a complex constraint system (ranges, unions, intersections, etc.) on the types. Subsequent ASN.1 revisions support open types (providing a sort of dynamic typing), versioning to support forward/backward compatibility, user-defined constraints, parameterized specifications, and so-called *information objects* which provide an expressive way to describe relations between types.

So far, we have only highlighted the data description language itself. A set of *encoding rules* specify how the ASN.1 messages are serialized for transmission on the wire. Encoder and decoder pairs are always with respect to a specific schema and encoding rule. There are at least nine standardized ASN.1 encoding rules. Most rules describe 8-bit byte (octet) encodings, but three rule sets are dedicated to XML encoding. Common encoding rules include the Basic Encoding Rules (BER), Distinguished Encoding Rules (DER), and Packed Encoding Rules (PER). The encoding rules do not specify the transport layer protocol to use (or any lower-level protocols, such as the link or physical layer).

### **3.2 Example ASN.1 Specification**

To get a concrete flavor of ASN.1, we present an example data *schema*. Let us assume we are defining messages that are sent (TX) and received (RX) in a query-response protocol.

```
MsgTx ::= SEQUENCE {
  txID INTEGER(1..5),
  txTag UTF8STRING
}
MsgRx ::= SEQUENCE {
  rxID INTEGER(1..7),
  rxTag SEQUENCE(SIZE(0..10)) OF INTEGER
}
```
We have defined two top-level types, each a SEQUENCE type. A SEQUENCE is an named tuple of fields (like a C struct). The MsgTx sequence contains two fields: txID and txTag. These are typed with built-in ASN.1 types. In the definition of MsgRx, the second field, rxTag, is the SEQUENCE OF structured type; it is equivalent to an array of integers that can have a length between 0 and 10, inclusively. Note that the txID and rxID fields are *constrained* integers that fall into the given ranges.

ASN.1 allows us to write values of defined types. The following is a value of type MsgTx:

```
msgTx MsgTx ::= {
  txID 1,
  txTag "Some msg"
}
```
#### **3.3 ASN.1 Security**

There are currently over 100 vulnerabilities associated with ASN.1 in the MITRE Common Vulnerability Enumeration (CVE) database [14]. These vulnerabilities cover many vendor implementations as well as encoders and decoders embedded in other software libraries (e.g., OpenSSL, Firefox, Chrome, OS X, etc.). The vulnerabilities are often manifested as low-level programming vulnerabilities. A typical class of vulnerabilities are unallowed memory reads/writes, such as buffer overflows and over-reads and NULL-pointer dereferences. While generally arcane, ASN.1 was recently featured in the popular press when an ASN.1 vender flaw was found in telecom systems, ranging from cell tower radios to cellphone baseband chips [11]; an exploit could conceivably take down an entire mobile phone network.

Multiple aspects of ASN.1 combine to make ASN.1 implementations a rich source for security vulnerabilities. One reason is that many encode/decode pairs are hand-written and ad-hoc. There are a few reasons for using ad-hoc encoders/decoders. While ASN.1 compilers exist that can generate encoders and decoders (we describe one in Sect. 4.1), many tools ignore portions of the ASN.1 specification or do not support all encoding standards, given the complexity and breadth of the language. A particular protocol may depend on ASN.1 language features or encodings unsupported by most existing tools. Tools that support the full language are generally proprietary and expensive. Finally, generated encoders/decoders might be too large or incompatible with the larger system (e.g., a web browser), due to licensing or interface incompatibilities.

Even if an ASN.1 compiler is used, the compiler will include significant handwritten libraries that deal with, e.g., serializing or deserializing base types and memory allocation. For example, the unaligned packed encoding rules (UPER) require tedious bit operations to encode types into a compact bit-vector representation. Indeed, the recent vulnerability discovered in telecom systems is not in protocol-specific generated code, but in the associated libraries [11].

Finally, because ASN.1 is regularly used in embedded and performancecritical systems, encoders/decoders are regularly written in unsafe languages, like C. As noted above, many of the critical security vulnerabilities in ASN.1 encoders/decoders are memory safety vulnerabilities in C.

# **4 Our Tools for Generating and Verifying ASN.1 Code**

We briefly introduce the two tools used in this work. First we introduce our ASN.1 compiler for generating the encode/decode pair, then we introduce the symbolic analysis engine used in the verification.

### **4.1** *High-Assurance ASN.1 Workbench* **(HAAW)**

Our *High-Assurance ASN.1 Workbench* (HAAW) is a suite of tools developed by Galois that supports each stage of the ASN.1 protocol development lifecycle: specification, design, development, and evaluation. It is composed of an interpreter, compiler, and validator, albeit with varying levels of maturity. HAAW is implemented in Haskell.

The HAAW compiler is built using semi-formal design techniques and is thoroughly tested to help ensure correctness. The implementation of the HAAW compiler is structured to be as manifestly correct as feasible. It effectively imports a (separately tested) ASN.1 interpreter which is then "partially-evaluated" on the fly to generate code. The passes are as follows: An input ASN.1 specification is "massaged" to a specification-like form which can be interpreted by a built-in ASN.1 interpreter. This specification-like form is combined with the interpreter code and is converted into a lambda-calculus representation; to this representation we apply multiple optimization rules; we finally "sequentialize" to a monadic lambda-calculus (where we are left with the lambda calculus, sequencing operators, and encoding/decoding primitives), this last representation is then transformed into C code. The generated code is linked with a library that encodes and decodes the basic ASN.1 types.

Moreover, while the HAAW compiler improves the quality of the code generated, we verify the generated code and libraries directly, so HAAW is not part of the trusted code-base.

### **4.2 The Software Analysis Workbench (SAW)**

The *Software Analysis Workbench* (SAW)1 is Galois' open-source, state-of-theart symbolic analysis engine for multiple programming languages. Here we briefly introduce SAW, see Dockins *et al.* [6] for more details.

An essential goal of SAW is to generate semantic models of programs independent of a particular analysis task and to interface with existing automated reasoning tools. SAW is intended to be mostly automated but supports userguidance to improve scalability.

The high-level architecture of SAW is shown in Fig. 1. At the heart of SAW is *SAWCore*. SAWCore is SAW's intermediate representation (IR) of programs. SAWCore is a dependently-typed functional language, providing a functional representation of the semantics of a variety of imperative and functional languages.

1 saw.galois.com.

**Fig. 1.** SAW architecture, reproduced from [6].

SAWCore includes common built-in rewrite rules. Additionally, users can provide domain-specific rewrite rules, and because SAWCore is a dependently-typed language, rewrite rules can be given expressive types to prove their correctness.

SAW currently supports automated translation of both *low-level virtual machine* (LLVM) and *Java virtual machine* (JVM) into SAWCore. Thus, programming languages that can be compiled to these two targets are supported by SAW. Indeed, SAW can be used to prove the equivalence between programs written in C and Java.

SAWCore can also be generated from Cryptol. Cryptol is an open-source language2 for the specification and formal verification of bit-precise algorithms [10], and we use it to specify portions of our code, as we describe in Sect. 6.

A particularly interesting feature of Cryptol is that it is a typed functional language, similar to Haskell, but includes a size-polymorphic type system that includes linear integer constraints. To give a feeling for the language, the concatenate operator (#) in Cryptol has the following type:

### (#) : fst, snd, a (fin fst) => [fst]a -> [snd]a -> [fst + snd]a

It concatenates two sequences containing elements of type a, the first of length fst—which is constrained to be of finite (fin) length (infinite sequences are expressible in Cryptol)—and the second of length snd. The return type is a sequence of a's of length fst + snd. Cryptol relies on *satisfiability modulo theories* (SMT) solving for type-checking.

SAWCore is typically exported to various formats supported by external third-party solvers. This includes SAT solver representations (and inverter graphs (AIG), conjunctive normal form (CNF), and ABC's format [3]), as well as SMT-Lib2 [2], supported by a range of SMT solvers.

2 https://cryptol.net/.

SAW allows bit-precise reasoning of programs, and has been used to prove optimized cryptographic software is correct [6]. SAW's bit-level reasoning is also useful for encode/decode verification, and in particular, ASN.1's UPER encoding includes substantial bit-level operations.

Finally, SAW includes *SAWScript*, a scripting language that drives SAW and connects specifications with code.

# **5 Properties: Encode/Decode Self Consistency**

Ideally, we would prove full functional correctness for the encode/decode pair: that they correctly implement the ASN.1 UPER encoding/decoding rules for the ASN.1 types defined in SAE J2735. However, to develop a specification that would formalize all the required ASN.1 constructs, their semantics, and the proper UPER encoding rules would be an extremely large and tedious undertaking (decades of "man-years"?). Moreover, it is not clear how one would ensure the correctness of such a specification.

Instead of proving full functional correctness, we prove a weaker property by proving consistency between the encoder and decoder implementations. We call our internal consistency property *self-consistency*, which we define as the conjunction of two properties, *round-trip* and *rejection*. We show that selfconsistency implies that decode is the inverse of encode, which is an intuitive property we want for an encode/decode pair.

The *round-trip property* states that a valid message that is encoded and then decoded results in the original message. This is a completeness property insofar as the decoder can decode all valid messages.

A less obvious property is the *rejection property*. The rejection property informally states that any invalid byte stream is rejected by the decoder. This is a soundness property insofar as the decoder *only* decodes valid messages.

In the context of general ASN.1 encoders/decoders, let us fix a schema *S* and an encoding rule. Let *MS* be the set of all ASN.1 abstract messages that satisfy the schema. Let *B* the set of all finite byte streams. Let *encs* : *Ms* → *B* be an encoder, a total function on *Ms*. Let *error* be a fixed constant such that *error* ∈ *Ms*. Let the total function *decs* : *B* → (*Ms* ∪ {*error*}) be its corresponding decoder.

The round-trip and rejection properties can respectively be stated as follows:

### **Definition 1 (Round-trip)**

$$\forall m \in M\_s. dec\_s(enc\_s(m)) = m.$$

**Definition 2 (Rejection)**

$$\forall b \in B.dec\_s(b) = error \lor enc\_s(dec\_s(b)) = b.$$

The two properties are independent: a decoder could properly decode valid byte streams while mapping invalid byte streams to valid messages. Such a decoder would be allowed by Round-trip but not by Rejection. An encode/decode pair that fails the Rejection property could mean that *dec* does not terminate normally on some inputs (note that *error* is a valid return value of *dec*). Clearly, undefined behavior in the decoder is a security risk.

**Definition 3 (Self-consistency).** *An encode/decode pair encS and decS is* self-consistent *if and only if it satisfies the round-trip and rejection properties.*

Self-consistency does not require any reference to a specification of ASN.1 encoding rules, simplifying the verification. Indeed, they are applicable to any encode/decode pair of functions.

However, as noted at the outset, self-consistency does not imply ful functional correctness. For example, for an encoder *encS* and decoder *decS* pair, suppose the messages *MS* = {*m*0*, m*1} and the byte streams *B* includes {*b*0*, b*1} ⊆ *B*. Suppose that according to the specification, it should be the case that *encS*(*m*0) = *b*0, *encS*(*m*1) = *b*1, *decs*(*b*0) = *m*0 and *dec*(*b*1) = *m*1, and for all *b* ∈ *B* such that *b* = *b*0 and *b* = *b*1, *decS*(*b*) = *error* . However, suppose that in fact *encS*(*m*0) = *b*1, *encS*(*m*1) = *b*0, *decS*(*b*0) = *m*1 and *decS*(*b*1) = *m*0, and for all other *b* ∈ *B*, *dec*(*b*) = *error* . Then *encS* and *decS* satisfy both the round-trip and rejection properties, while being incorrect.

That said, if self-consistency holds, then correctness reduces to showing that either encoder or decoder matches its specification, but showing both hold is unnecessary.

In our work, we formally verify self-consistency and memory safety. We also give further, informal, evidence of correctness by both writing individual test vectors and by comparing our test vectors to that produced by other ASN.1 compilers.

# **6 Verification**

Figure 2 summarizes the overall approach to generating and verifying the encode/decode pair, which we reference throughout this section.

### **6.1 First Steps**

The given SAE J2735 ASN.1 specification (J2735.asn) is given as input to HAAW to generate C code for the encoder and decoder. A HAAW standard library is emitted (the dotted line from HAAW to libHAAW.c in Fig. 2 denotes that the standard library is not specific to the SAE-J2735 specification and is not compiled from HAAW).

We wrote the round-trip and rejection properties (Sect. 5) as two C functions. For example, the round-trip property is encoded, approximately, as follows:

```
bool round_trip(BSM *msg_in) {
  unsigned char str[BUF_SIZE];
  enc(msg_in, str);
```
**Fig. 2.** Code generation and verification flow.

```
BSM *msg_out;
  dec(msg_out, str);
  return equal_msg(msg_in, msg_out);
}
```
The actual round trip property is slightly longer as we need to deal with C level setup, allocation, etc. This is why we chose to implement this property in C (rather than in SAWScript).

Now all we need to do is verify, in SAWScript, that the C function round trip returns 1 *for all inputs*. At this point, it would be nice to say the power of our automated tools was sufficient to prove round trip without further programmer intervention. This, unsurprisingly, was not the case. Most of the applications of SAW have been to cryptographic algorithms where code typically has loops with statically known bounds. In our encoder/coder code we have a number of loops with unbounded iterations: given such code we need to provide some guidance to SAW.

In the following sections we present how we were able to use SAW, as well as our knowledge of our specific code, to change an intractable verification task into one that could be done (by automated tools) in less than 5 h. An important note: the rest of this section describes SAW techniques that allow us to achieve tractability, they do not change the soundness of our results.

### **6.2 Compositional Verification with SAW Overrides**

SAW supports *compositional verification*. A function (e.g., compiled from Java or C) could be specified in Cryptol and verified against its specification. That Cryptol specification can then be used in analyzing the remainder of the program, such that in a symbolic simulation, the function is replaced with its specification. We call this replacement an *override*. Overrides can be used recursively and can dramatically improve the scalability of a symbolic simulation. SAW's scripting language ensures by construction that an override has itself been verified.

Overrides are like lemmas, we prove them once, separately, and can re-use them (without re-proof). The lemma that an override provides is an equivalence between a C function and a declarative specification provided by the user (in Cryptol). The effort to write a specification and add an override is often required to manage intractability of the automated solvers used.

### **6.3 Overriding "copy bits" in SAW**

There are two critical libHAAW functions that we found to be intractable to verify using symbolic simulation naively. Here we describe generating overrides for one of them:

```
copy_bits
  ( unsigned char * dst
  , uint32_t *dst_i
  , unsigned char const * src
  , uint32_t *src_i
  , uint32_t const length)
{
  uint32_t src_i_bound = *src_i + length;
  while (*src_i < src_i_bound) {
    copy_overlapping_bits (dst, dst_i, src, src_i, src_i_bound);
  }
  return 0;
}
```
The above function copies length bits from the src array to the dst array, starting at the bit indexed by src i in src and index dst i in dst; src i and dst i are incremented by the number of bits copied; copy overlapping bits is a tedious but loop-free function with bit-level computations to convert to/from a bit-field and byte array. This library function is called by both the encoder and decoder.

One difficulty with symbolically executing copy bits with SAW is that SAW unrolls loops. Without a priori knowledge of the size of length and src i, there is no upper bound on the number of iterations of the loop. Indeed, memory safety is dependent on an invariant holding between the indices, the number of bits to copy, and the length of the destination array: the length of the destination array is not passed to the function, so there is no explicit check to ensure no write-beyond-array in the destination array.

Even if we could fix the buffer sizes and specify the relationship between the length and indexes so that the loop could be unrolled in theory, in practice, it would still be computationally infeasible for large buffers. In particular, we would have to consider every valid combination of the length and start indexes, which is cubic in the bit-length of the buffers.

To override copy bits, we write a specification of copy bits in Cryptol. The specification does not abstract the function, other than eliding the details of pointers, pointer arithmetic, and destructive updates in C. The specification is given below:

```
copy_bits : dst_n, src_n
            [dst_n][8] -> [32] -> [src_n][8] -> [32] -> [32]
            -> ([dst_n][8], [32], [32])
copy_bits dst0 dst_i0 src src_i0 length = (dst1, dst_i1, src_i1)
  where
  dst_bits0 = join dst0
  src_bits0 = join src
  dst1 = split (copy dst_bits0 0)
  copy dst_bits i =
    if i == length
    then dst_bits
    else copy dst_bits'' (i + 1)
    where
    dst_bits'' = update dst_bits (dst_i0 + i)
                   (src_bits0 @ (src_i0 + i))
  dst_i1 = dst_i0 + length
  src_i1 = src_i0 + length
```
We refer to the *Cryptol User Manual* for implementation details [10], but to provide an intuition, we describe the type signature (the first three lines above): the type is polymorphic, parameterized by dst n and src n. A type [32] is a bit-vector of length 32. A type [dst n][8] is an array of length dst n containing byte values. The function takes a destination array of bytes, a 32-bit destination index, a source array of bytes, a source index, an a length, and returns a triple containing a new destination array, and new destination and source indices, respectively. Because the specification is pure, the values that are destructively updated through pointers in the C implementation are part of the return value in the specification.

# **6.4 Multiple Overrides for "copy bits" in SAW**

Even after providing the above override for copy bits, we are *still* beyond the limits of our underlying solvers to automatically prove the equivalence of copy bits with its Cryptol specification.

However, we realize that for the SAE J2735 encode/decode, copy bits is called with a relatively small number of specific concrete values for the sizes of the dst and src arrays, the indexes dst i and src i, and the length of bits to copy length. The only values that we need to leave symbolic are the bit values within the dst and src arrays. Therefore, rather than creating a single override for an arbitrary call to copy bits, we generate separate overrides for each unique set of "specializable" arguments, i.e., dst i, src i, and length.

Thus we note another feature of SAW: SAW allows us to specify a set of concrete function arguments for an override; for each of these, SAW will specialize the override. (I.e., it will prove each specialization of the override.) In our case this turns one intractable override into 56 tractable ones. The 56 specializations (which corresponds to the number of SEQUENCE fields in the BSM specification) were not determined by trial and error but by running instrumented code.

It is important to note that the consequence of a missing overrride specialization cannot change the soundness of SAW's result: Overrides in SAW cannot change the proof results, they only change the efficiency of proof finding. If we had a missing override specialization for copy bits we would only be back where we started: a property that takes "forever" to verify.

This approach works well for the simple BSM Part I. However, once we begin to verify encoders/decoders for more complex ASN.1 specifications (e.g., containing CHOICE and OPTIONAL constructs), this method will need to be generalized.

### **6.5 Results**

A SAW script (script.saw) ties everything together and drives the symbolic execution in SAW and lifts LLVM variables and functions into a dependent logic to state pre- and post-conditions and provide Cryptol specifications as needed. Finally, SAW then generates a SMT problem; Z3 [5] is the default solver we use.

Just under 3100 lines of C code were verified, not counting blank or comment lines. The verification required writing just under 100 lines of Cryptol specification. There are 1200 lines of SAW script auto-generated by the test harness in generating the override specifications. Another 400 lines of SAW script is hand-written for the remaining overrides and to drive the overall verification.

Executed on a modern laptop with an Intel Core i7-6700HQ 2.6 GHz processor and 32 GB of memory, the verification takes 20 min to prove the round-trip property and 275 min to prove the rejection property. The round-trip property is less expensive to verify because symbolic simulation is sensitive to branching, and for the round-trip property, we assert the data is valid to start, which in turn ensures that all of the decodings succeed. In rejection, on the other hand, we have a branch at each primitive decode, and we need to consider both possibilities (success and failure).

# **7 Discussion**

### **7.1 LLVM and Definedness**

Note that our verification has been with respect to the LLVM semantics not the C source of our code. SAW does not model C semantics, but inputs LLVM as the program's semantics (we use clang to generate LLVM from the C). By verifying LLVM, SAW is made simpler (it need only model LLVM semantics rather than C) and we can do inter-program verification more easily. The process of proving that a program satisfies a given specification within SAW guarantees definedness of the program (and therefore memory safety) as a side effect. That is, the translation from LLVM into SAWCore provides a well-defined semantics for the program, and this process can only succeed if the program is well-defined. In some cases, this well-definedness is assumed during translation and then proved in the course of the specification verification. For instance, when analyzing a memory load, SAW generates a semantic model of what the program does if the load was within the bounds of the object it refers to, and generates a side condition that the load was indeed in bounds.