Correctness is becoming of paramount concern in more and more areas such as safety-critical systems or compilation into silicon while more and more hardware ressource constraints have to be considered, in particular for embedded systems. Static analysis of programs, which consists in analyzing the source code or the intermediary code, allows determining accurate informations about program behavior using general mathematical frameworks. For example, the polytope model allows modeling nested loops as polyhedra whose contained integer points are associated to iterations. It provides mathematical tools for quantitative analysis and optimizing transformations. In the context of this model, we developped in the past years parametric analysis tools having a lot of applications in analysis and optimization of nested loops. In particular, our tools provide the computation of the Ehrhart polynomial of a parameterized polytope which can translate to the number of iterations of a parameterized loop nest, the number of array elements accessed by a parameterized loop nest, the data access order of a loop nest, etc. However, the polytope model is limited to loops whose loop bounds are affine functions over the enclosing loop indices, and array references are affine functions over the loop indices. Linearity of the considered functions is one of the main limitations in formal analysis. Many behavior modeling issues where interactions between hardware and software are considered, as cache behavior of programs, involve nonlinear expressions. Compilers implementing advanced optimization transformations are also limited by this fact. In particular, multivariate polynomial functions arise in many situations resulting from linearized subscripts in array reference functions, or from induction variable recognition, and compilers fail in handling such expressions. We propose an extension of the theory of Bernstein expansion to handle parameterized multivariate polynomial expressions. Bernstein expansion allows bounding the range of a multivariate polynomial considered over a box. Numerical applications of this theory have been proposed to the resolution of system of strict polynomial inequalities. It has been shown that Bernstein expansion is generally more accurate than classic interval methods. Moreover for sufficiently small boxes, the exact range is obtained. We handle parameterized multivariate polynomials, for which ranges are bound by polynomials over the parameters, by generalizing Bernstein expansion. Sufficient conditions over the parameters for strict parameterized inequalities solutions are therefore constructed. Bernstein polynomials are particular polynomials that form a basis for the space of polynomials. Hence any polynomial can be expressed into this basis through coefficients, the Bernstein coefficients, that have interesting properties and that can be computed through a direct formula. Due to the Bernstein convex hull property, the value of the polynomial is then bounded by the values of the minimum and maximum Bernstein coefficients. The direct formula allows symbolic computation of these Bernstein coefficients giving a supplementary interest to the use of this theory. Another main interesting consequence is that the involved computations have quite low complexity. An appropriate instrumentation of this model allows automatic and inexpensive resolutions of complex program analysis issues as nonlinear dependence analysis, dead code elimination or minimum memory amount needed for array contraction.
Prof. Dr. Philippe Clauss Professor in computer science Universite Louis Pasteur, Strasbourg, France ICPS-LSIIT laboratory Research domains: analysis, optimization and compiling of programs ; embedded systems ; parallel programming.
Sprecher: Prof. Dr. Philippe Clauss Wann: Freitag, 27. Februar 2004, 14:00 Uhr (s.t.) Wo: HS 2, Universität Klagenfurt