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 rel...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2019-03-01
|
| Series: | IET Cyber-Physical Systems |
| Subjects: | |
| Online Access: | https://digital-library.theiet.org/content/journals/10.1049/iet-cps.2018.5008 |
| _version_ | 1818725806132690944 |
|---|---|
| author | Chandan Karfa Dipankar Sarkar Chittaranjan Mandal |
| author_facet | Chandan Karfa Dipankar Sarkar Chittaranjan Mandal |
| author_sort | Chandan Karfa |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-17T21:48:09Z |
| format | Article |
| id | doaj.art-f8917bf6127444a3a9ab35ebf33593ca |
| institution | Directory Open Access Journal |
| issn | 2398-3396 |
| language | English |
| last_indexed | 2024-12-17T21:48:09Z |
| publishDate | 2019-03-01 |
| publisher | Wiley |
| record_format | Article |
| series | IET Cyber-Physical Systems |
| spelling | doaj.art-f8917bf6127444a3a9ab35ebf33593ca2022-12-21T21:31:24ZengWileyIET Cyber-Physical Systems2398-33962019-03-0110.1049/iet-cps.2018.5008IET-CPS.2018.5008Verification of parallelising transformations of KPN modelsChandan Karfa0Dipankar Sarkar1Chittaranjan Mandal2Department of Computer Science and Engineering, Indian Institute of TechnologyDepartment of Computer Science and Engineering, Indian Institute of TechnologyDepartment of Computer Science and Engineering, Indian Institute of TechnologyParallelising 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.https://digital-library.theiet.org/content/journals/10.1049/iet-cps.2018.5008parallel processingsystem-on-chipmultiprocessing systemssignal processinggraph theoryformal verificationKahn process networksheterogeneous multiprocessor systemssignal processing applicationsverification frameworksverification problemsequential behaviourKPN behaviourKPN modelsarray data dependence graphsADDG construction method |
| spellingShingle | Chandan Karfa Dipankar Sarkar Chittaranjan Mandal Verification of parallelising transformations of KPN models IET Cyber-Physical Systems parallel processing system-on-chip multiprocessing systems signal processing graph theory formal verification Kahn process networks heterogeneous multiprocessor systems signal processing applications verification frameworks verification problem sequential behaviour KPN behaviour KPN models array data dependence graphs ADDG construction method |
| title | Verification of parallelising transformations of KPN models |
| title_full | Verification of parallelising transformations of KPN models |
| title_fullStr | Verification of parallelising transformations of KPN models |
| title_full_unstemmed | Verification of parallelising transformations of KPN models |
| title_short | Verification of parallelising transformations of KPN models |
| title_sort | verification of parallelising transformations of kpn models |
| topic | parallel processing system-on-chip multiprocessing systems signal processing graph theory formal verification Kahn process networks heterogeneous multiprocessor systems signal processing applications verification frameworks verification problem sequential behaviour KPN behaviour KPN models array data dependence graphs ADDG construction method |
| url | https://digital-library.theiet.org/content/journals/10.1049/iet-cps.2018.5008 |
| work_keys_str_mv | AT chandankarfa verificationofparallelisingtransformationsofkpnmodels AT dipankarsarkar verificationofparallelisingtransformationsofkpnmodels AT chittaranjanmandal verificationofparallelisingtransformationsofkpnmodels |