Delahaye Pierre-Yves - Extraction de contrats 42 à partir de programmes SystemC - Résultats

De Ensiwiki
Aller à : navigation, rechercher


Extraction de contrats 42 à partir de programmes SystemC

Labo Verimag
Equipe Synchrone
Encadrants Kevin.Marquet@imag.fr,Matthieu.Moy@imag.fr


Etudiant

Pierre-Yves Delahaye (SLE)


Introduction

Le travail présenté ici a été réalisé au sein du laboratoire Verimag de Grenoble. Celui-ci travaille sur la mise au point d'outils théoriques et techniques destinés à faciliter le développement de systèmes embarqués sûrs, et ce à des coûts compétitifs.

Les industries qui développent de nouveaux systèmes embarqués sont aujourd'hui confrontées à deux défis principaux :

  • réduire le coût et le temps de développement
  • faire face à l'augmentation de la complexité de ces systèmes


Eléments de pré-requis

Pour relever ces deux principaux défis, une bibliothèque C++ a été mise en place : SystemC. Elle est aujourd'hui considérée comme un standard dans l'industrie des systèmes embarqués.

La bibliothèque SystemC

La bibliothèque SystemC repose donc sur le langage C++, et permet une modélisation modulaire de haut niveau de la partie matérielle des systèmes embarqués. On trouve ci-dessous un exemple de modélisation permise par SystemC.


Deux modules SystemC qui communiquent


On remarque la présence de deux modules, qui communiquent entre eux via des ports d'entrée (en vert), et de sortie (en rouge). Chaque module SystemC a un comportement décrit par un (ou plusieurs) processus (ici T1 et T2). Les processus permettent d'appliquer des traitements aux signaux reçus en entrée des modules, et d'envoyer vers d'autres modules des signaux résultant de ces traitements.

Le haut niveau d'abstraction permis par SystemC, en se focalisant davantage sur la synchronisation des modules au niveau entrées/sorties, que sur le fonctionnement interne de chacun d'eux, permet de réduire le coût et le temps de développement des systèmes embarqués. En effet, on peut tester le système par simulation dès les premières étapes de son développement, sans avoir besoin de connaître les détails d'implémentation de chaque composant. On est alors en mesure de corriger rapidement d'éventuelles erreurs dans les choix de conception, ce qui limite les surcoûts fianciers et les retards dans le développement, liés à des dysfonctionnements détectés trop tardivement. En outre, être en mesure de simuler la partie matérielle de ces systèmes dès les premières phases de développement, c'est donner la possibilité de commencer le développement de la partie logicielle très tôt, sans avoir besoin d'attendre que la partie matérielle soit totalement aboutie. C'est donc là aussi un élément clé dans la réduction du temps de développement.

Outre son haut niveau d'abstraction, SystemC permet également comme on l'a vu sur la figure ci-dessus d'envisager les systèmes sous la forme de modules, sortes de sous-entités des systèmes, communiquant entre eux. Cette façon de concevoir les systèmes permet à différentes équipes de développer en parallèles différents modules, qui seront par la suite assemblés pour constituer le système final. On peut également réutiliser des modules déjà développés par le passé. On réduit ainsi les conséquences négatives de l'augmentation de la complexité des systèmes embarqués, en morcelant le travail de conception.

Le formalisme 42

Imaginons que dans le cadre du développement d'un nouveau système, une équipe ait besoin d'un module développé plusieurs années auparavant, par des personnes qu'il est difficile de recontacter. Le problème qui se pose est de savoir si le module que l'on souhaite réutiliser va pouvoir se synchroniser correctement avec le reste du système. Il faudrait pour cela avoir un modèle comportemental de ce module, au niveau de ses entrées/sorties.

Ce modèle comportemental peut être obtenu grâce au formalisme 42, actuellement en cours de définition à Verimag, avec pour principaux contributeurs Tayeb Bouhadiba, et Florence Maraninchi.

Qu'est-ce que 42 ?

Le formalisme 42 permet de modéliser un système, avec trois éléments principaux :

  • des composants (qui correspondent aux modules SystemC)
  • des contrats (un pour chaque composant)
  • un contrôleur

Nous donnons ci-dessous un exemple de modélisation 42 d'un système.


Modélisation 42 d'un système


Les composants sont des entités dotées de ports d'entrée et de sortie, comme les modules SystemC. Au-dessus de ces composants, sur le plan hiérarchique, on trouve le contrôleur. C'est en quelque sorte le chef d'orchestre : il gère le fonctionnement des composants les uns par rapport aux autres.

Les contrats 42

Enfin, chaque composant est équipé d'un contrat. C'est le contrat qui va donner le fameux modèle comportemental d'un composant, nécessaire pour savoir s'il va pouvoir collaborer correctement avec les autres composants du système.

Voici un exemple de contrat 42.


Exemple de contrat 42


Il s'agit donc d'un graphe, constitué d'états et de transitions. Chaque transition est de la forme : {data_req} control_inputs / control_outputs {data_prod}

  • data_req représente l'ensemble des signaux de données, fournis par d'autres composants, nécessaires à la réalisation de la transition
  • control_inputs repésente l'ensemble des signaux que doit délivrer le contrôleur pour que la transition puisse s'effectuer
  • control_outputs représente l'ensemble des signaux produits, à destination du contrôleur
  • data_prod représente l'ensemble des signaux que le composant va adresser aux autres composants avec lesquels il communique

On le voit, le contrat 42 est en quelque sorte le mode d'emploi d'un composant : il permet de connaître le contexte nécessaire (signaux en entrée) pour produire des signaux dont d'autres composants auront besoin.

Avec le formalisme 42, on est donc capable d'associer un modèle comportemental, sous forme de contrat, à chaque module SystemC.

Pour revenir à notre équipe qui souhaite réutiliser un module déjà développé, ce qui l'intéresserait tout particulièrement, c'est d'être capable, à partir de la description SystemC du module, de pouvoir obtenir automatiquement le contrat 42.

Cette génération automatique de contrats 42, à partir du code SystemC de modules constituant un système, a été l'objet de ce TER.

Travail réalisé

On l'a vu, un contrat 42 se focalise sur les entrées/sorties d'un composant. Dès lors, il s'avère nécessaire, pour extraire des contrats 42, de s'intéresser aux primitives SystemC de communication entres modules. Un autre élément sur lequel s'est porté notre travail durant le TER a été le traitement des structures de contrôle (if,while,for) que l'on retrouve très souvent dans n'importe quel programme.

Nous ne présenterons pas ici les algorithmes d'extraction de contrats 42 qui ont été mis au point. On les trouvera dans le rapport qui peut être téléchargé à partir du lien en bas de page.

Traitement des primitives SystemC : wait et notify

Lorsque le processus d'un module SystemC contient une primitive wait ou notify, il y a alors une interaction en jeu avec les autres modules :

  • wait(e:event) : l'exécution du processus est stoppée, il rend la main à l'ordonnanceur, et l'exécution ne reprendra que lorsqu'un autre processus, donc un autre module, aura produit l'événement attendu
  • notify(e:event) : le processus en attente de l'événement notifié devient éligible par l'ordonnanceur

La mise au point d'un algorithme de traitement de ces primitives, pour construire un contrat 42, ne pose pas de problème paticulier.

Les structures de contrôle : if, while, for

La mise au point d'un algorithme pour traiter les structures de contrôle a mis en évidence une difficulté.

Ainsi, lorsqu'un programme SystemC comporte plusieurs blocs if..then..else consécutifs (voir exemple ci-dessous), on a deux stratégies possibles pour extraire le contrat 42 :

  • la première conduit à une explosion du nombre d'états du contrat 42
  • la deuxième augmente la granularité par rapport au programme SystemC


Blocs.jpg


Regardons plus en détail ces deux stratégies.

Explosion du nombre d'états

La stratégie représentée par la figure ci-dessous fait exploser le nombre d'états du contrat.


Explosion du nombre d'états


On fait partir de l'état A une branche par parcours possible des blocs if..then..else. Le nombre d'états générés est alors exponentiel.

Augmentation de la granularité

Sur la figure suivante, le nombre d'états créés n'est pas exponentiel, mais la granularité augmente par rapport au programme SystemC.


Augmentation de la granularité


Ici, on crée un état B intermédiaire, entre les deux blocs if..then..else. Cet état n'aurait peut-être pas été présent si on avait distingué tous les parcours possibles, comme précédemment. Or, toute transition entre deux états correspond à une section atomique de code. Ici, on a donc "coupé" une section atomique de code SystemC en deux : la granularité augmente.

La stratégie choisie

On a choisi d'implémenter l'algorithme correspondant à la deuxième stratégie, sachant que les deux présentent des inconvénients.

En effet, faire exploser le nombre d'états du contrat peut rendre difficile son traitement ultérieur (par exemple pour vérifier certaines propriétés sur les entrées/sorties). Et augmenter la granularité peut, lors de l'analyse du contrat, faire apparaître des erreurs qui en réalité n'existent pas, puisque les sections atomiques ne sont plus les mêmes au niveau du contrat 42 généré, que dans le programme SystemC d'origine.

Exemple de résultat fourni par l'outil d'extraction développé

Voici, pour un exemple de programme SystemC, le contrat 42 généré par l'outil développé pendant le TER.

Resultat.jpg


On est donc maintenant capable d'extraire un contrat 42, à partir d'un programme SystemC, en prenant en compte le primitives wait et notify, et les strucutures de contrôle.

La sortie peut être mise sous la forme de fichier xml, comme dans l'exemple ci-dessus.

Conclusion

Avant le TER, nous avions une définition de la correspondance entre le processus d'un module SystemC, et son contrat 42. Aujourd'hui, nous sommes capables d'extraire automatiquement ce contrat 42, à partir du programme SystemC.

Ceci dit, tout n'a bien évidemment pas été traité. Ainsi, un des éléments de communication entre les modules, outre les primitives wait et notify, réside dans les appels de fonctions d'un module à l'autre. La définition des contrats 42 en tient compte, mais notre outil ne gère pas ces appels de fonction.

Nous l'avons dit, l'un des intérêts d'une génération de contrat 42 est d'obtenir le "mode d'emploi" d'un module, à partir de sa description SystemC. Mais une fois qu'on a ce "mode d'emploi", cette description comportementale, ce qui pourrait être intéressant, ce serait d'exploiter le contrat 42 et de vérifier automatiquement, grâce à un nouvel outil, que ce contrat est compatible avec les autres contrats relatifs aux autres composants du système. On pourrait ainsi savoir si le module que l'on souhaite réutiliser va pouvoir s'intégrer au reste du système.


Références

  • Béatrice Bérard, Michel Bidoit, François Laroissinie, Antoine Petit, et Philippe Schnoebelen. Vérification de logiciels : techniques et outils du model-checking. Vuibert, 1999.
  • Tayeb Bouhadiba, Florence Maraninchi, et Giovanni Funchal. Formal and executable contracts for transaction-level modeling in SystemC. Technical Report TR-2009-7, Verimag Research Report, 2009.
  • Bell Labs. Spin : general tool description. [1]
  • Florence Maraninchi et Tayeb Bouhadiba. 42 : Programmable models of computation for a component-based approach to heterogeneous embedded systems. 2007.
  • Florence Maraninchi et Tayeb Bouhadiba. 42 : Programmable models of computation for the component-based virtual prototyping of heterogeneous embedded systems. Technical Report TR-2009-1, Verimag Research Report, 2009.
  • Kévin Marquet et Matthieu Moy. PinaVM : a SystemC front-end based on an executable intermediate representation. Technical Report TR-2010-8, Verimag Research Report, 2010.
  • Kévin Marquet, Matthieu Moy, et Bertrand Jeannet. An asynchronous semantics of SystemC in Promela. Technical Report TR-2009-7, Verimag Research Report, 2010.


Documents additionnels