NDLI: Translation validation of loop and arithmetic transformations in the presence of recurrences

Content Provider	ACM Digital Library
Author	Banerjee, Kunal Mandal, Chittaranjan Sarkar, Dipankar
Abstract	Compiler optimization of array-intensive programs involves extensive application of loop transformations and arithmetic transformations. Hence, 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. A major obstacle for verification of such programs is posed by the presence of recurrences, whereby an element of an array gets defined in a statement S inside a loop in terms of some other element(s) of the same array which have been previously defined through the same statement S. 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. Another technique which works better for recurrences does not handle arithmetic transformations. In this work, array data-dependence graphs (ADDGs) are used to represent both the original and the optimized versions of the program and a validation scheme is proposed where the cycles due to recurrences in the ADDGs are suitably abstracted as acyclic subgraphs. Thus, this work provides a unified equivalence checking framework to handle loop and arithmetic transformations along with most of the recurrences -- this combination of features had not been achieved by a single verification technique earlier.
Starting Page	31
Ending Page	40
Page Count	10
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/2980930.2907954
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	51
Issue Number	5
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Recurrence Array data-dependence graph (addg) Equivalence checking Loop transformations Arithmetic transformations Translation validation
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Translation validation of loop and arithmetic transformations in the presence of recurrences

Verification of Loop and Arithmetic Transformations of Array-Intensive Behaviors

Translation Validation of Optimizing Transformations of Programs Using Equivalence Checking

Translation Validation of Transformations of Embedded System Specifications Using Equivalence Checking

Tree dependence analysis

Data-race detection: the missing piece for an end-to-end semantic equivalence checker for parallelizing transformations of array-intensive programs

Evaluating value-graph translation validation for LLVM

Proving optimizations correct using parameterized program equivalence

Loop transformations for NUMA machines

Translation validation of loop and arithmetic transformations in the presence of recurrences

Similar Documents

Translation validation of loop and arithmetic transformations in the presence of recurrences

Verification of Loop and Arithmetic Transformations of Array-Intensive Behaviors

Translation Validation of Optimizing Transformations of Programs Using Equivalence Checking

Translation Validation of Transformations of Embedded System Specifications Using Equivalence Checking

Tree dependence analysis

Data-race detection: the missing piece for an end-to-end semantic equivalence checker for parallelizing transformations of array-intensive programs

Evaluating value-graph translation validation for LLVM

Proving optimizations correct using parameterized program equivalence

Loop transformations for NUMA machines

Translation validation of loop and arithmetic transformations in the presence of recurrences