Program Termination and Worst Time Complexity with Multi-Dimensional Affine Ranking Functions

Christophe Alias 1 Alain Darte 1 Paul Feautrier 1 Laure Gonnord 1 Clément Quinson 1
1 COMPSYS - Compilation and embedded computing systems
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : A standard method for proving the termination of a flowchart program is to exhibit a ranking function, i.e., a function from the program states to a well-founded set, which strictly decreases at each program step. Our main contribution is to give an efficient algorithm for the automatic generation of multi-dimensional affine nonnegative ranking functions, a restricted class of ranking functions that can be handled with linear programming techniques. Our algorithm is based on the combination of the generation of invariants (a technique from abstract interpretation) and on an adaptation of multi-dimensional affine scheduling (a technique from automatic parallelization). We also prove the completeness of our technique with respect to its input and the class of rankings we consider. Finally, as a byproduct, by computing the cardinal of the range of the ranking function, we obtain an upper bound for the computational complexity of the source program, which does not depend on restrictions on the shape of loops or on program structure. This estimate is a polynomial, which means that we can handle programs with more than linear complexity. The method is tested on a large collection of test cases from the literature. We also point out future improvements to handle larger programs.
Type de document :
Rapport
[Research Report] 2009, pp.31
Liste complète des métadonnées

Littérature citée [41 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00434037
Contributeur : Christophe Alias <>
Soumis le : vendredi 20 novembre 2009 - 15:43:54
Dernière modification le : mardi 16 janvier 2018 - 15:42:53
Document(s) archivé(s) le : jeudi 17 juin 2010 - 18:33:24

Fichier

RR-7037.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00434037, version 1

Collections

Citation

Christophe Alias, Alain Darte, Paul Feautrier, Laure Gonnord, Clément Quinson. Program Termination and Worst Time Complexity with Multi-Dimensional Affine Ranking Functions. [Research Report] 2009, pp.31. 〈inria-00434037〉

Partager

Métriques

Consultations de la notice

302

Téléchargements de fichiers

139