Verification of parallelising transformations of KPN models

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.