Léo Stefanesco
Max Planck Institute for Software Systems
https://www.stefanesco.com/
Date(s) : 15/09/2022 iCal
11 h 00 min - 12 h 30 min
Le modèle le plus couramment utilisé pour étudier les programmes concurrents est celui de la cohérence séquentielle (SC), où les opérations des différents processus sont entrelacés. Ce modèle est trop strict en pratique, pour deux raisons : il est incompatible avec des optimisations courantes des compilateurs, et les processeurs modernes implémentent des modèles mémoires plus lâches, qu’on qualifie de « faibles ».
Cet exposé est un aperçu des formalisations axiomatiques de ces modèles, basés sur des graphes annotés ; ainsi que des logiques de programmes qui permettent de raisonner sur des programmes s’exécutant sur de telles mémoires.
Emplacement
Site Sud, Luminy, Ancienne BU, Salle Séminaire2 (RdC)
Catégories