Verification of parallelising transformations of KPN models

Abstract

Parallelising transformations of Kahn process networks (KPNs) are important mechanisms for achieving speedup for deployment on heterogeneous multiprocessor systems particularly in the domain of signal processing applications. Correctness of such parallelising transformations is crucial for their reliable applications. In this study, verification frameworks for checking correctness of sequential to KPN behavioural transformation and KPN level transformations are presented. To the best of the authors’ knowledge, these are the first such approaches for verification problems. The sequential behaviour and the KPN behaviours are both modelled as array data dependence graphs (ADDGs) and the verification problem is posed as the problem of checking of equivalence between the two ADDGs. The key aspect of the proposed scheme is to model a KPN behaviour as an ADDG. Correctness of KPN to ADDG construction method is proved. Experimental results supporting usability of this scheme are also provided.

1 Introduction

Multiple processors operating at a lower clock frequency can provide the same performance with a lower energy consumption [1] than as a single processor at a much higher clock frequency. Therefore, multiprocessor implementations not only deliver the necessary computational power, but also provide the required power efficiency. Naturally, modern-day embedded system design trends are towards multiprocessor systems. Embedded systems generally consist of hardware components, real-time firmware and application software running on them. However, both hardware and software components have their inherent heterogeneity. Hardware components consist of general purpose and special purpose processors (which again can be hard-core or soft-core FPGA based), specialised ASICs and so on. Similarly, the software components are based on different application tasks which are modelled using different models of computation in the high level. To cope with the multiprocessor characteristics, a parallel model of computation is needed as the programming model. There are two basic approaches to achieve parallelism. One is to seek a parallelised solution to the given problem. The other approach is to take up suitable sequential solution and parallelise it. The first option relies on the ability of a system designer to manually partition the application's core, memory and control across the platform hardware components [2]. Such an approach is time consuming and much more error prone. According to the second option, parallelism is automatically extracted by a compiler. A parallelising compiler performs a suite of transformations on a sequential program to convert it to a parallel program. Clearly, the second option is more amenable to routine handling and is now commonly used [3]. In the case of multimedia and signal processing applications, Kahn process network (KPN) [4] model of computation is a fair choice for representing parallel behaviour. In fact, KPN model has been used in many of the present day embedded system tools like Compaan [5], Artemis [6], Daedalus [7], Metropolis [8], Espam [9]. The localised control and distributed memory in a KPN are the two key ingredients that allow program heterogeneous multiprocessor KPN [4] is a deterministic model of computation which consists of a set of processes and a set of first-in-first-out (FIFO) communication channels. The processes, which are individually sequential programs, run in parallel. They communicate data among themselves through unidirectional FIFO channels. The FIFOs, which ideally of unbounded capacity, are used for point-to-point communication among the processes. A process may write any amount of data to a FIFO. Blocking happens when reading from an empty channel (i.e. blocking read) which serves as a synchronising mechanism between the processes. At any given time, a process is either computing or waiting on one of its empty input FIFO channels. FIFOs are represented by data streams and processes by functions that map streams into streams. A stream is a finite or infinite sequence of data elements.

The parallel process network models are obtained from the sequential behaviour in an automated way or manually may not be suitable for the target architectural platform. Moreover, the overall achieved performance obtained as a result of mapping may not be satisfactory from the point of view of the data throughput and/or memory usage. In this case, it is necessary to manipulate the amount of concurrency in the functional model. Too little concurrency may not be desirable since it may not completely make use of the architectural capabilities. Too much concurrency, in contrast, may require too large overhead to eventually manage in the architecture, which may increase the overall latency. The transformation techniques like computation migration, process splitting, channel merging, process clustering, and unfolding and skewing may be used to control the concurrency in the KPN behaviour according to the architectural constraints [10–13]. The verification task, therefore, is to show the equivalence between two KPN behaviours.

Verifying correctness of parallelising transformations is an important step in ensuring dependability of embedded systems. The verification task here involves showing the equivalence between a sequential behaviour and its corresponding parallel KPN behaviour. Obviously, the overall data transformation of the KPN behaviour can only be captured if the global data dependencies are captured. The challenge lies in capturing the data dependencies spread over all the concurrent KPN processes independent of their possible interleaving. Formal verification, an attractive alternative to traditional methods of testing and simulation, tend to be expensive, time consuming and hopelessly inadequate for embedded systems. There are two fundamental approaches of formal verification of compilers. The first approach proves that the steps of the compiler are correct by construction. In this setting, to prove that an optimisation is correct, one must prove that for any input program, the optimisation produces a semantically equivalent program. The primary advantage of correct by construction techniques is that optimisations are known to be correct when the compiler is built, before they are run even once. Most of the techniques that provide correct by construction guarantees require user interaction [14]. Moreover, correct by construction proofs are harder to achieve because they must show that any application of the optimisation is correct. Despite the fact that a significant amount of work has been carried out for verifying that synthesis steps are correct by construction, the state-of-the-art techniques fall far short of the goal [15]. However, one can at least show that, for each translation that a compiler performs, the output produced has the same behaviour as the original behaviour. This approach is called translation validation. Although this approach does not guarantee the correctness of the compilation process, it at least guarantees that any errors in translation will be caught when the particular steps of ES design tool are performed, preventing such errors from propagating any further in the synthesis process. In this paper, we work on developing translation validation methodologies for sequential to KPN transformations applied during embedded systems.

The objectives of this work are to show the equivalence between a sequential behaviour and its corresponding parallel KPN behaviours and to show equivalence between two KPN behaviours. Application programs in signal processing and multimedia domains primarily involve nested loops. The translation process explores the loop level parallelism in such programs. Therefore, processes in the generated KPN also involve nested loops. Since, all the loop bounds are finite, the amount of data communicated through a FIFO channel is also finite. In the original definition of KPN, each process, however, maps a set of input sequences (from the incoming FIFOs) into a set of output sequences (to the outgoing FIFOs) where the input sequences can be finite or infinite. Therefore, a restricted class of KPNs are considered in this work where each process of the KPN is a nested loop program and the amount of data communicated through a FIFO is finite. Array data dependence graphs (ADDGs), first proposed by Shashidhar [16], have been used for verification of loop transformations applied on array-intensive behaviours. His work considers a restricted class of programs which must have static control-flow, affine indices and bounds, uniform recurrences and single assignment form. In [17], the authors have reported an extension to Shashidhar's original work for the same restricted class of programs to handle algebraic transformations based on commutativity, associativity and distributivity, constant folding, simplification of arithmetic expressions and so on. Since the present work also addresses array and loop intensive behaviours, we have adopted ADDGs as the models for the behaviours.

The contributions of the paper are as follows. (i) An ADDG-based equivalence checking method for verification of sequential to KPN transformations is presented. We have also presented similar equivalence checking method for verification of some optimising transformation on KPNs. Our verification flow is depicted in Fig. 1. Specifically, we first construct ADDGs from both sequential and KPN behaviours. The equivalence between the sequential behaviour and its corresponding KPN behaviour is then established by checking equivalence between two ADDGs. Similarly, equivalence between the input KPN and the transformed KPN are established by showing equivalence of two ADDGs. (ii) We have shown that ADDGs can be used to model parallel KPN behaviours. The challenge is in showing that ADDGs can actually capture the data dependencies spread over all the concurrent KPN processes independent of their possible interleaving. In particular, to model a KPN as an ADDG, the KPN processes are first represented as ADDGs which are then composed. Special processing is required for capturing FIFOs in ADDG. (iii) The correctness of the ADDG composition step is proved for a deadlock-free KPN. (iv) A case study of verification of computation migration transformation is presented. (v) The experimental results are presented for both transformations. An initial version of the work is presented in [18].

[IMAGE OMITTED. SEE PDF]

The paper is organised as follows. The related works are discussed in Section 2. The ADDG and other notions are discussed briefly in Section 3. The scheme of modelling a KPN as an ADDG is given in Section 4. The equivalence checking method of ADDGs is given in Section 5. The correctness of the method is given in Section 6.1. A case study on verification of computation migration is discussed in Section 7. Some experimental results are given in Section 8. Finally, the paper is concluded in Section 9.

2 Background and related works

The KPN is a deterministic parallel model of computations (MoC) that explicitly specifies tasks as processes and distributed memory units as FIFO channels. In fact, KPN model has been used in many of the present day embedded system tools like Compaan [2], Artemis [6], Daedalus [7], Metropolis [8], MAMPs [19] and Espam [9] in the domain of signal processing applications. The processes, which are individually sequential programs, run in parallel. They communicate data among themselves through unidirectional FIFO channels. The FIFOs, which are ideally of unbounded capacity, are used for point-to-point communication among the processes. A process may write any amount of data to a FIFO. Blocking happens when reading from an empty channel (i.e. blocking read) which serves as a synchronising mechanism between the processes.

Tools like Compaan [2] or Espam [9] automatically convert nested loop programs into its functionally equivalent KPNs. However, tools like Artemis [6], Daedalus [7], Metropolis [8], MAMPs [19] do not prove the correctness of their transformations. Moreover, the sequential to parallel and the parallel level transformations are applied manually in many scenarios which are error prone. Therefore, verification of both sequential to KPN and KPN level transformations are extremely important in ensuring reliability of such systems. To the best of our knowledge, these two particular verification problems are not addressed in the literature. In this paper, we work on developing translation validation methodologies for sequential to KPN transformations and KPN level transformations.

Process algebra uses algebraic approaches to study the communications of the concurrent systems. There are three typical calculus systems: calculus of communicating systems (CCS) [20], communicating sequential processes [21] and algebra of communicating processes [22]. In these languages, the behaviour of concurrent system, which is a collection of all computations and interactions among process, can be studied. Applications of process algebra exist in diverse fields such as safety critical systems, network protocols and biology. A number of verification techniques based on process algebra has been developed for proving the correctness of concurrent systems. Among the popular verification techniques are model checking, equivalence checking and theorem proving. The ultimate goal of these techniques is to prove that a concurrent system will always perform the right computations, or never perform wrong computations. In many critical applications, like the on-board software of an aeroplane, a software failure is undesirable. By formally verifying such systems, their reliability can be improved. The paper [23] formulates basic CCS, with observational equivalence and strong equivalence defined inductively. The Hennessy-Milner logic is introduced in this work which provides a logical characterisation of process equivalence. In [24], the formulation of bisimulation relation of process algebra is introduced. Strong bisimulation and weak bisimulation became the central notion of equivalence in process theory.

In model checking, a model of a concurrent system is constructed together with a desired property that this system should have. It is then checked whether the model satisfies the property. The model is represented by a finite state machine and the property is formulated in a temporal logic [25]. The technique originated from works by Clarke and Emerson [26], and Queille and Sifakis [27]. For finite systems, model checking is effectively decidable, meaning that it can be done fully automatically by a computer program. Indeed, the development of automated model checkers like, EMC [26], CESAR [27], SPIN [28], SMV [29] and CADP [30], played an important role in the successful application of the technique to real-life sequential systems like hardware circuit designs. However, limitations of the approach were encountered when it was applied to more complex, concurrent software systems. The parallelism between the processes of such systems leads to a combinatorial blow-up of the number of states that the system can be in, yielding state spaces that are too large to handle for traditional model checkers. This problem is known as the state (space) explosion problem and a range of techniques has been developed to address it, including: symbolic representation of state spaces using binary decision diagrams [31], partial order reduction [32], abstract interpretation [33], symmetry reduction [34] and compositional reasoning [35].

An approach for symbolic model checking of process networks is introduced in [36]. The authors have identified the problem with binary decision diagram based symbolic model checking of process networks and introduced a representation of multi-valued functions called interval decision diagrams. Raudvere et al. [37] proposed some non-semantic preserving transformations of process networks during refinement steps of embedded system design involving lower-level implementation details. In this approach, a set of verification properties for every such transformation are defined as CTL* formulae. The verification tasks are divided into two steps: (i) the local correctness of the transformation is checked by proving these properties using a model checking tool, and (ii) the global influence of the refinement to the entire system is studied through static analysis. In [38], the designs at different abstraction levels are automatically translated into Promela description and verified using SPIN model checker [28].

When a sequential behaviour is transformed into a parallel behaviour, it is necessary to ensure that (i) the transformed behaviour satisfies certain properties of the systems and (ii) it is functionally equivalent to the initial behaviour. For the first task, model checking is used as the primary verification approach for embedded system design. For the second task, model checking, however, cannot be used as it is more appropriate for property verification but not for behavioural verification. For a complex system (such as an embedded system), however, correctness of a synthesisable specification is not restricted to some liveness or safety properties only; instead, it depicts the behaviour at a high abstraction level in a procedural form. When a behaviour is transformed towards an optimised implementation, it is important to show that the transformed behaviour preserves the functional behaviour of the initial specification. The state-of-the-art embedded system verification literature is lacking in this aspect. The objective of this work is to show the functional equivalence between a sequential behaviour and its corresponding KPN behaviour and equivalence between two KPN behaviours.

3 Array data dependence graphs

$$

Definition 1

(ADDG): The ADDG of a sequential behaviour is a directed graph $G=(V,E)$, where the vertex set V is the union of the set A of array nodes and the set F of operator nodes and the edge set $E=\{⟨a,f⟩|a\in A,f\in F\}\cup \{⟨f,a⟩|f\in F,a\in A\}$. An edge of the form $⟨a,f⟩$ is a write edge; it captures the dependence of the left-hand side (lhs) array node of an assignment statement on the operator corresponding to the right-hand side (rhs) expression. An edge of the form $⟨f,a⟩$ is a read edge; it captures the dependence of the rhs operator on the (rhs) operand arrays of the statement. An assignment statement S of the form $l[{\mathit{e}}_l]=f(r_1[{\mathit{e}}_1],\dots ,r_k[{\mathit{e}}_k])$, where ${\mathit{e}}_1,\dots ,{\mathit{e}}_k$ and ${\mathit{e}}_l$ are the vectors of index expressions of the arrays $r_1,\dots ,r_k$ and l, appears as a subgraph $G_S$ of G, where $G_S=⟨V_S,E_S⟩$, $V_S=A_S\cup F_S$, $A_S=\{l,r_1,\dots ,r_k\}\subseteq A$, $F_S=\{f\}\subseteq F$ and $E_S=\{⟨l,f⟩\}\cup \{⟨f,r_i⟩,1\le i\le k⟩\}\subseteq E$. The write edge $⟨l,f⟩$ is associated with the statement name S. The vertex set $A_I\subset A$ with out-degree zero are the input array nodes and $A_O\subset A$ with in-degree zero are the output array nodes in the ADDG.

A sequential program can be represented as an ADDG under the following restrictions: single-assignment, affine indices and bounds, static control-flow and uniform recurrences [16]. In a single-assignment form program, any variable other than the loop indices can be replaced with an array variable [16] with as many elements as the number of times the variable is assigned in the program. Therefore, without loss of generality, it is assumed that all the statements in the behaviours involve only array variables. In fact, the application domain that we are considering also consists of array intensive behaviours.

Fig. 2 shows a sequential behaviour and its corresponding ADDG. The example is taken from [39]. Certain information will be extracted from each statement S of the behaviour and associated with the write edge labelled with S in the ADDG. Let us first consider for this purpose the generalised x-nested loop structure given in Fig. 3 in which S occurs. Each index $i_k$ has a lower limit $L_k$ and a higher limit $H_k$ and a step constant (increment/decrement) $r_k$. The parameters $L_k,H_k$ and $r_k$ are all integers. The statement S executes under the condition $C_D$ over the loop indices $i_k,1\le k\le x,$ within the loop body. All the index expressions $e_1,\dots ,e_k$ of the array d and the expressions $e_{11}^{\mathrm{\prime }},\dots ,e_{1l_1}^{\mathrm{\prime }},\dots ,e_{m1}^{\mathrm{\prime }},\dots ,e_{m{l}_m}^{\mathrm{\prime }}$ of the corresponding arrays $u_1,\dots ,u_m$ in the statement S are affine arithmetic expressions over the loop indices.

[IMAGE OMITTED. SEE PDF]

[IMAGE OMITTED. SEE PDF]

$$

Definition 2

(Iteration domain of the statement S ($I_S$)): For each statement S within a generalised loop structure with nesting depth x, the iteration domain $I_S$ of the statement is a subset of ${\mathbb{Z}}^x$ defined as$I_S=\{[i_1,i_2,\dots ,i_x]|\underset{k=1}{\overset{x}{\wedge }}(L_k\le i_k\le H_k\wedge C_D\wedge \mathrm{\exists }{\alpha }_k\in \mathbb{Z}(i_k={\alpha }_k{r}_k+L_k))\}$ where $i_k,L_k,H_k,r_k,1\le k\le x$, are integers.

For the statements $S1$ and $S2$ of Fig. 2a, the respective iteration domains are$I_{S1}=\{[i,j]|1\le i\le M\wedge 4\le j\le N\wedge (\mathrm{\exists }{\alpha }_1,{\alpha }_2\in \mathbb{N}|i={\alpha }_1+1\wedge j={\alpha }_2+4)\}$ and$I_{S2}=\{[l,m]|3\le l\le M\wedge 3\le m\le N-1\wedge l+m\le 7\wedge (\mathrm{\exists }{\alpha }_1,{\alpha }_2\in \mathbb{N}|l={\alpha }_1+3\wedge m={\alpha }_2+3)\}$ Each point $[i_1,i_2,\dots ,i_x]$ in $I_S$ denotes exactly one execution of the statement S. Each statement of a program defines the elements of an array (occurring in the lhs) using the elements of a set of operand arrays (appearing in the rhs). Therefore, for each statement, we may speak of a definition domain and a definition mapping of the lhs array in the statement. The former comprises the domain from which the lhs array indices assume values and the latter provides the mapping between the elements of the iteration domain of the statement to the definition domain of the lhs array. Similarly, for each rhs array of each statement, we have an operand domain and an operand mapping of the rhs array in the statement. The former comprises the domain from which the indices of rhs array of the statement assume values and the latter provides the mapping between the elements of the iteration domain of the statement to the operand domain of the rhs array. There are one operand domain and one operand mapping for each of the arrays in the rhs of the statement. The following definitions are in order.

$$

Definition 3

(Definition mapping (${}_S{M}_d$)): The definition mapping describes the association between the elements of the iteration domain of a statement and the elements of its lhs array d (depicted as suffix)${}_S{M}_d=I_S\to {\mathbb{Z}}^{k}s.t.\forall \mathit{v}\in I_S,\mathit{v}\mapsto [e_1(\mathit{v}),\dots ,e_k(\mathit{v})]\in {\mathbb{Z}}^k.$

The image of the function ${}_S{M}_d$ is called the definition domain of the lhs array d, denoted as ${}_S{D}_d$; so, ${}_S{D}_d{=}_S{M}_d(I_S)$.

$$

Definition 4

(Operand mapping (${}_S{M}_{u_n}$)): The operand mapping describes the association between the elements of the iteration domain of a statement and the elements of the rhs array $u_n$ (depicted as suffix)${}_S{M}_{u_n}=I_S\to {\mathbb{Z}}^{l_n}s.t.\forall \mathit{v}\in I_S,\mathit{v}\mapsto [e_{n1}(\mathit{v}),\dots ,e_{n{l}_n}(\mathit{v})]\in {\mathbb{Z}}^{l_n}.$

The image ${}_S{M}_{u_n}(I_S)$ is the operand domain of the rhs array $u_n$ in the statement S, denoted as ${}_S{U}_{u_n}$.

$$

Definition 5

(Dependence mapping (${}_S{M}_{d,u_n}$)): It describes the association of the index expression(s) of the lhs array d which is defined through S to the index expression of the operand array $u_n,1\le n\le m$, i.e. one of the rhs arrays of S$\begin{array}{rl}{}_S{M}_{d,u_n}=& \{[e_1,\dots ,e_k]\to [e_1^{\mathrm{\prime }},\dots ,e_{l_n}^{\mathrm{\prime }}]|([e_1,\dots ,e_k]{\in }_S{D}_d\wedge \\ & [e_1^{\mathrm{\prime }},\dots ,e_{l_n}^{\mathrm{\prime }}]{\in }_S{U}_{u_n}\wedge \mathrm{\exists }\mathit{v}\in I_S|([e_1,\dots ,e_k]{=}_S{M}_d(\mathit{v})\\ & \wedge [e_1^{\mathrm{\prime }},\dots ,e_{l_n}^{\mathrm{\prime }}]{=}_S{M}_{u_n}(\mathit{v})))\}\end{array}$ The defined array d is k-dimensional and $e_1,\dots ,e_k$ are its index expressions over the loop indices $\mathit{v}$; the array $u_n$ is an $l_n$-dimensional array, and $e_1^{\mathrm{\prime }},\dots ,e_{l_n}^{\mathrm{\prime }}$ are its index expressions over the indices $\mathit{v}$.

The dependence mapping ${}_S{M}_{d,u_n}$ can be obtained by the right composition ($\mathrm{♢}$) (The right composition operation is defined as $(f\mathrm{♢}g)(x)=g(f(x))$) of the inverse of definition mapping of d (i.e. ${(}_S{M}_d{\hspace{0.17em})}^{-1}$) and the operand mapping of $u_n$ (i.e. ${}_S{M}_{u_n}$), i.e. by${}_S{M}_{d,u_n}={(}_S{M}_d{\hspace{0.17em})}^{-1}{\mathrm{♢}}_S{M}_{u_n}$ Specifically, ${}_S{M}_{d,u_n}{(}_S{D}_d){=}_S{M}_{u_n}({(}_S{M}_d{\hspace{0.17em})}^{-1}{(}_S{D}_d)){=}_S{M}_{u_n}(I_S){=}_S{U}_{u_n}$.

The domain of the dependence mapping ${}_S{M}_{d,u_n}$ is the definition domain of d, i.e. ${}_S{D}_d$. The range of ${}_S{M}_{d,u_n}$ is the operand domain ${}_S{U}_{u_n}$. There would be one such mapping from the defined array to each of the operand arrays in the rhs of S.

For two consecutive statements Q defining an array y in terms of an array z and P defining an array x in terms of the array y, the dependence mapping between the array x and the array z, i.e. ${}_{PQ}{M}_{x,z}$, can be obtained from the mappings ${}_P{M}_{x,y}$ and ${}_Q{M}_{y,z}$ by right composition ($\mathrm{♢}$) of ${}_P{M}_{x,y}$ and ${}_Q{M}_{y,z}$. The following definition captures this computation.

$$

Definition 6

(Transitive dependence): ${}_{PQ}{M}_{x,z}{=}_P{M}_{x,y}{\mathrm{♢}}_Q{M}_{y,z}$ $=\{[i_1,\dots ,i_{l_1}]\to$ $[k_1,\dots ,k_{l_3}]$ $|\mathrm{\exists }[j_1,\dots ,j_{l_2}]s.t.$ $[i_1,\dots ,i_{l_1}]$ $\to [j_1,\dots ,j_{l_2}]{\in }_P{M}_{x,y}\wedge$ $[j_1,\dots ,j_{l_2}]\to [k_1,\dots ,k_{l_3}]{\in }_Q{M}_{y,z}\}$, where y is used in P and is defined in Q.

The domain ${}_{PQ}{D}_x$ say, of the resultant dependence mapping (i.e. ${}_{PQ}{M}_{x,z}$) is the subset of domain of ${}_P{M}_{x,y}$ such that $\forall i{\in }_{PQ}{D}_x{,}_P{M}_{x,y}(x)=\{j|j\in range{(}_P{M}_{x,y})\cap domain{(}_Q{M}_{y,z})\}$. Thus, ${}_{PQ}{D}_x{=}_P{M}_{x,y}^{-1}{(}_Q{M}_{y,z}^{-1}{(}_Q{U}_z){\cap }_P{M}_{x,y}{(}_P{D}_x))$. Similarly, the range of ${}_{PQ}{M}_{x,z}$ is ${}_{PQ}{U}_z{=}_Q{M}_{y,z}{(}_P{M}_{x,y}{(}_P{D}_x)\cap {}_Q{M}_{y,z}^{-1}{(}_Q{U}_z))$.

$$

Example 1

Let us consider the behaviour and its corresponding ADDG of Fig. 2. Let us now consider the statements $S4$ and $S2$ of the behaviour. We have$I_{S4}=\{[l,m]|3\le l\le M\wedge 3\le m\le N-1\wedge (\mathrm{\exists }{\alpha }_1,{\alpha }_2\in \mathbb{Z}|l={\alpha }_1+3\wedge m={\alpha }_2+3)\},$${}_{S4}{D}_{\text{out}1}=I_{S4},{}_{S4}{U}_{r2}=I_{S4},$${}_{S4}{M}_{\text{out}1,r2}=\{[l,m]\to [l,m]|[l,m]{\in }_{S4}{D}_{\text{out}1}\},$$I_{S2}=\{[l,m]|3\le l\le M\wedge 3\le m\le N-1\wedge l+m\le 7\wedge (\mathrm{\exists }{\alpha }_1,{\alpha }_2\in \mathbb{Z}|l={\alpha }_1+3\wedge m={\alpha }_2+3)\},$${}_{S2}{D}_{r2}=I_{S2},$${}_{S2}{U}_{r1}=\{[l-1,m-2]|[l,m]\in I_{S2}\}$ and${}_{S2}{M}_{r2,r1}=\{[l,m]\to [l-1,m-2]|[l,m]{\in }_{S2}{D}_{r2}\}.$

The transitive dependence mapping ${}_{S4S2}{M}_{\text{out}1,r1}$ can be obtained from ${}_{S4}{M}_{\text{out}1,r2}$ and ${}_{S2}{M}_{r2,r1}$ by the composition operator $\mathrm{♢}$ as follows:$\begin{array}{rl}{}_{S4S2}{M}_{\text{out}1,r1}& {=}_{S4}{M}_{\text{out}1,r2}{\mathrm{♢}}_{S2}{M}_{r2,r1}\\ & =\{[l,m]\to [l,m]|[l,m]{\in }_{S4}{D}_{\text{out}1}\}\mathrm{♢}\{[l,m]\to \\ & [l-1,m-2]|[l,m]{\in }_{S2}{D}_{r2}\}\\ & =[l,m]\to [l-1,m-2]|[l,m]{\in }_{S4}{D}_{\text{out}1}\}\end{array}$

3.1 Construction of the ADDG from a sequential behaviour

Let us now discuss how the ADDG of a given sequential program can be obtained. The method of obtaining the ADDG for a parallel KPN behaviour is described in the next section. Initially, the ADDG $G=(V,E)$ is empty, i.e. $V=\varnothing$ and $E=\varnothing$. We read the statements of the behaviour sequentially according to their positions from top. Corresponding to a statement S of the form $l[{\mathit{e}}_l]=f(r_1[{\mathit{e}}_1],\dots ,r_k[{\mathit{e}}_k])$ read, our ADDG construction mechanism works as follows:

• It extracts the iteration domain of the statement ($I_S$), the definition mapping (${}_S{M}_l$) and the definition domain (${}_S{D}_l$) of the lhs array, and the operand mapping (${}_S{M}_{r_i}$) and the operand domain (${}_S{U}_{r_i}$) of each rhs array $r_i,1\le i\le k$; it then computes the dependence mapping ${}_S{M}_{l,r_i}$ accordingly as described above.

• It next constructs the subgraph $G_S$ of S where $G_S=⟨V_S,E_S⟩$, $V_S=A_S\cup F_S$, $A_S=\{l,r_1,\dots ,r_k\}$, $F_S=\{f\}$ and1$E_S=\{⟨l,f⟩\}\cup \{⟨f,r_i⟩,1\le i\le k⟩\}\subseteq E.$ The write edge $⟨l,f⟩$ is associated with the statement name S and the read edge $⟨f,r_i⟩,1\le i\le k,$ is associated with the dependence mapping ${}_S{M}_{l,r_i}$. The subgraph $G_S$ is added to G. Specifically, $V=V\cup V_S$ and $E=E\cup E_S$.

3.2 Slices

A slice is a connected subgraph of an ADDG which has an array node as its start node (having no edge incident on it), only array nodes as its terminal nodes (having no edge emanating from them), all the outgoing edges (read edges) from each of its operator nodes and exactly one outgoing edge (write edge) from each of its array nodes.

The subgraph corresponding to each statement in the ADDG in Fig. 2 represents a slice. Also, the subgraph of each of the statement sequences $⟨S2S1⟩$, $⟨S3S1⟩$, $⟨S4S2⟩$, $⟨S4S3⟩$, $⟨S4S2S1⟩$ and $⟨S4S3S1⟩$ represents a slice in this ADDG. The start array node of a slice depends on each of the terminal array nodes through a sequence of statements. Therefore, the dependence mapping between the start array node and each of the terminal array nodes of a slice can be computed as the transitive dependence mapping over the sequence of statements from the start node to the terminal node, in question, using Definition 6. In addition, it is required to store how the start array is dependent functionally on the terminal arrays in a slice. We denote this notion as the data transformation of a slice.

$$

Definition 7

(Data transformation of a slice g ($r_g$)): It is an abstract algebraic expression e over the terminal array names of the slice such that e represents how the value of the start (output) array of the slice depends functionally on the terminal (input) arrays; the exact index expressions are abstracted out from e.

It may be noted that the dimensions of the arrays are left implicit and are accounted for in the dependence mapping. The data transformation $r_g$ can be obtained by using a backward substitution method [40] on the slice from its output array node up to the input array nodes. The backward substitution method of finding $r_g$ is based on symbolic simulation. The steps of the backward substitution method, for example, for computation of data transformation for the slice represented by the statement sequence $⟨S4S2S1⟩$ in the ADDG in Fig. 2b are as follows:

• $\text{out}1\Leftarrow F4(r2)$ [at the node $r2$],
• $\Leftarrow F4(F2(r1))$ [at the node $r1$],
• $\Leftarrow F4(F2(F1(\text{in}1,\text{in}2)))$ [at the nodes $\text{in}1$ and $\text{in}2$].

The characteristic formula (${\tau }_g$) of a slice $g(a,⟨v_1,\dots ,v_n)⟩)$ is given as the tuple2${\tau }_g=⟨r_g,{⟨}_g{M}_{a⇝v_1},\dots {,}_g{M}_{a⇝v_n}⟩⟩,$ where ${}_g{M}_{a⇝v_i},1\le i\le n,$ denotes the dependence mapping between a and $v_i$.

$$

Definition 8

(IO-slice): A slice is said to be an IO-slice iff its start node is an output array node and the terminal nodes are input array nodes.

It is required to capture the dependence of each output array on the input arrays. Therefore, IO-slices are of our interest. It may be noted that the slices represented by the statement sequences $⟨S4S2S1⟩$ and $⟨S4S3S1⟩$ are the only two IO-slices in the ADDG in Fig. 2b.

4 Modelling a KPN as an ADDG

The main challenge is to capture the data dependencies which spread over all the concurrent KPN processes independent of their possible interleaving in an ADDG. The KPN processes are synchronised by the blocking read from empty FIFO. For a deadlock-free KPN, every FIFO element is eventually read out by the consumer process. Therefore, whatever the execution order of the processes, the data dependency across FIFO can be obtained from the first-in-first-out property. The idea is to honour the first-in-first-out property of the FIFO during capturing data dependencies across processes. The presence of deadlock, however, hampers the correctness of the data dependence computed across FIFOs. In this work, we assume the KPNs are deadlock free. The deadlock issue is discussed in Section 6.1.

The basic steps involved in modelling a KPN as an ADDG are as follows:

• Each process of the KPN is first modelled as an ADDG.
• The ADDGs corresponding to the processes are then composed to obtain the ADDG of the KPN.

Let us first introduce an example of sequential to KPN code transformation which serves as a running example for illustrating our method.

$$

Example 2

Let us consider the nested loop sequential behaviour of Fig. 2a. The structure of the KPN behaviour obtained from the above sequential behaviour is given in Fig. 4. This KPN behaviour consists of four processes and four FIFO channels as shown in the figure. The detailed behaviour of the processes of the KPN is given in Fig. 5. In particular, process $P1$ computes the elements of $r1$, process $P2$ computes those elements of $r2$ which are actually computed by the statement $S2$ in the sequential behaviour, process $P3$ computes those elements of $r2$ which are actually computed by the statement $S3$ in the sequential behaviour and process $P4$ computes the elements of the array $\text{out}1$ as in statement $S4$ in the sequential behaviour. Since the elements of $r2$ gets defined by the elements of $r1$, $P1$ sends the required elements of $r1$ to processes $P2$ and $P3$ accordingly through $\text{FIFO}1$ and $\text{FIFO}2$, respectively. Similarly, the elements of $r2$ are communicated to $P4$ for $\text{out}1$ from $P2$ and $P3$ through $\text{FIFO}3$ and $\text{FIFO}4$, respectively. Therefore, the elements of the arrays $r1$, $r2$ and $\text{out}1$ are computed in parallel in the KPN.

[IMAGE OMITTED. SEE PDF]

[IMAGE OMITTED. SEE PDF]

4.1 Modelling KPN processes as ADDGs

Each individual process in the KPN behaviour except for the get and the put FIFO primitives within the processes is a sequential program using arrays and can be modelled using ADDGs. We shall show that these two primitives can also be encompassed within the ADDG framework by utilising the first-in-first-out property of FIFOs. We may model a FIFO channel as a one-dimensional array associated with two indices namely, ‘out-pointer’ for get and ‘in-pointer’ for ‘put’ operations. Let the FIFO F communicate data from a process $P_1$ to another process $P_2$ in a KPN. In the ADDG, the FIFO F is realised as a one-dimensional array F with in-pointer $F\text{In}$ and out-pointer $F\text{Out}$, say. The statement $F.\text{put}(x)$ in $P_1$ is visualised as the assignment $F[++F\text{In}]=x$ in $P_1$. Similarly, the statement $y=F.\text{get}()$ in $P_2$ is now visualised as $y=F[F\text{Out}++]$ in $P_2$. One might argue that the blocking read property of the KPN is violated by this assignment. That is not the case during verification. Since we assume that the KPN is deadlock free, even if a consumer process is waiting for a data to be written in a particular FIFO, the data will eventually be written into the FIFO by the producer process and consumer process will consume it. The statement $y=F[F\text{Out}++]$ captures this notion. The modified behaviours of the KPN processes given in Fig. 5 are shown in Fig. 6. The individual variables are converted to arrays in order to represent them as ADDGs in the above behaviour.

[IMAGE OMITTED. SEE PDF]

Each process of the KPN can be modelled as an ADDG when its FIFOs are realised as arrays as identified above. The ADDGs of the four processes of the KPN in Fig. 6 are depicted in Fig. 7. We refer to a FIFO and the linear array corresponding to it by the same name.

[IMAGE OMITTED. SEE PDF]

4.2 Computation of the dependence mappings involving FIFOs

The exact mapping between the indices of the loop under which the statement is executed and the index of the linear array corresponding to FIFO is missing because the index expressions (basically a variable) of the linear array are not in terms of the loop indices. So, we need to represent the index variable of the linear array (corresponding to each FIFO) in terms of the loop indices under which the statement is executed. In Fig. 7a, for instance, the definition mapping and its domain for the linear array $\text{FIFO}1$ are required to obtain the dependency mappings ${}_{S11}{M}_{\text{FIFO}1,\text{in}1}$ and ${}_{S11}{M}_{\text{FIFO}1,\text{in}2}$ between the indices of the arrays $\text{in}1$ and $\text{in}2$ and the index $f1\text{In}$ of the array $\text{FIFO}1$. For this, we need to express $f1\text{In}$ in terms of the loop indices i and j.

Let us consider a general behaviour given in Fig. 8 to evolve a formulation of this mapping. In this behaviour, the array FIFO1 is computed from the values of m multi-dimensional arrays $u_1,\dots ,u_m$ in a loop with a nesting depth x. Here, $e_{i1},\dots ,e_{i{l}_i},1\le i\le m$, are affine expressions and $C_D$ is a condition over the loop indices $i_1,\dots ,i_x$. Our objective is to find the relation between $f1\text{In}$ and $i_1,\dots ,i_x$. This relation may be linear or non-linear. It can be mechanically found out whether the relation is linear or not. In the following, we evolve the mechanical steps of synthesising the relation through a case analysis.

[IMAGE OMITTED. SEE PDF]

Case 1: The relation is linear: We have the following sub-cases.

Subcase 1.1: The condition $C_D$ of Fig. 8 is identically true:

Here the closed form of the linear relation is given by the following equation:3$\begin{array}{rl}f1\text{In}& =(i_1-L_1)/r_1\times \{((H_2-L_2)/r_2+1)\times \cdots \times ((H_x-L_x)/r_x+1)\}\\ & +(i_2-L_2)/r_2\times \{((H_3-L_3)/r_3+1)\times \cdots \times ((H_x-L_x)/r_x+1)\}\\ & +\cdots +(i_x-L_x)/r_x\end{array}$

Subcase 1.2: The condition $C_D$ is not identically true: The relation may or may not involve all the loop indices $i_1,\dots ,i_x$. Accordingly, we have two subcases.

Subcase 1.2.1: The relation involves all the loop index variables:

The general form of the relation between $f1\text{In}$ and $i_1,\dots ,i_x$ is4$f1\text{In}=i_1\times {\alpha }_1+i_2\times {\alpha }_2+\cdots +i_x\times {\alpha }_x+{\alpha }_{x+1},$ where ${\alpha }_1,\dots ,{\alpha }_{x+1}$ are real constants whose values are to be found. Let in a particular iteration l, the value of $i_k$ be $a_{l,k},1\le k\le x,$ and the value of $f1\text{In}$ be $c_l$. Placing these values in (2), we have5$a_{l,1}\times {\alpha }_1+a_{l,2}\times {\alpha }_2+\cdots +a_{l,x}\times {\alpha }_x+{\alpha }_{x+1}=c_l$ Here, $a_{l,1},\dots ,a_{l,x}$, $c_l$, are some known integer values obtained through exhaustive simulation of the loop from the first to the $l\text{th}$ iterations. Let n iterations of the loop body satisfy the condition $C_D$. Considering sequentially all such n iterations of the loop, we can have n equations of the form$a_{1,1}\times {\alpha }_1+a_{1,2}\times {\alpha }_2+\cdots +a_{1,x}\times {\alpha }_x+{\alpha }_{x+1}=c_1$$a_{2,1}\times {\alpha }_1+a_{2,2}\times {\alpha }_2+\cdots +a_{2,x}\times {\alpha }_x+{\alpha }_{x+1}=c_2$$⋮$$a_{n,1}\times {\alpha }_1+a_{n,2}\times {\alpha }_2+\cdots +a_{n,x}\times {\alpha }_x+{\alpha }_{x+1}=c_n$ Solving these equations by any linear program solvers such as, lp_solve [41] or any SMT solver such as, Yices [42], we can obtain the values of ${\alpha }_1,\dots ,{\alpha }_{x+1}$ and hence the relation between $f1\text{In}$ and $i_1,\dots ,i_x$. Following example illustrates the above mechanism.

$$

Example 3

Let us consider the statement S11 of $P1$ in the behaviour given in Fig. 6. Let us now extract the relation between the index $f1\text{In}$ of $\text{FIFO}1$ and the loop indices i and j. The relation can be represented as$f1\text{In}=i\times {\alpha }_1+j\times {\alpha }_2+{\alpha }_3$ We need to find the values of ${\alpha }_1$ ${\alpha }_2$ and ${\alpha }_3$. Let us consider the first iteration $i=1,j=4$ with $f1\text{In}=0$, we have${\alpha }_1+4\times {\alpha }_2+{\alpha }_3=0$ For the second iteration $i=1,j=5$ with $f1\text{In}=1$, we have${\alpha }_1+5\times {\alpha }_2+{\alpha }_3=1$ The statement $S11$ does not execute for the remaining iterations with $i=1$ (and $6\le j\le M$) since the condition $C_D$ (i.e. $-i-j+6\ge 0\wedge -i+M-2\ge 0$) under which S11 executes fails in these iterations. For the next iteration which satisfies $C_D$, $i=2,j=4$ with $f1\text{In}=2$, we have$2\times {\alpha }_1+4\times {\alpha }_2+{\alpha }_3=2$ None of the remaining iterations of the loop satisfies the condition $-i-j+6\ge 0\wedge -i+M-2\ge 0$. Therefore, the statement S1 executes only three times. Solving the above three equations, we have ${\alpha }_1=2$, ${\alpha }_2=1$, ${\alpha }_3=-6$. Therefore, $f1\text{In}=2\times i+j-6$.

Subcase 1.2.2: The relation is independent of some loop index variables:

In this case, the linear system of equations is under constrained, i.e. among the equations obtained through exhaustive enumeration of the loops, there is actually less than $x+1$ linearly independent equations. For an under-constrained linear system, there are infinite solutions, i.e. an infinite number of assignments to ${\alpha }_1,\dots ,{\alpha }_{x+1}$ satisfy those equations. The value $f1\text{In}$ ($f1\text{Out}$) remains the same for all the assignments. The solver returns one of the possible solutions. The following example illustrates this subcase.

$$

Example 4

Let us consider the behaviour of the producer process given in Fig. 9. Clearly, the statement $S1$ iterates 11 times. So, we find 11 equations of the form $k\times {\alpha }_1+k\times {\alpha }_2+{\alpha }_3=k,0\le k\le 10$. For $k=0$, we obtain ${\alpha }_3=0$. With ${\alpha }_3=0$, the remaining ten equations actually reduces to ${\alpha }_1+{\alpha }_2=1$. It may be noted that these ten equations are linearly dependent. No unique value of ${\alpha }_1$ and ${\alpha }_2$ can be obtained since we have only one equation over them. Here, we have an infinite number of assignments to ${\alpha }_1$ and ${\alpha }_2$ of the form ${\alpha }_1=x$ and ${\alpha }_2=-(x-1),\forall x\in \mathbb{N}$. The solver returns any one of them as a solution.

It will be observed subsequently that computation of transitive dependence over a FIFO necessitates equating $f1\text{In}$ equal to $f1\text{Out}$. If the solution returned by the solver for $f1\text{In}$ differs from that returned for $f1\text{Out}$ (for the under constrained cases), the process is not impaired (because equating $f1\text{In}=f1\text{Out}$ takes place under the explicit condition $C_D$). In particular, for this example, let us assume that we also have the same loop in the consumer process where data from $\text{FIFO}1$ are read. Let the solver returns ${\alpha }_1=p$ and ${\alpha }_2=-(p-1),p\in \mathbb{N}$ for $f\text{In}$ and returns ${\alpha }_1=q$ and ${\alpha }_2=-(q-1),q\in \mathbb{N}$ for $f\text{Out}$. Based on the values returned by the solver, we obtain $f\text{In}=p\times i-(p-1)\times j$ and $f\text{Out}=q\times i-(q-1)\times j$. Clearly, $f\text{In}=f\text{Out}$, $\forall i,j$, $0\le i\le 10$ $\wedge 0\le j\le 10$ $\wedge i==j$. Therefore, an arbitrary choice does not hamper the dependence mapping computations over a FIFO.

[IMAGE OMITTED. SEE PDF]

Case 2: The relation is not linear:

In this case, there does not exist any assignment of ${\alpha }_1,\dots ,{\alpha }_{x+1}$ which satisfy all the above equations. The solver reports that the constraints are unsatisfiable. The following example illustrates the fact.

$$

Example 5

Let us consider the behaviour of the process in Fig. 10a. The corresponding values of $f1\text{In}$ for different values of (i, j) of this behaviour are shown in Fig. 10b. It can be shown that the relation between $f1\text{In}$ and $i,j$ is $f1\text{In}=(i\times (i-1))/2+(j-1)$ (and the corresponding dependence mapping is6${}_{S1}{M}_{\text{FIFO},a}=\{[(i\times (i-1))/2+(j-1)]\to [i][j]|$ $0\le i\le 5\wedge 0\le j\le 5\}$). Clearly, this is a non-linear relation. In this case, our method will generate 15 equations (corresponding to 15 entries of Fig. 10b). When these equations are submitted to lp_solve or Yices, the latter reports that the constraints are unsatisfiable indicating, thereby, that no linear relation exists.

[IMAGE OMITTED. SEE PDF]

Omega calculator [43] is used for computing the dependence mappings. The inherent limitation of Omega calculator is that it only supports Presburger formulas (Presburger formulas contain affine constraints, the usual logical connectives, and existential and universal quantifiers). Non-linear dependence mappings cannot be handled by Omega calculator. Therefore, when the relation between $f1\text{In}$ and $i_1,\dots ,i_x$ is not linear, we have to put the relations in their exhaustively enumerated forms to the Omega calculator. Accordingly, the dependence mapping for the statement $S1$ in Fig. 10a is represented as7$\begin{array}{rl}{}_{S1}{M}_{\text{FIFO}1,a}& =\{[0]\to [1][1]\}\cup \{[1]\to [2][1]\}\cup \{[2]\to [2][2]\}\cup \{[3]\to [3][1]\}\\ & \cup \dots \cup \{[13]\to [5][4]\}\cup \{[14]\to [5][5]\}\end{array}$ Finally, our scheme to obtain the relation between $f1\text{In}$ ($f1\text{Out}$) and $i_1,\dots ,i_x$ is given as Algorithm 1 (see Fig. 11). Our method required the simulation of each loop individually that contains FIFO operation(s) once to identify relation between FIFO index and loop indices. This cannot be avoided in our method. However, it is better than simulation based verification of the behaviour where (i) all the loops will be simulated for all test cases and (ii) all the loops of the behaviour will be simulated simultaneously. On the hand, we have to (i) only simulate the loops that contains FIFO operations and (ii) each loop will be simulated separately exactly once and (iii) if the FIFO operation is not under any condition inside the loop, we do not have to simulate the loop.

[IMAGE OMITTED. SEE PDF]

4.3 Composition of ADDGs of KPN processes

The next task is to compose the ADDGs obtained from the individual processes to obtain the ADDG of the KPN. Let $F_k$ be the FIFO used as the communication channel between the producer process $P_i$ and the consumer process $P_j$. Let $G_i$ and $G_j$ be the ADDGs obtained from $P_i$ and $P_j$, respectively, with $F_k$ depicted as a linear array. In this case, $F_k$ would be a start node in $G_i$ and a terminal node in $G_j$. While computing the transitive dependence across the linear array corresponding to the FIFO channel $F_k$, we use the ‘first-in-first-out’ property of the FIFO; in other words, we make the in-pointer $f\text{In}$ of $F_k$ equal to the out-pointer fOut of $F_k$ to obtain the transitive dependence.

The composition of two ADDGs can be formally defined as follows. Let $G_1=(V_1,E_1)$ and $G_2=(V_2,E_2)$ be the respective ADDGs of any two processes $P_1$ and $P_2$ of a KPN. Let there be k FIFOs $F_1,\dots ,F_k$ between $P_1$ and $P_2$. We assume that $P_1$ and $P_2$ may have some common input and output arrays, but all the internal arrays of the processes have distinct names. Let $P_1$ and $P_2$ have m common input arrays $I_1,\dots ,I_m$ and n common output arrays $O_1,\dots O_n$. Therefore, $V_1\cap V_2=\{F_1,\dots ,F_k,I_1,\dots ,I_m,O_1,\dots O_n\}$. The composed ADDG $G_{12}$ of $G_1$ and $G_2$ is $G_{12}=G_1\mathrm{♢}{G}_2=(V_1\cup V_2,E_1\cup E_2)$. The input array nodes $I_1,\dots ,I_m$ become the terminal nodes and the output array nodes $O_1,\dots O_n$ become the start nodes in the composed ADDG $G_{12}$. The linear arrays $F_1,\dots ,F_k$ are either start nodes or terminal nodes in $G_1$ and $G_2$ depending upon the direction of the FIFOs $F_1,\dots ,F_k$. Let $F_1$ be a start node in $G_1$ and a terminal node in $G_2$. It means that the direction of $F_1$ is from (producer) process $P_1$ to (consumer) process $P_2$. The linear array nodes $F_l,1\le l\le k$ become internal array node in $G_{12}$. Specifically, we need to compose the slices in $G_2$, which have $F_1$ as terminal nodes, with the slices in $G_1$, which have $F_1$ as start nodes, to obtain the transitive dependencies between the output and the input arrays in $G_{12}$. Let $g_2(B,⟨B_1,\dots ,B_p,F_1⟩)$ be one such slice in $G_1$ and $g_1(F_1,⟨A_1,\dots ,A_k⟩)$ be one such slice in $G_2$. The slices $g_1$ and $g_2$ are depicted as Figs. 12a and b, respectively. Let the characteristic formulas of the two slices $g_2$ and $g_1$ be ${\tau }_{g_2}=⟨f_1(B_1,\dots ,B_p,F_1),{⟨}_{g_2}{M}_{B,B_1},\dots {,}_{g_2}{M}_{B,B_p}{,}_{g_2}{M}_{B,F_1}⟩⟩$ and ${\tau }_{g_1}=⟨f_2(A_1,\dots ,A_k),{⟨}_{g_1}{M}_{F_1,A_2},\dots {,}_{g_1}{M}_{F_1,A_k}⟩⟩$, respectively. Let the slice $g(B,⟨B_1,\dots ,B_p,A_1,\dots ,A_k⟩)$ as shown in Fig. 12c be the composition of $g_1$ and $g_2$, i.e. $g=g_2\mathrm{♢}{g}_1$. The characteristic formula of g is8${\tau }_g=⟨f_1(B_1,\dots ,B_p,f_2(A_1,\dots ,A_k)),{⟨}_{g_2}{M}_{B,B_1},\dots {,}_{g_2}{M}_{B,B_p}{,}_g{M}_{B,A_1},\dots {,}_g{M}_{B,A_k}⟩⟩,$ where ${}_g{M}_{B,A_z}={}_{g_2}{M}_{B,F_1}\mathrm{♢}{}_{g_1}{M}_{F_1,A_z},$ $1\le z\le k$. So, the data transformation of the resultant slice g is obtained by replacing the occurrence(s) of $F_1$ in $f_1(B_1,\dots ,B_p,F_1)$ by $f_2(A_1,\dots ,A_k)$. The dependence mapping between B and $A_z,1\le z\le k,$ is obtained from ${}_{g_2}{M}_{B,F_1}$ and ${}_{g_1}{M}_{F_1,A_z}$ using transitive dependence computation over two sequences of statements. The transitive dependencies for the FIFOs from $P_1$ to $P_2$ can be obtained in a similar way.

[IMAGE OMITTED. SEE PDF]

$$

Example 6

Let us consider the ADDGs in Fig. 7. It may be recalled that these ADDGs are obtained from the KPN processes given in Fig. 6. Clearly, the ADDGs in Figs. 7b and c can be composed with the ADDG in Fig. 7a. Similarly, the ADDG in Fig. 7d can be composed with the ADDGs in Figs. 7b and c. The resultant ADDG of the KPN is depicted in Fig. 13b. The ADDG of the original sequential behaviour (given in Fig. 2a) is depicted in Fig. 13a. We have to establish the equivalence between these two ADDGs of Fig. 13.

Let us now compute the transitive dependence across the FIFO1 in the resultant ADDG. We have9$\begin{array}{rl}{}_{S_{11}}{M}_{\text{FIFO}1,\text{in}1}& =\{[f1\text{In}]\to [i,j]|f1\text{In}\\ & =(2\times i+j-6)\wedge 1\le i\le M\wedge 4\le j\le N\\ & \wedge -i-j+6\ge 0\wedge -i+M-2\ge 0\}.\end{array}$ We also have10$\begin{array}{rl}{}_{S_{15}{S}_{13}}{M}_{\text{FIFO}3,\text{FIFO}1}& =\{[f3\text{In}]\to [f1\text{Out}]|f3\text{In}\\ & =(l+2\times m-3)\wedge f1\text{Out}\\ & =(l+2\times m-3)\wedge 3\le l\le M\wedge 3\le n\\ & \le N-1\wedge l-4\le 0\wedge m+l-7\le 0\}.\end{array}$ It may be noted that the value of $f1\text{In}$ in ${}_{S_{11}}{M}_{\text{FIFO}1,\text{in}1}$ and the values of $f3\text{In}$ and $f1\text{Out}$ in ${}_{S_{15}{S}_{13}}{M}_{\text{FIFO}3,\text{FIFO}1}$ are obtained by the method discussed above. Therefore, the transitive mapping from $\text{FIFO}3$ can be obtained by composing ${}_{S_{15}{S}_{13}}{M}_{\text{FIFO}3,\text{FIFO}1}$ with ${}_{S_{11}}{M}_{\text{FIFO}1,\text{in}1}$. Specifically, ${}_{S_{15}{S}_{13}{S}_{11}}{M}_{\text{FIFO}3,\text{in}1}$$=\{[f3\text{In}]\to [i,j]|1\le i\le M\wedge 4\le j\le N$$\wedge -i-j+6\ge 0\wedge -i+M-2\ge 0\wedge 3\le l\le M$$\wedge 3\le n\le N-1\wedge l-4\le 0\wedge m+l-7\le 0$$\wedge \mathrm{\exists }f1\text{In},f1\text{Out}([f1\text{In}]\to [i,j]{\in }_{S_{11}}{M}_{\text{FIFO}1,\text{in}1}$$\wedge [f3\text{In}]\to [f1\text{Out}]{\in }_{S_{15}{S}_{13}}{M}_{\text{FIFO}3,\text{FIFO}1})$$\wedge f3\text{In}=(l+2\times m-3)\wedge f1\text{Out}=(l+2\times m-3)$$\wedge f1\text{In}=(2\times i+j-6)\wedge f1\text{In}=f1\text{Out}\}.$

[IMAGE OMITTED. SEE PDF]

5 Equivalence problem formulation

Let $G_S$ be the ADDG corresponding to an input behaviour and $G_T$ be the ADDG corresponding to the transformed behaviour obtained from the input behaviour through loop and arithmetic transformations. In the following, the definition of equivalence between the two ADDGs is evolved. The detail can be found in [17].

$$

Definition 9

(Matching IO-slices): Two IO-slices $g_1$ and $g_2$ of an ADDG G are said to be matching, denoted by $g_1\simeq g_2$, if the data transformations of both the slices are equivalent.

Let the characteristic formula of $g_i(a,⟨v_1,\dots ,v_l⟩),i=1,2$, be $⟨r_{g_i},{⟨}_{g_i}{M}_{a⇝v_1},\dots {,}_{g_i}{M}_{a⇝v_l}⟩⟩$, where a is an output array and $v_1,\dots ,v_l$ are the input arrays. These two slices are matching slices if $r_{g_1}$ and $r_{g_2}$ are equivalent. Due to single assignment form of the behaviour, the domain of the dependence mapping between the output array a and the input array $v_j$ in the slices $g_1$ and $g_2$ of the ADDG G, however, are non-overlapping.

$$

Definition 10

(IO-slice class): An IO-slice class is a maximum set of matching IO-slices.

Let a slice class be $C_g(a,⟨v_1,\dots ,v_l⟩)=\{g_1,\dots ,g_k\}$ where each slice involves l input arrays $v_1,\dots ,v_l$ and the output array a. Let the characteristic formula of the member slice $g_i,1\le i\le k,$ be $⟨r_{g_i},{⟨}_{g_i}{M}_{a⇝v_1},\dots {,}_{g_i}{M}_{a⇝v_l}⟩⟩$. Due to single assignment form of the behaviour, the domain of the dependence mappings between the output array a and the input array $v_m,1\le m\le l,$ in the slices of $C_g$ must be non-overlapping, that is ${}_{g_i}{M}_{a⇝v_m}$ and ${}_{g_j}{M}_{a⇝v_m}$, $1\le i,j\le k,$ are non-overlapping. The domain of the dependence mapping ${}_{C_g}{M}_{a⇝v_m}$ from a to $v_m$ over the entire class $C_g$ is the union of the domains of ${}_{g_i}{M}_{a⇝v_m},1\le i\le k$. So, the characteristic formula of the slice class $C_g$ is $⟨r_{C_g},{⟨}_{C_g}{M}_{a⇝v_1},\dots {,}_{C_g}{M}_{a⇝v_l}⟩⟩$, where $r_{C_g}$ is the data transformation of any of the slices in $C_g$ and ${}_{C_g}{M}_{a⇝v_m},1\le m\le l$, is${}_{C_g}{M}_{a⇝v_m}=\bigcup _{1\le i\le k}{g}_i{M}_{a⇝v_m}$ Therefore, the characteristic formula of a slice class has the same structure as that of a single slice. The characteristic formula of a slice class $C_g$ is denoted as ${\tau }_{C_g}$.

$$

Definition 11

(Corresponding IO-slice class): A slice class $C_1$ of an ADDG $G_S$ and a slice class $C_2$ of $G_T$ are said to be the corresponding slice class, denoted as $C_1\simeq C_2$, iff ${\tau }_{C_1}={\tau }_{C_2}$.

$$

Definition 12

(Equivalence of ADDGs): An ADDG $G_S$ is said to be equivalent to an ADDG $G_T$ iff for each IO-slice class $C_S$ in $G_S$, there exists an IO-slice class $C_T$ in $G_T$ such that $C_S\simeq C_T$, and vice-versa.

The equivalence checking method is given in Algorithm 2 (see Fig. 14).

[IMAGE OMITTED. SEE PDF]

6 Correctness and complexity

6.1 Correctness of the composition operation

We now show that the composition operation correctly captures the data dependence of a deadlock-free KPN. The (sequential to KPN) transformation process, however, may introduce deadlock in the generated KPN. Deadlock detection in an KPN needs specialised treatments and several methods are already reported to detect deadlock in KPN networks [44–47]. Before converting KPNs to ADDGs by our method, therefore, such deadlock detection methods should be applied to check deadlock in KPNs. We, therefore, assume that the KPN is deadlock free to prove the correctness of the composition operation.

$$

Theorem 1

The ADDG composition mechanism captures correctly the data dependence across the deadlock-free KPN processes.

$$

Proof

Let there be a FIFO $F_1$ from a KPN process $P_1$ to another KPN process $P_2$. Let $G_1$ and $G_2$ be the ADDGs of $P_1$ and $P_2$, respectively. Let $S_i$ be a statement in $P_1$ defining $F_1$ and $S_j$ be a statement in $P_2$ where $F_1$ is read into an array, A say.

Fig. 12a depicts the IO-slice $g_1(F_1,A_1,\dots ,A_k)$ of $G_1$ ending in the write edge $S_i$. Similarly, Fig. 12b depicts the IO-slice $g_2(B,B_1,\dots ,F_1,\dots ,B_p)$ of $G_2$, where B is an output array of $P_2$; the statement $S_j$ appears as a write edge corresponding to reading of the FIFO into the array A.

In general, let $g(C,I_1,\dots ,I_n)$ be a slice having the last write edge with statement labels $S_t$ in an ADDG of a process P. Let $\pi$ be any path from the start array C to some terminal array $I_j$, for some $j,1\le j\le n$. Let the sequence of write edges in $\pi$ be $⟨S_t,S_1,S_2,\dots ,S_k⟩$, where $S_t$, $S_1,\dots ,S_k$ are the statement labels. The following properties are satisfied by $\pi$.

• Property 1: The sequence of statements $⟨S_t,S_1,S_2,\dots ,S_k⟩$ in $\pi$ gives the reverse execution sequence (not necessarily occurring consecutively in the process body) through which the output array C gets defined.
• Property 2: Let $A_1,\dots ,A_k$ are the respective arrays, not necessarily distinct, defined by the statements $S_1,\dots ,S_k$. (The statement $S_t$ defines the output array C.) All the elements of the arrays $A_i,1\le i\le k$, and the output array C, assigned along the path $\pi$ over the iteration domains of statements $S_i$ and $S_t$ get properly defined by virtue of having all the operand array elements defined before use in $\pi$. Thus, the dependence mapping ${}_{\pi }{M}_{C,I_j}$ is well defined.

If the composed ADDGs maintain these properties, then the composition process captures the dependence across the (deadlock free) KPN processes correctly.

In the composed ADDG of Fig. 12c, let us, therefore, consider a path $\pi \cdot S_i\cdot {\pi }_1$ comprising the prefix $\pi$ from the output array B to $F_1$ followed by the path $S_i\cdot {\pi }_1$ in the slice $g_1$ from $F_1$ to some terminal array $A_l$ of the slice $g_1$ (There may be more than one such path in the slice $g_2$ and hence in the composed ADDG G.).

Property 1 holds in the prefix $\pi$ and the suffix $S_i\cdot {\pi }_1$ of the path $\pi \cdot S_i\cdot {\pi }_1$ by construction of the ADDGs $G_1$ and $G_2$, respectively. Hence, the property holds for the entire path $\pi \cdot S_i\cdot {\pi }_1$ if it holds for the statement sequence $S_j\cdot S_i$ in the path; this fact, however, is ensured by the FIFO operations put and get and by the blocking read operational semantics of KPN processes. It may be noted that the output array may not actually get defined if $P_1$ or $P_2$ or both cannot proceed because of deadlock.

Now, regarding property 2 for the path $S_i\cdot {\pi }_1$, the dependence mappings ${}_{S_i\cdot {\pi }_1}{M}_{F_1,A_1}{,}_{S_i\cdot {\pi }_1}{M}_{F_1,A_2},\dots {,}_{S_i\cdot {\pi }_1}{M}_{F_1,A_k}$, obtained during construction of the ADDG $G_1$, are well formed satisfying property 2. Hence, the mapping ${}_{S_i\cdot {\pi }_1}{M}_{F_1,A_l}$ is well defined. So is the dependence mapping ${}_{\pi }{M}_{B,F_1}$ for the path $\pi$, ensured during construction of the ADDG $G_2$. Also, the composition step of $G_1$ and $G_2$ ensures that the mapping ${}_{\pi \cdot S_i\cdot {\pi }_1}{M}_{B,A_l}$ is well defined satisfying property 2 for the path $\pi \cdot S_i\cdot {\pi }_1$. Again, if $P_1$ or $P_2$ or both are in deadlock, the mapping ${}_{\pi \cdot S_i\cdot {\pi }_1}{M}_{B,A_l}$, although constructed by the composition process, will not actually be realised.□

Thus, the presence of deadlocks invalidates the composition of ADDGs. The following example illustrates the fact.

$$

Example 7

Let us consider the KPN in Fig. 15. This KPN has a deadlock around the channel FIFO1 since the process $P_1$ puts 50 elements in FIFO1 whereas the process $P_2$ tries to get 60 elements from it. So, the process $P_2$ remains blocked on read from empty channel after consuming 50 elements from FIFO1. As a result, the second loop of $P_2$ and hence the process $P_3$ never execute. So, none of the elements of the array c gets defined.

Let us now discuss the composition mechanism in this KPN. It might be noted that each of the input and output pointers of the three FIFOs is the same as the corresponding loop index i in this example. The dependence mapping in $P_1$ is${}_{S1}{M}_{\text{FIFO}1,a}=\{[i]\to [i]|0\le i\le 49\}.$ The dependence mappings in $P_2$ are${}_{S2}{M}_{b,\text{FIFO}1}=\{[i]\to [i]|0\le i\le 59\}{.}_{S3}{M}_{\text{FIFO}2,b}=\{[i]\to [i]|0\le i\le 49\}.$ So, ${}_{S3S2}{M}_{\text{FIFO}2,\text{FIFO}1}{=}_{S3}{M}_{\text{FIFO}2,b}{\mathrm{♢}}_{S2}{M}_{b,\text{FIFO}1}=\{[i]\to [i]|0\le i\le 49\}$.

The dependence mapping in $P_3$ is${}_{S4}{M}_{c,\text{FIFO}2}=\{[i]\to [i]|0\le i\le 49\}.$ The composition of $P_3$ and $P_2$ around FIFO2 gives${}_{S4S3S2}{M}_{c,\text{FIFO}1}{=}_{S4}{M}_{c,\text{FIFO}2}{\mathrm{♢}}_{S3S2}{M}_{\text{FIFO}2,\text{FIFO}1}=\{[i]\to [i]|0\le i\le 49\}.$ The composition of composed behaviour of $P_3$ and $P_2$ with $P_1$ around FIFO1 gives${}_{S4S3S2S1}{M}_{c,a}{=}_{S4S3S2}{M}_{c,\text{FIFO}1}{\mathrm{♢}}_{S1}{M}_{\text{FIFO}1,a}=\{[i]\to [i]|0\le i\le 49\}.$ Therefore, the ADDG construction mechanism constructs the dependence mapping from the array c to the array a for the first 50 elements communicated through FIFO1 by ignoring the fact that second loop of $P_2$ and the process $P_3$ never execute due to deadlock around FIFO1.

It may be noted that while computing (in the last step) the mapping ${}_{S4S3S2S1}{M}_{c,a}$, inferring deadlock from the fact that ${|}_{S1}{U}_a|{<}_{S4S3S2}{M}_{FIFO1}$ is not always correct. To illustrate this fact, let us assume that in Fig. 15, there is another loop body

• for (i = 0; i < 9; i + +)
• S5: FIFO1.put(f2(d[i])); after the first loop body in process $P_1$ in Fig. 15. In this case, the process $P_1$ puts 60 elements in FIFO1. Therefore, there will not be any deadlock in this KPN with this modification. However, the fact that ${|}_{S1}{U}_a|{<}_{S4S3S2}{M}_{\text{FIFO}1}$ is still true while computing the mapping ${}_{S4S3S2S1}{M}_{c,a}$.

[IMAGE OMITTED. SEE PDF]

In general, therefore, the composition mechanism fails to detect this kind of deadlocks.

6.2 Complexity of modelling a KPN as an ADDG

Let the number of processes in the KPN be p and the maximum number of statements in a process be s. So, the total number of statements in the KPN is $O(sp)$. Let the total number of FIFOs in the KPN be f. For a get (or put) statement, we first model the associated FIFO as a one-dimensional array. Complexity of this step is linear in the number of get and put statements. So, the complexity of this step is $O(sp)$. To compute the dependency mapping involving FIFO, we construct a set of linear equations over the array indices (using Algorithm 1 (Fig. 11)). Here, the linear equations consist of addition operations and multiplication with constants, where the latter can be replaced by repeated additions. Hence, the corresponding system of equations involves Presburger arithmetic. Let us assume the complexity of this step is $O(g(n))$, where n is the size of the equations. In our case, the size of the formula depends on the nesting depth of the loop and the number of loop iterations in the behaviour. For the behaviour in Fig. 8, n would be $x\times (H_1-L_1)\times \cdots \times (H_x-L_x)$. We use YICES to solve these equations. Table 1 shows run times of YICES for different formula sizes. Although time required to verify Presburger formulas is super-exponential on the size of the formula [43, 48], it is clear from the table that YIECS is actually very efficient for the task involved in the present case. The ADDGs of the individual processes are composed around the individual FIFOs to obtain the ADDG of the KPN. So, the number of composition operations is $O(f)$. Therefore, the complexity of modelling a KPN as an ADDG is $O(sp+g(n)+f)$.

Table 1 YICES runtime for different formula sizes

Nesting depth × Number of loop iterations	Time, s
$2\times {10}^4$	0.685
$2\times {10}^6$	68.671
$3\times {10}^3$	0.134
$3\times {10}^5$	9.678
$3\times {10}^6$	94.854
$3\times {10}^7$	155.854
$4\times {10}^3$	0.155
$4\times {10}^5$	8.432
$4\times {10}^6$	84.540

6.3 Correctness of equivalence checking of ADDGs

Two behaviours (or synonymously, their ADDGs $G_S$ and $G_T$) are said to be equivalent iff for every inputs, both the behaviours produce the same set of outputs. Following theorem captures the soundness of our method.

$$

Theorem 2

(Soundness): If Algorithm 2 (Fig. 14) terminates successfully in step 13, then the two ADDGs $G_S$ and $G_T$ are equivalent.

$$

Proof

Let there be l IO-slice classes $g_{s_1},\dots ,g_{s_l}$ in the set ${\mathcal{C}}_{S_g}$ of slice classes of $G_S$ which start from the output array o. Our method finds that the set ${\mathcal{C}}_{T_g}$ of IO-slice classes in ADDG $G_T$ comprises exactly l slice classes $g_{t_1},\dots ,g_{t_l},$ say which also start from array o such that $g_{s_i}\simeq q_{t_i},1\le i\le l$. Each slice class $g_{s_i}$ defines a part of the array o. Since the behaviours are considered to be in single assignment form, the parts of o defined by $g_{s_i},1\le i\le l$, are non-overlapping. Also, there is no other slice class that starts from o in ${\mathcal{C}}_{S_g}$. Therefore, $g_{s_i},1\le i\le l$, together define the whole array. Moreover, there cannot be any more slice class other than $g_{t_1},\dots ,g_{t_l}$ in ${\mathcal{C}}_{T_g}$ starting from o; otherwise, our method will find a possible non-equivalence of that slice class in step 12 of Algorithm 2 (Fig. 14). In the same way, we can show that for all other output arrays, there are equal number of slice classes in ${\mathcal{C}}_{T_g}$ and in ${\mathcal{C}}_{T_g}$ which start from that array. Therefore, if Algorithm 2 (Fig. 14) proceeds up to step 12, then both the ADDGs have equal number of slice classes and there is a one-to-one correspondence between the slice classes of the ADDGs. Let the ADDG $G_S$ have slice classes $g_{s_1},\dots ,g_{s_n}$ and the ADDG $G_T$ has slice classes $g_{t_1},\dots ,g_{t_n}$ and $g_{s_i}\simeq q_{t_i},1\le i\le n$. Let us assume that the ADDG $G_S$ is not equivalent to the ADDG $G_T$ even if there is a one-to-one correspondence between the slices of ${\mathcal{C}}_{T_g}$ and ${\mathcal{C}}_{T_g}$. In the following, the assumption is proved to be wrong by contradiction.

The two ADDGs $G_S$ and $G_T$ are not equivalent in the following cases:

• The final values of some elements of one output array are different in two ADDGs: As discussed above, each element of any output array is defined through a slice. Since we are considering the same set of elements of an output array, they must be associated with some corresponding slice class of $G_S$ and $G_T$. Let us assume that the slice classes $g_{s_i}$ and $g_{t_i}$ be associated with those elements of the output array in $G_S$ and $G_T$, respectively. Since transformations do not match for these elements, the data transformations of $g_{s_i}$ and $g_{t_i}$ should be different. However, step 6 of Algorithm 2 (Fig. 14) already ensures that $r(g_{s_i})\simeq r(g_{t_i})$ (contradiction).
• The association between the index of an output array, o say, and an input array, in say, is not the same for some elements of an output array: As reasoned above in case (i), those elements of o must be associated with the corresponding slice class of $G_S$ and $G_T$. Let us assume that the slice classes $g_{s_i}$ and $g_{t_i}$ be associated with those elements of o in $G_S$ and $G_T$, respectively. Since, the association between the index of o and that of the array in is not the same for those elements of o, the mappings ${}_{g_{s_i}}{M}_{o,in}$ and ${}_{g_{t_i}}{M}_{o,in}$ are not the same. However, step 6 of Algorithm 2 (Fig. 14) already ensures that ${}_{g_{s_i}}{M}_{o,in}{\simeq }_{g_{t_i}}{M}_{o,in}$ (contradiction).

Hence, the ADDGs $G_S$ and $G_T$ are indeed equivalent.□

6.3.1 Complexity of Algorithm 2 (equivalence checking between two ADDGs)

Let the number of slices in the two ADDGs $G_S$ and $G_T$ be $s_1$ and $s_2$, respectively. Let the complexity of normalisation of the data transformations and the index expressions for a slice requires $f(\parallel F\parallel )$ time, where F is the length of an arithmetic expression and f is some that captures the time complexity of normalisation operation. Each slice needs to compare with every other slices of $G_S$ ($G_T$) to find the slice classes in $G_S$ ($G_T$). So, the complexity of finding the slice classes in $G_S$ ($G_T$) is $O(s_1^2\times \parallel F\parallel )$ ($O(s_2^2\times \parallel F\parallel )$). To find the equivalent of a slice class of $G_S$ in $G_T$, we have to compare the data transformations and the dependence mappings of each slice of $G_S$ with every slice class of $G_T$. Therefore, the complexity of equivalence checking between the slice classes of $G_S$ and $G_T$ is $O(s_1\times s_2\times \parallel F\parallel )$. So, the overall complexity of the Algorithm 2 (Fig. 14) is $O(f(\parallel F\parallel )+s^2\times \parallel F\parallel ))$, where s is maximum of $s_1$ and $s_2$.

There are two key steps of our method: (i) construction of ADDG from a given KPN and (ii) showing equivalence between two ADDGs. As shown in Theorem 1, the proposed method in this work can always obtain an ADDG from a deadlock-free KPN. On the other hand, we have proved the soundness of our equivalence checking method in Theorem 2. Given the undecidability results of the equivalence problem of flow chart schemas [40], completeness of the algorithm, however, is unattainable. Overall, we propose a sound method for verification of parallelising transformations of KPN models.

7 Case study: verification of computation migration transformation

A computation migration transformation relocates computations from one process to another so that the overheads of synchronisation and inter-process communication get reduced [11]. The number of processes remains the same under this transformation. However, the number of communication channels between processes may change. Some of the channels of the original process are removed and some new channels are added to the KPN. The primary motivation of this transformation is to reduce the number of channels or the total volume of communication over all the channels.

Let us consider the KPNs in Fig. 16. The initial KPN consists of three processes and four FIFO channels. Each rectangular box within a process defines an array. In Fig. 16a, the FIFO $\text{FIFO}1$ from the array a of the process $P1$ to the array c of the process $P2$ indicates that the elements of a is defined in process $P1$, communicated through $\text{FIFO}1$ to the process $P2$ and then used to define the elements of the array c. All such edges between processes in the KPNs in Fig. 16 have similar meaning. In Fig. 16b where both a and c reside in the process $P1$, the directed edge from a to c simply indicates that the elements of the array a are used to define the elements of the array c. All such edges with the processes in the KPNs in Fig. 16 are interpreted likewise. In short, the directed edges capture the define-use relation between the arrays. The transformed behaviour after computation migration is shown in Fig. 16b. Since the computation defining the array c is migrated from process $P2$ to process $P1$, the FIFOs $\text{FIFO}1$ and $\text{FIFO}3$ are not required and hence removed. A new FIFO $\text{FIFO}5$, however, is to be added between processes $P1$ and $P3$. The detailed behaviours of the processes of these two KPNs are given in Fig. 17.

[IMAGE OMITTED. SEE PDF]

[IMAGE OMITTED. SEE PDF]

The ADDGs of the initial and the transformed KPNs of Fig. 17 obtained by our method are depicted in Fig. 18. Both the ADDGs in Fig. 18 have three slices. They are $g_{11}(b,⟨\text{in}1,\text{in}2⟩)$, $g_{12}(d,⟨\text{in}1,\text{in}2⟩)$ and $g_{13}(f,⟨\text{in}1,\text{in}2⟩)$ in the ADDG in Fig. 18a and $g_{21}(b,⟨\text{in}1,\text{in}2⟩)$, $g_{22}(d,⟨\text{in}1,\text{in}2⟩)$ and $g_{23}(f,⟨\text{in}1,\text{in}2⟩)$ in the ADDG in Fig. 18b. Since some FIFOs are removed and some new FIFOs are introduced in the transformed KPN by computation migration transformation, the computation of the transitive dependencies from the output arrays to the inputs arrays would be different in the ADDGs. The steps used by our ADDG based method in establishing equivalence between the ADDGs are as follows.

[IMAGE OMITTED. SEE PDF]

The characteristic formulas of the slices in the ADDG in Fig. 18a are${\tau }_{g_{11}}=⟨f_2(f_3(f_1(\text{in}1),f_5(\text{in}2))),{⟨}_{S3S6S4S2S1}{M}_{b,\text{in}1}{,}_{S3S6S4S9S8}{M}_{b,\text{in}2}⟩⟩,$${\tau }_{g_{12}}=⟨f_4(f_3(f_1(\text{in}1),f_5(\text{in}2))),{⟨}_{S5S4S2S1}{M}_{b,\text{in}1}{,}_{S5S4S9S8}{M}_{b,\text{in}2}⟩⟩$ and${\tau }_{g_{13}}=⟨f_6(f_3(f_1(\text{in}1),f_5(\text{in}2))),{⟨}_{S10S7S4S2S1}{M}_{b,\text{in}1}{,}_{S10S7S4S9S8}{M}_{b,\text{in}2}⟩⟩,$ where all the mappings are of the form $\{[i]->[i]|0\le i\le 99\}$. The details of computation of the dependence mappings of the slices are intuitive and hence, are not shown explicitly.

The characteristic formulas of the slices in the ADDG in Fig. 18b are${\tau }_{g_{21}}=⟨f_2(f_3(f_1(\text{in}1),f_5(\text{in}2))),{⟨}_{S3S4S1}{M}_{b,\text{in}1}{,}_{S3S4S9S8}{M}_{b,\text{in}2}⟩⟩,$${\tau }_{g_{22}}=⟨f_4(f_3(f_1(\text{in}1),f_5(\text{in}2))),{⟨}_{S5S12S4S1}{M}_{b,\text{in}1}{,}_{S5S12S4S9S8}{M}_{b,\text{in}2}⟩⟩$ and${\tau }_{g_{23}}=⟨f_6(f_3(f_1(\text{in}1),f_5(\text{in}2))),{⟨}_{S10S11S4S1}{M}_{b,\text{in}1}{,}_{S10S11S4S9S8}{M}_{b,\text{in}2}⟩⟩,$ where all the mappings are of the form $\{[i]->[i]|0\le i\le 99\}$. The details of computation of the dependence mappings are not shown explicitly for the same reason. Clearly, $g_{1k}\equiv g_{2k},1\le k\le 4$. Hence, the two ADDGs are equivalent.

8 Experimental results

The methodology described in this paper has been implemented and run on a 2.0 GHz Intel^® Core™ 2 Duo machine. We have integrated the SMT solver Yices [42] in our tool to find the relation between $f\text{In}$ ($f\text{Out}$) and the loop indices. For obtaining the dependence mappings of the slices, our tool relies on the Omega calculator [43].

Our verification framework has two components: (i) a method to convert a KPN to its equivalent ADDG, and (ii) an equivalence checking method of two ADDGs. Accordingly, we plan our experimentation in two parts: (i) in the first part, we test the equivalence checker and (ii) in the second part, we test the overall verification framework. The two parts are summarised below.

To test the ADDG based equivalence checking method in the first part of the experimentation, we consider three benchmark examples: the sobel edge detection (SOB), debauches 4-coefficient wavelet filter (WAVE) and Laplace algorithm to edge enhancement of northerly directional edges (LAP). We then apply a variety of loop transformations and arithmetic transformations on these behaviours. Specifically, test cases have been obtained by applications of the following loop and arithmetic transformations: (i) SOB1: loop fusion, commutative and distributive, (ii) SOB2: loop reorder, commutative and distributive, (iii) WAVE: loop un-switching and commutative, (iv) LAP1: expression splitting and loop fission, (v) LAP2: loop unrolling, commutative and distributive, and (vi) LAP3: loop spreading, commutative and remaining. We then construct ADDGs from both the source and the transformed behaviours and then apply our equivalence checker. The results are summarised in Table 2. The maximum nesting depth of the loops, numbers of loop bodies, arrays and slices in the source and the transformed behaviours are shown in columns two to eight in Table 2. The execution time of our tool for these test cases are tabulated in column nine of the table. In the last two cases, the number of slices differs from the source ADDG to the transformed ADDG, the method successfully forms the slice classes and establishes their equivalence. In all of the cases, our method was able to establish the equivalence in <12 s. Next, we take the source and the transformed behaviours of the previous experiment. We, however, intentionally change the index expressions of some of the arrays or limits of the loops in the transformed behaviours. As a result, some dependence mappings (involving those arrays) do not match with the original behaviour. Similarly, we change the rhs expressions of some statements of the transformed behaviours to create another set of erroneous test cases. As a result, the data transformations of some of the slices do not match with the corresponding slices of the original behaviour. The execution time of our tool for these two cases are tabulated in columns 10 and 11, respectively. Our tool is able to find the non-equivalence in all the cases in <2 s as shown in Table 2.

Table 2 Results for several benchmarks

	Nest	Loops	Arrays	Slices	Exec. time, s
Cases	depth	src	tran	src	tran	src	tran	eq	not-eq1	not-eq2
(1)	(2)	(3)	(4)	(5)	(6)	(7)	(8)	(9)	(10)	(11)
SOB1	2	3	1	4	4	1	1	01.53	0.62	0.75
SOB2	2	3	3	4	4	1	1	11.21	0.72	0.46
WAVE	1	1	2	2	2	4	4	07.05	0.73	0.59
LAP1	2	1	3	2	4	1	1	02.31	0.43	0.32
LAP2	2	1	1	2	2	1	2	07.58	0.26	0.24
LAP3	2	1	4	2	4	1	2	02.12	1.14	1.13

In our second (part of our) experimentation, we transform these three benchmark examples and the sequential behaviours of Fig. 2a (PRG) into KPNs using the method given in [2]. We then apply our modelling mechanism to construct ADDGs from these KPNs. The ADDG based equivalence checker is applied next to establish the equivalence between the ADDG corresponding to the sequential behaviour and the ADDG corresponding to the KPN for each case. The number of processes and FIFOs in the KPN, the numbers of arrays, slices and slice classes in the sequential behaviours and its corresponding KPN behaviours and the execution times are tabulated for each of the test cases in Table 3. In all the cases, our method was able to establish the equivalence in <12 s.

Table 3 Results for sequential to KPN transformation

	KPN	Array	Slice	Slice class	Exec. time, s
Benchmark	Process	FIFO	Seq	KPN	Seq	KPN	Seq	KPN
PRG	4	4	6	10	2	6	2	2	03.49
SOB	5	14	4	18	1	1	1	1	11.30
WAVE	5	16	2	18	4	4	2	2	09.22
LAP	2	9	2	11	1	1	1	1	06.17

To test the KPN level transformations, we consider different transformations techniques as shown in Table 4. The number of processes, the number of FIFOs, the number of slices and the execution time of our method are tabulated in Table 4. We could not run the example of message vectorisation since the present implementation of our method does not support message de-vectorisation. For all other cases, our method succeeds in establishing the equivalence in <2 s.

Table 4 Results for KPN level transformations

	Processes	FIFOs	Slices	Time, s
Benchmark	src	trans	src	trans	src	trans
channel merging	2	2	2	1	4	8	0.601
channel splitting	2	2	1	2	2	1	0.398
process splitting	2	3	1	2	2	4	0.367
process merging	4	3	4	4	3	3	0.500
computation migration	3	3	4	3	3	3	1.204

9 Conclusion

This paper presents an equivalence checking method for verification of sequential to parallel KPN and KPN level code transformations often used in multimedia and signal processing applications. The problems are suitably mapped to the equivalence problem of ADDGs. The FIFO communication among the KPN processes has necessitated non-trivial enhancement of the basic ADDG construction method from sequential programs. The method visualises the FIFOs as linear arrays, each with two pointers, one for the consumer and the other for the producer. Significant processing is needed to obtain the relationship of these pointers with the loop iterators; the association can be non-linear even for simple cases. The method then composes the individual ADDGs into a single ADDG around the FIFOs. It has formally established that as long as the association of the FIFO pointers with loop iterators are linear and there is no deadlock, the composed ADDG captures the dependencies across all KPN processes. A correctness proof of construction mechanism is provided. The experimental results on several test cases demonstrate the effectiveness of our method.

References

Horowitz, M., Indermaur, T., Gonzalez, R.: ‘Low‐power digital design’. IEEE Symp. on Low Power Electronics, San Diego, CA, USA, 1994, pp. 8–11

Turjan, A.: ‘Compiling nested loop programs to process networks’. PhD thesis, Leiden University, 2007

Turjan, A., Kienhuis, B., Deprettere, E.: ‘Translating affine nested‐loop programs to process networks’. CASES'04, Washington DC, USA, 2004, pp. 220–229

Kahn, G.: ‘The semantics of a simple language for parallel programming’. Proc. of IFIP Congress, Stockholm, Sweden, 1974, pp. 471–475

Compaan, 2000

Artemis, 2005. Available at http://ce.et.tudelft.nl/artemis/

Daedalus, 2008. Available at http://daedalus.liacs.nl/Site/Daedalus home.html

Metropilis, 2008. http://embedded.eecs.berkeley.edu/metropolis/

Nikolov, H., Stefanov, T., Deprettere, E.: ‘Systematic and automated multiprocessor system design, programming, and implementation’, IEEE TCAD ICS, 2008, 27, (3), pp. 542–555

Davare, A., Zhu, Q., Sangiovanni‐Vincentelli, A.: ‘A platform‐based design flow for kahn process networks’. Technical Report 2006‐30, UC Berkeley, March 2006

Fei, Y., Ravi, S., Raghunathan, A. et al.: ‘Energy‐optimizing source code transformations for operating system‐driven embedded software’, Trans. Embedded Comput. Syst., 2007, 7, (1), pp. 1–26

Meijer, S., Nikolov, H., Stefanov, T.: ‘On compile‐time evaluation of process partitioning transformations for kahn process networks’. CODES‐ISSS'09, Grenoble, France, 2009, pp. 31–40

Meijer, S., Nikolov, H., Stefanov, T.: ‘Throughput modeling to evaluate process merging transformations in polyhedral process networks’. Proc. of Int. Conf. Design, Automation and Test in Europe (DATE'10), Dresden, Germany, 2010, pp. 747–752

Kundu, S., Tatlock, Z., Lerner, S.: ‘Proving optimizations correct using parameterized program equivalence’. PLDI ‘09, Dublin, Ireland, 2009, pp. 327–337

Kundu, S., Lerner, S., Gupta, R.: ‘Translation validation of high‐level synthesis’, IEEE Trans. CAD ICS, 2010, 29, (4), pp. 566–579

Shashidhar, K.C.: ‘Efficient automatic verification of loop and data‐flow transformations by functional equivalence checking’. PhD thesis, Department of Computer Science, Katholieke Universiteit Leuven, Belgium, 2008

Karfa, C., Banerjee, K., Sarkar, D. et al.: ‘Verification of loop and arithmetic transformations of array‐intensive behaviors’, IEEE Trans. CAD ICS, 2013, 32, (11), pp. 1787–1800

Karfa, C., Sarkar, D., Mandal, C.: ‘Verification of KPN level transformations’. 26th Int. Conf. on VLSI Design, Pune, India, 2013, pp. 338–343

Kumar, A., Fernando, S., Ha, Y. et al.: ‘Multiprocessor systems synthesis for multiple use‐cases of multiple applications on fpga’, ACM Trans. Des. Autom. Electron. Syst., 2008, 13, (3), pp. 40:1–40:27

Milner, R.: ‘A calculus of communicating systems’ (Springer‐Verlag, Berlin, Heidelberg, 1982)

Hoare, C.A.R.: ‘Communicating sequential processes’, Commun. ACM, 1978, 21, (8), pp. 666–677

Bergstra, J., Klop, J.: ‘Process algebra for synchronous communication’, Inf. Control, 1984, 60, (1), pp. 109–137

Hennessy, M., Milner, R.: ‘On observing nondeterminism and concurrency’. Proc. of the 7th Colloquium on Automata, Languages and Programming, Berlin, Heidelberg, 1980, pp. 299–309

Park, D.: ‘Concurrency and automata on infinite sequences’. Proc. of the 5th GI‐Conf. on Theoretical Computer Science, London, UK, 1981, pp. 167–183

Pnueli, A.: ‘The temporal logic of programs’. 18th Annual Symp. on Foundations of Computer Science (sfcs 1977), San Diego, California, USA, October 1977, pp. 46–57

Clarke, E.M., Emerson, E.A.: ‘Design and synthesis of synchronization skeletons using branching‐time temporal logic’. Logic of Programs, Workshop, Berlin, Heidelberg, 1982, pp. 52–71

Queille, J.‐P., Sifakis, J.: ‘Specification and verification of concurrent systems in cesar’. Proc. of the 5th Colloquium on Int. Symp. on Programming, London, UK, 1982, pp. 337–351

Holzmann, G.J.: ‘The model checker spin’, IEEE Trans. Softw. Eng., 1997, 23, pp. 279–295

McMillan, K.L.: ‘Symbolic model checking’ (Kluwer Academic Publishers, Norwell, MA, USA, 1993)

Fernandez, J.‐C., Garavel, H., Kerbrat, A. et al.: ‘Cadp – a protocol validation and verification toolbox’. Proc. of the 8th Int. Conf. on Computer Aided Verification, CAV ‘96, London, UK, 1996, pp. 437–440

Burch, J.R., Clarke, E.M., Long, D.E. et al.: ‘Symbolic model checking for sequential circuit verification’, IEEE Trans. Comput.‐Aided Des. Integr. Circuits Syst., 1994, 13, (4), pp. 401–424

Godefroid, P.: ‘Using partial orders to improve automatic verification methods’. Proc. of the 2Nd Int. Workshop on Computer Aided Verification, CAV ‘90, Berlin, Heidelberg, 1991, pp. 176–185

Dams, D., Gerth, R., Grumberg, O.: ‘Abstract interpretation of reactive systems’, ACM Trans. Program. Lang. Syst., 1997, 19, (2), pp. 253–291

Clarke, E.M., Enders, R., Filkorn, T. et al.: ‘Exploiting symmetry in temporal logic model checking’, Form. Methods Syst. Des., 1996, 9, (1–2), pp. 77–104

Abadi, M., Lamport, L.: ‘Conjoining specifications’, ACM Trans. Program. Lang. Syst., 1995, 17, (3), pp. 507–535

Strehl, K., Thiele, L.: ‘Interval diagrams for efficient symbolic verification of process networks’, IEEE Trans. CAD ICS, 2000, 19, (8), pp. 939–956

Raudvere, T., Sander, I., Jantsch, A.: ‘Application and verification of local nonsemantic‐preserving transformations in system design’, IEEE Trans. CAD ICS, 2008, 27, (6), pp. 1091–1103

Chen, X., Hsieh, H., Balarin, F. et al.: ‘Formal verification for embedded system designs’, Des. Autom. Embedded Syst., 2003, 8, pp. 139–153

Kienhuis, B., Rijpkema, E., Deprettere, E.F.: ‘Compaan: deriving process networks from matlab for embedded signal processing architectures’. CODES'00, San Diego, CA, USA, 2000, pp. 13–17

Manna, Z.: ‘Mathematical theory of computation’ (McGraw‐Hill Kogakusha, Tokyo, 1974)

lp_solve, 2010. http://lpsolve.sourceforge.net/5.5/

The Yices SMT Solver. Available at http://yices.csl.sri.com/

Kelly, W., Rosser, E., Pugh, B. et al.: ‘The omega calculator and library’, version 2.1, 2008. Available at http://www.cs.umd.edu/projects/omega/

Cheung, E., Chen, X., Hsieh, H. et al.: ‘Runtime deadlock analysis for system level design’, Des. Autom. Embedded Syst., 2009, 13, pp. 287–310

Jiang, B., Deprettere, E., Kienhuis, B.: ‘Hierarchical run time deadlock detection in process networks’. IEEE Workshop on Signal Processing Systems, Washington DC, USA, 2008, pp. 239–244

Olson, A., Evans, B.: ‘Deadlock detection for distributed process networks’. IEEE Int. Conf. on Acoustics, Speech, and Signal Processing, Philadelphia, PA, USA, 2005, vol. 5, pp. v/73–v/76

Parks, T.M.: ‘Bounded scheduling of process networks’. PhD thesis, EECS Department, University of California, Berkeley, 1995

Oppen, D.C.: ‘A 222pn upper bound on the complexity of presburger arithmetic’, J. Comput. Syst. Sci., 1978, 16, (3), pp. 323–332