Sujets de recherches actuels de la chaire « Algorithmes, machines et langages »

[Gérard Berry]

La recherche effectuée actuellement dans le cadre de la chaire concerne trois aspects : l’orchestration de services Web, la composition musicale et les nouvelles notations musicales pour la musique algorithmique, et la vérification formelle d’un noyau de compilation d’Esterel.

L’orchestration de services Web et d’objets connectés et traitée en collaboration avec l’équipe de Manuel Serrano à l’Inria Sophia-Antipolis. Les services Web sont des programmes disponibles sur des ordinateurs accessibles par Internet, avec lesquels on peut communiquer par le protocole http standard. Au lieu de rendre des pages HTML à afficher sur l’écran, ces services Web retournent des résultats directement interprétables par le programme appelant, réalisant ainsi un système général d’appel de procédures à distance sur le réseau. Les objets connectés (du smartphone à la maison en passant par la voiture) sont également accessibles de la même façon. Le système distribué engendré par les services et les objets connectés est fondamentalement asynchrone, mais accessible dans le modèle client-serveur assez simple fourni par le protocole http du Web. Notre travail s’appuie sur Hop, langage conçu par Manuel Serrano pour rendre beaucoup plus simple les traitements asynchrones. Hop remplace la tour de Babel des langages du Web par un langage unique qui permet d’écrire les programmes distribués sous forme d’un seul code source, puis de le compiler et distribué les fragments de code locaux dans les différents système où ces fragments doivent s’exécuter. Ceci ne suffit pas : il faut gérer de façon harmonieuse tous les événements associés aux communications réseau ou fournis par les objets connectés, ce qu’on appelle « orchestrer l’application ». Pour cela, une approche synchrone est idéale. Nous avons donc défini et implémenté la couche langage spécialisée HipHop à l’intérieur de Hop. Ce langage synchrone peut être vu comme une version très dynamique d’Esterel : si un avion a toujours deux ailes et trois trains de roues, les applications Web sont fondamentalement dynamiques, avec des composants pouvant apparaître ou disparaître à tout moment ou provoquer de nombreuses erreurs à l’exécution. Nous avons montré que la sémantique mathématique d’Esterel peut être préservée dans ce cadre dynamique, tout en gardant la possibilité de faire évoluer dynamiquement le texte même du programme HipHop entre deux réactions à des événements. Le principe de réaction synchrone permet en effet de séparer proprement les étapes de réactions aux événements des étapes de reconfiguration, ce qui ne peut pas se faire dans les formalismes asynchrones classiquement associés au Web. Tout ceci a été présenté dans le cours 2013-2014. Mais HipHop n’est pour l’instant qu’un prototype, et son développement doit être poursuivi dans le but d’un vrai passage à l’échelle.

Le second sujet concerne l’informatique musicale. Il est traité en collaboration avec des chercheurs et des compositeurs de l’IRCAM ainsi qu’avec Philippe Manoury, compositeur et professeur au conservatoire de Strasbourg. Les compositeurs de musique contemporaine travaillent depuis longtemps sur des musiques mixtes mêlant interprètes humains et sons électroniques. Jusqu’à une date récente, les parties électroniques étaient soit enregistrées, soit jouées en temps réel par l’ordinateur selon un tempo figé, que les interprètes humains étaient alors obligés de respecter. Le superbe travail de thèse d’Arshia Cont (chercheur à l’IRCAM) lui a permis de développer le système Antescofo de suivi prédictif de partitions. Ce système permet d’identifier en temps réel les différents événements écrits dans la partition (notes par exemple) et de comprendre puis dans une certaine mesure prévoir la façon dont les musiciens jouent : tempo, articulation, etc. Il devient alors possible d’asservir l’électronique aux interprètes et non l’inverse. D’importance évidente pour les compositeurs et interprètes, ce système est maintenant utilisé en concert partout dans le monde. Comme il détecte les événements en temps réel, il permet aussi de conditionner le lancement de parties électroniques complexes à la détection d’événement ou de suites d’événements. Se pose alors le problème de la notation de ces parties : l’ordinateur n’étant pas limité par ses capacités de lecture, il n’y a plus besoin d’égrener les notes sur des portées comme dans une partition classique. De plus, il est tout à fait possible d’introduire de l’aléatoire dans les parties électronique. La bonne façon de noter la musique doit alors évoluer vers une nouvelle notion de partition algorithmique, où les sons et leurs enchaînements sont engendrés par des algorithmes arbitrairement complexes. Un autre problème important est celui de la gestion des erreurs qui ne manquent pas de se produire à l’exécution, qu’elles soient des erreurs humaines des interprètes ou des erreurs du système de suivi en temps-réel. Tout ceci milite pour la création de langages algorithmiques dédiés à la musique. Un langage prototype largement fondé sur les concepts d’Esterel est actuellement développé pour Antescofo et déjà utilisé en concert. Mais il faudra aller beaucoup plus loin dans ce domaine fascinant et encore largement ouvert.

 Le sujet le plus récent est celui de la construction d’un compilateur prouvé du langage Esterel noyau vers des schémas de circuit électroniques. Il est l’objet du travail de post-doc de Lionel Rieg, ATER attaché à la chaire depuis septembre 2014. L’idée est de programmer conjointement le compilateur et sa preuve dans le système de vérification Coq, qui permettra ensuite d’extraire automatiquement un code Caml efficace pour le compilateur. Ce travail s’appuiera sur la sémantique formelle d’Esterel telle qu’établie par Gérard Berry puis améliorée par Olivier Tardieu au milieu des années 2000. Nous nous attendons à des difficultés sur des points fins de la traduction, comme dans toute aventure de ce type. L’intention est aussi d’utiliser ce travail comme exemple de preuve formelle dans les cours à venir, reliant ainsi le nouveau cours aux précédents dédiés aux langages synchrones