Abstract
An application program can go through significant optimizing and parallelizing transformations, both automated and human guided, before being mapped to an architecture. Formal verification of these transformations is crucial to ensure that they preserve the original behavioural specification. PRES+ model (Petri net based Representation of Embedded Systems) encompassing data processing is used to model parallel behaviours more vividly. This paper presents a translation validation tool for verifying optimizing and parallelizing code transformations by checking equivalence between two PRES+ models, one representing the source code and the other representing its optimized and (or) parallelized version.
S. Bandyopadhyay is now working at HPI, Potsdam, Germany, email: soumyadip.bandyopadhyay@hpi.de
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Bondhugula, U., Hartono, A., Ramanujam, J., Sadayappan, P.: Pluto: a practical and fully automatic polyhedral program optimization system. In: PLDI (2008)
Par4All. http://www.par4all.org/
Bae, H., Mustafa, D., Lee, J.W., Aurangzeb, A., Lin, H., Dave, C., Eigenmann, R., Midkiff, S.P.: The cetus source-to-source compiler infrastructure: overview and evaluation. IJPP 41(6), 753–767 (2013)
Lidman, J., Quinlan, D.J., Liao, C., McKee, S.A.: Rose: FTTransform-a source-to-source translation framework for exascale fault-tolerance research. In: DSN Workshop, pp. 1–6 (2012)
Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI, pp. 83–94 (2000)
Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998). doi:10.1007/BFb0054170
Rinard, M., Diniz, P.: Credible compilation. Technical report MIT-LCS-TR-776, MIT (1999)
Vafeiadis, V., Balabonski, T., Chakraborty, S., Morisset, R., Nardelli, F.: Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In: POPL, pp. 209–220 (2015)
Kundu, S., Lerner, S., Gupta, R.: Validating high-level synthesis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 459–472. Springer, Heidelberg (2008). doi:10.1007/978-3-540-70545-1_44
Feng, X., Hu, A.J.: Cutpoints for formal equivalence verification of embedded software. In: Proceedings of the 5th ACM International Conference on Embedded Software, EMSOFT 2005, pp. 307–316 (2005)
Bandyopadhyay, S., Sarkar, D., Mandal, C.: An efficient equivalence checking method for petri net based models of programs. In: ICSE, pp. 827–828 (2015)
Bandyopadhyay, S., Sarkar, D., Mandal, C.A., Banerjee, K., Duddu, K.R.: A path construction algorithm for translation validation using PRES+ models. PPL 26(2), 1–25 (2016)
Bandyopadhyay, S., Sarkar, D., Banerjee, K., Mandal, C.: A path-based equivalence checking method for petri net based models of programs. In: ICSOFT, pp. 319–329 (2015)
Bandyopadhyay, S., Sarkar, D., Mandal, C.: An efficient path based equivalence checking for petri net based models of programs. In: ISEC, pp. 70–79 (2016)
Gupta, S., Dutt, N., Gupta, R., Nicolau, A.: SPARK: a high-level synthesis framework for applying parallelizing compiler transformations. In: Proceedings of International Conference on VLSI Design, pp. 461–466 (2003)
Banerjee, K., Karfa, C., Sarkar, D., Mandal, C.: Verification of code motion techniques using value propagation. IEEE TCAD 33(8), 1180–1193 (2014)
Karfa, C., Mandal, C.A., Sarkar, D.: Formal verification of code motion techniques using data-flow-driven equivalence checking. TODAES 17(3), 30 (2012)
Acknowledgment
Santonu Sarkar has been partially supported by Science and Engineering Research Board, Govt. of India project (SB/S3/EECE/0170/2014) for this research work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Bandyopadhyay, S., Sarkar, S., Sarkar, D., Mandal, C. (2017). SamaTulyata: An Efficient Path Based Equivalence Checking Tool. In: D'Souza, D., Narayan Kumar, K. (eds) Automated Technology for Verification and Analysis. ATVA 2017. Lecture Notes in Computer Science(), vol 10482. Springer, Cham. https://doi.org/10.1007/978-3-319-68167-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-68167-2_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-68166-5
Online ISBN: 978-3-319-68167-2
eBook Packages: Computer ScienceComputer Science (R0)