Remy Delanaux (avec Gwen Salaun) : Stabilité des systèmes communicants

De Ensiwiki
Aller à : navigation, rechercher
Cornues.png
Titre du projet Stabilité des systèmes communicants
Cadre IRL

Labo INRIA, LIG
Équipe CONVECS
Encadrants Gwen SALAÜN et Lakhdar AKROUN


Introduction

Les systèmes communicants

De très nombreux systèmes et programmes informatiques répartis peuvent être modélisés et fonctionnent comme des systèmes communicants, c'est à dire par des messages qui transitent via des canaux de communication, en particulier par une succession d'envois et de réceptions de ces messages. On peut citer par exemple des architectures Web Client/Serveur : le client va envoyer un message au serveur, et en attendre sa réponse. Mais aussi par exemple le fonctionnement d'une gare, d'un système de réservation de billets, ou même d'un distributeur de boissons... Dans tous les cas, on peut formaliser ce système communicant par des systèmes de transitions labellisés (abrégé en LTS, pour Labeled Transition System), représentant chacun une brique fonctionnelle du système, et où les différents états du système servent de nœuds, et les transitions représentent les échanges de messages (avec un symbolisme différent selon la nature du message : par convention, le nom du message est par exemple suivi d'un "!" si il s'agit d'une envoi, et d'un "?" s'il s'agit d'une réception). Chaque LTS du système étudié est appelé un "pair" (parfois remplacé par son original anglais, peer).


Exemple de système modélisé par des LTS
Exemple de système modélisé par des LTS

Systèmes asynchrones : entre buffers et stabilité

Les systèmes communicants peuvent fonctionner de façon synchrone (imaginez une discussion au téléphone : les 2 interlocuteurs sont au téléphone en même temps, l'appelant doit attendre une réponse de l'appelé pour réaliser l'appel) ou asynchrone (un échange de mail par exemple ; les envois et réceptions peuvent être détachés dans le temps). Dans notre cas, tous les systèmes sont considérés asynchrones au départ, et certaines vérifications formelles permettent de vérifier sa synchronisabilité, c'est-à-dire si le système se comporte de la même façon pour toutes les bornes de buffers possibles, commençant à 1 [1] : le cas échéant, le traitement en est simple, puisque si le système est synchronisable, on peut étudier sa version synchrone, forcément stable d'après sa définiton.

Dans le cas contraire, il faut bien pouvoir conserver les messages envoyés mais pas encore reçus par le destinataire : cela se fait dans des buffers, modélisés par une FIFO. Si le système est cyclique, il peut y avoir besoin de buffers infinis, donc d'un espace d'états infini pour représenter tous les états possibles du système. Pire encore : savoir si un système se comporte "correctement" (pas d'interblocage, par exemple) est indécidable [2].

On peut toutefois utiliser des techniques de vérification formelles utilisées pour les systèmes finis, en cherchant des sous-classes de systèmes infinis analysables, car possédant d'autres propriétés.


Résultats à exploiter

Le point de départ du sujet vient d'un résultat récent de l'équipe CONVECS [3] définissant la notion de stabilité présentée ci-dessus, et montrant que si un système est stable à partir d'une certaine borne spécifique de taille de buffer, alors il reste stable pour toutes les bornes supérieures. Ainsi, une fois cette borne trouvée, on peut étudier plus facilement le comportement de systèmes, puisqu'il suffit d'analyser les propriétés du système à cette borne (si elle existe), et on peut affirmer ensuite que ces propriétés restent valides à des valeurs de bornes de buffers supérieures.

Il s'agit maintenant de voir quelles améliorations sont possibles à tous les niveaux pour détecter cette propriété de stabilité.


Analyse de problèmes ouverts

La stabilité étant actuellement plutôt coûteuse à montrer (d'autant qu'elle n'est pas toujours décidable), on cherche à trouver sur quels paramètres influer pour pouvoir répondre plus vite à cette question de stabilité d'un système. Voici les pistes que l'équipe et moi avons exploré pour cela.

Calcul des bornes de buffers

- Vérifications d'équivalence : couteux

Performances

- Amélioration du code ? - Difficile d'influer, vu que vient globalement des tests d'équivalence, venant d'une boite à outils externe

Analyse structurelles de systèmes

Certains systèmes sont structurellement stables ou instables ; c'est-à-dire que l'ont sait dire, de par leur forme, s'il existera ou non une borne de stabilité qu'on pourra trouver par vérification formelle ensuite. Ces systèmes sont le plus souvent très simples, mais ils permettent d'éliminer a priori, par un pré-traitement, toute une famille de systèmes qu'on aurait à traiter.

Uniformité des bornes

- ?


Réflexions théoriques et formelles

Une fois ces pistes explorées, il a fallu décider sur quel aspect le travail allait s'orienter : le choix a été fait assez rapidement, en se dirigeant vers la réflexion et l'implémentation d'un pré-traitement pour détection de stabilité (ou de non-stabilité), et accélérer ainsi le temps de traitement en utilisant des algorithmes d'analyse structurelle. Cette approche présente moins de blocages et de besoins théoriques, et reste tout aussi utile à l'analyse de systèmes existants, notamment pour des travaux futurs.


Comprendre le problème

- Prétraitement : principe - Quoi mettre en place, et pour quoi

Détection de dépendances de cycles

- cf. Analyse structurelle - séquences - cycles d'émission - cycles indépendants - ...


Limites de l'approche

Une fois les structures simples éliminées des systèmes à traiter, on se rend vite compte que la complexité de ceux-ci augmente rapidement : le plus souvent, ces LTS présentent des cycles complexes, imbriqués, interdépendants, et sans propriété particulière (mélange d'émissions et de réceptions, ...). Si l'on devait continuer la méthode de la même façon qu'auparavant, on arrivait rapidement à devoir faire un nouvel algorithme (ou une nouvelle partie d'algorithme) pour chaque type de système envisagé, car il n'est pas simple de rendre générique des algorithmes poussés sur la détection de certains types de cycles.



Réalisations et résultats

Reprise du code existant

Un des principaux aspects du projet était de reprendre comme base un code déjà existant, consistant en un fichier unique, conséquent, écrit en Python, et interagissant avec une "boite à outils" externe, développée et maintenue par l'INRIA depuis plusieurs années[2], et qui permet d'effectuer des opérations sur les systèmes communicants décrits par un format précis (dans un langage de haut niveau, simple à écrire, qui est ensuite parsé par ces outils).

Le code étant déjà conséquent (2000+ lignes), et étant amené à se développer, j'ai eu pour tâche de réaliser un nettoyage et un refactoring du code, pour améliorer la lisibilité et l'organisation du code. La gestion des classes étant plutôt simple en Python objet, la tâche n'était pas nécessairement complexe, mais elle a nécessité de reparcourir tout le code pour en tirer la sémantique et les contextes d'utilisation de chaque fonction, pour savoir où la placer dans la chaîne d'exécution. Ainsi, à partir d'un simple fichier "async.py", la structure est devenue comme suit :


[image/schéma de la structure et des intégrations]


Un des soucis potentiels de cette tâche est que certaines fonctions étaient codées sans être utilisées, simplement par anticipation (théorique) des étapes qui allaient suivre. Et, n'étant pas dans la tête des anciens codeurs, il n'était pas forcément aisé de savoir si la fonction allait être à re-coder ou non, car une simple description de la fonction et de ce qu'elle fait n'indique pas toujours son utilisation exacte.


Algorithmes et tests

L'autre aspect qui s'est avéré être le cœur de mon activité pendant ce module IRL, était la réflexion concernant des algorithmes de détections de structures sur les systèmes asynchrones, puis leur implémentation et leur test en Python dans les scripts du projet. J'ai pu implémenter certains de ces algorithmes, qui sont assez similaires mais ont chaque fois un traitement un peu différent.

- Détection de séquences ...

- Détection de cycles non indépendants ...

- Détection de cycles dépendants ...

- Détection de cycle en début de graphe ... ...


Il est à noter que même si ces algorithmes sont très similaires, ils ont été implémentés dans des fonctions séparés, pour faciliter à la fois la mise en place et la validation des fonctions. Pour des développements futurs, il sera sans doute possible de factoriser des parties de ces algorithmes, mais toutefois ce dédoublement de morceaux de fonctions n'a que peu d'implications sur l'exécution, car le traitement se fait de toute manière rapidement (surtout comparé aux tests formels éventuels après ce pré-traitement).

Pour valider ces algorithmes, j'avais à ma disposition plusieurs centaines de LTS décrits dans le format de haut niveau cité plus haut, plus ou moins complexes, et modélisant parfois des systèmes réels ; j'ai pu par ailleurs développer mes propres exemples en me basant sur ceux qui étaient déjà présents : le schéma est simple, il y a un fichier par "pair" du système, et chaque ligne (excepté la première, qui indique le nombre total de sommets et de transitions) indique une transition, à la fois sa source, sa destination, et le message qu'elle porte. Pour tester rapidement les fonctions de traitement, j'ai par ailleurs écrit un script en en Bash, testant le pré-traitement sur tous les exemples disponibles, et classant les résultats pour associer une quantité à chaque type de système détecté. C'était une manière simple et évolutive d'évaluer mes algorithmes, avec possibilité de vérifier à la main si les données sont correctes après coup.


Observations

Le travail ayant surtout une portée théorique, et n'attendant pas particulièrement de résultat concrets, ce que j'ai pu obtenir de ces implémentations n'est pas forcément concret, mais a permis d'y voir plus clair sur les éventuelles directions à prendre concernant à la fois le comportement de systèmes asychrones, et l'analyse structurelle de ceux-ci.

Notamment, en étudiant la proportion de systèmes éliminés sur cette panoplie de systèmes classiques/réels, on a pu remarquer que beaucoup de systèmes sont en fait très complexes (même si en apparence ils n'en ont pas l'air), et difficile à classer structurellement par des algorithmes simples.

Par conséquent, il devient difficile de jouer sur l'efficacité de la vérification de stabilité si même un pré-traitement n'arrive pas à éliminer la majorité des cas. Toutefois, il permet d'éviter une vérification couteuse en temps dans une partie non-négligeable des systèmes existants, qui sont certes les plus simples, mais qui sont aussi visibles dans le monde réel.


Futurs travaux ?

- Autres études théoriques - Algorithmes plus génériques


Références

[1] S. BASU, T. BULTAN, M. OUEDERNI, "Deciding Choreography Realizability", POPL 2012.

[2] D. BRAND, P. ZAFIROPOULO, "On Communicating Finite-State Machines", J.ACM, 1983.

[3] G. SALAÜN, L. YE, "Stability of Asynchronously Communicating Systems", 2014.

[4] H. GARAVEL, F. LANG, R. MATEESCU (Inria Grenoble), "Compositional verification of asynchronous concurrent systems using CADP", Acta Informatica, 2015.