Voir la source de Remy Delanaux (avec Gwen Salaun) : Stabilité des systèmes communicants

{{Projet IRL étudiant
 |titre= Stabilité des systèmes communicants
 |encadrants=[mailto:gwen.salaun@inria.fr,lakhdar.akroun@inria.fr Gwen SALAÜN et Lakhdar AKROUN]
 |labo=INRIA, LIG
 |equipe=CONVECS
}}

Rapport : [[Fichier:Rapport_DELANAUX_IRL_2015.pdf]]

Slides de soutenance : [[Fichier:Slides_IRL_Delanaux.pdf]]


= 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'').


[[Fichier:exemple_lts_client_serveur.png|vignette|alt=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, dans un conteneur global (appelé CADP). 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. 

[[Fichier:Methodologie_generale.png|center|alt=Méthodologie générale de vérification de stabilité|Méthodologie générale de vérification de stabilité]]

Dans ce schéma décrivant la méthodologie générale de vérification de la stabilité d'un système, mon pré-traitement se trouve entre la vérification de synchronisabilité et les premiers calculs heuristiques de borne de départ.

== 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 : ils sont stables, car finis, par définition.

*Systèmes à cycle unique : si le cycle n'est pas un cycle entièrement composé d'émissions, ces systèmes sont stables également (que ce soit parce qu'un seul pair est cyclique, ou que chacun contient un cycle, par exemple). En effet, un cycle d'émissions cause l'instabilité car les produits d'automates deviendront toujours plus gros.

*Systèmes à cycles indépendants : Si les pairs d'un système contiennent plusieurs cycles avec aucun message en commun, alors le système est stable. Il s'agit en gros d'une extension du cas des systèmes à un cycle, mais plus compressé.

*Systèmes à cycles dépendants : par souci de simplicité, on ne considère alors plus que les systèmes '''démarrant par un cycle''' (pour chaque pair). 
**Avec même séquences de messages : la tâche se complique si les cycles sont interdépendants (alphabets des messages non disjoints). Toutefois, si les cycles ont exactement la même séquence de messages, le système est stable : il se comporte en fait de façon synchrone, comme vu auparavant.
**A alphabet complémentaire : si les messages sont complémentaires, c'est-à-dire qu'après analyse des cycles initiaux, il y a autant de réceptions que d'émissions pour chaque message, ou plus de réceptions (une "tendance" à la réception forcera la stabilité, alors que les émissions forceront les produits d'automates à grossir), alors le système est stable.
**Cycles simples séparés par des séquences : le dernier cas étudié, qui n'a pas été complètement résolu. Si le système se termine par une séquence, alors le système est stable. Toutefois, s'il finit par un cycle, il faut étudier le comportement de celui-ci, et ceci ne marche plus pour un système complexe.

== 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 le montre la figure ci-contre.


[[Fichier:structure_code.png]]


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 : on parcourt les transitions de chaque pair jusqu'à retomber sur un état déjà atteint par une transition. Si cela ne se produit pas, le système est séquentiel.

*Cycles uniques : on réalise le même type de parcours, mais en s'autorisant cette fois un cycle. On vérifie ensuite qu'on a bien une séquence (pour éviter les cycles imbriqués). On vérifie également la nature du cycle trouvé (émissions ou non).

*Détection de cycles indépendants : on parcourt toutes les transitions des pairs du système en détectant les cycles et on s'arrête lorsqu'on trouve un état dans le cycle courant déjà parcouru dans un cycle précédent.

*Détection de cycles dépendants : pour chaque pair (on en considère 2 à partir d'ici), on vérifie qu'on a bien un cycle initial, et on stocke les messages le composant.
**à même séquence  de messages : on vérifie l'ordre des messages entre les 2 pairs, le cas échant le système est valide.
**à alphabets complémentaires : une fois le cycle initial stocké, on compte le nombre de messages d'émissions et de réception ; on associe chaque message à une valeur, incrémentée si il y a émission, décrémentée si réception. Si le total est négatif ou nul, le système est stable.
**séparés par des séquences (avec fin par un cycle ou un séquence) : l'algorithme n'a pas été réalisé jusqu'au bout, mais il permet de détecter la structure sans réaliser le traitement ; il faudrait ensuite détecter le type de cycle présent en fin de système, s'il y en a un, et le traiter correctement.


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 ==

Sur plus de 300 systèmes fournis et écrits, plus de la moitié ont pu être classifiés par ce pré-traitement, qui permet d'éviter un calcul très long pour une partie des systèmes, dont beaucoup provenaient de systèmes réels concrets.

Par ailleurs, l'algorithme de pré-traitement se comporte de façon linéaire. Il est au pire polynomial, mais il parcourt des quantités finies et faibles (nombre de boucles, nombre de transitions), et s'exécute donc rapidement, ceci malgré les appels récursifs exécutés notamment pour la détection de cycle. Ceci reste dans tous les cas bien moins coûteux que les traitements structurels de CADP.

= 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 asynchrones, 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.
A l'avenir, il faudrait continuer à réaliser des études théoriques sur ce type de pré-traitement à base d'analyse structurelles, en rendant plus génériques les algorithmes de détections concrets, mais aussi en trouvant éventuellement des méthodes théoriques pour déterminer quels types de systèmes il est possible de classer, sans devoir rentrer dans le détail qui finalement reviendrait à détecter un système unique qu'une véritable classe de systèmes.

A titre personnel, ce projet IRL m'a permis de découvrir le monde de la recherche de l'intérieur, à la fois dans la méthode de travail, mais aussi dans l'environnement, le fonctionnement, et la façon de penser l'informatique. Ce stage fut très instructif et m'a permis d'apprendre beaucoup à la fois sur le plan théorique, technique, mais aussi méthodologique. 


= 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.