Arguments cadencés dans un compilateur Lustre vérifié

Lustre est un langage synchrone pour programmer des systemes avec des schemas-blocs desquels un code imperatif de bas niveau est genere automatiquement. Des travaux recents utilisent l'assistant de preuve Coq pour specifier un compilateur d'un noyau de Lustre vers le langage Clight de CompCert pour ensuite generer du code assembleur. La preuve de correction de l'ensemble relie la semantique de flots de Lustre avec la semantique imperative du code assembleur. Chaque flot dans un programme Lustre est associe avec une « horloge » statique qui represente ses instants d'activation. La compilation transforme les horloges en des instructions conditionnelles qui determinent quand les valeurs associees sont calculees. Les travaux precedents faisaient l'hypothese simplificatrice que toutes les entrees et sorties d'un bloc partagent la meme horloge. Cet article decrit une facon de supprimer cette restriction. Elle exige d'abord d'enrichir les regles de typage des horloges et le modele semantique. Ensuite, pour satisfaire le modele semantique de Clight, on ajoute une etape de compilation pour assurer que chaque variable passee directement a un appel de fonction a ete initialisee.