Fabien DAGNAT

Figure 1.1 : Aperçu du processus de spécification et réalisation de reconfigurations.

---

Dans ce processus, nous mettons en évidence deux formes pour les reconfigurations. À un haut niveau d’abstraction, les plans de reconfiguration considèrent le modèle Synoptic du logiciel. De même que les modèles Synoptic servent de base à la génération de code, les plans de reconfiguration sont utilisés pour produire des scripts. De plus bas niveau, les scripts mettent en œuvre les reconfigurations en prenant en compte les détails d’implémentation du code généré du logiciel de vol. Les deux générateurs de code (application et reconfiguration) doivent donc être coordonnés (figure 1.2).

Vérification d’une reconfiguration Dans le processus, nous reconnaissons le besoin de vérifier et valider les reconfigurations. Plusieurs propriétés sont à vérifier :

• la reconfiguration doit être exécutable pour la version actuelle du logiciel ;
• la phase transitoire pendant l’exécution de la reconfiguration, au cours de laquelle certains éléments du logiciel sont désactivés, doit satisfaire des propriétés spécifiques ; il s’agit d’assurer un service minimum pendant la reconfiguration ;
• le résultat de la reconfiguration doit satisfaire les propriétés nouvellement attendues.

Les propriétés à vérifier peuvent être de l’ordre des contraintes spatiales et temporelles. Il peut s’agir de contraintes d’ordonnançabilité et de qualité de service. Il peut également s’agir de propriétés fonctionnelles.

Ces vérifications peuvent être réalisées soit au niveau abstrait, soit après la phase de génération de code. La validation formelle d’un plan de reconfiguration peut être réalisée de manière globale, en prouvant la conformité du résultat de son exécution vis-à-vis des spécifications visées. Pour limiter l’étendue des vérifications à réaliser, il est possible d’exploiter les éléments inchangés dans la spécification et dans le code. Il est possible d’optimiser encore cet objectif de preuve en se dotant d’un support de vérification modulaire, un système de contrats, par exemple [9].

Afin de déterminer l’étendue des vérifications à réaliser, à la manière d’un Makefile, un outil de configuration basé sur un système de contrat mettrait en œuvre la méthodologie suivante, et ce pour chaque module à reconfigurer :

1. Prouver la conformité du module au contrat initial
2. Si le contrat est respecté, le module est intégré au plan de reconfiguration
3. Si le contrat n’est pas respecté, alors 1/ les garanties (trop faibles) du module ont un impact sur les hypothèses des modules qui l’utilisent, ou/et 2/ les hypothèses (trop fortes) du module ont un impact sur les modules qu’il utilise.
4. Tous ces modules doivent faire l’objet du test de conformité 1.
   1. amont du module reconfiguré, pour savoir si leurs garanties sont compatibles avec les hypothèses du nouveau contrat
   2. en aval pour savoir si leurs hypothèses sont compatibles avec les garanties du nouveau contrat.

Ceci comme le ferait un Makefile en vérifiant la conformité des dates de modules.

Une stratégie alternative est possible :

1. Pour le groupe de modules reconfigurés, prouver la conformité au contrat initial aux frontières de ce groupe.
2. Si le contrat est respecté, le plan de reconfiguration est accepté.
3. Si le contrat n’est pas respecté, alors 1/ les garanties (trop faibles) du groupe de modules ont un impact sur les hypothèses des modules qui l’utilisent, ou/et 2/ les hypothèses (trop fortes) du group de modules ont un impact sur les modules qu’il utilise.
4. Tous ces modules, à la frontière extérieure, doivent être intégrés au groupe de modules reconfigurés. La reconfiguration doit modifier ces modules.

Compilation de la reconfiguration L’empaquetage de la reconfiguration contient le script de bas niveau. La reconfiguration peut par ailleurs insérer de nouveaux éléments dans le logiciel. Les nouvelles portions de code sont empaquetées avec la reconfiguration, qui est ainsi auto-contenue. Ce nouveau code répond à des besoins identifiés lors de la conception de la reconfiguration. Son développement suit le processus standard utilisé pour l’ingénierie de la version initiale du logiciel.

 

---

Figure 1.2: Génération du code des applications et de leurs reconfigurations.

---

En amont des phases de vérification et de génération de code, nous définissons une phase de conception de la reconfiguration. Pour cette phase, qui doit résulter en une première version du plan de reconfiguration, nous identifions trois démarches possibles.

• Figure 1.3, la conception de la reconfiguration est dirigée par le modèle du logiciel à mettre à jour. Lors d’une phase de maintenance, ce logiciel est modifié de manière à prendre en compte les nouveaux besoins et les rapports de défaillance. Le résultat de la phase de maintenance est le modèle modifié du logiciel. Le plan de reconfiguration est alors la liste des différences identifiées entre les versions du logiciel.
• Figure 1.4, la conception est dirigée par la reconfiguration. À partir des besoins et des rapports de défaillance, c’est directement le plan de reconfiguration qui est réalisé. Au centre du raisonnement se trouvent alors les changements qui doivent être appliqués au logiciel. Ce n’est que dans une seconde phase que, par simulation de la reconfiguration, la nouvelle version du modèle du logiciel est appliquée. En simulant la reconfiguration sur plusieurs branches, il est possible de propager une même reconfiguration sur plusieurs variantes du logiciel.
• Il est également possible de suivre des approches hybrides. Par exemple, il est possible de fixer une frontière dans le modèle autour d’une zone que l’on souhaite reconfigurer. Puis, on applique la première approche sur ce bout de modèle. L’intérêt de cette approche hybride est de pouvoir appliquer la reconfiguration obtenue à plusieurs logiciels à condition que leurs modèles contiennent ce bout de modèle. Attention, toutefois, chaque reconfiguration doit être revalidée systématiquement vu les contraintes globales des LV. Une fois validée, le plan de déploiement obtenu doit pouvoir s’appliquer à tous les LV concernés.

 

---

Figure 1.3: Dirigée par le modèle du logiciel.	Figure 1.4: Dirigée par la reconfiguration.

---

ReCaml

Les mécanismes habituels de reconfiguration ne sont pas appropriés pour plusieurs raisons :

• la chaîne de compilation synchrone ne préserve a priori pas la modularité du code, alors qu’il s’agit d’un impératif des mécanismes actuels. Le document SPa5b [3] montre cependant que différentes stratégies de génération de code sont applicables afin de préserver la modularité du code et aussi sa réutilisabilité.
• les mécanismes actuels ne prennent pas en compte les contraintes temporelles.
• il est difficile de prédire le comportement des reconfigurations car il peut dépendre du timing de son exécution.

Pour répondre à ces problèmes, nous avons pris comme modèle un langage fonctionnel fortement typé (Caml) afin de concevoir un mécanisme spécifique de reconfiguration (ReCaml [7]). Même si ce langage n’est pas synchrone, il partage avec Synoptic des caractéristiques telles que le typage et la décomposition fonctionnelle des programmes.

Lors de la conception de ReCaml, nous avons adopté plusieurs principes. Tout d’abord, nous faisons de la reconfiguration un véritable programme à part entière. Cela signifie notamment que nous en acceptons toute la complexité, quitte à fournir ultérieurement des outils. Dans ce programme, le développeur doit expliciter intégralement le comportement de la reconfiguration. En n’acceptant aucun comportement implicite, la reconfiguration est plus facilement prédictible. Enfin, la reconfiguration doit au moins pouvoir être typée statiquement. Il s’agit d’une première étape pour rendre les reconfigurations plus fiables.

Fondations Avec ReCaml, le fonctionnement des reconfigurations est le suivant. Lorsqu’une reconfiguration doit être exécutée, les nouveaux segments de code sont tout d’abord chargés en mémoire. Puis l’exécution de l’application est suspendue. Son état est réifié. Il est passé en paramètre pour exécuter le code de la reconfiguration, que nous appelons compensation. La compensation a pour rôle de faire le nécessaire, en fonction de l’état dans lequel l’exécution a été suspendue, afin d’intégrer la reconfiguration dans l’exécution. Pour cela, la compensation peut employer tous les moyens à sa disposition, tels que finir des activités en cours ou exécuter des fonctions spécifiques. Lorsque la compensation estime sa tâche accomplie, l’état capturé est rechargé afin de reprendre l’exécution de l’application.

Dans ReCaml, la réification de l’état de l’exécution est basée sur le concept de continuation. Le traitement de cet état repose sur sa décomposition en activations de fonctions, c’est-à-dire en environnements d’évaluation des appels. La compensation fonctionne donc en dépilant les appels de l’état capturé jusqu’à ce que soient traités tous les appels qui doivent l’être. Autrement dit, la compensation parcourt le graphe d’appel du logiciel à partir de l’état auquel la reconfiguration est déclenchée. L’environnement d’évaluation et le « reste à faire » sont identifiés grâce au site de retour. Un type statique est associé à chaque site de retour afin de pouvoir vérifier que l’opération de décomposition des continuations est utilisée correctement.

 

---

Figure 1.5: Fonctionnement d’une opération « match_cont » pour décomposer une continuation.

---

La figure 1.5 résume le mécanisme de base « match_cont ». La continuation passée en paramètre, dont l’exécution doit se poursuivre au site de retour , est décomposée en 2 sous-continuations : l’appel en sommet de pile, qui contient le site de retour ; et le reste, qui dans la continuation initiale aurait poursuivi l’exécution au retour du sommet de la pile. Des valeurs, par exemple x₁, peuvent par ailleurs être récupérée dans le sommet de la pile. Afin de pouvoir associer un type à chaque valeur et sous-continuation, on associe le type { τ₁, τ₂, [ x₁ → τ_x1 ] } au site de retour . Les types des sites de retour sont composés :

• du type de retour qui permet de reprendre l’exécution (τ₁), c’est-à-dire le type de retour de la fonction appelée au site de retour ;
• du type de retour de l’appel en sommet de pile (τ₂), c’est-à-dire le type de retour de la fonction englobante, à la frontière entre les 2 sous-continuations produites ;
• et de l’environnement de typage au site de retour (x₁ → τ_x1) qui fournit les types des variables accessibles dans la pile.

Dans la figure 1.5, tous les types sont statiques. Aucun système de types dynamiques n’est introduit afin de pouvoir réaliser les vérifications dès la compilation de la reconfiguration.

Dans le graphe d’appel, chaque site de retour désigne l’arc d’un appel. Le squelette algorithmique de la compensation d’une reconfiguration repose donc sur des fonctions associées aux nœuds du graphe d’appel. La fonction associée au nœud f est mise en œuvre par une opération « match_cont », qui contient autant de clauses que d’arcs arrivant à ce nœud f. Chaque clause est responsable de compenser l’arc correspondant, réalisant une étape dans le parcours du graphe d’appel.

La compensation d’un arc peut prendre diverses formes. C’est le développeur de la reconfiguration qui doit préciser ce qui doit être fait. S’il faut poursuivre l’exécution de l’ancienne version, la sous-continuation qui capture l’appel au sommet de la pile peut être exécutée. Sinon, le développeur doit écrire le code correspondant au comportement souhaité. Pour cela, le développeur peut s’inspirer du code des différentes versions. Une des opérations classiques que pourra réaliser le développeur de la reconfiguration est la conversion des données qui ont besoin d’être convertie (entre l’ancienne version et la nouvelle).

Dans notre approche, le développeur a une maîtrise totale du comportement effectif de la reconfiguration, au prix d’une complexité de définition d’une reconfiguration accrue. Mais, nous sommes persuadés qu’en général, il existe des patrons de reconfiguration assez classiques (surtout dans le cadre d’un domaine précis) et que nous pourrons ainsi proposer au-dessus de ce mécanisme des outils simplifiant la définition des reconfigurations simples. La complexité ne devra être affrontée par le développeur de la reconfiguration que dans les cas où la reconfiguration est complexe ou ne correspond à aucun patron identifié.

Illustration Pour illustrer ces concepts, nous avons conçu une preuve de concept basée sur le calcul d’un nombre de Fibonacci. Ainsi, un code classique et naïf comme il se rencontre dans tous les tutoriaux de programmation est exécuté.

Une première mise à jour consiste à changer le type de retour de la fonction afin d’éviter les dépassements de capacité. Pour cette mise à jour, la compensation de chaque arc consiste à convertir les résultats intermédiaires vers le nouveau type de données et à terminer le calcul en utilisant la nouvelle version de la fonction (qui manipule des éléments du nouveau type). L’introspection de la pile d’appels permet de déterminer le contexte d’évaluation afin de détecter les résultats intermédiaires incorrects dûs à un dépassement de capacité. Cette détection permet de ne recalculer que les résultats effectivement incorrects.

La seconde mise à jour réalisée consiste à passer de l’algorithme naïf à 2 appels récursifs, de complexité exponentielle, à l’algorithme basé sur une fenêtre glissante de 2 nombres de Fibonacci, de complexité linéaire. Pour accomplir cette mise à jour, il faut trouver parmi les résultats intermédiaires 2 nombres de Fibonacci consécutifs. La nature de l’algorithme initial ne donne pas de moyen immédiat pour obtenir ces résultats. Il est nécessaire de parcourir l’ensemble des résultats intermédiaires, qui sont répartis sur l’ensemble des appels actifs. À nouveau, c’est bien l’introspection de la pile d’exécution qui permet de construire l’état à partir duquel l’exécution peut reprendre.

Cet exemple est décrit en partie dans [7] et un article plus détaillé est en cours de rédaction pour présenter le système réalisé.

Conception du mécanisme et du langage de reconfiguration

Pour concevoir le mécanisme concret de reconfiguration, nous modélisons les concepts en rapport avec la reconfiguration. Il s’agit notamment d’identifier les caractéristiques des unités architecturales telles que Synoptic les définit. La figure ?? (TODO, méta-modèle de composant ?) et les méta-modèles de Synoptic montrent une vision synthétique de ces caractéristiques. En les formalisant, nous alimentons la réflexion sur le mécanisme de reconfiguration.

 

---

Figure 1.6: Mécanisme de reconfiguration modulaire.

---

Chaque concept architectural définit des opérations de reconfiguration spécifiques. Il se traduit par un élément du mécanisme de reconfiguration propre, comme le montre la figure 1.6. Par exemple, le concept de hiérarchie de l’architecture définit des opérations pour placer les éléments les uns à l’intérieur des autres ; le concept d’assemblage définit des opérations pour connecter et déconnecter les éléments ; le concept d’instance définit des opérations pour créer et détruire des éléments. En dissociant de la sorte les différents concepts architecturaux, nous apportons une réponse modulaire à la conception du mécanisme de reconfiguration de l’architecture. Il est ainsi possible de suivre les évolutions de Synoptic.

La conception modulaire du mécanisme est reflétée dans une construction modulaire du langage de reconfigurations. Comme le montre la figure 1.7, à partir d’un langage généraliste, nous proposons d’ajouter les éléments de langage qui correspondent aux opérations souhaitées. Pour chaque concept architectural, ce sont à la fois des constructions d’introspection et des constructions de reconfigurations qui sont ajoutées.

 

---

Figure 1.7: Modularisation du langage de reconfiguration.

---

Ce travail a été présenté à une conférence [6].

Discussion

Le mécanisme proposé répond partiellement aux problèmes spécifiques posés dans le cadre de SPaCIFY. Il permet de s’affranchir de la modularité du code. Le comportement effectif est explicite et prédictible. Nous n’avons cependant pas encore étudié la prise en compte des contraintes temporelles ni les problèmes d’ordonnancement des reconfigurations. Le mécanisme actuel ne traite pas les applications multi-tâches. En formalisant le mécanisme et en introduisant un typage statique, nous contribuons à la construction de futurs procédés de vérification des reconfigurations, sans pour autant apporter de réponse complète. Ces problèmes (temps-réel, ordonnancement, multi-tâche et vérification) restent actuellement ouverts.

Même s’il permet d’abstraire par des constructions langagières les détails d’implémentation, le mécanisme proposé est de bas niveau. Le développeur de reconfiguration doit avoir une bonne connaissance des différentes versions du logiciel de vol afin par exemple de mettre en œuvre le parcours du graphe d’appel inversé. Nous pensons qu’un outillage est impératif afin de rendre l’approche viable. À relativement court terme, il est par exemple tout à fait envisageable de générer automatiquement le squelette algorithmique qui réalise le parcours du graphe d’appel d’un programme particulier. De même, nous commençons à identifier des comportements récurrents dont l’automatisation de la génération épargnerait au développeur certaines tâches systématiques. C’est le cas par exemple lorsqu’on souhaite simuler un comportement de dynamic rebinding.

Dans le cadre des résultats de SPaCIFY, le mécanisme ReCaml est au niveau de la preuve de concept. Le langage support est un λ-calcul typé rudimentaire, privé par exemple du polymorphisme. Des travaux concernant les mécanismes fondamentaux de ReCaml semblent indispensables avant de pouvoir intégrer un langage de programmation réaliste.

Bibliography

[1] First ACM Workshop on Hot Topics in Software Upgrades, Nashville, Tennessee, USA, octobre 2008.

[2] Joe Armstrong : Programming Erlang: software for a concurrent world. The Pragmatic PRogrammers, 2007.

[3] Loïc Besnard, Thierry Gautier et Jean-Pierre Talpin : Spa5 bis - code generation strategies for synoptic using the polychrony platform, 2009.

[4] Eric Bruneton, Thierry Coupaye, Matthieu Leclercq, Vivien Quéma et Jean-Bernard Stefani : The Fractal component model and its support in Java. Software: Practice and Experience, 36(11-12):1257–1284, septembre 2006. Spec. issue on experiences with auto-adaptive and reconfigurable systems.

[5] Jérémy Buisson, Cecilia Carro et Fabien Dagnat : Issues in applying a model driven approach to reconfigurations of satellite software. In First ACM Workshop on Hot Topics in Software Upgrades [1].

[6] Jérémy Buisson et Fabien Dagnat : Experiments with Fractal on modular reflection. In Software Engineering Research, Management and Applications, pages 179–186, Prague, Czech Republic, août 2008.

[7] Jérémy Buisson et Fabien Dagnat : Introspecting continuations in order to update active code. In First ACM Workshop on Hot Topics in Software Upgrades [1].

[8] Geoff Coulson, Gordon Blair, Paul Grace, Francosi Taiani, Ackbar Joolia, Kevin Lee, Jo Ueyama et Thirunavukkarasu Sivaharan : A generic component model for building systems software. ACM Transactions on Computer Systems, 26(1), février 2008.

[9] Yann Glouche, Paul Le Guernic, Jean-Pierre Talpin et Thierry Gautier : A boolean algebra of contracts for logical assume-guarantee reasoning. Rapport technique, INRIA, 2008.

[10] Jeff Kramer et Jeff Magee : The evolving philosophers problem: dynamic change management. IEEE Transaction on Software Engineering, 16(11):1293–1306, novembre 1990.

[11] Yves Vandewoude, Peter Ebraert, Yolande Berbers et Theo D’Hondt : Tranquility: a low disruptive alternative to quiescence for ensuring safe dynamic updates. IEEE Transactions on Software Engineering, 33(12):856–868, décembre 2007.