Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-vous

TL;DR

This paper introduces a framework for analyzing complex multithreaded recursive programs with rendez-vous synchronization, using abstractions and automata techniques to handle undecidability issues.

Contribution

It proposes a novel abstraction framework based on Kleene algebras for analyzing synchronized recursive multithreaded programs with dynamic thread creation.

Findings

Framework effectively models multithreaded recursive programs

Automata-based saturation and constraint solving enable analysis

Iterative abstraction refinement improves precision

Abstract

We present in this paper a generic framework for the analysis of multi-threaded programs with recursive procedure calls, synchronisation by rendez-vous between parallel threads, and dynamic creation of new threads. To this end, we consider a model called Synchronized Dynamic Pushdown Networks (SDPNs) that can be seen as a network of pushdown processes executing synchronized transitions, spawning new pushdown processes, and performing internal pushdown actions. The reachability problem for this model is unfortunately undecidable. Therefore, we tackle this problem by introducing an abstraction framework based on Kleene algebras in order to compute an abstraction of the execution paths between two regular sets of configurations. We combine an automata theoretic saturation procedure with constraint solving in a finite domain. We then apply this framework to an iterative abstraction refinement scheme, using multiple abstractions of increasing complexity and precision.

Equations

$$Path{s}_M(C,C^{\prime })\cap {\tau }^{\ast }=\varnothing$$

$$pr{e}_{\Pi }^{\ast }(M,C)=\left\{(c^{\prime },\pi )\mid c^{\prime }\in pr{e}^{\ast }(M,C),\pi \in Path{s}_M(\{c^{\prime }\},C)\right\}$$

$$Id\subseteq \lambda (t)$$

$$a\cdot \lambda (s_{p^{\prime }},{\gamma }^{\prime },q)\subseteq \lambda (s_p,\gamma ,q)$$

$$a\cdot Id\subseteq \lambda (s_p,\gamma ,s_{p^{\prime }})$$

$$\bigcup _{q^{\prime }\in Q}a\cdot (\lambda (s_{p^{\prime }},{\gamma }_1,q^{\prime })\circ \lambda (q^{\prime },{\gamma }_2,q))\subseteq \lambda (s_p,\gamma ,q)$$

$$\bigcup _{s^{\prime \prime }{\stackrel{\epsilon }{\to }}_{A_{pr{e}^{\ast }}}{s}^{\prime }}a\cdot (\lambda (s_{p_2},{\gamma }_2,s^{\prime \prime })(\{\epsilon \})\text{shuffle}\lambda (s_{p_1}^{\prime },{\gamma }_1,q))\subseteq \lambda (s_p,\gamma ,q)$$

$${\pi }^{\prime }\in {\lambda }_1(\{\epsilon \})\text{shuffle}{\lambda }_2(\{\epsilon \})\text{shuffle}{\lambda }_3\circ {\lambda }_4(\{\epsilon \})\text{shuffle}{\lambda }_5(\{\epsilon \})$$

$$\pi =a\cdot {\pi }^{\prime }\in a\cdot ({\lambda }_1(\{\epsilon \})\text{shuffle}{\lambda }_2(\{\epsilon \})\text{shuffle}{\lambda }_3\circ {\lambda }_4(\{\epsilon \})\text{shuffle}{\lambda }_5(\{\epsilon \}))$$

$$\pi \in {\lambda }_1(\{\epsilon \})\text{shuffle}(a\cdot ({\lambda }_2(\{\epsilon \})\text{shuffle}{\lambda }_3)\circ {\lambda }_4(\{\epsilon \}))\text{shuffle}{\lambda }_5(\{\epsilon \})$$

$${\pi }^{\prime }\in {\lambda }_1(\{\epsilon \})\text{shuffle}{\lambda }_2\circ {\lambda }_3(\{\epsilon \})\text{shuffle}{\lambda }_4(\{\epsilon \})$$

$$\pi =a\cdot {\pi }^{\prime }\in a\cdot ({\lambda }_1(\{\epsilon \})\text{shuffle}{\lambda }_2\circ {\lambda }_3(\{\epsilon \})\text{shuffle}{\lambda }_4(\{\epsilon \}))$$

$$\pi \in {\lambda }_1(\{\epsilon \})\text{shuffle}a\cdot {\lambda }_2\circ {\lambda }_3(\{\epsilon \})\text{shuffle}{\lambda }_4(\{\epsilon \})$$

$$c_1=(p_1^{\prime }{w}_1^{\prime }\dots p_{i-1}^{\prime }{w}_{i-1}^{\prime }{q}_{i}u{\gamma }_2\dots {\gamma }_j{p}_{i+1}^{\prime }{w}_{i+1}^{\prime }\dots p_n^{\prime }{w}_n^{\prime })$$

$$(e_1\text{shuffle}\dots e_{i-1}\text{shuffle}({\lambda }^{\prime }\circ {\lambda }_2\dots \circ {\lambda }_j)\text{shuffle}{e}_{i+1}\dots \text{shuffle}{e}_n)$$

$$\pi =\tau \cdot a_2\cdot \dots a_k\in ((a\cdot S_1)\cup (\overline{a}\cdot S_1^{\prime })\cup S_1^{\prime \prime })\text{shuffle}\dots$$

$$r_1=p_i^{\prime }{\gamma }_1{\stackrel{a}{\to }}_M{q}_{i}u$$

$$r_2=p_j^{\prime }{\alpha }_1\stackrel{\overline{a}}{\to }{q}_j{u}^{\prime }$$

$$\alpha (L)=\underset{a_1\dots a_n\in L}{⨁}{v}_{a_1}\odot \dots \odot v_{a_n}$$

$$\beta (x)=\left\{a_1\dots a_n\in 2^{Ac{t}^{\ast }}\mid v_{a_1}\odot \dots \odot v_{a_n}\le x\right\}$$

$$pr{e}_K^{\ast }(M,C)=\left\{(c^{\prime },\pi )\mid c^{\prime }\in pr{e}^{\ast }(M,C),\pi \le \alpha (Path{s}_M(\{c^{\prime }\},C))\right\}$$

$$(v_{a_1},\dots ,v_{a_n})\text{shuffle}(v_{b_1},\dots ,v_{b_m})$$

$$=v_{a_1}\odot ((v_{a_2},\dots ,v_{a_n})\text{shuffle}(v_{b_1},\dots ,v_{b_m}))\oplus v_{\overline{a_1}}\odot ((v_{a_1},\dots ,v_{a_n})\text{shuffle}$$

$$(v_{b_2},\dots ,v_{b_m}))\oplus v_{\tau }\odot ((v_{a_2},\dots ,v_{a_n})\text{shuffle}(v_{b_2},\dots ,v_{b_m}))$$

$$=v_{a_1}\odot ((v_{a_2},\dots ,v_{a_{l+1}})\text{shuffle}(v_{b_1},\dots ,v_{b_l}))\oplus v_{\overline{a_1}}\odot ((v_{a_1},\dots ,v_{a_l})\text{shuffle}$$

$$(v_{b_2},\dots ,v_{b_{l+1}}))\oplus v_{\tau }\odot ((v_{a_2},\dots ,v_{a_{l+1}})\text{shuffle}(v_{b_2},\dots ,v_{b_{l+1}}))$$

$$(v_{a_1},\dots ,v_{a_n})\text{shuffle}(v_{b_1},\dots ,v_{b_m})$$

$$=v_{a_1}\odot ((v_{a_2},\dots ,v_{a_l})\text{shuffle}(v_{b_1},\dots ,v_{b_l}))\oplus v_{\overline{a_1}}\odot ((v_{a_1},\dots ,v_{a_l})\text{shuffle}$$

$$(v_{b_2},\dots ,v_{b_l}))\oplus v_{\tau }\odot ((v_{a_2},\dots ,v_{a_l})\text{shuffle}(v_{b_2},\dots ,v_{b_l}))$$

$$=(v_{a_1},\dots ,v_{a_l})\text{shuffle}(v_{b_1},\dots ,v_{b_l})$$

Full text

paths, Kleene abstractions

The use of parallel programs has grown in popularity in the past fifteen years, but these remain nonetheless fickle and vulnerable to specific issues such as race conditions or deadlocks. Static analysis methods for this class of programs remain therefore more relevant than ever.

Pushdown Systems (PDSs) are a natural model for programs with sequential, recursive procedure calls, as shown by Esparza et al. in [EHRS00]. Thus, networks of pushdown systems can be used to model multithreaded programs, where each PDS in the network models a sequential component of the whole program. In this context, Dynamic Pushdown Networks (DPNs) were introduced by Bouajjani et al. in [BMOT05].

Intuitively, this class of automata consists of a network of pushdown systems running independently in parallel. Each member of a DPN can, after a transition, spawn a new PDS which is then introduced as a new member of the network. Thus, DPNs can be used to represent a network of threads where each thread can recursively call procedures, perform internal actions, or spawn a new thread.

However, this model cannot represent synchronization between different threads or parallel components. In order to handle communication in multithreaded programs, Bouajjani et al. introduced in [BET03] communicating pushdown systems (CPDSs), a model which consists of a tuple of pushdown systems synchronized by rendez-vous on execution paths. However, CPDSs have a constant number of processes and cannot therefore handle dynamic creation of new threads.

Hence, we introduce a more accurate model, namely, synchronized dynamic pushdown networks (SDPNs) that combines DPNs with CPDSs in order to handle dynamic thread creation and communication at the same time.

A SDPN can be seen as a DPN where PDS processes can synchronize via rendez-vous by sending and receiving messages. In a SDPN, pushdown processes can apply internal actions labeled by a letter $\tau$ without synchronization, just like a DPN, but can also synchronize through channels.

To do so, we represent each channel by a pair of letters, as an example $a$ and $\overline{a}$, that can be used to label transitions. If one thread can execute an action labeled with a signal $a$, and another thread another action labeled with $\overline{a}$, then both threads can synchronize and execute their respective transitions simultaneously, in a single step labeled by $\tau$.

We consider the reachability problem for SDPNs, that is, finding if a critical configuration can be reached from the set of starting configurations of the program. An equivalent problem is to compute the set $Paths(\mathcal{C},\mathcal{C^{\prime}})$ of execution paths leading from a configuration in $\mathcal{C}$ to a configuration in $C^{\prime}$ and check if it is empty. This problem unfortunately remains undecidable for synchronized pushdown systems, as proven by Ramalingam in [Ram00].

Therefore, the set of execution paths $Paths(C,C^{\prime})$ cannot be computed in an exact manner. To overcome this problem, we proceed in a manner similar to the method outlined in [BET03]: our approach is based on the computation of an abstraction $\alpha(Paths(\mathcal{C},\mathcal{C^{\prime}}))$ of the execution paths language. To this aim, we propose techniques based on:

• •

the representation of regular sets of configurations of SDPNs with finite word automata;

• •

the use of these automata to determine a set of constraints whose least fixpoint characterizes the set of execution paths of the program; to compute this set of constraints, (1) we consider a relaxed semantics on SDPNs that allows partially synchronized runs, (2) we abstract sets of execution paths as functions in a Kleene algebra, instead of simple elements of the abstract domain, and (3) we use a shuffle product on abstract path expressions to represent the interleaving and potential synchronization of parallel executions;

• •

the resolution of this set of constraints in an abstract domain; we consider in particular the case where the abstract domain is finite; the set of constraints can then be solved using an iterative fixpoint computation.

Note that the main contribution of our approach with regards to the methods outlined [BET03, Tou05] is the introduction of functions to represent sets of abstracted path expressions and the use of a shuffle product to model the interleaving of threads. The abstraction framework as defined in these papers cannot be applied to SDPNs due to the presence of dynamic thread creation, hence, the need for functions and shuffling.

We can then apply this over-approximation framework for the reachability problem to an iterative abstraction refinement scheme inspired by the work of Chaki et al. in [CCK*+*06]. The idea is the following: (1) we do a reachability analysis of the program, using a finite domain abstraction of order $n$ in our over-approximation framework; if the target set of configurations is not reachable by the abstract paths, it is not reachable by actual execution paths either; otherwise, we obtain a counter-example; (2) we check if the counter-example can be matched to an actual execution of the program; (3) if it does, then we have shown that the target set of configurations is actually reachable; (4) otherwise, we refine our abstraction and use instead a finite domain abstraction of order $n+1$ in step (2). This scheme is then used to prove that a Windows driver first presented in [QW04] can reach an erroneous configuration, using an abstraction of the original program. An updated version of this driver is then shown to be error-free.

This paper is a full, corrected version of [PT17].

Paper outline. In Section $1$ of this paper, we define synchronized dynamic pushdown networks (SDPNs). We study in Section $2$ the reachability problem for this class of automata. We introduce in Section $3$ an automata-theoretic representation of sets of paths, and prove in Section $4$ that the set of execution paths between two sets of configurations $C$ and $C^{\prime}$ of a SDPN is the least solution of a set constraints. Since we can’t solve these constraints, we present in Section $5$ an abstraction framework for paths based on Kleene algebras. In Section $6$, we apply this framework to over-approximate the reachability problem. In Section $7$, we present a iterative abstraction refinement scheme that relies on our abstraction framework and apply it to a model of an actual program in section $8$. Finally, we describe the related work in Section $9$ and show our conclusion in Section $10$.

1 Synchronized dynamic pushdown networks

1.1 Dynamic pushdown networks

We briefly introduce this class of automata:

Definition 1 (Bouajjani et al. [BMOT05])

A dynamic pushdown network (DPN) is a triplet $M=(P,\Gamma,\Delta)$ where $P$ is a finite set of control states, $\Gamma$ a finite stack alphabet disjoint from $P$, and $\Delta\subseteq(P\Gamma\times P\Gamma^{*})\cup(P\Gamma\times P\Gamma^{*}P\Gamma^{*})$ a finite set of transition rules featuring:

• •

simple pushdown operations in $(P\Gamma\times P\Gamma^{*})$ of the form $p\gamma\rightarrow p^{\prime}w$;

• •

thread spawns in $(P\Gamma\times P\Gamma^{*}P\Gamma^{*})$ of the form $p\gamma\rightarrow p_{1}w_{1}p_{2}w_{2}$.

Let $Conf_{M}=\left(P\Gamma^{*}\right)^{*}$ be the set of configurations of a DPN $M$. A configuration $p_{1}w_{1}\ldots p_{n}w_{n}$ represents a network of $n$ processes where the $i$-th process is in control point $p_{i}$ and has stack content $w_{i}$, as shown in Figure 1 where a single word in $Conf_{M}$ is used to represent the state of three PDSs in a network.

We define an immediate successor relation $\rightarrow_{M}$ on $Conf_{M}$ according to the following semantics:

• •

if $p\gamma\rightarrow p^{\prime}w$ in $\Delta$, then $\forall u,v\in Conf_{M}$, $\forall w^{\prime}\in\Gamma^{*}$, $up\gamma w^{\prime}v\rightarrow_{M}up^{\prime}ww^{\prime}v$; a thread applies a pushdown operation on its own stack, as shown in Figure 2;

• •

if $p\gamma\rightarrow p_{1}w_{1}p_{2}w_{2}$ in $\Delta$, then $\forall u,v\in Conf_{M}$, $\forall w^{\prime}\in\Gamma^{*}$, $up\gamma w^{\prime}v\rightarrow_{M}up_{1}w_{1}p_{2}w_{2}w^{\prime}v$; a thread spawns a new son with its own stack and control state, as shown in Figure 3.

Let $\rightarrow^{*}_{M}$ be the transitive and reflexive closure of this relation. Given a set $\mathcal{C}\subseteq Conf_{M}$ of configurations, we introduce its set of predecessors $pre^{*}(M,\mathcal{C})=\{c\in Conf_{M}\mid\exists c^{\prime}\in\mathcal{C},c\Rightarrow_{\mathcal{M}}c^{\prime}\}$. If $\mathcal{C}$ is regular, this set can be effectively computed:

Theorem 1.1 (Bouajjani et al. [BMOT05])

Given a DPN $M$ and a regular set of configurations $\mathcal{C}\subseteq Conf_{M}$, the set $pre^{*}(M,\mathcal{C})$ of predecessors is regular.

The saturation algorithm used to compute $pre^{*}(M,\mathcal{C})$ is detailled in Section 4.1.

1.2 The model and its semantics

We introduce a new model:

Definition 2

A synchronized dynamic pushdown Network (SDPN) is a tuple $M=(Act,P,\Gamma,\Delta)$ where $Act$ is a finite set of actions, $P$ a finite set of control states, $\Gamma$ a finite stack alphabet disjoint from $P$, and $\Delta\subseteq(P\Gamma\times Act\times P\Gamma^{*})\cup(P\Gamma\times Act\times P\Gamma^{*}P\Gamma^{*})$ a finite set of transition rules.

If $(p\gamma,a,w)\in\Delta$, $p\in P$, $\gamma\in\Gamma$, $a\in Act$, and $w\in P\Gamma^{*}\cup P\Gamma^{*}P\Gamma^{*}$, we write that $p\gamma\xrightarrow{a}w\in\Delta$. There are two types of transition rules in a SDPN:

• •

rules of the form $p\gamma\xrightarrow{a}p^{\prime}w$ in $P\Gamma\times Act\times P$ allow a pushdown process in the network to pop a symbol $\gamma$ from its stack, push a word $w$, then move from state $p$ to $p^{\prime}$; these rules are standard pushdown rules and model a thread calling or ending procedures while moving through its control flow;

• •

rules of the form $p\gamma\xrightarrow{a}p^{\prime\prime}w^{\prime}p^{\prime}w$ in $P\Gamma\times Act\times P\Gamma^{*}P\Gamma^{*}$ allow a pushdown process in the network to pop a symbol $\gamma$ from its stack, push a word $w$, move from state $p$ to $p^{\prime}$, then spawn a new pushdown process in state $p^{\prime\prime}$ and with initial stack $w^{\prime}$; these rules model dynamic creation of new threads.

We assume that the set $Act$ contains a letter $\tau$ that represents internal or synchronized actions, and that other letters in $Lab=Act\setminus\{\tau\}$ model synchronization signals. Moreover, to each synchronization signal $a$ in $Lab$, we can match an unique co-action $\overline{a}\in Lab$, such that $\overline{\overline{a}}=a$.

We introduce the set $Conf_{M}=\left(P\Gamma^{*}\right)^{*}$ of configurations of a SDPN $M$. In a manner similar to DPNs, a configuration $p_{1}w_{1}\ldots p_{n}w_{n}$ represents a network of $n$ processes where the $i$-th process is in control point $p_{i}$ and has stack content $w_{i}$.

1.2.1 The strict semantics.

We will model synchronization between threads as a form of communication by rendez-vous: two pushdown processes can synchronize if one performs a transition labelled with $a$ and the other, a transition labelled with $\overline{a}$. Intuitively, one thread sends a signal over a channel and the other thread waits for a signal to be received along the same channel.

To this end, we define a strict transition relation $\dashrightarrow_{M}$ on configurations of $M$ according to the following strict semantics:

(1)

given a symbol $a\in Act$, two rules $p\gamma\xrightarrow{a}w_{1}$ and $p^{\prime}\gamma^{\prime}\xrightarrow{\overline{a}}w^{\prime}_{1}$ in $\Delta$, and two configurations $u=u_{1}p\gamma u_{2}p^{\prime}\gamma^{\prime}u_{3}$ and $v=u_{1}w_{1}u_{2}w^{\prime}_{1}u_{3}$ of $M$, we have $u\dashrightarrow_{M}v$; two synchronized processes perform a simultaneous action, as shown in Figure 4;

(2)

given a rule $p\gamma\xrightarrow{\tau}w_{1}$ in $\Delta$ and two configurations $u=u_{1}p\gamma u_{2}$ and $v=u_{1}w_{1}u_{2}$ of $M$, we have $u\dashrightarrow_{M}v$; a process performs an internal action, as shown in Figure 5.

We say that $v$ is reachable from $u$ with regards to the strict semantics if $u\dashrightarrow^{*}_{M}v$, where $\dashrightarrow^{*}_{M}$ stands for the transitive closure of $\dashrightarrow_{M}$.

The strict semantics accurately model communication by rendez-vous. However, for technical matters, we also need to consider a relaxed semantics for SDPNs.

1.2.2 The relaxed semantics.

The relaxed semantics on SDPNs allows partially synchronized executions on a SDPN: a process can perform a transition labelled with $a\in Lab$ even if doesn’t synchronize with a matching process executing a transition labelled with $\overline{a}$.

We therefore introduce a relaxed transition relation $\rightarrow_{M}$ labelled in $Act$ on configurations of $M$:

(1) & (2)

given two configurations $u$ and $v$ of $M$, $u\dashrightarrow_{M}v$ if and only if $u\xrightarrow{\tau}_{M}v$; $\rightarrow_{M}$ features rules (1) and (2) of $\dashrightarrow_{M}$;

(3)

given a rule $p\gamma\xrightarrow{a}w_{1}$ in $\Delta$, a word $w_{1}\in(P\Gamma^{*})\cup(P\Gamma^{*})^{2}$, and two configurations $u=u_{1}p\gamma u_{2}$ and $v=u_{1}w_{1}u_{2}$ of $M$, we have $u\xrightarrow{a}_{M}v$; a process performs an action but does not synchronize, as shown in Figure 6.

The restriction of the relaxed semantics to rules (2) and (3) yields the DPN semantics, as defined by Bouajjani et al. in [BMOT05].

For a given word $\sigma=a_{1}\ldots a_{n}\in Act^{*}$ and two configurations $c$, $c^{\prime}$ of $M$, we write that $c\xrightarrow{\sigma}\!\!^{*}_{M}c^{\prime}$ if there are $n$ configurations $c_{1},\ldots,c_{n}$ of $M$ such that $c\xrightarrow{a_{1}}_{M}c_{1}\xrightarrow{a_{2}}_{M}c_{2}\ldots\xrightarrow{a_{n}}_{M}c_{n}$ and $c_{n}=c^{\prime}$. We then say that $c^{\prime}$ is reachable from $c$ with regards to the relaxed semantics. For a given set of configurations $C$, we introduce $pre^{*}(M,C)=\{c^{\prime}\mid\exists c\in C,\exists w\in\Gamma^{*},c^{\prime}\xrightarrow{w}\!\!^{*}_{M}c\}$.

For two subsets $C$ and $C^{\prime}$ of $Conf_{M}$, we define the set $Paths_{M}(C,C^{\prime})=\{\sigma\in Act^{*}\mid\exists c\in C,\exists c^{\prime}\in C^{\prime},c\xrightarrow{\sigma}\!\!^{*}_{M}c^{\prime}\}$ of all execution paths from $C$ to $C^{\prime}$, including paths with non-synchronized actions labelled in $Lab$.

1.3 From a program to a SDPN model

We can assume that the program is given by a control flow graph, whose nodes represent control points of threads or procedures and whose edges are labelled by statements. These statements can be variable assignments, procedure calls or returns, spawns of new threads, or communications between threads through unidirectional point-to point channels, where a thread sends a value $x$ through a channel $c$ and another thread waits for this value then assigns it to a variable $y$.

Without loss of generality, we assume that threads share no global variables and instead can only synchronize through channels. We distinguish local variables that belong to a single procedure from thread-local variables that can be accessed by any procedure called by a given instance of a thread. We also consider that both local and global variables may only take a finite number of values.

Given a control flow graph, we define a corresponding SDPN. The set of states $P$ is the set of all possible valuations of thread-local variables. The stack alphabet $\Gamma$ is the set of all pairs $(n,l)$ where $n$ is a node of the flow graph and $l$ is a valuation of the local variables of the current procedure.

Channels can be used to send and receive values. For each channel $c$ and value $x$ that can be sent through $c$, a label $(c!,x)$ and its co-action $(c?,x)=\overline{(c!,x)}$ belong to $Act$. The internal action $\tau$ belongs to $Act$ as well.

For each statement $s$ labelling an edge of the flow graph between nodes $n_{1}$ and $n_{2}$, we introduce the following transition rules in the corresponding SDPN, where $g_{1}$ and $g_{2}$ (resp. $l_{1}$ and $l_{2}$) are the valuations of thread-local (resp. procedure-local) variables before and after the execution of the statement:

• •

if $s$ is an assignment, rules of the form $g_{1}(n_{1},l_{1})\xrightarrow{\tau}g_{2}(n_{2},l_{2})$ represent $s$; assigning new values to variables in $g_{1}$ and $l_{1}$ results in new valuations $g_{2}$ and $l_{2}$;

• •

if $s$ is a procedure call, rules of the form $g_{1}(n_{1},l_{1})\xrightarrow{\tau}g_{2}(f_{0},l_{0})(n_{2},l_{2})$ represent $s$, where $f_{0}$ is the starting node of the called procedure and $l_{0}$ the initial valuation of its local variables;

• •

if $s$ is a procedure return, it is represented by rules of the form $g_{1}(n_{1},l_{1})\xrightarrow{\tau}g_{2}\varepsilon$; we simulate returns of values by introducing an additional thread-local variable and assigning the return value to it in the valuation $g_{2}$;

• •

if $s$ is a thread spawn, it is represented by rules of the form $g_{1}(n_{1},l_{1})\xrightarrow{\tau}g_{0}(n_{0},l_{0})g_{2}(n_{2},l_{2})$, where $g_{0}$ and $l_{0}$ are respectively the initial valuations of the thread-local and procedure-local variables of the new thread, and $n_{0}$ its starting node;

• •

if $s$ is an assignment of a value $x$ carried through a channel $c$ to a variable $y$, it is represented by rules of the form $g_{1}(n_{1},l_{1})\xrightarrow{(c?,x)}g_{2}(n_{2},l_{2})$ where $g_{1}$ and $g_{2}$ (resp. $l_{1}$ and $l_{2}$) are such that assigning the value $x$ to the variable $y$ in $g_{1}$ (resp. $l_{1}$) results in the new valuations $g_{2}$ (resp. $l_{2}$);

• •

if $s$ is an output through a channel $c$ of the value $x$ of a variable $y$, it is represented by rules of the form $g_{1}(n_{1},l_{1})\xrightarrow{(c!,x)}g_{2}(n_{2},l_{2})$ such that the variable $y$ has value $x$ in either $g_{1}$ or $l_{1}$.

Finally, we consider the starting configuration $g_{init}(n_{init},l_{init})$ where $g_{init}$ and $l_{init}$ are respectively the initial valuations of the thread-local and procedure-local variables of the main thread, and $n_{init}$ its starting node.

2 The reachability problem

As described previously in section 1.3, we can model the behaviour of a real multi-threaded program with a SDPN. Many static analysis techniques rely on being able to determine whether a given critical state is reachable or not from the starting configuration of a program.

Since checking reachability in a real program amounts to checking reachability in its corresponding SDPN w.r.t to the strict semantics, we want to solve the following reachability problem: given a SDPN $M$ and two sets of configuration $C$ and $C^{\prime}$, is there a configuration in $C^{\prime}$ that is reachable from $C$ with regards to the strict semantics?

It has unfortunately been proven by Ramalingam in [Ram00] that, even if $C$ and $C^{\prime}$ are regular, this problem is undecidable for synchronization sensitive pushdown systems, hence, SDPNs. Therefore, we reduce this problem to an execution path analysis of SDPNs with relaxed semantics.

2.1 From the strict to the relaxed semantics

It is easy to see that the following theorem holds:

Theorem 2.1

Let $M$ be a SDPN and $c$, $c^{\prime}$ two configurations of $M$; $c\dashrightarrow^{*}_{M}c^{\prime}$ if and only if $\exists n\geq 0$ such that $c\xrightarrow{\tau^{n}}\!\!^{*}_{M}c^{\prime}$.

Intuitively, an execution path with regards to the relaxed semantics of the form $\tau^{n}$ only uses internal actions or synchronized actions between two threads: a synchronization signal $a$ is always paired with its co-action $\overline{a}$. Any configuration reachable using this path can be reached with regards to the strict semantics as well. Such a path is said to be perfectly synchronized.

Therefore, the reachability problem amounts to determining whether:

[TABLE]

that is, if there is an execution path from $C$ to $C^{\prime}$ with regards to the relaxed semantics of the form $\tau^{n}$. Obviously, we can’t always compute $Paths_{M}(C,C^{\prime})$. Our idea is therefore to compute an abstraction (over-approximation) of the set $Paths_{M}(C,C^{\prime})$ and check the emptiness of its intersection with $\tau^{*}$: if it is indeed empty, then $C^{\prime}$ can’t be reached from $C$ with regards to the strict semantics.

It is worth noting that a configuration $p^{\prime}_{1}w^{\prime}_{1}p^{\prime}_{2}w^{\prime}_{2}$ reachable from $p_{1}w_{1}p_{2}w_{2}$ with regards to the strict semantics by synchronizing two rules $p_{1}w_{1}\xrightarrow{a}p^{\prime}_{1}w^{\prime}_{1}$ and $p_{2}w_{2}\xrightarrow{\overline{a}}p^{\prime}_{2}w^{\prime}_{2}$ using the synchronization rule (1) can obviously be reached with regards to the relaxed semantics by applying these two rules sequentially, using rule (3) twice, although the resulting path would obviously not be perfectly synchronized. Hence, the following theorem holds:

Theorem 2.2

Let $M$ be a SDPN and $c$, $c^{\prime}$ two configurations of $M$; $c^{\prime}$ is reachable from $c$ w. r. t. the relaxed SDPN semantics if and only if it is reachable w. r. t. the DPN semantics.

It implies that, since we can compute $pre^{*}(M,C)$ with regards to the DPN semantics thanks to Theorem 1.1, we can compute it with regards to the relaxed SDPN semantics as well.

2.2 Representing infinite sets of configurations

In order to compute an abstraction of $Paths_{M}(C,C^{\prime})$ we need to be able to finitely represent infinite sets of configurations of a SDPN $M$. To do so, we introduce a class of finite automata called $M$-automata:

Definition 3 (Bouajjani et al. [BMOT05])

Given a SDPN $M=(Act,P,\linebreak\Gamma,\Delta)$, an $M$-automaton is a finite automaton $A=(\Sigma,S,\delta,s_{init},F)$ such that:

• •

$\Sigma=P\cup\Gamma$ is the input alphabet;

• •

the set of states $S=S_{C}\cup S_{S}$ can be partitioned in two disjoint sets $S_{C}$ and $S_{S}$;

• •

$\delta\subseteq S\times\Sigma\times S$ is the set of transitions;

• •

$\forall s\in S_{C}$ and $\forall p\in P$, there is at most a single state $s_{p}$ such that $(s,p,s_{p})\in\delta$; moreover, $s_{p}\in S_{S}$ and $s$ is the only predecessor of $s_{p}$; transitions from states in $S_{C}$ are always labelled with state symbols in $P$ and go to dedicated states in $S_{S}$;

• •

states in $S_{C}$ do not have exiting transitions labelled with letters in $\Gamma$;

• •

states in $S_{S}$ do not have exiting transitions labelled in $P$; transitions labelled with letters in $\Gamma$ always go to states in $S_{S}$;

• •

transitions from $S_{S}$ to $S_{C}$ are always labelled with $\varepsilon$; these are the only allowed $\varepsilon$-transitions in the $M$-automaton;

• •

$s_{init}\in S_{C}$ is the initial state;

• •

$F\subseteq S_{C}$ is the set of final states.

An $M$-automaton is designed in such a manner that every path accepting a configuration $p_{1}w_{1}\ldots p_{n}w_{n}$ is a sequence of sub-paths $s_{i}\xrightarrow{p_{i}}_{\delta}s_{p}\xrightarrow{w_{i}}\!\!^{*}_{\delta}q\xrightarrow{\varepsilon}_{\delta}s_{i+1}$ where $s_{i}\in S_{C}$, $s_{i+1}\in S_{C}$ and every state in the path $s_{p}\xrightarrow{w_{i}}\!\!^{*}_{\delta}q$ is in $S_{S}$. Being a finite state automaton, an $M$-automaton accepts a regular language that is a subset of $Conf_{M}$. Any regular language in $(P\Gamma^{*})^{*}$ can be accepted by an $M$-automaton, as shown in Figure 7.

$M$-automata were introduced so that one could compute the set of predecessors of a DPN, hence, of a SDPN as well, by applying a saturation procedure to an $M$-automaton accepting the set of starting configurations, as shown by Bouajjani et al. in [BMOT05].

3 Representing the set of paths

In this section, we introduce an automata-theoretic representation of sets of synchronized paths by adding extra labels to $M$-automata.

3.1 $\Pi$-configurations

Let $\Pi=2^{Act^{*}}$ be the set of all possible languages on $Act$. We define a $\Pi$-configuration of $M$ as a pair $(c,\pi)\in Conf_{M}\times Act^{*}$. We can extend the transition relation $\longrightarrow_{M}$ to $\Pi$-configurations with the following semantics: $\forall a\in Act$, if $c\xrightarrow{a}_{M}c^{\prime}$, then $\forall\pi\in Act^{*}$, $(c,a\cdot\pi)\longrightarrow_{M,\Pi}(c^{\prime},\pi)$. The configuration $(c,a\cdot\pi)$ is said to be an immediate $\Pi$-predecessor of $(c^{\prime},\pi)$. The reachability relation $\leadsto_{M,\Pi}$ is the reflexive transitive closure of the relation $\longrightarrow_{M,\Pi}$.

Given a set of configurations $C$, we introduce the set of $\Pi$-predecessors $pre_{\Pi}^{*}(M,C)$ of all $\Pi$-configurations $(c^{\prime},\pi)\in Conf_{M}\times Act^{*}$ such that $(c^{\prime},\pi)\linebreak\leadsto_{M,\Pi}(c,\varepsilon)$ for $c\in C$. Obviously, we have:

[TABLE]

Intuitively, $(c^{\prime},\pi)$ is in $pre_{\Pi}^{*}(M,C)$ if one can reach a configuration $c\in C$ from $c^{\prime}$ by following a path $\pi$.

3.2 The shuffle product

Assuming we know the path languages of two different threads, we want to compute the path language of these two threads running in parallel.

Intuitively, this new language will be an interleaving of the two aforementioned sets, but can feature synchronized actions between the two threads as well.

To this end, we define inductively a shuffle operation $\shuffle:Act^{*}\times Act^{*}\rightarrow\Pi$ such that, given two paths, their shuffle product is the set of all possible interleaving (with synchronization) of these paths.

Let $w=a_{1}\ldots a_{n}$ and $w^{\prime}=b_{1}\ldots b_{m}$ be two such paths:

• •

$w\shuffle\varepsilon=\varepsilon\shuffle w=\{w\}$;

• •

if $b_{1}\neq\overline{a_{1}}$, then: $w\shuffle w^{\prime}=a_{1}\cdot[(a_{2}\ldots a_{n})\shuffle(b_{1}\ldots b_{m})]\cup b_{1}\cdot[(a_{1}\ldots a_{n})\shuffle(b_{2}\ldots b_{m})]$;

• •

if $b_{1}=\overline{a_{1}}$, then: $w\shuffle w^{\prime}=a_{1}\cdot[(a_{2}\ldots a_{n})\shuffle(b_{1}\ldots b_{m})]\cup b_{1}\cdot[(a_{1}\ldots a_{n})\shuffle(b_{2}\ldots b_{m})]\cup\tau\cdot[(a_{2}\ldots a_{n})\shuffle(b_{2}\ldots b_{m})]$; two synchronized actions $a_{1}$ and $\overline{a_{1}}$ result in an internal action $\tau$, hence, there is a component $\tau\cdot(w_{1}\shuffle w_{2})$ of the shuffle product where the two paths synchronize.

The shuffle operation is obviously commutative and associative, as outlined in [lot97]. We can extend naturally the operation $\shuffle$ to sets of paths: $\kappa_{1}\shuffle\kappa 2=\mathop{\bigcup}\limits_{\pi_{1}\in\kappa_{1},\pi_{2}\in\kappa_{2}}(\pi_{1}\shuffle\pi_{2})$. It is still commutative and associative.

3.3 $\Pi$-automata

We represent sets of $\Pi$-configurations of a SDPN $M$ with a class of labelled $M$-automata, called $\Pi$-automata.

Definition 4

Let $M=(Act,P,\Gamma,\Delta)$ be a SDPN, a $\Pi$-automaton is a finite automaton $A=(\Sigma,S,\delta,s_{init},F)$ where $\Sigma=P\cup\Gamma$ is the input alphabet, $S=S_{C}\cup S_{S}$ is a finite set of control states with $S_{C}\cap S_{S}=\emptyset$, $\delta\subseteq(S_{C}\times P\times S_{S})\cup(S_{S}\times\Gamma\times\Pi^{\Pi}\times S_{S})\cup(S_{S}\times\{\varepsilon\}\times S_{C})$ a finite set of transition rules (where $\Pi^{\Pi}$ is the set of functions from $\Pi$ to $\Pi$), $s_{init}$ an initial state, and $F$ a set of final states.

Moreover, $A$ is such that, if we consider the projection $\delta_{\Sigma}$ of $\delta$ on $S\times\Sigma^{*}\times S$, ignoring labels in $\Pi^{\Pi}$, then $(\Sigma,S,\delta_{\Sigma},s_{init},F)$ is a $M$-automaton.

Intuitively, a $\Pi$-automaton can be seen as an $M$-automaton whose transitions labelled by stack symbols in $\Gamma$ have been given an additional label in $\Pi^{\Pi}$. We can consider a simple $M$-automaton as a $\Pi$-automaton if we label each transition in $S_{S}\times\Gamma\times S_{S}$ with the identity function.

While it would be simpler to label transitions of a $M$-automaton with elements of $\Pi$, this representation would be flawed for the purpose of the algorithms outlined in Section 4.2. The intuition behind the use of functions in $\Pi^{\Pi}$ as labels is detailed there.

3.3.1 The transition relation.

Let $A$ be a $\Pi$-automaton. We define a simple transition relation $\longrightarrow_{A}$ according to the following semantics:

• •

if $(s,p,s^{\prime})\in\delta\cap(S\times(P\cup\{\varepsilon\})\times S)$, then $s\xrightarrow{p}_{A}s^{\prime}$;

• •

if $(s,\gamma,e,s^{\prime})\in\delta\cap(S_{S}\times\Gamma\times\Pi^{\Pi}\times S_{S})$, then $s\xrightarrow{(\gamma,e)}_{A}s^{\prime}$;

• •

if $s\xrightarrow{(w_{1},e_{1})}_{A}s_{1}$ and $s_{1}\xrightarrow{(w_{2},e_{2})}_{A}s^{\prime}$, then $s\xrightarrow{(w_{1}w_{2},e_{1}\circ e_{2})}_{A}s^{\prime}$, where $\circ$ is the composition operation on functions.

We then extend inductively this transition relation to a full path relation $\Longrightarrow_{A}\subseteq S\times\Sigma^{*}\times\Pi^{\Pi}\times S$:

• •

for each $s\in S_{S}$, $s\xRightarrow{(\varepsilon,Id)}_{A}s$, where $Id$ stands for the identity function;

• •

if there is a sequence $s_{0}\xrightarrow{(\gamma_{1},e_{1})}_{A}s_{1}\ldots s_{n-1}\xrightarrow{(\gamma_{n},e_{n})}_{A}s_{n}$ with $s_{0},\ldots,s_{n}\in S_{S}$, then $s_{0}\xRightarrow{(w,e)}_{A}s_{n}$, where $w=\gamma_{1}\ldots\gamma_{n}$ and $e=e_{1}\circ\ldots\circ e_{n}$; this is a simple sequence of actions along a single thread;

• •

if there is a sequence $s\xrightarrow{p_{1}}_{A}s_{p_{1}}\xRightarrow{(w_{1},e_{1})}_{A}q\xrightarrow{\varepsilon}_{A}s^{\prime}\xrightarrow{p_{2}}_{A}s^{\prime}_{p_{2}}\xRightarrow{(w_{2},e_{2})}_{A}q^{\prime}$ such that $q^{\prime},q\in S_{S}$ and $s,s^{\prime}\in S_{C}$, then $s\xRightarrow{(w,e)}_{A}q$, where $w=p_{1}w_{1}p_{2}w_{2}$ and $e:y\longrightarrow e_{1}(\{\varepsilon\})\shuffle e_{2}(y)$; the automaton represents two parallel processes $p_{1}w_{1}$ and $p_{2}w_{2}$ whose abstract execution paths must be shuffled; moreover, since the first process will no longer be extended by further transitions of the automaton, we get rid of the variable of $e_{1}$ by considering $e_{1}(\{\varepsilon\})$ instead.

Note that this path relation is well-defined because $\shuffle$ is associative.

A path $s_{0}\xRightarrow{(c,e)}_{A}s_{n}$ is said to be an execution of $A$ if $s_{0}=s_{init}$. It is then said to be accepting if $s_{n}\in F$. We then say that $A$ accepts $(c,\pi)$ for all $\pi\in\Pi$ such that $\pi\in e(\{\varepsilon\})$. This way, accepting execution paths in $\Pi$-automata can be used to represent whole sets of paths. We define the set $L_{\Pi}(A)$ of all $\Pi$-configurations of $M$ accepted by $A$.

4 Characterizing the set of paths

Let $C$ be a regular set of configurations of a SDPN $M=(Act,P,\Gamma,\Delta)$. We want to define a $\Pi$-automaton $A_{pre_{\Pi}^{*}}$ accepting $pre_{\Pi}^{*}(M,C)$. Our intuition is to add extra labels in $\Pi^{\Pi}$ to the $M$-automaton accepting $pre^{*}(M,C)$.

4.1 Computing $pre^{*}(M,C)$

Given a SDPN $M$ and a regular set $C$ of configurations of $M$ accepted by an $M$-automaton $A$, we want to compute an $M$-automaton $A_{pre^{*}}$ accepting $pre^{*}(M,C)$. Thanks to Theorem 2.2, we can apply the saturation procedure defined in [BMOT05] to $A$. Let us remind this procedure. Initially, $A_{pre^{*}}=A$, then we apply the following rules until saturation to $A_{pre^{*}}$:

$(R_{1})$

if $p\gamma\xrightarrow{a}p^{\prime}w\in\Delta$ and $s\xrightarrow{p^{\prime}w}\!\!^{*}_{A_{pre^{*}}}s^{\prime}$ for $s\in S_{S}$, $s^{\prime}\in S$, then add $s_{p}\xrightarrow{\gamma}\!\!^{*}_{A_{pre^{*}}}s^{\prime}$;

$(R_{2})$

if $p\gamma\xrightarrow{a}p_{1}\gamma_{1}p_{2}\gamma_{2}\in\Delta$ and $s\xrightarrow{p_{1}\gamma_{1}p_{2}\gamma_{2}}\!\!^{*}_{A_{pre^{*}}}s^{\prime}$ for $s\in S_{S}$, $s^{\prime}\in S$, then add $s_{p}\xrightarrow{\gamma}\!\!^{*}_{A_{pre^{*}}}s^{\prime}$.

$\longrightarrow^{*}_{A_{pre^{*}}}$ stands for the transitive closure of the transition relation on the finite state automaton $A_{pre^{*}}$. The initial and final states remain the same.

Let us remind the intuition of these rules. We consider a sub-path $s\xrightarrow{p^{\prime}w}\!\!^{*}_{A_{pre^{*}}}s^{\prime}$. By design of an $M$-automaton, $s$ should be in $S_{C}$ and there should be a path $s\xrightarrow{p^{\prime}}s_{p^{\prime}}\xrightarrow{w}\!\!^{*}s^{\prime}$ in the automaton. If we apply the saturation rule $(R_{1})$, we add an edge $s_{p}\xrightarrow{p}s^{\prime}$ to $A_{pre^{*}}$ and create a sub-path $s\xrightarrow{p\gamma}\!\!^{*}s^{\prime}$ in the automaton. Therefore, if $A_{pre^{*}}$ accepts a configuration $u_{1}p^{\prime}w^{\prime}u_{2}$ with a path $s_{init}\xrightarrow{u_{1}}\!\!^{*}s_{p^{\prime}}\xrightarrow{p^{\prime}w}\!\!^{*}s^{\prime}\xrightarrow{u_{2}}\!\!^{*}q_{F}$, $q_{F}\in F$, then it will accept its predecessor $u_{1}p\gamma u_{2}$ as well with a path $s_{init}\xrightarrow{u_{1}}\!\!^{*}s_{p}\xrightarrow{p\gamma}\!\!^{*}s^{\prime}\xrightarrow{u_{2}}\!\!^{*}q_{F}$. The role of $(R_{2})$ is similar.

Thus, when this saturation procedure ends, the $M$-automaton $A_{pre^{*}}$ accepts the regular set $pre^{*}(M,C)$.

4.2 From $pre^{*}(M,C)$ to $pre^{*}_{\Pi}(M,C)$

Given a SDPN $M$ and a regular set $C$ of configurations of $M$ accepted by an $M$-automaton $A$, we want to compute a $\Pi$-automaton $A_{pre^{*}_{\Pi}}$ accepting $pre^{*}_{\Pi}(M,C)$. To this end, we will add new labels to the $M$-automaton $A_{pre^{*}}$. Our intuition is the following: $A_{pre_{\Pi}^{*}}$ should be such that if we have $(c^{\prime},\pi)\leadsto_{M,\Pi}(c,\varepsilon)$, $c\in C$, then $c$ can be reached from $c^{\prime}$ by a path $\pi$.

In order to compute $A_{pre_{\Pi}^{\pi}}$, we proceed as follows: we first accept configurations in $C$ with the path $\varepsilon$, then, from there, set constraints on the labelling functions of transitions of $A_{pre^{*}}$ depending on the relationship between edges introduced by the previous saturation procedure. This way, we build iteratively a set of constraints whose least solution is the set of execution paths from $pre^{*}(M,C)$ to $C$.

To this end, each transition $t$ in $A_{pre^{*}}$ labelled in $\Gamma$ is given a second label $\lambda(t)\in\Pi^{\Pi}$. To do so, we compute a set of constraints whose smallest solution (according to the order $\subseteq$ of the language lattice) will be the labels $\lambda(t)$. If $t=q_{1}\xrightarrow{\gamma}q_{2}$, then we write $\lambda(t)=\lambda(q_{1},\gamma,q_{2})$.

4.2.1 The need for functions.

We will explain intuitively here why we label the automaton with functions and not with sets of paths in $\Pi$.

Let us consider a $M$-automaton labelled by sets of paths as shown in Figure 8. To a thread in configuration $p_{1}\gamma_{1}$, we match a set $\{a\}$ and to a thread in $p_{2}\gamma_{2}\gamma_{3}$, we match $\{b,c\}$. We assume there is a rule $p\gamma\xrightarrow{d}p_{1}\gamma_{1}p_{2}\gamma_{2}$ in $M$. By applying a saturation rule of the algorithm outlined in the previous section, we add a new dotted transition ${s_{1}}_{p}\xrightarrow{\gamma}q_{2}$. Intuitively, we label it with $d\cdot(\{a\}\shuffle\{b\})=\{dab,dba\}$: the label of the spawn action, followed by the synchronization of the paths matched to the two resulting threads.

However, assuming semantics similar to $\Pi$-automata, the automaton in Figure 8 would accept the configuration $(p\gamma\gamma_{3},\{dabc,dbac\})$ by going through states $s_{1}$, $p_{1}$, $q_{2}$, and $q_{3}$. But intuitively, we want to accept the set $\{dabc,dbac,dbca\}=d\odot(\{a\}\shuffle\{bc\})$ instead, as the action $c$ can appear before $a$ in the interleaving of the execution paths matched to the two threads.

We can consider instead the $\Pi$-automaton shown in Figure 9. The new dotted transition is labelled by the function $x\rightarrow d\cdot[a\shuffle(b\cdot x)]=\{dabx,dbax,dbxa\}$. The variable $x$ stands for the end of the paths matched to the second thread (in this case, the action $c$) that are not examined by the saturation rule but would nonetheless have to be shuffled with the path $a$ of the first thread.

The automaton in Figure 9 has an execution path labelled by $(p\gamma\gamma_{3},f:x\rightarrow\{dabcx,dbacx,dbcxa\})$ when it goes through states $s_{1}$, $p_{1}$, $q_{2}$, and $q_{3}$. Therefore, it accepts all the paths $f(\{\varepsilon\})=\{dabc,dbac,dbca\}$.

4.2.2 The constraints.

For two functions in $\Pi^{\Pi}$, we write that $f\subseteq g$ if $\forall x\in\Pi$, $f(x)\subseteq g(x)$. We now consider the following set of constraints on the labels of transitions of $A_{pre^{*}}$ in $S_{S}\times\Gamma\times S_{S}$, where $Q$ is the set of states of $A$:

$(Z_{1})$

if $t$ belongs to $A$, then:

[TABLE]

$(Z_{2})$

for each rule $p\gamma\xrightarrow{a}p^{\prime}\gamma^{\prime}\in\Delta$, for each $q\in Q$, for each $s\in S_{c}$:

[TABLE]

$(Z_{3})$

for each rule $p\gamma\xrightarrow{a}p^{\prime}\varepsilon\in\Delta$, for each $s\in S_{c}$:

[TABLE]

$(Z_{4})$

for each rule $p\gamma\xrightarrow{a}p^{\prime}\gamma_{1}\gamma_{2}\in\Delta$, for each $q\in Q$, for each $s\in S_{c}$:

[TABLE]

$(Z_{5})$

for each rule $p\gamma\xrightarrow{a}p_{2}\gamma_{2}p_{1}\gamma_{1}\in\Delta$, for each $q\in Q$, for each $s\in S_{c}$:

[TABLE]

In a manner similar to [BET05], we eventually define the labels of $A_{pre_{\Pi}^{*}}$ as the least solution of the set of constraints outlined above in the complete lattice of functions in $\Pi^{\Pi}$. By Tarski Theorem, this solution exists. The following theorem holds:

Theorem 4.1

Let $M$ be a SDPN and $A$ an $M$-automaton accepting a regular set of configurations $C$. Then the $\Pi$-automaton $A_{pre_{\Pi}^{*}}$ accepts the set $pre_{\Pi}^{*}(M,C)$.

Note that it doesn’t mean we can compute the labels: an iterative computation of the least solution may not terminate. We now explain intuitively the meaning of these constraints.

4.2.3 The intuition.

If $c$ is a configuration of $C$, then $A_{pre^{*}_{\Pi}}$ should accept $(c,\varepsilon)$. This is expressed by constraint $(Z_{1})$.

Let $c^{\prime}=p^{\prime}\gamma^{\prime}w\in pre^{*}(M,C)$. If $p\gamma\xrightarrow{a}p^{\prime}\gamma^{\prime}\in\Delta$ and $(c^{\prime},\pi)\in pre^{*}_{\Pi}(M,C)$, then $c=p\gamma w\in pre^{*}(M,C)$, $(c,a\cdot\pi)\leadsto_{M,\Pi}(c^{\prime},\pi)$, and $(c,a\cdot\pi)\in pre^{*}_{\Pi}(M,C)$. Hence, if $A_{pre^{*}_{\Pi}}$ accepts $(c^{\prime},\pi)$ and uses a transition $s_{p^{\prime}}\xrightarrow{\gamma^{\prime}}q$ while doing so, then it should accept $(c,a\cdot\pi)$ as well using a transition $s_{p}\xrightarrow{\gamma}q$, as shown in Figure 10. This is expressed by constraint $(Z_{2})$.

Let $c^{\prime}=p^{\prime}w\in pre^{*}(M,C)$. If $p\gamma\xrightarrow{a}p^{\prime}\varepsilon\in\Delta$ and $(c^{\prime},\pi)\in pre^{*}_{\Pi}(M,C)$, then $c=p\gamma w\in pre^{*}(M,C)$, $(c,a\cdot\pi)\leadsto_{M,\Pi}(c^{\prime},\pi)$, and $(c,a\cdot\pi)\in pre^{*}_{\Pi}(M,C)$. Hence, if $A_{pre^{*}_{\Pi}}$ accepts $(c^{\prime},\pi)$, then it should accept $(c,a\cdot\pi)$ as well using a transition $s_{p}\xrightarrow{\gamma}s^{\prime}_{p}$, as shown in Figure 11. This is expressed by constraint $(Z_{3})$.

Let $c^{\prime}=p^{\prime}\gamma_{1}\gamma_{2}w\in pre^{*}(M,C)$. If $p\gamma\xrightarrow{a}p^{\prime}\gamma_{1}\gamma_{2}\in\Delta$ and also $(c^{\prime},\pi)\in pre^{*}_{\Pi}(M,C)$, then $c=p\gamma w\in pre^{*}(M,C)$, $(c,a\cdot\pi)\leadsto_{M,\Pi}(c^{\prime},\pi)$, and $(c,a\cdot\pi)\in pre^{*}_{\Pi}(M,C)$. Hence, if $A_{pre^{*}_{\Pi}}$ accepts $(c^{\prime},\pi)$ and uses two transition $s_{p^{\prime}}\xrightarrow{\gamma_{1}}q^{\prime}$ and $q^{\prime}\xrightarrow{\gamma_{2}}q$ while doing so, then it should accept $(c,a\cdot\pi)$ as well using a transition $s_{p}\xrightarrow{\gamma}q$, as shown in Figure 12. Moreover, there can be many possible intermediate states $q^{\prime}$ between $s^{\prime}_{p}$ and $q$ such that $s_{p^{\prime}}\xrightarrow{\gamma_{1}}q^{\prime}$ and $q^{\prime}\xrightarrow{\gamma_{2}}q$. In the automaton $A_{pre^{*}_{\Pi}}$, the path $\pi$ should therefore be represented by the union for all possible intermediate state $q^{\prime}$ of the concatenation of the two labelling functions $\lambda(s_{p^{\prime}},\gamma_{1},q^{\prime})$ and $\lambda(q^{\prime},\gamma_{2},q)$. This is expressed by constraint $(Z_{4})$.

Let $c^{\prime}=p_{2}\gamma_{2}p_{1}\gamma_{1}w\in pre^{*}(M,C)$. If $p\gamma\xrightarrow{a}p_{2}\gamma_{2}p_{1}\gamma_{1}\in\Delta$ and $(c^{\prime},\pi)\in pre^{*}_{\Pi}(M,C)$, then $c=p\gamma w\in pre^{*}(M,C)$, $(c,a\cdot\pi)\leadsto_{M,\Pi}(c^{\prime},\pi)$, and $(c,a\cdot\pi)\in pre^{*}_{\Pi}(M,C)$, as shown in Figure 13. The two processes $p_{2}\gamma_{2}$ (thread 2 in 13) and $p_{1}\gamma_{1}$ (thread 1 in 13) are interleaved, hence, their execution paths must be shuffled: if $\pi_{1}$ is an execution path associated to $p_{1}\gamma_{1}$, and $\pi_{2}$, to $p_{2}\gamma_{2}$, then an path $\pi^{\prime}=\pi_{2}\shuffle\pi_{1}$ should be associated to $p_{2}\gamma_{2}p_{1}\gamma_{1}$. Moreover, if we consider a path $s_{p_{2}}\xrightarrow{\gamma_{2}}s^{\prime\prime}\xrightarrow{\varepsilon}s^{\prime}\xrightarrow{p_{1}}s^{\prime}_{p_{1}}\xrightarrow{\gamma_{1}}q$ in the automaton $A_{pre^{*}_{\Pi}}$, then no path $\pi_{2}$ associated to $p_{2}\gamma_{2}$ can be extended further, and should therefore be represented by $(\lambda(s_{p_{2}},\gamma_{2},s^{\prime})(\{\varepsilon\}))$. Again, we must also consider each possible intermediate state $s^{\prime\prime}$ in the previous path, hence, an union of functions. This is expressed by constraint $(Z_{5})$.

4.3 Proof of Theorem 4.1

In order to prove Theorem 4.1, we first show that $A_{pre_{\Pi}^{*}}$ accepts every $\Pi$ predecessor of $C$.

Lemma 1

We consider $c=p_{1}v_{1}\ldots p_{n}v_{n}\in C$, $s_{init}$ the initial state of $A$, and $F$ its set of final states. If $(c^{\prime}=(p^{\prime}_{1}w_{1}\ldots p^{\prime}_{l}w_{l}),\pi)\leadsto_{M,\Pi}(c,\varepsilon)$ for $\pi\in\Pi_{\Pi}$, then $\exists e\in\Pi^{\Pi}$ and $q_{F}\in F$ such that $\pi\leq e(\varepsilon)$ and $s_{init}\xRightarrow{(c^{\prime},e)}_{A_{pre_{\Pi}^{*}}}q_{F}$.

We then prove that every configuration accepted by $A_{pre_{\Pi}^{*}}$ is a $\Pi$ predecessor of $C$.

Lemma 2

$\forall\pi\in Act^{*}$, if there is an accepting execution $s_{init}\xRightarrow{(c^{\prime},e)}_{A_{pre_{\Pi}^{*}}}q_{F}$ such that $c^{\prime}=(p^{\prime}_{1}w^{\prime}_{1}\ldots p^{\prime}_{n}w^{\prime}_{n})$ and $\pi\leq e(\{\varepsilon\})$, there is a configuration $c$ such that $s_{init}\overset{c}{\rightarrow}_{A}q_{F}\in F$ and $(c^{\prime},\pi)\leadsto_{M,\Pi}(c,\varepsilon)$.

4.3.1 Proof of Lemma 1

We can expand the labelling of functions to paths by composing labels along the paths, in a manner similar to the semantics of $\Pi$-automata. Hence, $\lambda(s,w,q)$ is such that $s\xRightarrow{(w,\lambda(s,w,q))}_{A}q$.

We prove by induction on $k$ that if $c^{\prime}=((p^{\prime}_{1}w^{\prime}_{1}\ldots p^{\prime}_{l}w^{\prime}_{l}),\pi)\rightarrow^{k}_{M,\Pi}(c,\varepsilon)$, then $\exists e\in\Pi^{\Pi}$ and $q_{F}\in F$ such that $\pi\in e(\{\varepsilon\})$ and $s_{init}\xRightarrow{(c,e)}_{A_{pre_{\Pi}^{*}}}q_{F}$.

Basis:

if $k=0$, then $c^{\prime}=c$, and $\pi=\varepsilon$. Because of constraint $(Z_{1})$, each transition $t$ that exists both in $A$ and $A_{pre_{\Pi}^{*}}$ is such that $Id\subseteq\lambda(t)$. Hence, if we follow an accepting execution $s_{init}\xRightarrow{(c,e)}_{A_{pre_{\Pi}^{*}}}q_{F}$ only using transitions in $A$, it must be such that $\varepsilon\in e(\{\varepsilon\})$. Hence, $A_{pre_{\Pi}^{*}}$ accepts $(c,\varepsilon)$.

Induction step:

we consider $(c_{1}=(p^{\prime\prime}_{1}u_{1}\ldots p^{\prime\prime}_{j}u_{j}),\pi^{\prime})$ such that $(c^{\prime},\pi)\leadsto_{M,\Pi}(c_{1},\pi^{\prime})$ and $(c_{1},\pi^{\prime})\leadsto^{k}_{M,\Pi}(c,\varepsilon)$. We have the two following cases:

• •

if $j=l+1$, a new process has been created from $c^{\prime}$ to $c_{1}$ by a rule of the form $r=p^{\prime}_{i}\gamma\xrightarrow{a}p^{\prime\prime}_{i}u_{i}p^{\prime\prime}_{i+1}u^{\prime}_{i+1}$. Then, there are $t_{1}$, $t_{2}$ in $(P\Gamma^{*})^{*}$ such that $c_{1}=t_{1}p^{\prime\prime}_{i}u_{i}p^{\prime\prime}_{i+1}u_{i+1}t_{2}$ and $c^{\prime}=t_{1}p^{\prime}_{i}w^{\prime}_{i}t_{2}$, and there is $u\in\Gamma^{*}$ such that $w^{\prime}_{i}=\gamma u$ and $u_{i+1}=u^{\prime}_{i+1}u$.

By induction, as shown in figure 14, there is a path in $A_{pre_{\Pi}^{*}}$ such that it accepts $(c_{1},\pi^{\prime})$ and $\pi^{\prime}\in\lambda_{1}(\{\varepsilon\})\shuffle\lambda_{2}(\{\varepsilon\})\shuffle\lambda_{3}\circ\lambda_{4}(\{\varepsilon\})\shuffle\lambda_{5}(\{\varepsilon\})$, where $\lambda_{1}=\lambda(s_{init},t_{1},s)$, $\lambda_{2}=\lambda(s_{1},p^{\prime\prime}_{i}u^{\prime},s_{2})$, $\lambda_{3}=\lambda(s_{3},p^{\prime\prime}_{i+1}u^{\prime}_{i+1},s_{4})$, $\lambda_{4}=\lambda(s_{4},u,s_{5})$ and $\lambda_{5}=\lambda(s_{6},t_{2},q_{F})$. The saturation procedure creates a transition $({s_{1}}_{p^{\prime}_{i}},\gamma,s_{4})=a\cdot(\lambda_{2}(\{\varepsilon\})\shuffle\lambda_{3})$. Hence:

[TABLE]

[TABLE]

[TABLE]

Moreover, $A_{pre^{*}}$ accepts $c^{\prime}$ with the path $s_{init}\xrightarrow{t_{1}p^{\prime}_{i}\gamma ut_{2}}_{A_{pre^{*}}}q_{F}$. But we have $\lambda(s_{init},t_{1}p^{\prime}_{i}\gamma ut_{2},q_{F})\supseteq\lambda_{1}\shuffle(a\cdot(\lambda_{2}(\{\varepsilon\})\shuffle\lambda_{3})\circ\lambda_{4})\shuffle\lambda_{5}$ because of constraint $(Z_{5})$. $A_{pre_{\Pi}^{*}}$ therefore accepts $\pi$.

• •

if $j=l$, no new process has been created while moving from the configuration $c^{\prime}$ to the configuration $c_{1}$. Let $p^{\prime}_{i}\gamma\xrightarrow{a}_{M}p^{\prime\prime}_{i}u^{\prime}$ be the transition used to move from $c^{\prime}$ to $c_{1}$.

Let $t_{1}$ and $t_{2}$ be two words in $(P\Gamma^{*})^{*}$ such that $c_{1}=(t_{1}p^{\prime\prime}_{i}u_{i}t_{2})$ and $c^{\prime}=(t_{1}p^{\prime}_{i}w^{\prime}_{i}t_{2})$. There is $u\in\Gamma^{*}$ such that $w^{\prime}_{i}=\gamma u$ and $u_{i}=u^{\prime}u$.

By induction, as shown in figure 15, there is a path $\pi^{\prime}$ such that $A_{pre^{*}_{\Pi}}$ accepts $(c_{1},\pi^{\prime})$ and $\pi^{\prime}\in\lambda_{1}(\{\varepsilon\})\shuffle\lambda_{2}\circ\lambda_{3}(\{\varepsilon\})\shuffle\lambda_{4}(\{\varepsilon\})$, where $\lambda_{1}\linebreak=\lambda(s_{init},t_{1},s)$, $\lambda_{2}=\lambda(s_{1},p^{\prime\prime}_{i}u^{\prime},s_{2})$, $\lambda_{3}=\lambda(s_{2},u,s_{3})$ and $\lambda_{4}=\lambda(s_{4},t_{2},\linebreak q_{F})$.

The saturation procedures creates a transition $({s_{1}}_{p^{\prime}_{i}},\gamma,s_{2})$ such that we have $\lambda({s_{1}}_{p^{\prime}_{i}},\gamma,s_{2})=a\cdot(\lambda_{2})$. Moreover:

[TABLE]

[TABLE]

[TABLE]

The automaton $A_{pre^{*}}$ accepts $c^{\prime}$ with a path $s_{init}\xrightarrow{t_{1}p^{\prime}_{i}\gamma ut_{2}}_{A_{pre^{*}}}q_{F}$ such that $\lambda(s_{init},t_{1}p^{\prime}_{i}\gamma ut_{2},q_{F})\supseteq\lambda_{1}\shuffle a\cdot(\lambda_{2}\circ\lambda_{3})\shuffle\lambda_{4}$ because of constraints $(Z_{2},Z_{3},Z_{4})$. The automaton $A_{pre_{\Pi}^{*}}$ therefore accepts $\pi$.

4.3.2 Proof of Lemma 2

We prove this lemma by induction the length $\left|\pi\right|$ of $\pi$.

Basis:

if $\left|\pi\right|=0$, then $\pi=\varepsilon$; because of constraints $(Z_{2},Z_{3},Z_{4},Z_{5})$, paths that use new transitions introduced by the saturation procedure are of length at least $1$ and $(c^{\prime},\pi)$ can only be accepted by a sequence of transitions following constraint $(Z_{1})$, hence, transitions in $A$. Therefore, $c^{\prime}\in C$ and the property holds.

Induction step:

if $\left|\pi\right|=k>0$, let $\pi={a_{1}}\cdot{a_{2}}\cdot\ldots\cdot{a_{k}}$. If $A_{pre_{\Pi}^{*}}$ accepts $(c^{\prime},\pi)$, then there is an accepting execution $s_{init}=s_{1}\xRightarrow{(p^{\prime}_{1}w^{\prime}_{1},e_{1})}_{A_{pre_{\Pi}^{*}}}s_{2}\ldots s_{n}\linebreak\xRightarrow{(p^{\prime}_{n}w^{\prime}_{n},e_{1})}_{A_{pre_{\Pi}^{*}}}s_{n+1}\in F$ such that $\pi\in e_{1}(\{\varepsilon\})\shuffle e_{2}(\{\varepsilon\})\ldots\shuffle e_{n}(\{\varepsilon\})$, with $e_{i}=\lambda(s_{i},p^{\prime}_{i}w^{\prime}_{i},s_{i+1})$.

We have the two following cases:

• •

if $a_{1}\neq\tau$, for each $i\in\{1,\ldots,n\}$, we split $e_{i}(\{\varepsilon\})$ into two parts: ${a_{1}}\cdot S_{i}$, which represents the path expressions in $e_{i}$ starting with ${a_{1}}$, and $S^{\prime}_{i}$, which stands for the path expressions starting with another symbol than ${a_{1}}$. We have $e_{j}(\{\varepsilon\})=({a_{1}}\cdot S_{j})\cup S^{\prime}_{j}$ and $\pi=a_{1}a_{2}\ldots a_{k}\in(({a_{1}}\cdot S_{1})\cup S^{\prime}_{1})\shuffle\ldots(({a_{1}}\cdot S_{n})\cup S^{\prime}_{n})$.

Let $i$ be such that ${a_{2}}{a_{3}}\ldots{a_{k}}\in(({a_{1}}\cdot S_{1})\cup S^{\prime}_{1})\shuffle\ldots\shuffle(S_{i})\shuffle\ldots(({a_{1}}\cdot S_{n})\cup S^{\prime}_{n})$. The first symbol ${a_{1}}$ of $\pi$ must appear in one (let’s say the $i$-th) of the $n$ sets $e_{1}(\{\varepsilon\}),\ldots,e_{n}(\{\varepsilon\})$.

We define $w^{\prime}_{i}=\gamma_{1}\gamma_{2}\ldots\gamma_{j}$. We now consider the sub-sequence $s_{i}=s_{i_{1}}\linebreak\xRightarrow{(p^{\prime}_{i}\gamma_{1},\lambda_{1})}_{A_{pre_{\Pi}^{*}}}s_{i_{2}}\ldots\xRightarrow{(\gamma_{j},\lambda_{j})}s_{i_{j+1}}$ of the accepting execution outlined earlier. We have $e_{i}=\lambda_{1}\circ\lambda_{2}\ldots\circ\lambda_{j}$.

Since there are paths starting with ${a_{1}}$ in $e_{i}$, then there are words starting with ${a_{1}}$ in $\lambda_{1}$ as well. Therefore, there is a rule $r=p^{\prime}_{i}\gamma_{1}\xrightarrow{a_{1}}_{M}q_{i}u$ in $M$ and a transition $({s_{i}}_{q_{i}},u,s_{i_{2}})$ in $A_{pre^{*}}$, from which a transition $({s_{i}}_{p^{\prime}_{i}},\gamma_{1},s_{i_{2}})$ labelled by $\lambda_{1}$ can be added by the saturation rules in such a manner that the inequality ${a_{1}}\cdot\lambda({s_{i}}_{q_{i}},u,s_{i_{2}})\subseteq\lambda_{1}$ holds.

The automaton $A_{pre_{\Pi}^{*}}$ then has an accepting execution labelled by:

[TABLE]

and:

[TABLE]

where $\lambda^{\prime}=\lambda({s_{i}}_{q_{i}},u,s_{i_{2}})$.

We have ${a_{1}}\cdot\lambda^{\prime}({s_{i}}_{q_{i}},u,s_{i_{2}})\subseteq\lambda_{1}$ and ${a_{1}}\cdot\lambda^{\prime}\circ\lambda_{2}\ \ldots\circ\lambda_{j}(\{\varepsilon\})={a_{1}}\cdot S_{i}$, hence $\lambda^{\prime}\circ\lambda_{2}\ldots\circ\lambda_{j}(\{\varepsilon\})=S_{i}$.

If we apply rule $r$ to $(c,\pi)$, we move to a configuration $(c_{1},\pi^{\prime})$, with $\pi^{\prime}={a_{2}}\ldots{a_{k}}$ and $\pi^{\prime}\in(({a_{1}}\cdot S_{1})\cup S^{\prime}_{1})\shuffle\ldots\shuffle(S_{i})\shuffle\ldots(({a_{1}}\cdot S_{n})\cup S^{\prime}_{n})=e_{1}(\{\varepsilon\})\shuffle\ldots e_{i-1}(\{\varepsilon\})\shuffle(\lambda^{\prime}\circ\lambda_{2}\ldots\circ\lambda_{j})(\{\varepsilon\})\shuffle e_{i+1}(\{\varepsilon\})\ldots\shuffle e_{n}(\{\varepsilon\})$. Moreover, $\left|\pi^{\prime}\right|<\left|\pi\right|$.

If we apply the induction hypothesis, there is $c$ such that $s_{init}\xrightarrow{c}_{A}q_{F}$ and $(c_{1},\pi^{\prime})\leadsto_{M,\Pi}(c,\varepsilon)$. Since $(c^{\prime},\pi)\leadsto_{M,\Pi}(c_{1},\pi^{\prime})$, $(c^{\prime},\pi)\leadsto_{M,\Pi}(c^{\prime},\varepsilon)$.

• •

if $a_{1}=\tau$, from $c$, the automaton $M$ can either move to another configuration if two of its processes synchronize with an action $a$ or apply an internal action; we focus on the first case, the second case being similar to the previous unsynchronized action in terms of pushdown operations.

For $i\in\{1,\ldots,n\}$, we split $e_{i}(\{\varepsilon\})$ in three parts: the set ${a}\cdot S_{i}$ of path expressions starting by $a$, the set ${\overline{a}}\cdot S^{\prime}_{i}$ of path expressions starting by $\overline{a}$, and the set $S^{\prime\prime}_{i}$ of path expressions starting with another symbol than $a$ or $\overline{a}$. We have $e_{i}(\{\varepsilon\})=({a}\cdot S_{i})\cup({\overline{a}}\cdot S^{\prime}_{i})\cup S^{\prime\prime}_{i}$ and:

[TABLE]

Let $i$ and $j$ be two integers such that ${a_{2}}\cdot\ldots{a_{k}}\in(({a}\cdot S_{1})\cup({\overline{a}}\cdot S^{\prime}_{1})\cup S^{\prime\prime}_{1})\shuffle\ldots\shuffle\ldots(S_{i})\shuffle\ldots(S^{\prime}_{j})\shuffle\ldots(({a}\cdot S_{n})\cup({\overline{a}}\cdot S^{\prime}_{n})\cup S^{\prime\prime}_{n}))$. The symbol $\tau$ of $\pi$ comes from a shuffle of a word in ${a}\cdot S_{i}$, hence in $e_{i}(\{\varepsilon\})$, and a word in ${\overline{a}}\cdot S^{\prime}_{j}$, hence in $e_{j}(\{\varepsilon\})$.

We define $w^{\prime}_{i}=\gamma_{1}\gamma_{2}\ldots\gamma_{l}$. We now consider the sub-sequence $s_{i}=s_{i_{1}}\linebreak\xRightarrow{(p^{\prime}_{i}\gamma_{1},\lambda_{1})}_{A_{pre_{\Pi}^{*}}}s_{i_{2}}\ldots\xRightarrow{(\gamma_{l},\lambda_{l})}s_{i_{l+1}}$ of the accepting execution outlined earlier.

We also define $w^{\prime}_{j}=\alpha_{1}\alpha_{2}\ldots\alpha_{m}$ as well as the sub-sequence $s_{j}=s_{j_{1}}\linebreak\xRightarrow{(p^{\prime}_{j}\alpha_{1},\lambda^{\prime}_{1})}_{A_{pre_{\Pi}^{*}}}s_{j_{2}}\ldots\xRightarrow{(\alpha_{m},\lambda^{\prime}_{m})}s_{j_{m+1}}$ of the accepting execution outlined earlier.

We have $e_{i}=\lambda_{1}\circ\lambda_{2}\ldots\circ\lambda_{l}$. There are paths starting by $a$ in $e_{i}$, hence in $\lambda_{1}$ as well, and there is therefore a rule:

[TABLE]

By the saturation rules, from the transition $({s_{i}}_{q_{i}},u,s_{i_{2}})$, we add a new transition $({s_{i}}_{p^{\prime}_{i}},\gamma_{1},s_{i_{2}})$ labelled by $\lambda_{1}$ such that $a\cdot\lambda({s_{i}}_{q_{i}},u,s_{i_{2}})\subseteq\lambda_{1}$.

We have $e_{j}=\lambda^{\prime}_{1}\circ\lambda^{\prime}_{2}\ldots\circ\lambda^{\prime}_{m}$. There are paths starting by $\overline{a}$ in $e_{j}$, hence in $\lambda^{\prime}_{1}$ as well, and there is a rule:

[TABLE]

By the saturation rules, from the transition $({s_{j}}_{q_{j}},u^{\prime},s_{j_{2}})$, we add a new transition $({s_{j}}_{p^{\prime}_{j}},\alpha_{1},s_{j_{2}})$ labelled by $\lambda^{\prime}_{1}$ such that ${\overline{a}}\cdot\lambda({s_{j}}_{q_{j}},u^{\prime},s_{j_{2}})\subseteq\lambda^{\prime}_{1}$.

We define $v_{1}=\gamma_{2}\ldots\gamma_{l}$ and $v_{2}=\alpha_{2}\ldots\alpha_{m}$.

The automaton $A_{pre_{\Pi}^{*}}$ then has an accepting execution labelled by $c_{1}=(p^{\prime}_{1}w^{\prime}_{1}\ldots p^{\prime}_{i-1}w^{\prime}_{i-1}q_{i}uv_{1}\ldots q_{j}u^{\prime}v_{2}\ldots p^{\prime}_{n}w^{\prime}_{n})$ and $(e_{1}\shuffle\ldots e_{i-1}\shuffle(\lambda\circ\lambda_{2}\ldots\circ\lambda_{l})\shuffle\ldots(\lambda^{\prime}\circ\lambda^{\prime}_{2}\ldots\circ\lambda^{\prime}_{m})\ldots\shuffle e_{n})$, where $\lambda=\lambda({s_{i}}_{q_{i}},u,s_{i_{2}})$ and $\lambda^{\prime}=\lambda({s_{j}}_{q_{j}},u^{\prime},s_{j_{2}})$.

We have $a\cdot\lambda\subseteq\lambda_{1}$ and $a\cdot\lambda\circ\lambda_{2}\ldots\circ\lambda_{l}(\{\varepsilon\})=a\cdot S_{i}$, hence $\lambda\circ\lambda_{2}\ldots\circ\lambda_{l}(\{\varepsilon\})=S_{i}$. Moreover, ${\overline{a}}\cdot\lambda^{\prime}\subseteq\lambda^{\prime}_{1}$ and ${\overline{a}}\cdot\lambda^{\prime}\circ\lambda^{\prime}_{2}\ldots\circ\lambda^{\prime}_{m}((\{\varepsilon\}))={\overline{a}}\cdot S^{\prime}_{j}$, hence $\lambda^{\prime}\circ\lambda^{\prime}_{2}\ldots\circ\lambda^{\prime}_{m}(\{\varepsilon\})=S^{\prime}_{j}$.

If we apply $r_{1}$ and $r_{2}$ in a synchronized manner to the configuration $(c,\pi)$, we move to another configuration $(c_{1},\pi^{\prime})$, where $\pi^{\prime}={a_{2}}\ldots{a_{k}}$ and $\pi^{\prime}\in(({a}\cdot S_{1})\cup({\overline{a}}\cdot S^{\prime}_{1})\cup S^{\prime\prime}_{1})\shuffle\ldots(S_{i})\shuffle\ldots(S^{\prime}_{j})\shuffle\ldots(({a}\cdot S_{n})\cup({\overline{a}}\cdot S^{\prime}_{n})\cup S^{\prime\prime}_{n})=e_{1}(\{\varepsilon\})\shuffle\ldots e_{i-1}(\{\varepsilon\})\shuffle(\lambda\circ\ldots\circ\lambda_{l})(\{\varepsilon\})\shuffle\ldots(\lambda^{\prime}\circ\lambda^{\prime}_{2}\ldots\circ\lambda^{\prime}_{m})(\{\varepsilon\})\ldots\shuffle e_{n}(\{\varepsilon\})$.

Since $\left|\pi^{\prime}\right|<\left|\pi\right|$, we can apply the induction hypothesis. There is a configuration $c$ such that $s_{init}\xrightarrow{c}_{A}q_{F}$ and $(c_{1},\pi^{\prime})\leadsto_{M,\Pi}(c,(\varepsilon))$. Since $(c^{\prime},\pi)\leadsto_{M,\Pi}(c_{1},\pi^{\prime})$, it follows that $(c^{\prime},\pi)\leadsto_{M,\Pi}(c,\varepsilon)$.

5 An abstraction framework for paths

We can’t compute the exact set $Paths_{M}(C,C^{\prime})$, we will therefore over approximate it. To do so, we use the following mathematical framework, basing our technique on the approach presented by Bouajjani et al. in [BET03].

5.1 Abstractions and Galois connections

Let $\mathcal{L}=(2^{Act^{*}},\subseteq,\cup,\cap,\emptyset,Act^{*})$ be the complete lattice of languages on $Act$.

Our abstraction of $\mathcal{L}$ requires a lattice $E=(D,\leq,\sqcup,\sqcap,\bot,\top)$, from now on called the abstract lattice, where $D$ is a set called the abstract domain, as well as a pair of mappings $(\alpha,\beta)$ called a Galois connection, where $\alpha:2^{Act^{*}}\to D$ and $\beta:D\to 2^{Act^{*}}$ are such that $\forall x\in 2^{Act^{*}}$, $\forall y\in D$, $\alpha(x)\leq y\Leftrightarrow x\subseteq\beta(y)$.

$\forall L\in\mathcal{L}$, given a Galois connection $(\alpha,\beta)$, we have $L\subseteq\beta(\alpha(L))$. Hence, the Galois connection can be used to overapproximate a language, such as the set of execution paths of a SDPN.

Moreover, it is easy to see that $\forall L_{1},\forall L_{2}\in\mathcal{L}$, $\alpha(L_{1})\sqcap\alpha(L_{2})=\bot$ if and only if $\beta(\alpha(L))\cap\beta(\alpha(L))=\emptyset$. We therefore only need to check if $\alpha(Paths_{M}(C,C^{\prime}))\sqcap\alpha(\tau^{*})=\bot$. From then on, $\alpha(Paths_{M}(C,C^{\prime}))$ will be called the abstraction of $Paths_{M}(C,C^{\prime})$, although technically the set $\beta(\alpha(Paths_{M}(C,C^{\prime}))$ is the actual over-approximation.

5.2 Kleene algebras

We want to define abstractions of $\mathcal{L}$ such that we can compute the abstract path language $\alpha(Paths_{M}(C^{\prime},C))$, assuming the sets $C^{\prime}$ and $C$ are regular. In order to do so, we consider a special class of abstractions, called Kleene abstractions.

An idempotent semiring is a structure $K=(A,\oplus,\odot,\overline{0},\overline{1})$, where $\oplus$ is an associative, commutative, and idempotent ($a\oplus a=a$) operation, and $\odot$ is an associative operation. $\overline{0}$ and $\overline{1}$ are neutral elements for $\oplus$ and $\odot$ respectively, $\overline{0}$ is an annihilator for $\odot$ ($a\odot\overline{0}=\overline{0}\odot a=\overline{0}$) and $\odot$ distributes over $\oplus$.

$K$ is an $Act$-semiring if it can be generated by $\overline{0}$, $\overline{1}$, and elements of the form $v_{a}\in A$, $\forall a\in Act$. A semiring is said to be closed if $\oplus$ can be extended to an operator over countably infinite sets while keeping the same properties as $\oplus$.

We define $a^{0}=\overline{1}$, $a^{n+1}=a\odot a^{n}$ and $a^{*}=\mathop{\bigoplus}\limits_{n\geq 0}a^{n}$. Adding the $*$ operation to an idempotent closed $Act$-semiring $K$ transforms it into a Kleene algebra.

5.3 Kleene abstractions

An abstract lattice $E=(D,\leq,\sqcup,\sqcap,\bot,\top)$ is said to be compatible with a Kleene algebra $K=(A,\oplus,\odot,\overline{0},\overline{1})$ if $D=A$, $x\leq y\Leftrightarrow x\oplus y=y$, $\bot=\overline{0}$ and $\sqcup=\oplus$.

A Kleene abstraction is an abstraction such that the abstract lattice $E$ is compatible with the Kleene algebra and the Galois connection $\alpha:2^{Act^{*}}\to D$ and $\beta:D\to 2^{Act^{*}}$ is defined by:

[TABLE]

[TABLE]

Intuitively, a Kleene abstraction is such that the abstract operations $\oplus$, $\odot$, and $*$ can be matched to the union, the concatenation, and the Kleene closure of the languages of the lattice $\mathcal{L}$, $\overline{0}$ and $\overline{1}$ to the empty language and $\{\varepsilon\}$, $v_{a}$ to the language $\{a\}$, the upper bound $\top\in K$ to $Act^{*}$, and the operation $\sqcap$ to the intersection of languages in the lattice $\mathcal{L}$.

In order to compute $\alpha(L)$ for a given language $L$, each word $a_{1}\ldots a_{n}$ in $L$ is matched to its abstraction $v_{a_{1}}\odot\ldots\odot v_{a_{n}}$, and we consider the sum of these abstractions.

We can check if $\alpha(Paths_{M}(C,C^{\prime}))\sqcap\mathop{\bigoplus}\limits_{n\geq 0}v_{\tau}^{n}=\bot$; if it is indeed the case, then $\beta(\alpha(Paths_{M}(C,C^{\prime})))\cap\tau^{*}=\emptyset$, and since $\beta(\alpha(Paths_{M}(C,C^{\prime})))$ is an over-approximation $Paths_{M}(C,C^{\prime})$, it follows that $Paths_{M}(C,C^{\prime})\cap\tau^{*}=\emptyset$.

A finite-chain abstraction is an abstraction such that the lattice $(K,\oplus)$ has no infinite ascending chains. In this paper, we rely on a particular class of finite-chain abstractions, called finite-domain abstractions, whose abstract domain $K$ is finite, such as the following examples:

5.3.1 Prefix abstractions.

Let $n$ be an integer and $W(n)=\left\{w\in Act^{*}\mid\left|w\right|\leq n\right\}$ be the set of words of length smaller than $n$. We define the $n$-th order prefix abstraction $\alpha^{pref}_{n}$ as follows: the abstract lattice $A=2^{W}$ is generated by the elements $v_{a}=\left\{a\right\}$, $a\in Act$; $\oplus=\cup$; $U\odot V=\{\text{pref}_{n}(uv)\mid u\in U,v\in V\}$ where $\text{pref}_{n}(w)$ stands for the prefix of $w$ of length $n$ (or lower if $w$ is of length smaller than $n$); $\overline{0}=\emptyset$; and $\overline{1}=\left\{\varepsilon\right\}$. From there, we build an abstract lattice where $\top=W$, $\sqcap=\cap$, and $\leq=\subseteq$. This abstraction is accurate for the $n$-th first steps of a run, then approximates the other steps by $Act^{*}$.

We can apply a prefix abstraction of order 2 to the example shown in Figure 16. For ease of representation, we show a control flow graph, although we could use the procedure outlined in section 1.3 to compute an equivalent SDPN. We also consider without loss of generality that spawns, calls, and returns are silent $\varepsilon$-transitions.

We check that, starting from an initial set of configurations $C$ with a single thread $M$ in state $m_{0}$, the set $C^{\prime}$ where $M$ is in state $m_{2}$ can’t be reached with regards to the strict semantics.

We have $\alpha^{pref}_{2}(Paths_{M}(C,C^{\prime}))=\{b,b\tau,ba,b\overline{a}\}$, $\alpha^{pref}_{2}(\tau^{*})=\{\varepsilon,\tau,\tau\tau\}$, and $\alpha^{pref}_{2}(Paths_{M}(C,C^{\prime}))\cap\alpha^{pref}_{2}(\tau^{*})=\emptyset$, hence, $C^{\prime}$ can’t be reached from $C$ with regards to the strict semantics. Intuitively, the transition labelled with $b$ in thread $M$ can’t synchronize as there isn’t any transition labelled with $\overline{b}$ in the whole program.

5.3.2 Suffix abstractions.

Let $W$ be the set of words of length smaller than $n$. We define the $n$-th order suffix abstraction $\alpha^{suff}_{n}$ as follows: the abstract lattice $A=2^{W}$ is generated by the elements $v_{a}=\left\{a\right\}$, $a\in Act$; $\oplus=\cup$; $U\odot V=\{\text{suff}_{n}(uv)\mid u\in U,v\in V\}$ where $\text{suff}_{n}(w)$ stands for the suffix of $w$ of length $n$ (or lower if $w$ is of length smaller than $n$); $\overline{0}=\emptyset$; and $\overline{1}=\left\{\varepsilon\right\}$. From there, we build an abstract lattice where $\top=W$, $\sqcap=\cap$, and $\leq=\subseteq$. This abstraction is accurate for the $n$-th last steps of a run, then approximates the other steps by $Act^{*}$.

We apply a suffix abstraction of order $2$ to the example shown in Figure 17. We check that, starting from an initial set of configurations $C$ with a single thread $M$ in state $m_{0}$, the set $C^{\prime}$ where $M$ is in state $m_{2}$ can’t be reached with regards to the strict semantics.

We have $\alpha^{suff}_{2}(Paths_{M}(C,C^{\prime}))=\{b,ab,\overline{a}b,\tau b\}$, $\alpha^{suff}_{2}(\tau^{*})=\{\varepsilon,\tau,\tau\tau\}$, and $\alpha^{suff}_{2}(Paths_{M}(C,C^{\prime}))\cap\alpha^{suff}_{2}(\tau^{*})=\emptyset$, hence, $C^{\prime}$ can’t be reached from $C$ with regards to the strict semantics. Intuitively, the transition labelled with $b$ in thread $M$ can’t synchronize as there isn’t any transition labelled with $\overline{b}$ in the whole program.

It is worth noting that the reachability problem in Example 17 can’t be solved by a prefix abstraction, no matter its order. The reason is that $\forall n\geq 0$, there is an execution path $\tau^{n}b\in Paths_{M}(C,C^{\prime})$, hence, $\tau^{n}\in\alpha^{pref}_{n}(Paths_{M}(C,C^{\prime}))$. Intuitively, the two self-pointing loops of nodes $m_{1}$ and $n_{1}$ can synchronize.

Conversely, we can’t use a suffix abstraction to solve the reachability problem in Example 16. The reason is that $\forall n\geq 0$, there is an execution path $b\tau^{n}\in Paths_{M}(C,C^{\prime})$, hence, $\tau^{n}\in\alpha^{suff}_{n}(Paths_{M}(C,C^{\prime}))$. Intuitively, the self-pointing loop of node $m_{2}$ can synchronize with the self-spawning loop in thread $N$.

Thus, these two abstractions (prefix and suffix) complement each other.

6 Abstracting the set of paths

Since we can’t compute the solution of the constraints outlined in 4.2 on paths, our intuition now is to solve them in an abstract finite domain defined by a Kleene abstraction where we can compute the least pre-fixpoint, in a manner similar to [BET05].

6.1 From the language of paths to the Kleene abstraction

We abstract the the complete lattice of languages $\mathcal{L}=(2^{Act^{*}},\subseteq,\cup,\cap,\emptyset,Act^{*})$ by a finite domain Kleene abstraction on an abstract lattice $E=(D,\leq,\sqcup,\sqcap,\bot,\top)$ and a Klenne algebra $K=(A,\oplus,\odot,\overline{0},\overline{1})$, as defined in Section 5.3.

Intuitively:

• •

the set $\Pi$ is abstracted by $K$;

• •

the operator $\cdot$ is abstracted by $\odot$;

• •

the operator $\cup$ is abstracted by $\sqcup=\oplus$;

• •

the operator $\subseteq$ is abstracted by $\leq$;

• •

the operator $\cap$ is abstracted by $\sqcap$;

• •

$\emptyset$ is abstracted by $\bot=\overline{0}$;

• •

$\{\varepsilon\}$ is abstracted by $\overline{1}$;

• •

$Act^{*}$ is abstracted by the set of path expressions $\Pi_{K}$, that is, the smallest set such that:

• –

$\overline{1}\in\Pi_{K}$;

• –

if $\pi\in\Pi_{K}$, then $\forall a\in Act$, $v_{a}\odot\pi\in\Pi_{K}$.

We can define $K$-configurations in $Conf_{M}\times\Pi_{K}$ and $K$-automata in a similar manner to $\Pi$-configurations and $\Pi$-automata. For a given set of configurations $C$, we introduce the set $pre_{K}^{*}(M,C)$ of $K$-configurations $(c,\pi)$ such that $(c,\pi)\leadsto_{M,K}(c^{\prime},\overline{1})$ for $c^{\prime}\in C$. The following property obviously holds:

[TABLE]

The abstract path expression $\pi$ is meant to be the abstraction of an actual execution path from $c$ to $c^{\prime}$.

To do so, we need to define the shuffle operation to paths expressions. However, it has to be well-defined: given two representations $v_{a_{1}}\odot\ldots\odot v_{a_{n}}=v_{b_{1}}\odot\ldots\odot v_{b_{m}}$ of a same path expression, $\forall w\in\{v_{a}|a\in Act\}^{*}$, we must have $(v_{a_{1}},\ldots,v_{a_{n}})\shuffle w=(v_{b_{1}},\ldots,v_{b_{m}})\shuffle w$.

To this end, we first inductively define a shuffle operation $\shuffle:(\{v_{a}|a\in Act\}^{*})^{2}\rightarrow K$ such that, given two sequences representing path expressions, their shuffle product is the set of all possible interleaving (with synchronization) of these sequences.

Let $w=(v_{a_{1}},\ldots,v_{a_{n}})$ and $w^{\prime}=(v_{b_{1}},\ldots,v_{b_{m}})$ be two such sequences:

• •

$(v_{a_{1}},\ldots v_{a_{n}})\shuffle(\varepsilon)=(\varepsilon)\shuffle(v_{a_{1}},\ldots v_{a_{n}})=\{v_{a_{1}}\odot\ldots\odot v_{a_{n}}\}$;

• •

if $b_{1}\neq\overline{a_{1}}$, then $((v_{a_{1}},\ldots,v_{a_{n}}))\shuffle(v_{b_{1}},\ldots,v_{b_{m}})=v_{a_{1}}\odot((v_{a_{2}},\ldots,v_{a_{n}})\shuffle(v_{b_{1}},\ldots,v_{b_{m}}))\oplus v_{b_{1}}\odot((v_{a_{1}},\ldots,v_{a_{n}})\shuffle(v_{b_{2}},\ldots,v_{b_{m}}))$;

• •

if $b_{1}=\overline{a_{1}}$, then $((v_{a_{1}},\ldots,v_{a_{n}}))\shuffle(v_{b_{1}},\ldots,v_{b_{m}})=v_{a_{1}}\odot((v_{a_{2}},\ldots,v_{a_{n}})\shuffle(v_{b_{1}},\ldots,v_{b_{m}}))\oplus v_{b_{1}}\odot((v_{a_{1}},\ldots v_{a_{n}})\shuffle(v_{b_{2}},\ldots,v_{b_{m}}))\oplus v_{\tau}\odot((v_{a_{2}},\ldots,v_{a_{n}})\shuffle(v_{b_{2}},\ldots,v_{b_{m}}))$; two synchronized actions $a_{1}$ and $\overline{a_{1}}$ result in an internal action $\tau$, hence, there is a component $v_{\tau}\odot(w_{1}\shuffle w_{2})$ of the shuffle product where the two paths synchronize.

We now that prove that the shuffle product is well-defined on path expressions for the prefix and suffix abstractions. We define the length $\left|\pi\right|$ of a path expression $\pi$ as the length $n$ of the smallest sequence $(v_{a_{1}},\ldots,v_{a_{n}})$ such that to $\pi=v_{a_{1}}\odot\ldots\odot v_{a_{n}}$, length 0 meaning that $\pi=\overline{1}$.

Note that this sequence is unique for the prefix and suffix abstractions; we can therefore define a function $\theta(\pi)=(v_{a_{1}},\ldots,v_{a_{n}})$ that matches to a path expression its smallest representation.

Lemma 3

The shuffle product is well-defined for the prefix abstraction.

Proof

We will show by induction on $m+n$ that, given two sequences $(v_{a_{1}},\ldots,\linebreak v_{a_{n}})$ and $(v_{b_{1}},\ldots,v_{b_{m}})$, we have $(v_{a_{1}},\ldots,v_{a_{n}})\shuffle(v_{b_{1}},\ldots,v_{b_{m}})=\theta(v_{a_{1}}\odot\ldots\odot v_{a_{n}})\shuffle\theta(v_{b_{1}}\odot\ldots\odot v_{b_{m}})$, i.e., that the shuffle of two path sequences is equal to the shuffle of their smallest representations.

• •

if $n\leq l$ and $m\leq l$, $\theta(v_{a_{1}}\odot\ldots\odot v_{a_{n}})=(v_{a_{1}},\ldots,v_{a_{n}})$ and $\theta(v_{b_{1}}\odot\ldots\odot v_{b_{m}})=(v_{b_{1}},\ldots,v_{b_{m}})$, by definition of the $l$-th prefix abstraction: indeed, the smallest representation in this abstraction of a word of length smaller than $l$ is itself.

• •

if $n>l$ and $m>l$, note that $\theta(v_{a_{1}}\odot\ldots\odot v_{a_{n}})=(v_{a_{1}},\ldots,v_{a_{l}})$ and $\theta(v_{b_{1}}\odot\ldots\odot v_{b_{m}})=(v_{b_{1}},\ldots,v_{b_{l}})$ by definition of the $l$-th prefix. If we suppose that $b_{1}=\overline{a_{1}}$:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

if we apply the induction hypothesis. However, by definition of the prefix abstraction, given two sequences $(v_{x_{1}},\ldots,v_{x_{l}})$ and $w$ and $\forall x_{0}\in Act$, $v_{x_{0}}\odot((v_{x_{1}},\ldots,v_{x_{l}})\shuffle w)=v_{x_{0}}\odot((v_{x_{1}},\ldots,v_{x_{l-1}})\shuffle w)$. Intuitively, the symbols $v_{x_{1}},\ldots,v_{x_{l-1}}$ have to be inserted after $v_{x_{0}}$ but before $v_{x_{l}}$, and $v_{x_{l}}$ will therefore be cut out of the prefix when we concatenate $v_{x_{0}}$. Hence:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

The case $b_{1}\neq\overline{a_{1}}$ is similar. Hence, the induction holds.

As a consequence, the shuffle product is well-defined: if $v_{a_{1}}\odot\ldots\odot v_{a_{n}}=v_{b_{1}}\odot\ldots\odot v_{b_{m}}=\pi$, then for all sequences $w$, $(v_{a_{1}},\ldots,v_{a_{n}})\shuffle w=\theta(\pi)\shuffle w=(v_{b_{1}},\ldots,v_{b_{m}})\shuffle w$.

Lemma 4

The shuffle product is well-defined for the suffix abstraction.

Proof

We will show again by induction on $m+n$ that, given two sequences $(v_{a_{1}},\ldots,v_{a_{n}})$ and $(v_{b_{1}},\ldots,v_{b_{m}})$, we have $(v_{a_{1}},\ldots,v_{a_{n}})\shuffle(v_{b_{1}},\ldots,v_{b_{m}})=\theta(v_{a_{1}}\odot\ldots\odot v_{a_{n}})\shuffle\theta(v_{b_{1}}\odot\ldots\odot v_{b_{m}})$, i.e., that the shuffle of two path sequences is equal to the shuffle of their smallest representations.

• •

if $n\leq l$ and $m\leq l$, $\theta(v_{a_{1}}\odot\ldots\odot v_{a_{n}})=(v_{a_{1}},\ldots,v_{a_{n}})$ and $\theta(v_{b_{1}}\odot\ldots\odot v_{b_{m}})=(v_{b_{1}},\ldots,v_{b_{m}})$, by definition of the $l$-th suffix abstraction: indeed, the smallest representation in this abstraction of a word of length smaller than $l$ is itself.

• •

if $n>l$ and $m>l$, note that $\theta(v_{a_{1}}\odot\ldots\odot v_{a_{n}})=(v_{a_{n-l+1}},\ldots,v_{a_{l}})$ and $\theta(v_{b_{1}}\odot\ldots\odot v_{b_{m}})=(v_{b_{m-l+1}},\ldots,v_{b_{l}})$ by definition of the $l$-th suffix. If we suppose that $b_{1}=\overline{a_{1}}$:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

if we apply the induction hypothesis. However, by definition of the suffix abstraction, given two sequences $(v_{x_{1}},\ldots,v_{x_{l}})$ and $w$ and $\forall x_{0}\in Act$, $v_{x_{0}}\odot((v_{x_{1}},\ldots,v_{x_{l}})\shuffle w)=((v_{x_{1}},\ldots,v_{x_{l}})\shuffle w)$. Intuitively, the symbol $v_{x_{1}}$ is concatenated to shuffled paths that are already of length greater than $l$, hence, will be cut out of the suffix. Therefore:

[TABLE]

[TABLE]

The case $b_{1}\neq\overline{a_{1}}$ is similar. Hence, the induction holds.

As a consequence, the shuffle product is well-defined: if $v_{a_{1}}\odot\ldots\odot v_{a_{n}}=v_{b_{1}}\odot\ldots\odot v_{b_{m}}=\pi$, then for all sequences $w$, $(v_{a_{1}},\ldots,v_{a_{n}})\shuffle w=\theta(\pi)\shuffle w=(v_{b_{1}},\ldots,v_{b_{m}})\shuffle w$.

From now on, we consider that $\alpha$ is either the prefix or suffix abstraction of rank $l$.

6.2 Computing $pre^{*}_{K}(M,C)$

Given a SDPN $M$ and a regular set $C$ of configurations of $M$ accepted by an $M$-automaton $A$, we want to compute a $K$-automaton $A_{pre^{*}_{K}}$ accepting $pre^{*}_{K}(M,C)$. To this end, we will add new labels in $K^{K}$ to the $M$-automaton $A_{pre^{*}}$.

Let $Q$ be the set of states of $A$, hence, of $A_{pre^{*}}$ as well. We now consider the following set of constraints in the abstract domain on the labels of transitions of $A_{pre^{*}}$ in $S_{S}\times\Gamma\times S_{S}$:

$(Y_{1})$

if $t$ belongs to $A$, then:

[TABLE]

$(Y_{2})$

for each rule $p\gamma\xrightarrow{a}p^{\prime}\gamma^{\prime}\in\Delta$, for each $q\in Q$, for each $s\in S_{c}$:

[TABLE]

$(Y_{3})$

for each rule $p\gamma\xrightarrow{a}p^{\prime}\varepsilon\in\Delta$, for each $s\in S_{c}$:

[TABLE]

$(Y_{4})$

for each rule $p\gamma\xrightarrow{a}p^{\prime}\gamma_{1}\gamma_{2}\in\Delta$, for each $q\in Q$, for each $s\in S_{c}$:

[TABLE]

$(Y_{5})$

for each rule $p\gamma\xrightarrow{a}p_{2}\gamma_{2}p_{1}\gamma_{1}\in\Delta$, for each $q\in Q$, for each $s\in S_{c}$:

[TABLE]

Since $\alpha$ is a finite-domain abstraction, the set $K^{K}$ of functions in $K$ is finite as well. Let $t_{1},\ldots,t_{m}$ be an arbitrary numbering of the transitions of $A_{pre_{K}^{*}}$ labelled with functions in the abstract domain and let $k_{1},\ldots,k_{n}$ be an enumeration of the elements of the finite domain $K$ ($n=|K|$). The labelling constraints of section 4.2 define a system of inequalities on $m*n$ variables $x_{1},\ldots,x_{mn}$ such that its smallest solution is $t_{1}(k_{1}),\ldots,t_{1}(k_{n})$, $t_{2}(k_{1}),\ldots,t_{m}(k_{n})$. It is worth noting that we can replace two different inequalities $e_{1}(x)\leq t_{i}(x)$ and $e_{2}(x)\leq t_{i}(x)$ by a single inequality $e_{1}(x)\oplus e_{2}(x)\leq t_{i}(x)$. We therefore end up with a system of the form:

[TABLE]

where the functions $f_{i}$ are monomials in $K[x_{1},\ldots,x_{mn}]$. Finding the least solution of this system of inequalities amounts to finding the least pre-fixpoint of the monotonic and continuous function:

[TABLE]

By Tarski’s theorem, this fixpoint exists and is equal to $\bigoplus\limits_{i\geq 0}F^{i}(\overline{0})$.

In a finite-domain, this iterative computation always terminates in a number of steps bounded by the length of the longest ascending chain in $K$, hence, $l$ for a prefix or suffix abstraction of order $l$. There are $mn$ functions $f_{i}$, each with a number of $\oplus$, $\odot$, and $\shuffle$ operations in $O(|\Delta|\cdot|Q|)$. Moreover, according to [BMOT05], the size of the automaton $A_{pre^{*}}$ is $m=O(|Q|^{2}\cdot|\Delta|)$ . Each iteration step therefore features $O(n\cdot|\Delta|^{2}\cdot|Q|^{3})$ operations, and the whole procedure, $O(l\cdot n\cdot|\Delta|^{2}\cdot|Q|^{3})$ operations. For a prefix or suffix abstraction of order $l$, $n=2^{|Act|^{l}}$, hence, a total of $O(l\cdot 2^{|Act|^{l}}\cdot|\Delta|^{2}\cdot|Q|^{3})$ operations.

6.3 Finding the abstraction

We can compute an automaton $A_{pre_{K}^{*}}$ that accepts the set $pre_{K}^{*}(M,C^{\prime})$. We then want to find a $K$-automaton $A^{\prime}$ that accepts $pre_{K}^{*}(M,C^{\prime})\cap C\times\Pi_{K}$.

To do so, we define the intersection $A^{\prime}=(\Sigma,S^{\prime},\delta^{\prime},s^{\prime}_{init},F^{\prime})$ of the automaton $A_{pre^{*}}=(\Sigma,S,\delta,s_{init},F)$ with an $M$-automaton accepting $C$ called $A_{1}=(\Sigma,S_{1},\delta_{1},s_{1,init},F_{1})$ accepting $C$, where $S^{\prime}=S\times S_{1}$, $s^{\prime}_{init}=(s_{init},s_{1,init})$, $F=F\times F_{1}$, and $\delta=\{(q,q_{1})\xrightarrow{a}(q^{\prime},q^{\prime}_{1})\mid q\xrightarrow{a}q^{\prime}\in\delta,q\xrightarrow{a}q^{\prime}\in\delta_{1}\}$. Moreover, we label $A^{\prime}$ with abstract functions in such a manner that $\lambda((q,q_{1}),a,(q^{\prime},q^{\prime}_{1}))=\lambda(q,a,q^{\prime})$.

The $K)$-automaton $A^{\prime}$ then obviously accepts $pre_{K}^{*}(M,C^{\prime})\cap C\times\Pi_{K}$. Eventually, our abstraction is $\alpha(Paths_{M}(C,C^{\prime}))=\mathop{\bigoplus}\{\pi\mid(c,\pi)\in L_{K}(A^{\prime})\}$.

7 Using our framework in a iterative abstraction refinement scheme

Following the work of Chaki et al. in [CCK*+*06], we propose a semi-decision procedure that, in case of termination, allows us to answer exactly whether $Paths_{M}(C,C^{\prime})\cap\tau^{*}=\emptyset$.

We first model a program as a SDPN $M$, as shown in section 1.3, its starting configurations as a regular set $C$, and a set of critical configurations whose reachability we need to study as another regular set $C^{\prime}$.

We then introduce an iterative abstraction refinement scheme based on the finite-domain abstraction framework detailed previously, starting from $n=1$.

Abstraction:

we compute abstractions $\alpha(Paths_{M}(C,C^{\prime}))$ of the set of executions paths for $\alpha=\alpha^{pref}_{n}$ and $\alpha=\alpha^{suff}_{n}$;

Verification:

for $\alpha=\alpha^{pref}_{n}$ and $\alpha=\alpha^{suff}_{n}$, we check if $\alpha(Paths_{M}(C,C^{\prime}))\sqcap\alpha(\tau^{*})=\bot$; if it is indeed true, then we conclude that $C^{\prime}$ can’t be reached from $C$ using only internal or synchronized actions;

Counter-example validation:

if there is such a path, we then check if our abstraction introduced a spurious counter-example; this can be done in a finite number of steps by checking if this counter-example can be reached within the $n$-th first or last execution steps of the program, depending on which abstraction (prefix or suffix) provided us with a counter-example; if the counter-example is not spurious, then we conclude that $C^{\prime}$ is reachable from $C$ w.r.t. the strict semantics;

Refinement:

if the counter-example was spurious, we go back to the first step, but use this time finite-domain abstractions of order $n+1$.

If this procedure ends, we can decide the reachability problem.

8 A case study

We use an iterative abstraction refinement scheme to find an error in a Bluetooth driver for Windows NT. We consider here an abstracted version of a driver found in [QW04] that nonetheless keeps the erroneous trace, in a manner similar to [CCK*+*06] and [PST07]. We then fix the driver by changing one of its routines, then use the abstraction scheme to prove that this new version of the driver is correct.

We model the network of processes in the driver as a SDPN. New requests for the driver are represented by thread spawns, and the driver’s counter of active requests, by a counter on the stack, hence, a recursive process, making full use of our model’s features.

We were able to discover the bug by applying our finite-domain abstraction in an iterative abstraction refinement scheme: we start from abstractions of order 1 and increment the order until we deduce that the erroneous configuration is reachable using a prefix abstraction of size 12. We then correct one of the program’s subroutines accordingly and apply our iterative abstraction refinement scheme to prove it’s now error-free.

Note that this bug was also discovered in [CCK*+*06, QW04, PST07]. However, our approach is more complete and precise than these works: [QW04] can only discover errors, whereas our scheme can also prove that the modified version of the driver is correct; [CCK*+*06] does not handle dynamic thread creation, and thus had to guess the number of threads for which the error arises; and [PST07] models thread creation as parallel calls (not as spawns), where the father process waits for its children to terminate in order to resume its execution.

8.1 The program

The driver consists of a certain number of processes running in parallel. Amongst these processes is an arbitrary number of requests meant to be handled by the driver. An internal counter records the number of requests currently handled by the driver: it is incremented when a request starts handling a task, and decremented once the request terminates. At any time, a special process in the driver may send a ’stop’ signal; if it does, the driver switches an internal ’stopping’ flag to true. The driver, however, can’t stop yet and must wait until all requests have been processed.

Once the ’stopping’ flag is switched on, requests may no longer perform their tasks and must instead end while decrementing the counter of active requests. Once the counter reaches zero, an internal ’stopping event’ is switched to true, and the driver frees its allocated resources. If a request tries to perform a task after the resources have been released, it must abort and send an error.

Our intuition is that the ’stop’ signal can interrupt a request while the latter has already started handling its task after being told the driver was still running; the driver will then free its allocated resources and let the request resume its execution, leading to an error state where the request must abort because the resources it needs are now missing.

8.2 From the driver to the SDPN model

We model this network of processes as a SDPN. To do so, we consider that each thread has no internal variables and a single control state, as we switch the handling of the control flow to the stack by storing the current control point of each thread on its stack. The threads can communicate and handle flags and counters by using synchronized actions: as an example, two threads can synchronize over an action $stop$ in order to switch the ’stopping’ flag (represented by a control point) to true; a function Increment can also synchronize with a counter over an action $incr$ in order to increase this counter.

The driver uses the following processes:

COUNTER:

this process counts the number of requests the driver receives plus the thread STOP-D; this number is set to 1 initially, is incremented when the driver receives a new request, and is decremented when a request ends;

STOP-D:

this process may issue a request to stop the driver at any time; it has then to wait until all the other requests have finished their work, then, when it receives a signal sent by the function Decrement, can stop the driver and free its allocated resources;

STOPPING-FLAG:

this process is either in state FALSE-STOP-FLAG (from then on FSF) or state TRUE-STOP-FLAG (TSF), depending on whether STOP-D is trying to stop the driver or not; it is initially in state FSF, and moves to state TSF if it receives a message from STOP-D; no new thread can enter the driver if this process is in TSF;

STOPPING-EVENT:

it is either in state TRUE-STOP-EVENT (TSE) or FALSE-STOP-EVENT (FSE); this process enters state TSE if the driver stops, i.e. when the number of running REQUESTs reaches 0;

GEN-REQ:

this process can spawn new requests as long as the driver is not trying to stop, that is, if STOPPING FLAG isn’t in state TSF;

REQUEST:

when a new REQUEST enters the driver, it has to increment the number stored in COUNTER, perform a task, then decrement this number before exiting the driver; it uses two functions Increment and Decrement to do so.

If a REQUEST tries to perform its task but the allocated resources of the driver have been released, the program reaches an error state. We will check the reachability of this state.

Each process can be modelled by a SDPN as follows:

8.2.1 The process COUNTER.

Let $p_{0}$ be its unique state. The number of threads is represented by a stack. Its stack alphabet is $\{0,1\}$. Initially, the stack contains the word $10$, meaning that the number of request is zero and only STOP-D is running. It can then contain any word in $1^{*}0$. The number of 1’s in the stack corresponds to the number of running requests minus 1. The incrementation and decrementation procedures are done by receiving incr and decr actions from the functions Increment and Decrement.

COUNTER is represented by the following SDPN rules:

$(r_{1a})$

$p_{0}1\xrightarrow{\overline{incr}}p_{0}11$ and $(r_{1b})$ $p_{0}0\xrightarrow{\overline{incr}}p_{0}10$; these rules increment the counter when the process is asked to do so;

$(r_{2})$

$p_{0}1\xrightarrow{\overline{decr}}p_{0}\varepsilon$; this rule decrements the counter when the process is asked to do so;

$(r_{3}a)$

$p_{0}1\xrightarrow{not-zero}p_{0}1$ and $(r_{3}b)$ $p_{0}0\xrightarrow{is-zero}p_{0}0$; these rules test whether the counter is 0 or not and send this information to other threads.

8.2.2 The process STOPPING-FLAG.

Let $p_{1}$ be its unique state. The process has two control points FSF and TSF. STOPPING-FLAG is represented by the following SDPN rules:

$(r_{4})$

$p_{1}\mbox{FSF}\xrightarrow{\overline{stop}}p_{1}\mbox{TSF}$; the process receives a ’stop’ request from STOP-D and changes its flag;

$(r_{5})$

$p_{1}\mbox{TSF}\xrightarrow{stopR}p_{1}\mbox{TSF}$; the process sends a ’stop’ message to the incoming REQUESTs;

$(r_{6})$

$p_{1}\mbox{FSF}\xrightarrow{not-stopR}p_{1}\mbox{FSF}$; the process sends a ’non-stop’ request to the incoming REQUESTs.

8.2.3 The process STOPPING-EVENT.

Let $p_{2}$ be its unique state. The process has two control points FSE and TSE. STOPPING-EVENT is represented by the following SDPN rules:

$(r_{7})$

$p_{2}\mbox{FSE}\xrightarrow{\overline{has-stopped}}p_{2}\mbox{TSE}$; the process receives an ’has-stopped’ message and knows that the driver has stopped;

$(r_{8})$

$p_{2}\mbox{TSE}\xrightarrow{has-stopped}p_{2}\mbox{TSE}$; once the driver has stopped, it keeps sending the ’has-stopped’ message;

$(r_{9})$

$p_{2}\mbox{FSE}\xrightarrow{not-stopped}p_{2}\mbox{FSE}$; the process sends a ’not-stopped’ message if the driver is still running.

8.2.4 The process STOP-D.

Let $p_{3}$ be its unique state. It has three control points $s_{0}$, $s_{1}$, and $R$, the last one standing for ’release resources’. STOP-D is represented by the following SDPN rules:

$(r_{10})$

$p_{3}s_{0}\xrightarrow{stop}p_{3}f_{Decrement}s_{1}$; STOP-D sends a ’stop’ request to the process STOPPING-FLAG, and calls the function Decrement;

$(r_{11})$

$p_{3}s_{1}\xrightarrow{\overline{has-stopped}}p_{3}R$; if the driver has stopped, the allocated resources are released.

8.2.5 The process REQUEST.

The process REQUEST executes the following instructions:

• •

it starts by calling a function Increment; this function returns -1 (stack symbol $a_{-1}$) if the STOPPING-FLAG is set to TRUE, otherwise, it increments the counter, and returns 0 (stack symbol $a_{0}$);

• •

if Increment returns 0, then REQUEST performs its task if it can assert that STOPPING-EVENT is in state FSE (i.e., that the driver is still running);

• •

it calls afterwards a function Decrement that decrements the counter; if this counter has reached 0, it sends a message to inform STOPPING-EVENT that the driver has stopped since there are no more requests running.

The process REQUEST has three control points $r_{0}$, $r_{Work}$, $r_{End-Work}$, and $A$, the last one standing for ’abort’, and an unique state $p_{4}$. It can be modelled by the following SDPN rules:

$(r_{12})$

$p_{4}r_{0}\xrightarrow{\tau}p_{4}f_{Increment}$; first, the function Increment is called;

$(r_{13a})$

$p_{4}a_{0}\xrightarrow{\tau}p_{4}r_{Work}r_{End-Work}$ and $(r_{13b})$ $p_{4}r_{Work}\xrightarrow{\tau}\varepsilon$; if the function Increment returns 0, then REQUEST can perform its (abstracted) work;

$(r_{14})$

$p_{4}r_{End-Work}\xrightarrow{\overline{non-stopped}}p_{4}f_{Decrement}$; once the work is finished, the process checks if the driver is still running, i.e. that process STOPPING-EVENT is in FSE;

$(r_{15})$

$p_{4}r_{End-Work}\xrightarrow{\overline{has-stopped}}p_{4}A$; if it is not the case, the program has reached an erroneous configuration and aborts.

8.2.6 The process GEN-REQ.

Let $p_{5}$ be its unique state, and $g_{0}$ its unique control point. GEN-REQ is represented by the following SDPN rule:

$(r_{16})$

$p_{5}g_{0}\xrightarrow{\overline{non-stopped}}p_{4}r_{0}p_{5}g_{0}$; the process can spawn new requests as long as the driver is running.

8.2.7 The function Increment.

It has three control points $i_{0}$, $a_{0}$, and $a_{-1}$. The function Increment is represented by the following SDPN rules, as only REQUEST calls this function:

$(r_{17})$

$p_{4}f_{Increment}\xrightarrow{\overline{stopR}}p_{4}a_{-1}$; if STOPPING-FLAG is in TSF, the function returns $-1$;

$(r_{18a})$

$p_{4}f_{Increment}\xrightarrow{\overline{not-stopR}}p_{4}i_{0}$ and $(r_{18b})$ $p_{4}i_{0}\xrightarrow{incr}p_{4}a_{0}$; otherwise, it returns 0 and increments the counter.

8.2.8 The function Decrement.

It has two control points $d_{0}$ and $d_{1}$. The function Decrement is represented by the following SDPN rules, where $p$ stands for either $p_{3}$ or $p_{4}$, as only REQUEST and STOP-D call this function:

$(r_{19})$

$pf_{Decrement}\xrightarrow{decr}pd_{0}$; the counter is decremented;

$(r_{20})$

$pd_{0}\xrightarrow{\overline{not-zero}}p\varepsilon$; then, if it has not reached 0, the function terminates;

$(r_{21a})$

$pd_{0}\xrightarrow{\overline{is-zero}}pd_{1}$ and $(r_{21b})$ $pd_{1}\xrightarrow{has-stopped}\varepsilon$; otherwise, a message ’has-stopped’ is sent to STOPPING-EVENT.

We therefore model the program as a SDPN $M=(Act,P,\Gamma,\Delta)$, with:

• •

a set of control states $P=\{p_{0},p_{1},p_{2},p_{3},p_{4},p_{5}\}$;

• •

a set of stack symbols $\Gamma=\{0,1,\mbox{FSF},\mbox{TSF},\mbox{FSE},\mbox{TSE},s_{0},s_{1},R,r_{0},r_{Work},\linebreak r_{End-Work},A,g_{0},f_{Increment},i_{0},a_{0},a_{-1},f_{Decrement},d_{0},d_{1}\}$;

• •

a set of actions $Act=\{\tau,\}\cup L\cup\overline{L}$, where $L=\{incr,decr,is-zero,not-zero,stopR,not-stopR,has-stopped,non-stopped,stop\}$;

• •

a set of transitions $\Delta=\{r_{1a},r_{1b},\ldots,r_{21a},r_{21b}\}$.

In the initial configuration, the counter is set to one, the flags in the processes STOPPING-FLAG and STOPPING-EVENT to FALSE, and all processes but REQUESTs (that will later be spawned by GEN-REQ) are running. We then need to check if the SDPN model of the program can reach with perfect synchronization a configuration where the process COUNTER has released its ressources and reached a control point $R$, while a process REQUEST has aborted its task and reached a control point $A$.

Our goal is therefore to check if, from the initial configuration $c_{0}=p_{0}10\cdot p_{1}FSF\cdot p_{2}FSE\cdot p_{3}s_{0}\cdot p_{5}g_{0}$, a configuration in the forbidden set of configurations:

[TABLE]

is reachable.

8.3 An erroneous execution path

We write $(r_{i})\leftrightarrow(r_{j})$ if we apply two rules that synchronize. The erroneous execution path is the following, starting from configuration $c_{0}$

[TABLE]

$(r_{16})$ GEN-REQ spawns a REQUEST;

[TABLE]

$(r_{12})$ REQUEST calls Increment;

[TABLE]

$(r_{6})\leftrightarrow(r_{18a})$ STOPPING-FLAG sends $not-stopR$ to Increment;

[TABLE]

$(r_{10})\leftrightarrow(r_{4})$ STOP-D sends $stop$ to STOPPING-FLAG;

[TABLE]

$(r_{19})\leftrightarrow(r_{2})$ Decrement called by STOP-D sends $decr$ to COUNTER;

[TABLE]

$(r_{3b})\leftrightarrow(r_{21a})$ COUNTER sends $is-zero$ to Decrement called by STOP-D;

[TABLE]

$(r_{18b})\leftrightarrow(r_{1b})$ Increment called by REQUEST resume its execution, returns [math], and sends $incr$ to COUNTER;

[TABLE]

$(r_{21a})\leftrightarrow(r_{8})$ Decrement called by STOP-D sends a signal $has-stopped$ to procedure STOPPING-EVENT;

[TABLE]

$(r_{8})\leftrightarrow(r_{11})$ Decrement STOPPING-EVENT sends $has-stopped$ to STOP-D that releases resources;

[TABLE]

$(r_{13a})$ REQUEST starts its task;

[TABLE]

$(r_{13b})$ REQUEST performs its work;

[TABLE]

$(r_{8})\leftrightarrow(r_{15})$ STOPPING-EVENT sends $has-stopped$ to REQUEST that aborts;

[TABLE]

This is an erroneous configuration reachable in 12 steps. We can find it using a prefix abstraction of order 12.

9 Related work

Wenner introduced in [Wen10] a model of weighted dynamic pushdown networks (WDPNs), extending the work of Reps et al. on weighted pushdown systems in [RSJM05] to DPNs. WDPNs share some similarities with our abstraction framework on SDPNs: each transition is labelled by a weight in a bounded idempotent semiring, these weights can be composed along execution paths, and the sum of the weights of all execution paths between two sets of configurations can be computed, provided that a simple extension of the original semiring to an abstract set of execution hedges can be found. WDPNs, however, do not feature simultaneous, synchronized actions between pushdown processes. Moreover, in order to be efficient, the extensions of the abstract domain have to be chosen on a case-by-case basis in order to label tree automata, whereas our framework works for every finite-domain abstraction and only uses finite state automata.

Multi-stack pushdown systems (MPDSs) are pushdown systems with two or more stacks, and can be used to model synchronized parallel programs. Qadeer et al. introduced in [QR05] the notion of context, that is, a part of an execution path during which only one stack of the automaton can be modified. The reachability problem within a bounded number of context switches is decidable for MPDSs. However, MPDSs have a bounded number of stacks and, unlike SDPNs, cannot therefore handle the dynamic creation of new threads.

Bouajjani et al. introduced in [BESS05] asynchronous dynamic pushdown networks, or ADPNs. This model extends DPNs by adding a global control state to the whole network as a mean of communication between processes; each pushdown process can then apply rules either by reading its own local state or the global state of the network. The reachability problem within a bounded number of context switches is decidable for ADPNs, where a context here stands for a part of an execution path during which transitions altering global variables are all executed by the same process. This is an under-approximation of the actual reachability problem for synchronized parallel programs, whereas we compute in this paper an over-approximation of the same problem. The former can be used to find errors in a program but, unlike the latter, does not allow one to check that a program is free from errors.

Concurrent program with recursive procedures can be modeled as a network of synchronized pushdown systems. This model, called communicating pushdown systems (CPDSs), was introduced by Bouajjani et al. in [BET03]. The reachability problem being undecidable for this class of automata, a Kleene algebra framework was designed in order to find an over-approximation of the answer. Extensions of the abstraction framework of [BET03] were defined in [BET05, Tou05] to compute abstractions of execution paths of multi-threaded recursive programs communicating via rendez-vous. However, unlike SDPNs, the models considered in these articles cannot describe thread spawns, where the father of a new thread can resume its execution independently of its children.

10 Conclusion

Our first contribution in this paper is a new pushdown system model that can handle both synchronization by rendez-vous between parallel threads and thread spawns. The reachability problem being undecidable for this class of automata, we seek to over-approximate it by abstracting the set of paths between two regular sets of configurations $C$ and $C^{\prime}$.

To this end, we introduce relaxed semantics with weaker synchronization constraints and extend the Kleene algebra abstraction framework shown in [BET03]. We label an automaton accepting the set of predecessors of $C^{\prime}$ with functions on a finite Kleene abstraction. These functions depend on a set of constraints computed according to the pushdown rules used during the saturation procedure.

This over-approximation allows us to define an iterative abstraction refinement scheme. We then apply it to find an erroneous execution trace in a Windows Bluetooth driver.