ALIDECS

Langages et Atelier Intégré pour le Développement
de Composants Embarqués Sûrs


Ce projet est une ACI "Sécurité & Informatique"

 









 

FunLoft

FunLoft

Dans un cadre concurrent, il est naturel de demander que l'exécution d'un fragment de code séquentiel reste atomique, c'est-à-dire que la signification d'une séquence d'instructions exécutée par un composant parallèle reste invariante en présence d'autres composants parallèles. La séquence x:=1; x:=x+1 est d'un point de vue séquentiel strictement équivalente à l'affectation x:=2. Ce n'est plus vrai dans un cadre concurrent, si une autre affectation peut s'intercaler entre les deux instructions de la première séquence. La préservation de la signification d'une séquence d'instructions dans un contexte concurrent est fondamentalement un problème d'atomicité ; c'est à ce problème que l'on s'est attaqué, dans le cadre des FairThreads [6], un modèle qui mélange threads coopératifs et threads préemptifs.

Dans un premier temps, nous avons considéré le langage Cyclone et réalisé une implémentation de Loft en Cyclone. Ce travail a fait l'objet d'un rapport de recherche INRIA [5]. La conséquence de cette étude a été d'abandonner l'idée de partir de Cyclone et de concevoir un langage permettant d'analyser les atomes, pour être capable de prouver leur atomicité.

Dans une deuxième phase, on a conçu, en collaboration avec F. Dabrowski (participant à l'ACI CRISS), un langage réactif implémentant une version simplifiée du modèle des FairThreads, avec un seul scheduler et la possibilité pour les threads de se délier temporairement. Nous avons défini un système de types et d'effets avec contraintes pour assurer l'étanchéité mémoire : un thread délié n'a accès qu'à sa mémoire privée et ne risque dont pas d'interférer avec les autres threads liés. Les threads déliés ne peuvent pas non plus se gêner entre-eux ce qui garantit la proriété d'atomicité recherchée. Ce travail sera présenté à un colloque sur les threads[14].

On a également commencé à implémenter une variante du langage, appelée FunLoft. Les points principaux de cette implémentation sont : (1) Types inférés. En particulier, l'utilisateur n'a pas à indiquer le statut des références créées. (2) Traduction en Loft/FairThreads en C.

Pour tester l'expressivité du modèle de programmation, on a principalement implémenté trois exemples :

  • Automates cellulaires. Ces exemples sont interfacés avec la librairie SDL, pour l'affichage graphique. Ils reprennent des programmes Loft/C2. Dans ces exemples, chaque cellule est un thread. L'aspect mis en avant est principalement la possibilité de traiter des grands nombres de threads (dans le cas présent, 40000).
  • Simulation de proies/prédateurs. L'aspect qui est mis en avant par cet exemple est la création dynamique : lorsque les prédateurs ont détruit les proies, de nouvelles proies sont automatiquement recréées.
  • Exemple de producteurs/consommateurs.

Pascal Raymond 2006-11-16