Translation validation is the process of proving semantic equivalence between source and source-translation, i.e., checking the semantic equivalence between the target code (which is a translation of the source program being compiled) and the source code. In this paper, we propose a translation validation technique for Petri net based models of programs which verify several code optimizing transformations involving loop. These types of transformation have been used in several application domains such as scheduling phase of High level synthesis, high performance computations etc. Our Petri net based equivalence checker checks the computational equivalence between two one-safe colour Petri nets. In this work, we have taken two versions of CPNs one corresponds to the source program and the other, the target programs. Using path based analysis technique, we have developed a sound method for proving several code optimizing transformations involving loop. We have also compared our results with other Petri net based equivalence checkers.The experimental result shows the e cacy of the method.
General applications when executed on parallel and embedded systems often go through a series of semantic preserving transformations. This is done so that the resulting translated program can optimally utilize the underlying computing architecture like multi-core and vector registers. There are various methods of code transformations like code motions, common sub-expression eliminations, dead code elimination, etc and several loop based transformation techniques such as loop distribution, loop parallelization, etc. These transformations are either carried out automatically by some compilers, or done semi-automatically/manually be design experts. Validation of a compiler, to ensure correctness of code-translation, by the construction property is a di cult task. Using, behavioral and semantic veri cation techniques, it is possible to verify whether the translated (optimized) program has the same functionality as that of the original code.
Hence, there is a need for proving behavioral equivalence between the original and the translated programs. This process of proving semantic equivalence between ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). source and source-translation, i.e., checking the semantic equivalence between the target code (which is a translation of the source program being compiled) and the source code is called translation validation. Conventionally, the basic method for validation is to check the equality in input and output pairs between the source and the translated program. However, this is not a sound proof that strictly establishes equivalence between the programs.
Petri Nets have been a popular paradigm for modelling instruction-level parallel
behaviours [
In [
In this paper, we propose a translation validation technique based on a restricted CPN model of programs which veri es several code optimizing transformations involving loop. Through a small set of experimentations, we have compared our method with both SamaTulyata and CDFG based equivalence checkers. The major contributions of our work are as follows: { Development of e cient Petri net based models for programs. { Development of e cient equivalence checking algorithm which can handle various loop involving code-optimizing transformations.
This paper is organised as follows: Section 2 presents an overview of the general work ow of our method. Through a motivating example, we have illustrated our equivalence checking mechanism in Section 3. Section 4 provides the experimental results, comparing our tool with SamaTulyata and two other CDFG-based equivalence checking tools. Section 5 describes the related work. Finally, we conclude our paper by summarizing our results in Section 6. 2
into a nite number of paths. This is facilitated by the Path Constructor module that gives us the set of paths, Qs for Ms, and Qt for Mt. A path is characterized by its corresponding data transformation functions and related conditions of execution.
The notion of equivalence checking used is as follows: \8 paths 2 Ms 9 an equivalent path in Mt". The Path-based Equivalence Checker module takes the sets of paths for both the CPN models, and using the concept of extension of paths that we have developed, checks for equivalence between the paths and returns a Yes/No answer for the semantic equivalence between source and translated programs. The module never gives a false positive result. 3
The motivating example for this paper is depicted in Fig. 2. The source program depicted in Fig. 2.(a) computes the statement out = x + i + d;. In this program, the statement d + + increments d repeatedly with the loop variable i, until its value reaches 5. Consequently, the loop variable i reaches its maximum speci ed value, 10, and the program nally computes the value of the variable out. In the translated version, which is depicted in Fig. 2.(c), the variable d is directly initialised with the value 5. It is to be noted that the two programs are semantically equivalent. This translation is commonly known as loop-independent code-optimizing transformation. To prove the semantic equivalence we have derived the following steps. 3.1
A restricted CPN Model is an eight tuple N = hP; V; fpv; T; I; O; inP; outP i, { The set P = fp1; p2; :::; pmg is a nite non-empty set of places. { The set V is the set of variables of the program which N seeks to model. { The item fpv : P ! V [ f g depicts an association of the places of N to the program variables V ; the role of is explained shortly. fpv(p) assumes values from a domain Dp. Depending on the type of variable fpv(p), the token value at the place p may be of type Boolean, integer, structure, etc. { The set T = ft1; t2; :::; tng is a nite non-empty set of transitions.
Each transition t 2 T is associated with a guard condition gt : Dp1 Dp2 ::: Dpn ! f>; ?g j p1; p2; :::; pn are pre-places of transition t. { I P T is a nite non-empty set of input arcs which de ne the ow relation between places and transitions. { O T P is a nite non-empty set of output arcs which de ne the ow relation between transitions and places.
Each outgoing edge o = (t; p) is associated with a function fo : Dp1 Dp2 ::: Dpn ! Dp j p1; p2; :::; pn are pre-places of transition t { The set inP P, is the set of input places of the program. These are the places which are initially marked before the program is formally executed. { The set outP P, is the set of output places of the program. These are the places whose token value represents the output of the program.
De nition 1. A marking is a function M : P ! f0; 1g that denotes the absence or presence of a token in the places of the net. The restricted CPN model is one-safe. De nition 2. The ring of an enabled transition t, changes the marking M into a new marking M +. Let the input-set t = fp1; p2; :::; pag and output set t = fq1; q2; :::; qbg, these events occur simultaneously: { Tokens from the input-set t are removed. M +(pi) = 0 8 pi 2 t. { One token is added to each place in its output-set t . M +(qi) = 1 8 qi 2 t . { Each new token in t has a token value which is calculated evaluating the respective output function. 3.2
Fig. 2.(b) depicts the Petri net model corresponding to the source program in Fig. 2.(a). The model is derived from the rudimentary automated model constructor as reported in [SamaTulyata]. When the program starts, the token is initially in the inP ort place p1 and the transition t1 is executed. The token is removed from p1 and tokens go parallel, albeit with di erent values that are dependent on the function associated with the respective outgoing edge, to p2, p3, and p4 Transitions t2, t3 and t4 have their associated guard conditions. A particular transition is only executed when its respective guard condition is true. In this scenario, the current value of the token in p3 is 0. Transition t2 res because it's guard condition is true, the value of the tokens in p3 and p4 is incremented by 1. This loop executes repeatedly, incrementing p3 and p4, till the guard condition of t3 is satis ed. Then t3 res to increment the value of the token in p3 till the guard condition of t4 is satisi ed. Finally, the guard condition of t4 is true and the token with value x + i + d is sent to outP ort p5.
In Fig. 2.(d), places p02, p03, and p04 are associated with the values of the variables, i, x, and d respectively. Transition t01 assigns the values 0, 0, and 5 to their respective tokens. t02 is now enabled since p02 is it's pre-place and the associated guard condition for ring t02, i < 10 is true. t02 res to increment the value of the token in p02. This cycle executes another 9 times until the value of the token in p2, indicating the value of the variable i, equals 10. Once the token value equals 10, t03 is enabled and red, since its guard condition corresponding to p02, i 10 is satis ed. t03 sums the values of the tokens in p0 , p03, and p04 and transfers this value as a token to place 2 p05, which indicates the value of the variable out.
The abstraction begins with de ning the function which is associated with
each outgoing edge of the Petri net. It is a mapping from the edge e, such that
e 2 (t; p); 8t 2 T; p 2 P , to the particular function concerning token value
transformation, associated with the edge. This is in contrast to the previous model used in
[
In a general program with loops, we do not know how many times the loop will be executed. To prove semantic equivalence and represent the computation in the terms of nite number of paths, we cut the loops and construct the paths in the graph from cut-point to cut-point without any intermediate cut-point. In our equivalence checking mechanism, the notion of cut-points is as follows: { inP orts are cut-points. { outP orts are cut-points. { The places with back-edges are cut-points.
Using backward traversal and cone of in uence method, we nd the sequence of parallelizable functional paths, from cut-point to cut-point. If a function has been covered in one path, it need not be considered as part of another path. The corresponding paths in Fig. 2.(b) have been marked in Fig. 3.(a). They are: 1 = hf 1g; f 8gi, 2 = hf 2gi, 3 = hf 3gi, 4 = hf 4gi, 5 = hf 5gi, 6 = hf 6gi, 7 = hf 7gi Similarly, the paths in Fig. 2.(c) have been marked in Fig. 3.(b). They are: 1 = hf 2; 3g; f 5gi, 2 = hf 1gi, 3 = hf 4gi
Now we show the validity of the path-based equivalence checker i.e., any computation can be captured as a concatenation of parallel paths. The computation from the Petri net model of the source code in Fig. 3.(a) is p5 = hfp1; fp2; p3; p4gn+m; p5i. Similarly, the computation for the Petri net model of the translated code in Fig. 2(b) is p05 = hfp01; fp02; p03; p04gn; p05i.
The same computations can be written in terms of the sequence of transitions red. The method to do the same is as follows: The ith element of the computation in terms of the transitions is the transition/s that res when moving from marking i to i+1 in the previous version of the computation. So p5 = hft1g; ft2gn; ft3gm; ft4gi. Similarly, p05 = hft01g; ft02gn+m; ft03gi.
The same computation can the be expressed in terms of the delta functions we de ned earlier. To do so, we iterate once over the computation in terms of the transitions. For the new computation, we, append the deltas associated with each transition in the iteration, to the new computation.
So, p5 = hf 1; 2; 3g; f 4; 5gn; f 6; 7gm; 8i.
Similarly, p05 = hf 1; 2; 3g; f 4gn+m; 5i.
The steps to capture the same in terms of paths is as follows: 8 is the last member of the computation sequence p5 and is also the last member of the path 1. So 1 is appended to the computation sequence rp5 and all the -function members of 1 will be deleted from p5 . The method terminates when p5 = ;. For this computation, rp5 = hf 2 k 3g; f 4 k 5gn; f 6 k 7gm; 1i. Similarly, p05 = hf 2g; f 3gn+m; 1i.
r 3.4
The intuitive idea of the the equivalence checking mechanism is described in the following algorithmic steps:
step 1) The set of paths in the rst program and the second program are respectively: 0 = f 1; 2; 3; 4; 5; 6; 7g, 1 = f 1; 2; 3g
step 2) For the path 1, we have to nd the corresponding candidate path. There is no candidate path path for 1 because the set of pre-places of 1, has no direct correspondence with any path in 1. So, we have to extend 1.
step 3) Extension: The parallel paths set of 1 is f 2; 3g. For the path 2, the pre-place of 2 has direct correspondence with the pre-place of 2 and their data transformation and condition of execution are equivalent. Hence, 2 = 2. So, 2 is removed from the parallel list set of 1. Therefore, p3 corresponds with p0 . 2
Now, the pre-places of 4 correspond with pre-place of 3, but their data transformation and condition of execution do not match. So we have to extend 4. The parallel list set of 4 is the singleton f 6g. 6 also does not directly correspond to any path from 1. Hence we have to extend the path 4. The pre-places and post-places of 4 and 6 match. The concatenated path is of the form 0 = 4 k 6. This 0 = 3, since the data transformation and condition of execution of the paths match.
We are left with f 1; 3; 5; 7g and f 1g For 3, the post-path of 3 is f 5; 7g and f 5; 7g are the pre-path of 1. Now, the concatenated path is of the form 00 = ( 1 k ( 3 ( 5 k 7))). The pre-places of 00 correspond with the pre-places 1 and data-transformation is matched and the condition of execution is of the form (R 1 _ (R 3^(R 5_R 7))). Hence, 00 = 1
2 = 2; ( 4 k 6) = 3; ( 1 k ( 3 ( 5 k 7))) = 1 4 4.1
We have taken ve benchmark programs from HLS benchmark suite provided in
[
We have tested the prototype of our tool, SamaTulyataII 4, on a 2.5GHz Intel(R)
Core(TM)-i5-7200U processor. We feed the programs into [
Our proposed tool, SamaTulyataII, is able to validate several code-optimzing transformations involving loop. The CDFG-based methods fail to validate loopswapping transformation since the control structure is changed. Both SamaTulyata and FSMDEQX-VP cannot validate code-optimizing transformation involving loop, but the extended version of FSMDEQX-VP ie. FSMDEQX-EVP is able to validate.
In case the control structure of the program is altered, our tool is able to handle such cases. This is because our method captures instruction level parallelism vividly. 5
Translation validation was rst introduced by Pnueli et al. in [
Tvoc is a translation validation tool developed by Goldberg, et al. for optimizing
compilers that utilize structure preserving and structure modifying transformations
[
Path based validation methods handle both structure preserving transformations
and some non-structure preserving code optimizing transformations. One class of
the non structure preserving code optimizing transformation is loop involving code
optimization which is commonly used in scheduling phase of high level synthesis.
A path based equivalence checking mechanism using CDFG-based technique is
reported in [
We have developed an e cient method for checking equivalence between two scalar handling programs using Petri net based model. This method can handle several loop involved code optimizing transformations, code motion across loop, duplicating up, duplicating down, boosting up, boosting down, and loop swapping transformations. In this work we have considered those programs which works only for integer type variables with no function calls, arrays, or pointers. The major limitations of this method are that it cannot handle loop shifting, loop reversal, software pipe lining based transformations. Further work is aimed at overcoming these limitations and extension of our method to capture array handling programs.