8 octobre 2018

Emmanuel Haucourt (LIX - Ecole Polytechnique) 

Un programme concurrent est constitué de plusieurs processus
séquentiels qui s'exécutent simultanément et partagent des ressources.
Pour un processus séquentiel standard, le graphe de flot de contrôle
(GFC) est une sur-approximation classique (et omniprésente dans les
compilateurs et analyseurs statiques) de l'ensemble des traces
d'exécutions du programme. La propriété cruciale du graphe de flot de
contrôle est sa finitude. Définir l'équivalent de cette structure pour
les programmes concurrents n'a rien d'évident. La solution que l'on
propose est basée sur la notion d'espace partiellement ordonné. À chaque
GFC on associe sa réalisation géométrique dirigée, qui consiste à
remplacer chaque flèche du GFC par une copie du segment unité [0,1]
joignant la source de la flèche à son but. Un programme parallèle
constitué des processus séquentiels P_1,...,P_n sera alors représenté
par un sous-espace du produit cartésien E = G_1 x ... x G_n où G_i est
la réalisation du GFC's du i-ème processus. En effet, sous l'hypothèse
que le programme considéré est conservatif, on peut définir une fonction
de potentiel qui associe à chaque point de E la quantité de ressources
nécessaire au fonctionnement du programme en ce point. Si cette quantité
dépasse la quantité de ressources disponible, alors le point est
«interdit». L'ensemble des points interdits forme une sous partie de E
dont le complémentaire M est le modèle géométrique du programme. 
On a les résultats suivants:
1) les chemins (continus) dirigés sur M forment une sur-approximation de
l'ensemble des traces d'exécutions du programme
2) chaque chemin f possède un voisinage V dont tous les éléments g (qui
sont eux-mêmes des chemins dirigés sur M) son équivalent à f au sens où
l'état de la mémoire
de la machine abstraite à la fin de l'exécution de g ne dépend pas de g
3) l'ensemble des traces d'exécution forment un ouvert de l'espace des
chemins dirigés sur M
4) les modèles géométriques appartiennent à une classe d'objets qui
satisfait une propriété de décomposition unique vis-à-vis du produit
cartésien. À partir de la décomposition du modèle géométrique d'un
programme, on peut regrouper ses processus de manière à obtenir des
sous-programmes indépendants.

Les constructions et résultats annoncés ci-dessus seront illustrés de
nombreux exemples. :-)