Abstract
Array-intensive programs often undergo extensive loop transformations and arithmetic transformations during code optimization. Accordingly, translation validation of array-intensive programs requires manipulation of intervals of integers (representing domains of array indices) and relations over such intervals to account for loop transformations and simplification of arithmetic expressions to handle arithmetic transformations. Translation validation becomes more challenging in the presence of recurrences because recurrences lead to cycles in the data-dependence graph of a program which make dependence analyses and simplifications (through closed-form representations) of the data transformations difficult. To address the problem of translation validation of array-intensive programs, we have developed an equivalence checking framework, where both the original program and the optimized program are modeled as array data-dependence graphs (ADDGs), that can handle loop and arithmetic transformations along with most of the recurrences.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Banerjee, K., Karfa, C., Sarkar, D., Mandal, C.: Verification of code motion techniques using value propagation. IEEE Trans. CAD ICS 33(8), 1180–1193 (2014)
Banerjee, K., Mandal, C., Sarkar, D.: Translation validation of loop and arithmetic transformations in the presence of recurrences. In: LCTES, pp. 31–40 (2016)
Bouchebaba, Y., Girodias, B., Nicolescu, G., Aboulhamid, E.M., Lavigueur, B., Paulin, P.G.: MPSoC memory optimization using program transformation. ACM Trans. Design Autom. Electron. Syst. 12(4), 43 (2007)
Kadayif, I., Kandemir, M.T., Chen, G., Ozturk, O., Karaköy, M., Sezer, U.: Optimizing array-intensive applications for on-chip multiprocessors. IEEE Trans. Parallel Distrib. Syst. 16(5), 396–411 (2005)
Karfa, C., Banerjee, K., Sarkar, D., Mandal, C.: Equivalence checking of array-intensive programs. In: ISVLSI, pp. 156–161 (2011)
Karfa, C., Banerjee, K., Sarkar, D., Mandal, C.: Verification of loop and arithmetic transformations of array-intensive behaviours. IEEE Trans. CAD ICS 32(11), 1787–1800 (2013)
Karfa, C., Sarkar, D., Mandal, C.: Verification of datapath and controller generation phase in high-level synthesis of digital circuits. IEEE Trans. CAD ICS 29(3), 479–492 (2010)
Kundu, S., Lerner, S., Gupta, R.: Translation validation of high-level synthesis. IEEE Trans. CAD ICS 29(4), 566–579 (2010)
Shashidhar, K.C.: Efficient automatic verification of loop and data-flow transformations by functional equivalence checking. Ph.D. thesis, Katholieke Universiteit Leuven (2008)
Shashidhar, K.C., Bruynooghe, M., Catthoor, F., Janssens, G.: Functional equivalence checking for verification of algebraic transformations on array-intensive source code. In: DATE, pp. 1310–1315 (2005)
Verdoolaege, S.: isl: an integer set library for the polyhedral model. In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol. 6327, pp. 299–302. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15582-6_49
Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 599–613. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_44
Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. ACM Trans. Program. Lang. Syst. 34(3), 11 (2012)
Zory, J., Coelho, F.: Using algebraic transformations to optimize expression evaluation in scientific codes. In: IEEE PACT, pp. 376–384 (1998)
Acknowledgment
The authors would like to acknowledge Chandan Karfa, currently at IIT Guwahati, for his useful insights during the formulation of this work. The work of K. Banerjee was supported by TCS Research Fellowship. This work was also funded by DST Project No: SB/EMEQ-281/2013.
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
Banerjee, K., Mandal, C., Sarkar, D. (2017). An Equivalence Checking Framework for Array-Intensive Programs. 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_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-68167-2_6
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)