Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

access icon openaccess Verification of parallelising transformations of KPN models

This is an open access article published by the IET under the Creative Commons Attribution-NonCommercial-NoDerivs License (http://creativecommons.org/licenses/by-nc-nd/3.0/)
Received 13/04/2018, Accepted 11/03/2019, Revised 20/02/2019, Published 11/03/2019

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.

Inspec keywords: system-on-chip; signal processing; multiprocessing systems; graph theory; parallel processing; formal verification

Other keywords: verification frameworks; sequential behaviour; KPN behaviour; signal processing applications; Kahn process networks; array data dependence graphs; KPN models; ADDG construction method; verification problem; heterogeneous multiprocessor systems

Subjects: System-on-chip; Multiprocessing systems; System-on-chip; Formal methods; Signal processing and detection; Combinatorial mathematics; Digital signal processing; Combinatorial mathematics

References

    1. 1)
      • 12. 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.
    2. 2)
      • 13. 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.
    3. 3)
      • 45. 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.
    4. 4)
      • 10. Davare, A., Zhu, Q., Sangiovanni-Vincentelli, A.: ‘A platform-based design flow for kahn process networks’. Technical Report 2006-30, UC Berkeley, March 2006.
    5. 5)
      • 28. Holzmann, G.J.: ‘The model checker spin’, IEEE Trans. Softw. Eng., 1997, 23, pp. 279–295.
    6. 6)
      • 48. Oppen, D.C.: ‘A 222pn upper bound on the complexity of presburger arithmetic’, J. Comput. Syst. Sci., 1978, 16, (3), pp. 323–332.
    7. 7)
      • 36. Strehl, K., Thiele, L.: ‘Interval diagrams for efficient symbolic verification of process networks’, IEEE Trans. CAD ICS, 2000, 19, (8), pp. 939–956.
    8. 8)
      • 39. 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.
    9. 9)
      • 1. Horowitz, M., Indermaur, T., Gonzalez, R.: ‘Low-power digital design’. IEEE Symp. on Low Power Electronics, San Diego, CA, USA, 1994, pp. 8–11.
    10. 10)
      • 26. 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.
    11. 11)
      • 27. 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.
    12. 12)
      • 24. Park, D.: ‘Concurrency and automata on infinite sequences’. Proc. of the 5th GI-Conf. on Theoretical Computer Science, London, UK, 1981, pp. 167–183.
    13. 13)
      • 9. Nikolov, H., Stefanov, T., Deprettere, E.: ‘Systematic and automated multiprocessor system design, programming, and implementation’, IEEE TCAD ICS, 2008, 27, (3), pp. 542–555.
    14. 14)
      • 17. 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.
    15. 15)
      • 4. Kahn, G.: ‘The semantics of a simple language for parallel programming’. Proc. of IFIP Congress, Stockholm, Sweden, 1974, pp. 471–475.
    16. 16)
      • 7. Daedalus, 2008. Available at http://daedalus.liacs.nl/Site/Daedalus home.html.
    17. 17)
      • 3. Turjan, A., Kienhuis, B., Deprettere, E.: ‘Translating affine nested-loop programs to process networks’. CASES'04, Washington DC, USA, 2004, pp. 220–229.
    18. 18)
      • 43. 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/.
    19. 19)
      • 21. Hoare, C.A.R.: ‘Communicating sequential processes’, Commun. ACM, 1978, 21, (8), pp. 666–677.
    20. 20)
      • 29. McMillan, K.L.: ‘Symbolic model checking’ (Kluwer Academic Publishers, Norwell, MA, USA, 1993).
    21. 21)
      • 35. Abadi, M., Lamport, L.: ‘Conjoining specifications’, ACM Trans. Program. Lang. Syst., 1995, 17, (3), pp. 507–535.
    22. 22)
      • 37. 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.
    23. 23)
      • 47. Parks, T.M.: ‘Bounded scheduling of process networks’. PhD thesis, EECS Department, University of California, Berkeley, 1995.
    24. 24)
      • 23. 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.
    25. 25)
      • 19. 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.
    26. 26)
      • 42. The Yices SMT Solver. Available at http://yices.csl.sri.com/.
    27. 27)
      • 6. Artemis, 2005. Available at http://ce.et.tudelft.nl/artemis/.
    28. 28)
      • 33. Dams, D., Gerth, R., Grumberg, O.: ‘Abstract interpretation of reactive systems’, ACM Trans. Program. Lang. Syst., 1997, 19, (2), pp. 253–291.
    29. 29)
      • 8. Metropilis, 2008. http://embedded.eecs.berkeley.edu/metropolis/.
    30. 30)
      • 22. Bergstra, J., Klop, J.: ‘Process algebra for synchronous communication’, Inf. Control, 1984, 60, (1), pp. 109–137.
    31. 31)
      • 34. 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.
    32. 32)
      • 46. 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.
    33. 33)
      • 41. lp_solve, 2010. http://lpsolve.sourceforge.net/5.5/.
    34. 34)
      • 25. 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.
    35. 35)
      • 15. Kundu, S., Lerner, S., Gupta, R.: ‘Translation validation of high-level synthesis’, IEEE Trans. CAD ICS, 2010, 29, (4), pp. 566–579.
    36. 36)
      • 31. 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.
    37. 37)
      • 14. Kundu, S., Tatlock, Z., Lerner, S.: ‘Proving optimizations correct using parameterized program equivalence’. PLDI ‘09, Dublin, Ireland, 2009, pp. 327–337.
    38. 38)
      • 30. 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.
    39. 39)
      • 16. 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.
    40. 40)
      • 44. Cheung, E., Chen, X., Hsieh, H., et al: ‘Runtime deadlock analysis for system level design’, Des. Autom. Embedded Syst., 2009, 13, pp. 287–310.
    41. 41)
      • 11. 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.
    42. 42)
      • 2. Turjan, A.: ‘Compiling nested loop programs to process networks’. PhD thesis, Leiden University, 2007.
    43. 43)
      • 18. Karfa, C., Sarkar, D., Mandal, C.: ‘Verification of KPN level transformations’. 26th Int. Conf. on VLSI Design, Pune, India, 2013, pp. 338–343.
    44. 44)
      • 38. Chen, X., Hsieh, H., Balarin, F., et al: ‘Formal verification for embedded system designs’, Des. Autom. Embedded Syst., 2003, 8, pp. 139–153.
    45. 45)
      • 40. Manna, Z.: ‘Mathematical theory of computation’ (McGraw-Hill Kogakusha, Tokyo, 1974).
    46. 46)
      • 32. 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.
    47. 47)
      • 5. Compaan, 2000.
    48. 48)
      • 20. Milner, R.: ‘A calculus of communicating systems’ (Springer-Verlag, Berlin, Heidelberg, 1982).
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cps.2018.5008
Loading

Related content

content/journals/10.1049/iet-cps.2018.5008
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
Print this page
This is a required field
Please enter a valid email address