Part 1
Présentation de l'unité


Chapter 1
Équipes de recherche

1.1  Sémantique et Interprétation Abstraite


Part 2
Activité scientifique des équipes


Chapter 2
Sémantique et Interprétation Abstraite

L'équipe s'est constituée en octobre 1991 à l'occasion du recrutement comme professeur de Patrick Cousot. L'axe principal de recherche de l'équipe est l'interprétation abstraite [CC77,Cou96a] dans ses aspects théoriques concernant la conception et l'approximation de sémantiques [Cou97c] et ses aspects appliqués concernant l'analyse sémantique et la vérification de programmes [Cou96g]. Au travers d'un séminaire hebdomadaire, le groupe conserve des liens privilégiés avec l'équipe <<Sémantique, preuve et interprétation abstraite>> du LIX, que Patrick Cousot a créée et dirigée jusqu'au 1er octobre 1991.

2.1  Introduction

Les buts de recherche dans cette équipe sont de développer les modèles de sémantiques, les fondements de l'interprétation abstraite et l'analyse sémantique des programmes.
Les modèles de sémantiques :   ce travail concerne principalement les méthodes de présentation des sémantiques, l'étude des relations entre sémantiques permettant de construire des hiérarchies de descriptions obtenues par interprétation abstraite et les modèles du parallélisme permettant une distinction fine entre vrai parallélisme et non-déterminisme.
Les fondements de l'interprétation abstraite :   il s'agit d'étudier les diverses modélisations de la notion d'approximation discrète en sémantique. Les applications concernent la sémantique (par exemple le non-déterminisme peut être compris comme une approximation du parallélisme) et l'analyse de programme (par exemple l'analyse de nécessité pour les langages fonctionnels paresseux est traditionnelement comprise comme une approximation de leur sémantique dénotationnelle).
Les méthodes d'analyse et de manipulation de programmes par interprétation abstraite de sémantiques :   il s'agit de spécifier et de construire des analyseurs sémantiques pour la détermination automatique, statique et correcte de propriétés dynamiques des programmes. L'analyse sémantique de programmes peut s'organiser en deux parties relativement indépendantes : Cette dichotomie sert de base à la présentation de notre travail. Les applications, qui concernent la mise au point symbolique de programmes, la compilation, l'évaluation partielle, la transformation de programmes comme la parallélisation, les preuves (génération automatique d'invariants, preuves de terminaison), la vérification automatique de modèles (model-checking) etc., sont évidemment liées aux deux aspects. Les efforts ont porté principalement sur les langages fonctionnels (analyse de nécessité, des temps de liaison, typage), les langages logiques, l'analyse de programmes parallèles et plus récemment l'analyse des langages objets.

2.2  Sémantiques

2.2.1  Présentation de sémantiques et construction de hiérarchies de sémantiques par interprétation abstraite

Si toutes les méthodes de définition de sémantiques des langages de programmation procèdent de manière compositionnelle par induction sur la syntaxe, elles diffèrent généralement dans leur style de présentation, que ce soit par point fixe, sous forme équationnelle, de contraintes, de conditions de fermeture, par un système formel à base de règles ou par un jeu. Nous avons étendu tous ces modes de présentation aux comportements infinis [Cou95e,Cou97c], ce qui permet alors de montrer l'équivalence de ces divers modes de présentation [CC95a]. Ces présentations de sémantiques étant conservées par interprétation abstraite [CC95a], il devient possible de comprendre toutes les sémantiques d'un langage de programmation comme des approximations les unes des autres. Ceci permet de construire des hiérarchies de sémantiques [Cou95e,Cou97c] qui diffèrent seulement par la précision de la description de l'exécution et le mode de présentation. Par exemple [Cou95e] une sémantique opérationnelle du parallélisme peut s'approcher par le non-déterminisme. On obtient une sémantique de traces finies ou infinies. Ignorant les états intermédiaires, on obtient une sémantique dénotationnelle. Ignorant la non-terminaison, on obtient une sémantique naturelle. Considérant des ensembles d'états, on obtient les transformateurs de prédicats. Décrivant ces ensembles par des langages formels, on obtient des sémantiques axiomatiques sur lesquelles sont basées les méthodes de preuve [Cou97c]. Il s'agit à terme de trouver un modèle de sémantique et une présentation indépendants d'un langage de programmation particulier, rôle que jouent les systèmes de transition dans le cas des sémantiques opérationnelles de petits pas.

2.2.2  Modèles du vrai parallélisme par automates de dimension supérieure

Si les modèles mathématiques du calcul sont bien connus pour les langages séquentiels, il n'en va pas de même dans le cas du parallélisme où il faut prendre en considération l'exécution simultanée d'actions concurrentes, synchrones ou asynchrones. C'est pourquoi nous étudions les modèles opérationnels du << vrai >> parallélisme basés sur la notion d'automate de dimension supérieure issue des idées de Vaughan Pratt et Rob van Glabbeek (Stanford University). Ces modèles sont extrêmement flexibles puisqu'ils permettent de définir de façon dénotationnelle ou bien opérationnelle des langages parallèles aussi divers que Linda, Parallel Pascal (avec des variables partagées) ou Concurrent ML (communications via des messages). Par interprétation abstraite, ils permettent de construire effectivement un automate approché qui modélise les comportements dynamiques possibles du programme considéré, pour faire, par exemple, des analyses de systèmes infinis par model-checking abstrait.
Un automate de dimension supérieure est similaire aux automates classiques, dans le sens où l'on a toujours des états, et des transitions reliant les états. Pour exprimer le parallélisme, et même le vrai parallélisme (qui se distingue des traductions par entrelacements, identifiant non-déterminisme et parallélisme), on rajoute des transitions de dimension supérieure exhibant le degré d'asynchronie que l'on peut avoir dans l'exécution d'un programme. Ces transitions peuvent se représenter géométriquement, tout comme les transitions << ordinaires >> (de dimension 1, car ce sont des segments) et les états (ou transitions de dimension 0, car ce sont des points). Par exemple, l'entrelacement a.b+b.a (notation CCS) a pour représentation comme automate quatre transitions de dimension 1 formant le bord d'un carré. Remplir le carré consiste à rajouter une transition de dimension 2, et donc à indiquer l'indépendance des actions a et b. Les dimensions d'ordre supérieur décrivent donc le degré de parallélisme effectif lors de l'exécution d'opérations concurrentes. Cette information supplémentaire est importante pour effectuer certaines analyses de programmes comme l'exclusion mutuelle ou l'indépendance entre actions et valider des propriétés liées à la géométrie des systèmes de transitions (blocages, branchements, etc.).
On voit déjà dans l'exemple ci-dessus que certaines propriétés géométriques ont une signification en terme de propriétés des exécutions possibles. Ici le trou (carré vide) indique une exclusion mutuelle, alors que le carré plein dénote le vrai parallélisme. D'autres propriétés ont un caractère géométrique également comme les blocages (deadlocks), les branchements et confluences, et donc les équivalences sémantiques << branching-time >>, l'ordonnancement des actions, etc. Tout ceci peut se traiter algébriquement de façon élégante en utilisant des outils de topologie algébrique et d'algèbre homologique [Gou95b]. Le modèle lui-même des automates de dimension supérieure peut se formaliser à travers la notion de complexe double de modules (algèbre homologique). Des critères purement algébriques ont été développés pour définir et calculer les propriétés précédemment citées. Par interprétation abstraite, il en découle naturellement des algorithmes d'analyse d'ordonnancement [Gou95c]. À terme, on devrait pouvoir disposer d'un prototype d'analyseur permettant de prouver des propriétés de correction partielle concernant les accès à des objets partagés ou l'ordonnancement des synchronisations et des messages.
On peut définir diverses sortes de systèmes de transitions de dimension supérieure. Les systèmes totaux (HTS) décrivent toutes les transitions de dimension supérieure qui vérifient une propriété de confluence locale. Ils permettent de modéliser la confluence et le branchement à tout niveau de parallélisme. Les systèmes partiels (PHTS) permettent de plus de modéliser l'interférence entre plusieurs actions parallèles, comme par exemple la lecture et l'écriture par deux processeurs d'une même location mémoire.
Le caractère géométrique du modèle des automates de dimension supérieure incite à des généralisations intéressantes telles les automates décrivant les systèmes temps réel et les systèmes probabilistes. Nous avons montré comment obtenir des sémantiques opérationnelles vraiment parallèles, temps réel (éventuellement continu) [Gou96]. Les constructions catégoriques permettent d'ailleurs de donner des lois pour le temps très raisonnables. Enfin les méthodes géométriques développées dans le cas sans temps se transportent aisément au cas avec temps.

2.2.3  Hiérarchie de modèles du vrai parallélisme

Pour comparer les nombreux autres modèles du vrai parallélisme, nous avons développé une nouvelle sémantique opérationnelle du calcul de processus CCS enrichie avec des étiquettes permettant d'encoder l'arbre de dérivation des transitions. Cette information permet de retrouver de nombreux modèles sémantiques classiques sans entrelacement comme la causalité. Nous avons montré que l'approximation de la semantique enrichie par la sémantique de causalité est une interprétation abstraite modélisée par une correspondance de Galois entre les deux modèles. Des définitions similaires devraient permettre de retrouver de nombreux modèles sémantiques présentés dans la littérature [BP97].

2.3  Interprétation abstraite

2.3.1  Fondements de l'interprétation abstraite

L'interprétation abstraite consiste à approcher des propriétés concrètes des programmes par des propriétés abstraites. Au cas où toute propriété concrète a une meilleure approximation dans le domaine de propriétés abstraites, la correspondance entre les propriétés concrètes et abstraites s'établit traditionnellement par une correspondance de Galois. Cette propriété est très puissante car la sémantique concrète et l'approximation définie par la correspondance de Galois définit entièrement la sémantique abstraite qui se déduit constructivement de la sémantique concrète sans avoir à faire de nouvelles approximations. Cette hypothèse est souvent forte quand une propriété concrète peut s'approcher par plusieurs propriétés abstraites sans pour autant qu'il y en ait une plus précise que les autres. Pour prendre un exemple simple, c'est le cas quand il s'agit de décrire un langage sous contexte par une grammaire algébrique. Nous avons étudié les correspondances possibles dans ce cas qu'elles soient basées sur une relation d'approximation, une fonction de concrétisation, une fonction d'abstraction, étudié les situations duales et leurs cas particuliers où interviennent les correspondances de Galois. Ceci conduit à définir des notions de complétude relatives à divers degrés d'abstraction [Cou95d].
Quand les propriétés d'un programme sont exprimées comme solutions d'un système d'équations sur un domaine sémantique infini, l'utilisation d'une correspondance de Galois et d'équations abstraites formalise l'idée de simplification des équations par approximations discrètes. Une autre façon traditionnelle de procéder pour résoudre les équations consiste à utiliser un élargissement/ rétrécissement (widening/narrowing) ce qui formalise l'idée de résolution itérative avec accélération de la convergence par extrapolation. Cette seconde méthode est souvent méconnue ou mal employée (par exemple en utilisant un domaine fini pour effectuer les élargissements). Nous avons montré qu'elle est plus puissante que l'utilisation d'une correspondance de Galois dans un domaine satisfaisant garantissant la terminaison des itérés (satisfaisant par exemple la condition de chaîne). Plus précisément une telle correspondance peut être trouvée pour chaque programme mais il n'en existe en général aucune permettant de trouver pour tous les programmes d'un langage de programmation les mêmes résultats d'analyse de programmes que ceux obtenus en utilisant les techniques élargissement/ rétrécissement dans un domaine abstrait infini. Ceci a été utilisé pour résoudre des problèmes de convergence laissés ouverts ou résolus grossièrement [CC95c].
Comme évoqué précédemment, les techniques d'analyse sémantique de programmes ont été principalement présentées sous forme de points fixes ou équationnelles. Depuis peu, la présentation sous forme de règles est plus courante. Nous avons introduit GąSOS, une généralisation de SOS pour décrire des comportements infinis [Cou95f] et montré que les présentations sous forme de point fixe, équationnelle, de contraintes, de conditions de fermeture, par un système formel à base de règles ou par un jeu sont équivalentes et conservées par approximation basée sur une correspondance de Galois [CC95a].

2.3.2  Domaines abstraits pour l'analyse sémantique de programmes

L'étude d'un domaine abstrait consiste à imaginer un modèle mathématique de propri\' etés de programmes. Pour être utilisable pour l'analyse automatique de programmes, il faut en concevoir une repésentation machine efficace et trouver des algorithmes performants donnant une version abstraite des opérations/fonctions élémentaires que l'on trouve dans la plupart des langages de programmation.

Utilisation des BDDs en interprétation abstraite

Il s'agit d'utiliser une représentation symbolique des fonctions booléennes pour construire des interprétations abstraites plus performantes quand les propriétés abstraites sont exprimées sous forme de propositions logiques. Les représentations utilisées sont les TDGs (Typed Decision Graphs), une variante des BDDs (Boolean Decision Diagrams) plus compacte. Les TDGs sont utilisés pour représenter aussi bien le domaine abstrait au cours de l'interprétation abstraite que les fonctions abstraites (qui servent à calculer la sémantique particulière d'un programme). Dans cette optique, nous avons donné une méthode générale pour étendre des représentations en TDG à des ordres supérieurs c'est-à-dire des représentations des fonctions sur les domaines de départ. Cette méthode peut permettre de trouver un codage des fonctions abstraites étant donné un codage des domaines abstraits. Il existe des fonctions pour lesquelles la représentation sous forme de TDG n'est pas compacte, ce qui peut consommer énormément d'espace mémoire, mais aussi de temps, car la plupart des opérations sur les TDGs dépendent de leur taille. La solution spécifique à l'interprétation abstraite est d'approximer ces fonctions par d'autres prenant moins de place. Cette approximation peut servir dans le cadre d'un opérateur d'élargissement dynamique si le domaine abstrait est codé, ou encore elle peut servir à approximer dès le départ les fonctions abstraites elles-mêmes, accélérant chaque itération. Comme exemple d'utilisation de ces différents procédés, on a codé l'analyse de nécessité, pour aboutir à un algorithme très performant, qui permet de trouver des résultats là où aucune analyse à la Mycroft exacte ne peut aboutir faute de place mémoire [Mau94].

Utilisation des langages formels, grammaires et contraintes ensemblistes en interprétation abstraite

Il existe une classe de méthodes d'analyse de programmes basées sur l'usage de grammaires (introduite par N. Jones et S. Muchnick) ou sur celui de contraintes ensemblistes introduite par N. Heinze pour laquelle on a longtemps cru qu'il s'agissait de méthodes radicalement différentes de celles utilisées en interprétation abstraite. N. Heinze n'affirme-t-il pas, page 18 de sa thèse, que : << The finitary nature of abstract interpretation implies that there is a fundamental limitation on the accuracy of this approach to program analysis. There are decidable kinds of analysis that cannot be computed using abstract interpretation (even with widening and narrowing). The set-based analysis considered in this thesis is one example >>. Au contraire, nous avons montré que ces analyses basées sur l'approximation de languages formels par des grammaires ou des contraintes ensemblistes sont bien des interprétations abstraites isomorphes, avec calcul itératif de point fixe pour lequel on peut utiliser un élargissement, un transformateur de grammaires/contraintes finitaire ou même comme le fait implicitement N. Heinze de manière encore plus simple, un domaine abstrait qui est fini pour chaque programme particulier [CC95c]. Cette nouvelle compréhension des analyses par grammaires ou contraintes a quelques avantages. En particulier le processus d'approximation est formalisé de manière rigoureuse et non plus expliqué en prenant quelques exemples. On met en évidence un domaine abstrait d'usage général qui peut être combiné avec d'autres domaines abstraites (polyhèdres, congruences linéaires, etc.) pour analyser les valeurs numériques voire exprimer des conditions de contexte. Enfin, on montre que quelques affirmations sur les mérites respectifs de ces méthodes d'analyse et de l'interprétation abstraite sont pour le moins non justifiées [CC95c].

Représentation des grammaires et contraintes ensemblistes en interprétation abstraite

Comme nous venons de le dire, une classe importante de méthodes d'analyse de programme est basée sur l'approximation de langages formels par des grammaires et/ou des contraintes ensemblistes. Malgré un usage largement répandu de ces objets, même en dehors du cadre de l'analyse de programmes, on ne sait pas manipuler efficacement les grammaires avec contraintes ensemblistes. Il s'agit de trouver de nouvelles représentations de tels objets, tout en développant des algorithmes de point fixe utilisant ces objets qui soient suffisamment efficaces pour être utilisables en pratique. L'utilisation d'approximations valides permet éventuellement de restreindre la taille des représentations au cours des calculs.
L'approche la plus générale du problème consiste à considérer ces grammaires comme des ensembles (presque) quelconques, éventuellement infinis, d'arbres éventuellement infinis. Pour que la représentation de ces arbres soit efficace, il faut d'une part qu'elle soit canonique (les tests d'égalités, très utilisés en recherche de point fixe doivent être rapides) et d'autre part compacte. Cela implique la recherche des cycles de l'arbre et leur repliage maximum. Une méthode a été développée qui permet de représenter des structures récursives selon leur pliage maximum, et cela au cours même de leur construction. Cette propriété est maintenue au cours des opérations récursives sur ces structures à un faible coût.
Une façon de représenter certains ensembles infinis d'arbres, et en particulier les grammaires, consiste à partager les branches d'arbres communes. On passe ainsi des ensembles aux relations. Or un arbre dont les feuilles sont des ensembles est une relation carrée, propriété qui ne se conserve pas lors des opérations d'union. Gérer directement des relations dans toute leur généralité, même en permettant des approximations, semble beaucoup trop complexe. Une approche semble donner un compromis acceptable : l'utilisation de la décomposition d'une relation en parties exactes. Une représentation des relations exactes a été mise au point dans le cadre des ensembles d'arbre. Elle permet facilement lorsque la relation devient trop complexe à gérer de l'approximer par au-dessus et par en-dessous par des relations plus simples. La décomposition en relations exactes n'étant pas unique, elle pose les problème de canonicité d'une part, et d'autre part de recherche de la décomposition optimale pour la représentation.
Un fois ces problèmes résolus, il faudra encore vérifier expérimentalement l'intérêt pratique de ces résultats jusqu'à présent entièrement théoriques.

2.4  Typage par interprétation abstraite

Traditionnellement, le typage est une phase conceptuelle distincte de la définition de la sémantique dynamique du langage. Un système d'inférence de types peut se décomposer globalement comme suit : tout d'abord une algèbre de types, ensuite un ensemble de règles logiques affectant un type à chaque expression du langage, enfin un algorithme de reconstruction des types calculant le type le plus général d'une expression quelconque. Classiquement cet algorithme est basé sur l'algorithme d'unification de Robinson. Nous avons développé une autre approche qui consiste à comprendre le typage statique comme une interprétation abstraite d'une sémantique avec typage dynamique, que cette sémantique soit opérationnelle [Mon94b] ou dénotationnelle [Cou97f].

2.4.1  Élargissements pour le typage

Ayant formulé les systèmes de type comme des interprétations abstraites [Mon94b], nous avons amélioré les algorithmes de typage classiques en utilisant les techniques d'élargissement de l'interprétation abstraite. Cette approche permet de relâcher les restrictions arbitraires des algorithmes classiques de typage comme la restriction monomorphe des constantes définies récursivement en ML. Pour illustrer le propos, considérons le système ML+ d'Alan Mycroft. Pour le système de types ML+, le problème d'inférence de types est indécidable. Dans le formalisme de l'interprétation abstraite, cela se traduit par un calcul du plus grand point fixe qui ne termine pas systématiquement [Cou97f,Mon94b]. La solution classique à ce type de problèmes en interprétation abstraite consiste à introduire un opérateur d'élargissement pour accélérer la convergence. Nous avons exhibé toute une famille d'opérateurs d'élargissement qui modélisent le comportement de systèmes d'inférences déjà existants comme ceux de ML ou de Miranda, ou qui améliorent de façon substantielle les systèmes de types basés sur l'algèbre d'Hindley/Milner [Mon94b].

2.4.2  Combinaison de l'analyse statique et du typage

Un deuxième axe de recherche a consisté à combiner l'analyse de types avec d'autres types d'analyse. La combinaison de notre analyse avec les interprétations abstraites d'ensemble de valeurs numériques nous a permis :
Comme les types sont définis comme des valeurs abstraites, il est possible d'utiliser les types afin de représenter d'autres propriétés que celles habituellement utilisées en typage. Ainsi, nous nous sommes intéressés aux propriétés de l'analyse par nécessité pour les fonctions d'ordre supérieur en utilisant les méthodes initialement conçues pour les systèmes de types [Mon95b]. En fait, l'algorithme d'inférence obtenu fonctionne de manière satisfaisante, les résultats obtenus étant meilleurs que ceux de Kuo et Mishra.

2.4.3  Construction d'une hiérarchie de types par interprétation abstraite

Un troisième axe de recherche consiste à unifier les différents systèmes de types. Nous avons montré que notre modèle général permettait de modéliser les systèmes de types d'ordre supérieur. Dans un premier temps, nous nous sommes attaqués au système F (introduit par Girard et Reynolds) et il nous a été possible de montrer que ce système est une interprétation abstraite de la sémantique opérationnelle [Mon95a].
Très récemment, nous avons réussi à reconstruire la hiérarchie des systèmes de types du cube de Barendregt (à l'exception du calcul des constructions). Dans un autre domaine, il a été possible de définir une présentation générale uniforme des systèmes de types avec contraintes. Plus généralement, ces derniers systèmes sont très utiles pour la définition des systèmes de types pour des langages objets, pusiqu'ils autorisent la prise en compte de dépendances dynamiques, ce que bien entendu les systèmes de types classiques ne sont pas en mesure d'appréhender. Un intérêt de la présentation par interprétation abstraite est de pouvoir exhiber les différentes restrictions syntaxiques qui ont été proposées par Fuh et Mishra, par Mitchell et par Henglein comme des opérateurs d'élargissement. En conlusion, nous montrons comment définir des opérateurs d'élargissement basés sur des critères sémantiques en lieu et place des critères syntaxiques, ce qui autorise la définition d'algorithmes de résolution de contraintes beaucoup moins grossiers.
L'intérêt théorique de ce résultat est d'avoir enfin une définition uniforme des systèmes de types du premier ordre et des systèmes de types d'ordre supérieur. Il permet de rompre la distinction entre typage ad hoc et typage paramétrique et permet de :
L'intérêt pratique de ce résultat est qu'il permet, grâce à une formalisation claire de l'abstraction, de définir des approximations décidables (c'est-à-dire non seulement l'algorithme termine mais trouve la solution de manière efficace) des systèmes de types d'ordre supérieur à l'aide des opérateurs d'élargissement. Des expérimentations sont en cours afin de déterminer les performances respectives des divers opérateurs actuellement étudiés pour le système F.

2.5  Sémantiques abstraites

Une sémantique concrète décrit les comportements possibles d'un programme. Une sémantique abstraite fait de même en considérant des propriétés approchées du contrôle de l'exécution. Cette sémantique est généralement paramétrée par un domaine abstrait formalisant les propriétés considérées pour les objets manipulés par le programme.

2.5.1  Analyse sémantique de programmes fonctionnels d'ordre supérieur par interprétation abstraite

L'analyse de nécessité (strictness analysis) est traditionnellement basée sur une sémantique dénotationnelle dans laquelle les propriétés des fonctions f D1« D2 s'expriment par un élément de (D1)«(D2). Cette approche ne permet pas de rendre compte de nombreuses autres méthodes d'analyse (par exemple l'analyse de projection de J. Hughes et P. Wadler) comme étant des interprétations abstraites. Une première raison est que certaines propriétés (comme l'absence traduisant la non-utilisation d'un paramètre) ne s'expriment pas comme un élément de (D1)«(D2) mais plutôt comme un élément de (D1« D2). Une seconde raison vient du fait que les sémantiques dénotationnelles correspondent à des approximations où des informations essentielles sur le déroulement des calculs sont perdus, ce qui n'est pas le cas des sémantiques relationnelles [CC94a] et opérationnelles étendues à des comportements infinis [Cou95f]. Pour traiter ces problèmes nous avons généralisé l'approche des correspondances de Galois aux interprétations abstraites d'ordre supérieur en distinguant ordre partiel d'approximation et pré-ordre de calcul [CC94c].

2.5.2  Analyse de comportement par interprétation abstraite

L'analyse de comportement, introduite dans [CC94c], combine les analyses de programmes fonctionnels ne dépendant pas des valeurs manipulées par le programme. Ceci recouvre l'analyse de nécessité, l'analyse de terminaison à la Mycroft, l'analyse de projection (J. Hughes et P. Wadler), l'analyse d'équivalence partiel (PER analysis de S. Hunt), l'analyse de temps de liaison (binding time analysis), etc. Ce type d'analyse est utilisé pour la compilation de langages paresseux (pour transformer des appels par nécessité/par nom par des appels par valeurs qui sont nettement plus efficaces) et l'évaluation partielle (pour effectuer des calculs dès la compilation).
Un problème récurrent de länalyse de nécessité est celui de l'efficacité. Comme exemple d'utilisation des TDGs, nous avons codé l'analyse de nécessité, pour aboutir à un algorithme très performant, qui permet de trouver des résultats là où aucune analyse à la Mycroft exacte ne peut aboutir faute de place mémoire [Mau94].
L'analyse de nécessité traditionnelle comme ci-dessus est basée sur des domaines booléens simples pour lesquels les ordres abstraits d'approximation et de calcul coïncident. Ce n'est pas le cas pour les analyses de comportement [CC94c] dans laquelle on sépare les éléments statiques (pour lesquelles la terminaison est certaine) des éléments dynamiques (pour lesquels la non-terminaison est possible). La situation est alors compliquée par le fait qu'un pré-ordre de calcul conduit à un ensemble de solutions abstraites possibles dont il s'agit d'extraire les plus précises.
Pour étudier ce phénomène, nous avons étudié la combinaison de l'analyse de nécessité (strictness analysis) et des temps de liaison (binding time analysis) [V\'94,V\'95] pour un petit langage fonctionnel paresseux. Cette combinaison permet de trouver des résultats significatifs alors qu'elles échoueraient séparement. Le produit précision × vitesse d'analyse est à l'avantage de l'analyse combinée : le treillis abstrait est beaucoup plus grand que la somme disjointe des deux treillis utilisés pour l'analyse de nécessité et des temps de liaison, et les premières itérations de ces deux analyses sont communes. L'usage de correspondances de Galois relatives à une sémantique opérationnelle permet de caractériser exactement la perte d'information dans l'analyse.
Il est facile d'intégrer des analyses abstraites inférant des propriétés de la logique du premier ordre (pour exprimer terminaison sure, la non-terminaison sure, la dependance par rapport à des variables dont nous ne savions rien, etc.). Le fait de mettre la non-terminaison au même niveau que la terminaison dans le treillis abstrait nous empêche d'abstraire directement une fonction définie récursivement (donc par un plus petit point fixe pour un ordre où non-terminaison \sqsubseteq terminaison). Ce problème a été résolu en définissant des itérations abstraites qui contiennent toujours l'abstraction des itérations concrètes de notre fonction (du moins pour un nombre fini d'itérations). Le passage à la limite se justifie par le fait que nous inférons des propriètés de la logique du premier ordre, et qu'ainsi il existe un sous-modèle fini sur lequel les itérés abstraits sont également valables.
Ensuite, ce travail a été élargi de manière à pouvoir énoncer des propriétés générales concernant le comportement d'un programme, et en particulier celui de ses fonctions (terminaison, valeur, structures de données, types). Le langage initial a été élargi à l'ordre supérieur pour des structures de données arbitraires, avec la possibilité de distinguer des structures arbitrairement grandes, mais finies, des structures infinies. Cela a nécessité l'introduction de preuves de terminaison totales dans le cadre de l'interprétation abstraite, et l'introduction d'une fonction d'abstraction correspondant à la preuve du théorème de Tarski.
L'analyse doit maintenant être généralisé de manière à pouvoir traiter des langages de programmation réels : en pratique, cela consiste à donner le comportement d'un programme impératif avec tous les effets de bords qu'il est susceptible de générer. L'intérêt serait d'analyser des programmes écrits dans un petit langage orienté-objet. Les propriétés dégagées peuvent servir soit au compilateur, soit être délivrées en l'état au programmeur, ce qui lui fournit un metteur au point abstrait.

2.5.3  Analyse sémantique de programmes logiques par interprétation abstraite

Ce travail est basé sur une sémantique opérationnelle des petits pas de programmes Prolog (résolution SLD). Les principales contributions concernent l'usage de domaines abstraits infinis (les analyses classiques utilisent des treillis finis), en particulier des langages formels, grammaires et contraintes ensemblistes [Cou95g] et la combinaison des analyses descendantes et ascendantes (les analyses classiques utilisent l'une ou l'autre mais pas les deux) [Cou95c].

2.5.4  Analyse sémantique de programmes parallèles par interprétation abstraite

Certaines analyses fines de programmes parallèles comme l'exclusion mutuelle ou l'indépendance et la validation de propriétés liées à la géométrie des systèmes de transitions (blocages, branchements, etc.) requièrent l'usage de sémantiques qui décrivent véritablement le parallélisme entre processus concurrents à l'aide d'automates munis de transitions de dimension supérieure. Ces automates nous permettent de définir des sémantique approchées, calculables par interprétation abstraite en vue de l'analyse statique des programmes parallèles considérés. Cela a été réalisé pour différents types de langages (Linda, Parallel Pascal, CML) et une propriété de correction sémantique de l'interprétation abstraite a été prouvée. Deux techniques différentes permettent d'atteindre cet objectif :
Une caractérisation des interprétations abstraites entre deux automates de dimension supérieure a été donnée en terme d'adjonctions. La troncation est une adjonction qui permet de modéliser la sémantique d'un pool de n processeurs qui entrent en compétition afin d'exécuter un programme. Les repliements d'états permettent de simplifier les configurations abstraites et de rendre la sémantique approchée calculable statiquement.
L'implantation d'un analyseur de Parallel Pascal basé sur une telle sémantique a été efféctuée et est disponible sur le serveur WEB du DMI. Certaines techniques d'implémentation comme l'utilisation de transitions d'un grain plus grossier que dans les définitions sémantiques (Virtual Coarsening) permettent l'interprétation abstraite précise de programmes de taille raisonnable car elles diminuent fortement (au moins d'un facteur 4) le nombre d'états à considérer. Pour des algorithmes classiques d'exclusion mutuelle comme ceux de Dekker ou de Peterson, la preuve d'invariance est ainsi réalisée par l'interprète abstrait en quelques secondes de calcul. L'automate abstrait qui en résulte compte un millier d'états alors que le nombre d'états réels de ce programme est de l'ordre de cent mille. On gagne donc un facteur 100 sur la vérification de la propriété d'exclusion mutuelle dans cet exemple significatif [Cri96a].
D'autres programmes (avec des sémaphores par exemple) ont été analysés avec succès. L'analyseur adjoint au source du programme des invariants calculés à chaque point de contrôle. Il produit aussi l'automate qu'on peut visualiser ou bien fournir comme input à une deuxième passe d'analyse.

2.5.5  Combinaison de l'interprétation abstraite et du model-checking

La vérification de modèle (model-checking) est une technique séduisante puisque, contrairement à l'interprétation abstraite, elle fournit des résultats exacts. Malheureusement, et contrairement à l'interprétation abstraite, elle n'aboutit pas toujours, faute de temps, d'espace mémoire ou parce qu'il faut explorer exhaustivement un espace d'états infini. La vérification de modèle de modèle et l'analyse de programme par interprétation abstraite apparaissent donc comme complémentaires. Nous avons montré comment les combiner dans un calcul parallèle [CC97b], l'analyse du système, convenablement conduite en parallèle avec la vérification du modèle permettant de réduire l'espace des états devant être effectivement explorés. Dans cette combinaison l'analyse est approchée et le model-checking est exact de sorte que la terminaison n'est toujours pas assurée. Une autre approche, celle du model-checking abstrait est également explorée, pour garantir la terminaison au prix d'une perte de précision.

2.5.6  Logique temporelle et model-checking abstrait

L'idée du model-checking abstrait est de valider les formules de logique modale qui caractérisent certaines propriétés comme les blocages (deadlocks), l'équité ou l'exclusion mutuelle sur les systèmes de transitions approchés obtenus par interprétation abstraite, et d'en tirer une information sur la sémantique concrète. En effet, contrairement au model-checking traditionnel, le système de transitions d'un programme n'est pas calculable en général [Cri95,Cri96b].
On peut quand même tirer parti du fait qu'il existe d'excellents algorithmes de model-checking sur les automates. La difficulté principale est de réussir à transférer la validité d'une formule de logique temporelle suffisamment expressive de la sémantique abstraite vers la sémantique standard. Ce résultat a été obtenu pour le m-calcul complet grâce à une interprétation abstraite qui allie à la fois une approximation supérieure et une approximation inférieure des états concrets.
Un évaluateur de formules logiques du m-calcul est en ce moment testé en sortie de l'interprète abstrait pour réaliser un outil plus général d'analyse de programmes parallèles.

2.5.7  Ordonnancement de programmes parallèles

Dans le modèle des automates de dimension supérieure, on a la possibilité de distinguer de façon très fine les ordonnanceurs possibles d'un programme parallèle tournant sur une machine contrainte (nombre de processeurs limité, topologie de communication imposée, exclusion mutuelle obligatoire pour certains objets). Toutes ces conditions contraignent les exécutions possibles et on peut donner des critères géométriques (homotopie) pour déterminer s'il y en a encore (spécification/vérification) et même pour déterminer les meilleures possibles. A contrario, on peut aussi essayer de paralléliser au maximum un programme séquentiel afin d'occuper au maximum un type de machine donné. Ces deux problèmes se posent en des termes géométriques similaires, et sont naturellement exposés dans le cadre de l'interprétation abstraite [Gou95c].
Nous avons commencé à nous intéresser aux applications des sémantiques du vrai parallèlisme par automates de dimensions supérieures aux protocoles de systèmes distribués tolérants aux pannes. Un premier travail a permis de lier les considérations géométriques des automates de dimension supérieure à celles de M. Herlihy, N. Shavit et S. Rajsbaum concernant les systèmes distribués t-résilients (résistants à t pannes). Cela a permis de prouver à nouveau de façon sémantique un résultat de calculabilité sur les systèmes t-résilients à mémoire partagée (avec lecture et écriture atomique). Cette nouvelle vision des choses a rendu possible l'amélioration de l'algorithme d'Herlihy pour la génération automatique de protocoles sans attente [Gou97b], ainsi que la généralisation à d'autres systèmes (avec test & set etc.).

2.5.8  Analyse de programmes parallèles stochastiques

Nous avons étendu le p-calcul par des informations stochastiques qui donnent un modèle uniforme avec lequel il est possible d'étudier des propriétés qualitatives (comportements) et quantitatice (performances) des systèmes parallèles et distribués. À titre d'analyse de cas, nous avons étudié les procédures de transmission dans les réseaux de téléphonie mobile [Pri97].

2.5.9  Analyse sémantique de langages orientés objets par interprétation abstraite

L'objet de cette recherche, commencée récemment, est de définir un cadre sémantique pour l'interprétation abstraite des langages orientés objets. Les applications envisagées concernent le typage, l'optimisation dans les compilateurs (par exemple pour transformer des appels à des fonctions virtuelles en appels statiques) et la mise au point abstraite (où les valeurs utilisées pour la mise au point interactive sont abstraites c'est-à-dire à des ensembles de valeurs concrètes qu'il faudrait considérer individuellement dans les approches classiques).

2.6  Perspectives

Les perspectives doivent être situées dans le contexte fixé par le DMI. La croissance des surfaces occupées et du nombre de chercheurs est nulle, ce qui pose à la fois le problème de masse critique et d'accueil des post-doctorants (programme européen CHM), années sabbatiques, etc. L'équipe est largement constituée de jeunes chercheurs thésards dont le renouvellement est rapide et qui quittent l'équipe quand ils atteignent leur maturité scientifique. En dehors du responsable, il n'y a pas de chercheurs confirmés et d'ingénieurs de recherche affectés à des projets scientifiques à moyen terme, ce qui limite considérablement les possibilités de développements pratiques et du suivi de ces développements. La durée de vie de l'équipe, comme toutes celles du DMI, est limitée dans le temps, etc. Ces conditions de travail nous placent dans une position de relative faiblesse par rapport à nos partenaires et concurrents européens.
Malgré ces conditions difficiles, l'objectif essentiel est de fournir un excellent cadre de travail aux jeunes thésards. Nos atouts sont la qualité des chercheurs, des thèmes de recherche, des indispensables partenaires extérieurs et de l'animation scientifique que crèent le séminaire et les visiteurs extérieurs.
En ce qui concerne nos idées sur la sémantique et l'interprétation abstraite, elles se répandent doucement mais sûrement, notamment au travers d'écoles pour jeunes chercheurs : Le succès peut également se mesurer aux nombreuses conférences invitées1 dans des congrès ICCL'94 [Cou94], GULP-PRODE'95 [Cou95d], CAV'95 [Cou95a], POPL'97 [Cou97f], MFPS XIII [Cou97c], SAS'97 ou réunions thématiques (workshops) WAILL'95 [Cou95c], 4th Compulog [Cou95g], Venice workshop'95 [Cou96d], F.N.R.S. meeting [Cou97e].
Un certain nombre d'éléments prospectifs ont déjà été évoqués dans le compte-rendu du travail des quatre dernières années. Nous comptons nous concentrer sur quelques thèmes, comme par exemple :

Part 3
Eléments d'appréciation de l'activité du laboratoire


Chapter 3
Collaborations

Chapter 4
Missions, conférences et séminaires