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.
Actions (login required)
 |
View Item |
Altmetric
Altmetric