Sémantique localement abstraite, concrète globalement des langages de programmation concurrents

Une sémantique de langage de programmation formelle et mathématiquement rigoureuse est la condition essentielle pour la conception de logiques et de calculs qui permettent un raisonnement automatisé sur des programmes concurrents. Nous proposons une nouvelle sémantique modulaire conçue pour s'aligner harmonieusement avec les logiques de programme utilisées dans la vérification déductive et la spécification formelle des programmes concurrents. Notre sémantique sépare l'évaluation locale des expressions et des instructions effectuées dans un environnement abstrait et symbolique de leur composition en calculs globaux, moment où elles sont concrétisées. Cela permet l'ajout incrémental de nouveaux concepts de langage, sans nécessiter de réviser le cadre. La base est une généralisation de la notion de trace de programme en tant que séquence d'états évolutifs que nous enrichissons avec des descripteurs d'événements et des marqueurs de continuation. Cela permet de reporter les contraintes de planification du niveau de l'évaluation locale à l'étape de composition globale, où les prédicats de bonne formation sur la structure des événements caractérisent de manière déclarative un large éventail de modèles de parallélisme. Nous illustrons également comment une logique de programme et un calcul solides peuvent être définis pour cette sémantique.