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


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é : le cas échéant, le traitement en est simple, puisque si le système est synchro

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 [JACM83].

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<ref>Citation YE-SALAUN sur stabilité</ref> définissant la notion de stabilité presenté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.


Analyse de problèmes ouverts

La stabilité étant actuellement plutôt coûteuse à montrer (d'autant qu'elle n'est pas toujours présente), 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

- Focus sur le prétraitement : facile à implémenter, moins de blocages théoriques et tout aussi utile

Comprendre le problème

- ?

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

- Python + outils externes - Refactoring - Nettoyage - Fonctions à retirer/utiliser différemment ?


Algorithmes et tests

- Détection de séquences - Détection de cycles diverses - Pas forcément de souci de coût


Observations

- Proportion de systèmes éliminés sur panoplie de systèmes classiques/réels - Difficile de jouer sur l'efficacité - Pas forcément rentable : 1 système = 1 type de système ?


Futurs travaux ?

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