Programmation de systèmes réversibles et sûrs – REVER

En dépit du développement de nombreuses techniques pour aider à la construction de systèmes répartis fiables et disponibles
(notamment, mécanismes de traitement d'exceptions, mécanismes de reprise sur fautes et de recouvrement de fautes, protocoles de réplication, mécanismes de gestion de transactions), la programmation de systèmes sûrs de fonctionnement représente toujours un véritable défi. Ceci est dû en grande partie au fait que les abstractions à la disposition d'un progammeur ou d'un concepteur de système ou d'application sont très hétérogènes, en portée et en fonction, offrent différents compromis et différents modes d'application, se composent mal, n'ont aucune base sémantique commune, et souffrent de l'absence de primtives adaptées dans les langages de programmation actuels. Pour la pluapart, ces différentes
asbtractions sont seulement disponibles au travers de bibliothèques logicielles, qui font des hypothèses et imposent des contraintes différentes, voire antinomiques, en terme de modèle de programmation.

Le Projet REVER entend répondre au défi présenté ci-dessus en facilitant la programmation de systèmes intégrant des fonctions de reprise sur fautes et de recouvrement de fautes ("recoverable systems" en anglais, abrégés en "systèmes sûrs" pour les besoins de ce résumé). REVER se propose
de facliter la programmation de tels systèmes en adoptant une approche radicale, qui consiste à s'appuyer sur un modèle de programmation réversible. En gros, tous les mécanismes de reprise sur fautes ou de recouvrement de fautes ("recovery" en anglais) s'appuie peu ou prou sur la possibilté de renir à un état antérieur cohénret du système en cas de faute.
L'approche adoptée par REVER consiste à étudier les conséquences, en termes de programmation, de ce choix fondamental:
rendre réversible toute étape d'exécution d'un programme réparti
Plus précisément, il s'agit pour REVER d'étudier la possibilité de définir un ensemble d'abstractions de programmation, sémantiquement bien fondées et composables, en partant d'une base réversible, c'est-à-dire d'un modèle de programmation où il est possible de défaire, éventuellement pas à pas, toute exécution d'un programme de manière à le ramener à un état antérieur, cohérent avec l'exécution passée. L'hypothèse fondamentale que fait REVER est qu'en adoptant un tel substrat réversible, et qu'en le combinant avec des notions de compensation (pour prendre en compte des actions proprement irréversibles, par exemple toutes celles impliquant des effets réels dans le monde physique -- entrées/sorties)
et de modularité appropriées, il est en effet possible de développer des abstractions de programmation composables pour la programmation de systèmes sûrs.

Le programme de travail de REVER est articulé autour de trois objectifs principaux:

1. Etudier la sémantique de processus réversibles concurrents, en particulier les relations qui existent entre réversibilité et causalité, et les notions d'équivalence et de simulation entre processus réversibles.

2. Etudier la combinaison de notions de réversibilité, de compensation, d'isolation et de modularité pour obtenir des abstractions composables pour la programmation de systèmes sûrs.

3. Etudier l'introduction de telles abstractions au sein d'un langage de programmation réaliste (typiquement, orienté objet, fonctionnel), et leur implantation efficace dans un environnement multicoeur et réparti.

Le projet REVER s'étend sur 4 ans et est coordonné par l'INRIA. Les partenaires du projet sont: le CEA (équipe LIST/MeASI),
le laboratoire PPS (CNRS-U. Paris 7), et l'INRIA (équipes Focus et Sardes).