Transformation de programmes SystemC vers langage de vérification

{{Sujet ter
| labo = [http://www-verimag.imag.fr VERIMAG]
| titre = Transformation de programmes SystemC vers langage de vérification
| equipe = SYNCHRONE
| encadrants = Kevin.Marquet@imag.fr,Matthieu.Moy@imag.fr
}}
[[Catégorie:TER]]

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