Some Efficient Algorithms for the Tightest UTVPI Polyhedral Over-Approximation Problem

Patwardhan, Abhishek A and Upadrasta, Ramakrishna (2019) Some Efficient Algorithms for the Tightest UTVPI Polyhedral Over-Approximation Problem. In: 9th International Workshop on Polyhedral Compilation Techniques, 21-23 January, 2019, Spain.

Full text not available from this repository. (Request a copy)

Abstract

Many static analysis problems involve solving mathematical data-flow equations over numerical abstract domains. Convex polyhedra is one such abstract domain that is widely used to precisely capture affine relationships among program variables. However, the majority of the analysis problems based on convex polyhedral domains fail to scale for large problem sizes due to the high-complexity/exponential nature of operations defined over them (such as Feasibility, Optimization). The Unit-Two-Variable-Per-Inequality (UTVPI) Polyhedra (also called Octagons) has been proven to be a very useful abstract domain; due to its improved worst-case polynomial time complexity, as well as ease of implementation. In this paper, we present two new algorithms that compute the tightest UTVPI Over-Approximation (OA) of a given convex polyhedron by relying on elementary polyhedral operations. Our algorithms improve over the OA algorithm that is implemented in the state-of-the-art libraries. Our first algorithm is based on linear programming (LP); our second algorithm is based on Fourier-Motzkin elimination (projections) combined with only rotation operations. Both algorithms exploit the Octagonal nature of the OA that they aim to obtain; so, they are highly simple in nature (in theory as well as implementation), simple to reason about correctness and optimality, and also easy to implement. We implemented our two algorithms in the Integer Set Library (ISL), an open-source polyhedral compilation library. Though our work is preliminary, we believe that our algorithms will be useful in static analysis as well as polyhedral compilation applications like iterative optimization, codegeneration, cache miss calculation, and transitive closure.

[error in script]
IITH Creators:
IITH CreatorsORCiD
Upadrasta, RamakrishnaUNSPECIFIED
Item Type: Conference or Workshop Item (Paper)
Subjects: Computer science
Divisions: Department of Computer Science & Engineering
Depositing User: Team Library
Date Deposited: 28 Feb 2019 11:51
Last Modified: 28 Feb 2019 11:51
URI: http://raiithold.iith.ac.in/id/eprint/4852
Publisher URL:
Related URLs:

Actions (login required)

View Item View Item
Statistics for RAIITH ePrint 4852 Statistics for this ePrint Item