Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs

Christophe Alias 1 Alain Darte 1 Paul Feautrier 1 Laure Gonnord 2, 3
1 COMPSYS - Compilation and embedded computing systems
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
3 DART - Contributions of the Data parallelism to real time
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
Abstract : Proving the termination of a flowchart program can be done by exhibiting a ranking function, i.e., a function from the program states to a well-founded set, which strictly decreases at each program step. A standard method to automatically generate such a function is to compute invariants for each program point and to search for a ranking in a restricted class of functions that can be handled with linear programming techniques. Previous algorithms based on affine rankings either are applicable only to simple loops (i.e., single-node flowcharts) and rely on enumeration, or are not complete in the sense that they are not guaranteed to find a ranking in the class of functions they consider, if one exists. Our first contribution is to propose an efficient algorithm to compute ranking functions: It can handle flowcharts of arbitrary structure, the class of candidate rankings it explores is larger, and our method, although greedy, is provably complete. Our second contribution is to show how to use the ranking functions we generate to get upper bounds for the computational complexity (number of transitions) of the source program. This estimate is a polynomial, which means that we can handle programs with more than linear complexity. We applied the method on a collection of test cases from the literature. We also show the links and differences with previous techniques based on the insertion of counters.
Type de document :
Communication dans un congrès
Static Analysis Symposium, Sep 2010, Perpignan, France. 2010, 〈10.1007/978-3-642-15769-1〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00523298
Contributeur : Laure Gonnord <>
Soumis le : lundi 4 octobre 2010 - 17:24:24
Dernière modification le : mardi 16 janvier 2018 - 15:42:47
Document(s) archivé(s) le : mercredi 5 janvier 2011 - 02:57:15

Fichier

rankingCompsys_sas2010.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Christophe Alias, Alain Darte, Paul Feautrier, Laure Gonnord. Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. Static Analysis Symposium, Sep 2010, Perpignan, France. 2010, 〈10.1007/978-3-642-15769-1〉. 〈inria-00523298〉

Partager

Métriques

Consultations de la notice

356

Téléchargements de fichiers

315