Verimag

Détails sur le séminaire

Amphitéâtre MJK
6 mai 2013 - 14h00
Programmation efficace et sécurisé d'applications à mémoire partagée
par Emmanuel Sifakis de Verimag/UJF



Résumé : L'utilisation massive des plateformes multi-cœurs et multi-processeurs a pour effet
de favoriser la programmation parallèle à mémoire partagée. Néanmoins, exploiter
efficacement et de manière correcte le parallélisme sur ces plateformes reste un
problème de recherche ouvert.
De plus, leur modèle d'exécution sous-jacent, et notamment les modèles de mémoire
"relâchés", posent de nouveaux défis pour les outils d'analyse statiques et dynamiques.
Dans cette thèse nous abordons deux aspects importants dans le cadre de la
programmation sur plateformes multi-cœurs et multi-processeurs: l'optimisation
de sections critiques implémentées selon l'approche pessimiste, et l'analyse
dynamique de flots d'informations.
Les sections critiques définissent un ensemble d'accès mémoire qui doivent être
exécutées de façon atomique.
Leur implémentation pessimiste repose sur l'acquisition et le relâchement de
mécanismes de synchronisation, tels que les verrous, en début et en fin de
sections critiques.
Nous présentons un algorithme générique pour l'acquisition/relâchement des
mécanismes de synchronisation, et nous définissons sur cet algorithme un
ensemble de politiques particulier ayant pour objectif d'augmenter le parallélisme
en réduisant le temps de possession des verrous par les différentes threads.
Nous montrons alors la correction de ces politiques (respect de l'atomicité et
absence de blocages), et nous validons expérimentalement leur intérêt.
Le deuxième point abordé est l'analyse dynamique de flot d'information pour des
exécutions parallèles. Dans ce type d'analyse, l'enjeu est de définir
précisément l'ordre dans lequel les accès à des mémoires partagées peuvent avoir
lieu à l'exécution. La plupart des travaux existant sur ce thème se basent sur
une exécution sérialisée du programme cible. Ceci permet d'obtenir
une sérialisation explicite des accès mémoire mais entraîne un surcoût en temps
d'exécution et ignore l'effet des modèles mémoire relâchées.
A contrario, la technique que nous proposons permet de prédire l'ensemble des
sérialisations possibles vis-a-vis de ce modèle mémoire à partir d'une seule
exécution parallèle ("runtime prediction").
Nous avons développé cette approche dans le cadre de l'analyse de teinte,
qui est largement utilisée en détection de vulnérabilités.
Pour améliorer la précision de cette analyse nous prenons également en compte
la sémantique des primitives de synchronisation qui réduisent le nombre de
sérialisations valides.
Les travaux proposé ont été implémentés dans des outils prototype qui ont permit
leur évaluation sur des exemples représentatifs.




Contact | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 876957