|
Title
|
|
|
|
Translation validation of loop involving code optimizing transformations using Petri net based models of programs
| |
|
Author
|
|
|
|
| |
|
Abstract
|
|
|
|
| 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 efficacy of the method. |
| |
|
Language
|
|
|
|
English
| |
|
Source (book)
|
|
|
|
Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency, June 24, 2020
| |
|
Publication
|
|
|
|
CEUR-WS.org
,
2020
| |
|
ISSN
|
|
|
|
1613-0073
| |
|
Volume/pages
|
|
|
|
(2020)
, p. 1-9
| |
|