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

De Ensiwiki
Révision de 9 mai 2015 à 11:55 par Delanaur (discussion | contributions) (Analyse structurelles de systèmes)

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. Il faut alors 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. Pour ne pas se mettre de contraintes à la modélisation, on utilise en général des buffers non bornés (de taille infinie, donc), mais qui nécessitent donc potentiellement un espace d'états infini pour représenter tous les états possibles du système. Et il y a un problè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. Certaines vérifications formelles permettent par exemple de vérifier synchronisabilité d'un système, c'est-à-dire s'il 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éfinition. S'il n'est pas synchronisable, on peut par exemple chercher d'autres "fragments" de systèmes décidables, ce qui a amené à cette propriété de stabilité dont je vais parler.


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é d'un système, 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, et également pour des buffers non bornés en taille. 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

Les bornes de buffers testées ne sont pas choisies aléatoirement ou linéairement. En général, elles consistent en des heuristiques pour établir une borne de départ (exemples : prendre la plus longue séquence d'émissions, ou le nombre maximum d'émissions destinées au même pair), puis en l'utilisation d'algorithmes de recherche pour trouver la borne à partir de laquelle il y a stabilité. Ces algorithmes de recherche (en général, une recherche dichotomique, ou une simple incrémentation/décrémentation) ont des efficacités variables selon les systèmes traités, mais il arrive que certains durent plusieurs dizaines de minutes avant de donner une borne, voire tournent finalement plus d'une heure sans résultat (et dans ces cas-là, on ne peut rien conclure sur la stabilité). Il faudrait alors trouver un moyen d'optimiser ce calcul de bornes.

Performances

Le calcul de stabilité est très long, car composé de 2 phases très coûteuses réalisés par des outils externes maintenus par l'équipe. Il s'agit de calculs de produits d'automates itératifs, réalisés en boucle et sans optimisations, ainsi que de tests d'équivalence entre ces automates complexes (il faut imaginer plusieurs centaines d'états et de transitions). Il est difficile d'influer sur le calcul car les opérations hors-CADP sont peu coûteuses, et les outils externes n'ont rien à voir avec le script du projet en lui-même, et il est donc compliqué de toucher précisément aux calculs faits par les outils. Il faudrait s'immerger dans le code propre des outils et recoder ces opérations complexes, ce qui est impossible à réécrire de zéro et plus simplement dans le cadre de l'IRL.


Analyse structurelles de systèmes

Certains systèmes sont structurellement stables ou instables ; c'est-à-dire que l'on 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

Le système calcule une borne "minimale" pour le système complet ; c'est-à-dire que la même borne sera appliquée à chaque pair du système. Mais pourquoi chaque pair aurait-il besoin de la même taille de buffer ? Il est possible qu'il ait besoin de bien moins de place, et qu'une optimisation soit possible à ce niveau, puisqu'avec une borne exacte calculée pour chaque pair, le calcul itératif sera plus rapide, et les automates calculés seront plus petits. Toutefois, cela ajouterait potentiellement un surcoût au calcul des bornes, et rendrait finalement le calcul plus long de façon globale ; l'idée est bonne en théorie, mais n'améliore pas trop le calcul en pratique.


Contributions 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

Le principe est simple : mettre en place une série de fonctions par lesquelles va passer le programme avant d'exécuter les calculs de bornes et les tests d'équivalence chronophages, pour voir s'il n'est pas possible de dire quelque chose sur la stabilité d'un système avant de passer par des vérifications formelles plus poussées. Pour cela, il faut simplement trouver comment réaliser ce pré-traitement, comment le mettre en place, et en faire une implémentation efficace.

[schéma des étapes avec insertion de mon emplacement]


Détection de dépendances de cycles

En s'inspirant de ce qui a été vu dans les études d'analyses structurelles, il existe plusieurs formes simples (progressivement plus poussées) d'automates qu'il est possible de détecter, et de traiter. Plusieurs de ces structures simples ont pu être dégagées au cours du projet

  • Systèmes séquentiels
  • Systèmes à cycle unique :
    • Cycle d'émissions :
    • Autre type de cycle :
  • Systèmes à cycles indépendants
  • Systèmes à cycles dépendants (et cycle au démarrage) :
    • Avec même séquences de messages
    • A alphabet complémentaire
    • Cycles simples séparés par des séquences


Perspectives et cas restants

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 pratiques 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, CADP, 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 ...

- Cycles uniques -> Cycle d'émission : instable -> sinon : stable

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

- Détection de cycles dépendants /!\ en début de graphe -> à même séquence de messages -> à alphabet complémentaires -> séparés par des séquences (avec fin par un cycle ou un séquence)

...


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.


Résultats

- Statistiques - Coût : linéaire - Observations


Conclusion et futurs travaux

Le travail ayant surtout une portée théorique, une bonne partie du travail a été formelle, 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 ; mais des avancées techniques ont pu être faites également.

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.


- 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, W. SERWE, "CADP 2011: a toolbox for the construction and analysis of distributed processes", STTT 15(2), 2013.