Transformation de programmes SystemC vers langage de vérification
De Ensiwiki.
Sommaire |
Transformation de programmes SystemC vers langage de vérification
| Labo | VERIMAG |
| Equipe | SYNCHRONE |
| Encadrants | Kevin.Marquet@imag.fr,Matthieu.Moy@imag.fr
|
Contexte scientifique et technologique
Quiconque a programmé avec du parallélisme explicite, notamment des threads, sait qu'il est très facile de faire des erreurs aboutissant aux redoutés deadlocks et race conditions. S'il peut être tolérable de voir son navigateur Web « planter » de temps en temps pour de tels motifs, ces dysfonctionnements peuvent avoir des conséquences plus graves, par exemple la perte de sondes spatiales de la NASA...
Il est donc très intéressant de pouvoir démontrer automatiquement des propriétés sur des programmes parallèles (par exemple, absence de deadlocks). On s'intéresse ici à la vérification de programmes écrits en SystemC, une librairie C++ très utilisée pour la conception de systèmes embarqués. Cette librairie permet donc d'écrire des systèmes embarqués sous la forme de programmes multi-threads C++ en utilisant certaines primitives : attente sur du temps, attente/notification d'évènements par exemple.
Plusieurs outils tels que CADP ou SPIN permettent de vérifier automatiquement des propriétés mais ils vérifient des programmes écrits dans un langage bien particulier, qui n'est bien sûr pas SystemC. On cherche donc à transformer un programme SystemC dans un programme écrit dans le langage d'entrée de l'outil de vérification.
Cette tâche est difficile car, pour être efficace, elle demande de reconnaître les primitives SystemC, de les transformer efficacement dans le langage de l'outil cible. Aujourd'hui, on dispose d'un front-end, capable de charger un programme SystemC, d'en reconnaître les primitives SystemC. Le sujet de ce TER est maintenant à écrire le back-end : transformer la forme intermédiaire obtenue en un programme vérifiable par l'outil de vérification. Le choix de cet outil sera le résultat d'une petite bibliographie et de discussions avec les encadrants de ce projet.
Il s'agit d'un projet aussi bien orienté recherche qu'implémentation.
Compétences attendues et compétences fournies
Il est nécessaire de savoir programmer en C++ (par contre, inutile d'être un expert en fonctionnalités ésotériques du langage). Un étudiant avec de bonnes bases en C et en Java pourra apprendre le C++ pendant le TER.
Ce sujet permettra d'approfondir des notions vues en compilation ou d'autres cours (simulation, compilation, notions de calcul parallèle et de synchronisation vues en SEPC...), d'avoir un premier contact avec la vérification de programmes, la conception de systèmes embarqués, et plus généralement avec la recherche.
Pour les étudiants en filière SLE, ce TER serait une préparation idéale au module « Modélisation transactionnelle des systèmes sur puces » en 3A.
Sujet
- Faire connaissance avec SystemC
- Après une rapide bibliographie, choisir un outil de vérification efficace
- Définir une représentation dans le langage de cet outil vérification
- Définir les transformations possibles des instructions SystemC vers le langage de vérification
- On pourra comparer l'efficacité de cette approche aux travaux existants
Il s'agit d'avancer par petits bouts en travaillant d'abord sur une instruction donnée et en regardant comment elle peut être représentée dans le langage de vérification, puis en considérant d'autres instructions.
Bien entendu, les dernières étapes sont « optionnelles » au sens qu'on ne peut prévoir d'avance les éventuelles difficultés rencontrées !
Cadre de travail et perspectives
Matthieu Moy est enseignant Ensimag et connaît notamment bien le module de compilation. Kevin Marquet est post-doctorant et travaille sur la conception et la vérification de systèmes embarqués. Le travail se fera en coopération forte avec ce dernier. La familiarisation avec les problématiques et les outils utilisés sera très utile :
- si le stagiaire envisage de poursuivre dans une filière recherche vers la vérification de circuits ou de logiciels par analyse statique
- si le stagiaire envisage de travailler sur la conception de systèmes embarqués
