PRESGen: A Fully Automatic Equivalence Checker for Validating Optimizing and Parallelizing Transformations

ABSTRACT

Petri net has been a popular choice of model of computation (MoC) for representing parallel programs. PRES+ is an extension of the traditional Petri net model which is specially equipped to precisely model embedded systems. Since multi-core and multiprocessor systems have proliferated in the domain of embedded systems as well, it has become critical to validate the optimizing and parallelizing transformations which embedded system specifications go through before being implemented in the hardware. PRES+ model based equivalence checkers for validating such transformations already exist. However, construction of the PRES+ models from the original and the translated codes in these equivalence checkers was not done in an automated manner; thus, leaving scope for inaccurate representation of the PRES+ models since they had to be done manually. Moreover, PRES+ model tends to grow more rapidly with the program size when compared to other MoCs, such as FSMD. To tackle these problems, we propose a method for automated construction of PRES+ models from high-level language programs and using an existing translation scheme to convert PRES+ models to FSMD models, we validate the transformations using a state-of-the-art FSMD equivalence checker. Thus, we have effectively composed an end-to-end fully automatic equivalence checker for validating optimizing and parallelizing transformations. The experimental results demonstrate the practical applicability of our method.

References

1. S. Mohan and J. Helander. Temporal analysis for adapting concurrent applications to embedded systems. In Euromicro Conference on Real-Time Systems (ECRTS), pages 71--82, 2008.
2. E. Allen Emerson and Roopsha Samanta. An algorithmic framework for synthesis of concurrent programs. In Automated Technology for Verification and Analysis (ATVA), pages 522--530, 2011.
3. Peter Marwedel. Embedded System Design. Springer(India) Private Limited, New Delhi, India, 2006.
4. T J Kowalski and D E Thomas. The VLSI design automation system : What's in a knowledge base. In 22nd Design Automation Conference proceedings, pages 252--258, June 1985.
5. M. Shadad. An overview of VHDL language and technology. Procs. of the 23rd Design Automation Conference, 1986.
6. Y. S. Hong, K. H. Park, and M Kim. Automatic synthesis of data paths based on the path search algorithm. IEEE Computer, June 1988.
7. A. Kundig, R. E. Suhrer, and J. Dahler. Embedded Systems: New approaches to their formal description and design. Springer-Verlag, 1986.
8. Oliver H. Bailey. Embedded Systems: Desktop Integration. Wordware Publishing, Inc, 2005.
9. P. R. Panda, F. Catthoor, N. D. Dutt, K. Danckaert, E. Brockmeyer, C. Kulkarni, A. Vandercappelle, and P. G. Kjeldsberg. Data and memory optimization techniques for embedded systems. ACM Trans. Des. Autom. Electron. Syst., 6:149--206, April 2001.
10. David Gay, Philip Levis, Robert von Behren, Matt Welsh, Eric Brewer, and David Culler. The nesC language: A holistic approach to networked embedded systems. In PLDI, pages 1--11, 2003.
11. H. Trickey. Flamel: A high level hardware compiler. IEEE Trans. on CAD., 6:259--269, 1987.
12. G. Kahn. The semantics of a simple language for parallel programming. In Proceedings of IFIP Congress, pages 471--475. North Holland Publishing Company, 1974.
13. A. Turjan, B. Kienhuis, and Ed Deprettere. Translating affine nested-loop programs to process networks. In CASES '04: Proceedings of the 2004 international conference on Compilers, architecture, and synthesis for embedded systems, pages 220--229, 2004.
14. Guilherme Ottoni, Ram Rangan, Adam Stoler, Matthew J. Bridges, and David I. August. From sequential programs to concurrent threads. IEEE Comput. Archit. Lett., 5(1):2, 2006.
15. M. Girkar and C. D. Polychronopoulos. Automatic extraction of functional parallelism from ordinary programs. IEEE Trans. Parallel Distrib. Syst., 3(2):166--178, 1992.
16. Alexandru Turjan. Compiling Nested Loop Programs to Process Networks. PhD thesis, Leiden University, 2007.
17. Chandan Karfa. Hand-in-hand verification and synthesis of digital circuits. MS Thesis, IIT Kharagpur, 2007.
18. Youcef Bouchebaba, Bruno Girodias, Gabriela Nicolescu, El Mostapha Aboulhamid, Bruno Lavigueur, and Pierre Paulin. Mpsoc memory optimization using program transformation. ACM Trans. Des. Autom. Electron. Syst., 12(4):43:1--43:39, 2007.
19. Antoine Fraboulet, Karen Kodary, and Anne Mignotte. Loop fusion for memory space optimization. In ISSS '01: Proceedings of the 14th international symposium on Systems synthesis, pages 95--100, 2001.
20. I. Kadayif and M. Kandemir. Data space-oriented tiling for enhancing locality. Trans. on Embedded Computing Sys., 4(2):388--414, 2005.
21. Feihui Li and Mahmut Kandemir. Locality-conscious workload assignment for array-based computations in mpsoc architectures. In Proceedings of DAC '05, pages 95--100, 2005.
22. YongKang Zhu, Grigorios Magklis, Michael L. Scott, Chen Ding, and David H. Albonesi. The energy impact of aggressive loop fusion. In PACT '04: Proceedings of the 13th International Conference on Parallel Architectures and Compilation Techniques, pages 153--164, 2004.
23. Stephen Edwards, Luciano Lavagno, Edward A. Lee, and Alberto Sangiovanni-Vincentelli. Design of embedded systems: Formal models, validation, and synthesis. In Proceedings of the IEEE, pages 366--390, 1997.
24. M R Garey and D S Johnson. Complexity results for multi-processor scheduling under resource constraints. Procs. of 8-th Annual Princeton Conference on Information Sciences and Systems, 1974.
25. G. Lakshminarayana, S. Khouri, and N.K. Jha. Wavesched: A novel scheduling technique for control-flow intensive designs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 18(5):505--523, May 1999.
26. Mauricio Varea, Bashir M. Al-Hashimi, Luis Alejandro Cortés, Petru Eles, and Zebo Peng. Dual flow nets: Modeling the control/data-flow relation in embedded systems. ACM Trans. Embedded Comput. Syst., 5(1):54--81, 2006.
27. Mauricio Varea, Bashir M. Al-Hashimi, Luis Alejandro Cortés, Petru Eles, and Zebo Peng. Symbolic model checking of dual transition petri nets. In Proceedings of the Tenth International Symposium on Hardware/Software Codesign, CODES 2002, Estes Park, Colorado, USA, May 6--8, 2002, pages 43--48, 2002.
28. Luis Alejandro Cortés, Petru Eles, and Zebo Peng. Verification of embedded systems using a petri net based representation. In ISSS '00: Proceedings of the 13th international symposium on System synthesis, pages 149--155, Washington, DC, USA, 2000. IEEE Computer Society.
29. Luis Alejandro Cortés, Petru Eles, and Zebo Peng. Formal coverification of embedded systems using model checking. In 26th EUROMICRO 2000 Conference, Informatics: Inventing the Future, 5--7 September 2000, Maastricht, The Netherlands, pages 1106--1113, 2000.
30. Luis Alejandro Cortés, Petru Eles, and Zebo Peng. Verification of embedded systems using a petri net based representation. In Proceedings of the 13th International Symposium on System Synthesis, ISSS'00, Madrid, Spain, September 20--22, 2000., pages 149--156, 2000.
31. Michael D. Smith, Mark Horowitz, and Monica S. Lam. Efficient superscalar performance through boosting. In ASPLOS-V: Proceedings of the fifth international conference on Architectural support for programming languages and operating systems, pages 248--259, New York, NY, USA, 1992. ACM Press.
32. Mahmut Kandemir, N. Vijaykrishnan, Mary Jane Irwin, and Wu Ye. Influence of compiler optimizations on system power. IEEE Trans. Very Large Scale Integr. Syst., 9:801--804, December 2001.
33. Mahmut Taylan Kandemir. Reducing energy consumption of multiprocessor soc architectures by exploiting memory bank locality. ACM Trans. Des. Autom. Electron. Syst., 11(2):410--441, 2006.
34. C. V. Ramamoorthy, K. M. Chandy, and Mario J. Gonzalez. Optimal scheduling strategies in a multiprocessor system. IEEE Trans. on Computer, C-21(2):137--146, Feb. 1972.
35. J D Ullman. Polynomial complete scheduling problems. Operating Systems Review, 7(4), 1973.
36. V. Raghavan. Principles of Compiler Design. Tata McGraw Hill Education Private Limited, New Delhi, 2010.
37. E. G. Coffman Jr eds. Computer and Job Shop Scheduling Theory. John Wiley & Sons., 1976.
38. Luiz C. V. Dos. Santos and J.A.G Jress. A reordering technique for efficient code motion. In Procs. of the 36th ACM/IEEE Design Automation Conference, DAC '99, pages 296--299, New York, NY, USA, 1999. ACM.
39. Amir Pnueli, Ofer Strichman, and Michael Siegel. Translation validation for synchronous languages. In ICALP, pages 235--246, 1998.
40. George C. Necula. Translation validation for an optimizing compiler. In PLDI, pages 83--94, 2000.
41. M. Rinard and P. Diniz. Credible compilation. Technical Report MIT-LCS-TR-776, MIT.
42. S. Kundu, S. Lerner, and R. Gupta. Validating high-level synthesis. CAV '08, pages 459--472, 2008.
43. Soham Chakraborty and Viktor Vafeiadis. Formalizing the concurrency semantics of an LLVM fragment. In Proceedings of the 2017 International Symposium on Code Generation and Optimization, CGO 2017, Austin, TX, USA, February 4--8, 2017, pages 100--110, 2017.
44. R Camposano. Path-based scheduling for synthesis. IEEE transactions on computer-Aided Design of Integrated Circuits and Systems, Vol 10 No 1:85--93, Jan. 1991.
45. Chandan Karfa, Chittaranjan A. Mandal, Dipankar Sarkar, S. R. Pentakota, and Chris Reade. A formal verification method of scheduling in high-level synthesis. In ISQED, pages 71--78, 2006.
46. Chandan Karfa, Dipankar Sarkar, Chitta Mandal, and P. Kumar. An equivalence-checking method for scheduling verification in high-level synthesis. IEEE Trans. on CAD of Integrated Circuits and Systems, 27(3):556--569, 2008.
47. Chandan Karfa, Chittaranjan A. Mandal, and Dipankar Sarkar. Formal verification of code motion techniques using data-flow-driven equivalence checking. ACM Trans. Design Autom. Electr. Syst., 17(3):30, 2012.
48. K. Banerjee, C. Karfa, D. Sarkar, and Chittaranjan Mandal. Verification of code motion techniques using value propagation. IEEE TCAD, 33(8), 2014.
49. Soumyadip Bandyopadhyay, Kunal Banerjee, Dipankar Sarkar, and Chittaranjan A. Mandal. Translation validation for pres
50. models of parallel behaviours via an fsmd equivalence checker. In VDAT, pages 69--78, 2012.
51. Jean-Baptiste Voron and Fabrice Kordon. Transforming sources to Petri nets: A way to analyze execution of parallel programs. In SimuTools, page 13, 2008.
52. Soumyadip Bandyopadhyay. Equivalence checking in embedded systems design verification using PRES+ model. CoRR, abs/1010.4953, 2010.
53. Youngsik Kim, Shekhar Kopuri, and Nazanin Mansouri. Automated formal verification of scheduling process using finite state machines with datapath (FSMD). In ISQED, pages 110--115, 2004.
54. Bijan Alizadeh and Masahiro Fujita. Automatic merge-point detection for sequential equivalence checking of system-level and RTL descriptions. In ATVA, pages 129--144, 2007.
55. Soumyadip Bandyopadhyay, Dipankar Sarkar, Chittaranjan A. Mandal, Kunal Banerjee, and Krishnam Raju Duddu. A path construction algorithm for translation validation using PRES+ models. Parallel Processing Letters, 26(2):1--25, 2016.
56. M. Rahmouni and A. A. Jerraya. Formulation and evaluation of scheduling techniques for control flow graphs. In Proceedings of EuroDAC'95, pages 386--391, Brighton, 18--22 September 1995.
57. S. Gupta, N. Dutt, R Gupta, and A. Nicolau. SPARK: A high-level synthesis framework for applying parallelizing compiler transformations. In Proc. of Int. Conf. on VLSI Design, pages 461--466, Washington, DC, USA, Jan 2003. IEEE Computer Society.
58. Soumyadip Bandyopadhyay and Kunal Banerjee. Implementing an efficient path based equivalence checker for parallel programs. In Proceedings of the ACM Workshop on Software Engineering Methods for Parallel and High Performance Applications, Kyoto, Japan, May 31 - June 04, 2016, pages 3--10, 2016.
59. Soumyadip Bandyopadhyay and Kunal Banerjee. Implementing an efficient path based equivalence checker for parallel programs. In Proceedings of the ACM Workshop on Software Engineering Methods for Parallel and High Performance Applications, Kyoto, Japan, May 31 - June 04, 2016, pages 3--10, 2016.
60. Soumyadip Bandyopadhyay, Dipankar Sarkar, and Chittaranjan A. Mandal. Validating SPARK: high level synthesis compiler. In 2015 IEEE Computer Society Annual Symposium on VLSI, ISVLSI 2015, Montpellier, France, July 8--10, 2015, pages 195--198, 2015.
61. Soumyadip Bandyopadhyay, Dipankar Sarkar, and Chittaranjan A. Mandal. Translation validation using path-based equivalence checking of petri net based models of programs. In WEPL, 2015.
62. Soumyadip Bandyopadhyay. Behavioural verification of petri net based models of programs. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL(SRC) 2015, Mumbai, India, January 15--17, 2015, 2015.
63. Soumyadip Bandyopadhyay, Dipankar Sarkar, and Chittaranjan A. Mandal. Poster: An efficient equivalence checking method for petri net based models of programs. In 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16--24, 2015, Volume 2, pages 827--828, 2015.
64. Soumyadip Bandyopadhyay, Dipankar Sarkar, and Chittaranjan A. Mandal. An efficient path based equivalence checking for petri net based models of programs. In Proceedings of the 9th India Software Engineering Conference, Goa, India, February 18--20, 2016, pages 70--79, 2016.
65. Soumyadip Bandyopadhyay. Supporting code and examples. https://github.com/soumyadipcsis/Equivalence-checker/blob/master/thesisBench.zip, Jan 2017.