04 - Logiques de programmes : quand la machine raisonne sur ses logiciels

Xavier LeroyCollège de FranceScience du logicielAnnée 2020-2021Logiques de programmes : quand la machine raisonne sur ses logicielsLes processeurs multicœurs sont un exemple d'architecture parallèle à mémoire partagée, où plusieurs unités de calcul travaillent simultanément sur une mémoire commune. La programmation de ces architectures est difficile : il faut maîtriser les interférences possibles entre les actions des processus, et éviter les courses critiques (race conditions) entre des écritures et des lectures simultanées.Quelles logiques de programmes nous permettent de vérifier des programmes parallèles à mémoire partagée ? Pour répondre à cette question, le quatrième cours a introduit la logique de séparation concurrente (Concurrent Separation Logic, CSL), une extension de la logique de séparation avec des règles de raisonnement sur le parallélisme et l'exclusion mutuelle.La logique de séparation décrit très simplement le calcul parallèle sans partage de ressources, où les processus s'exécutent en parallèle sur des portions disjointes de la mémoire. C'est le cas de nombreux algorithmes récursifs sur les tableaux ou sur les arbres, où les appels récursifs s'effectuent sur des sous-arbres ou sous-tableaux disjoints.La CSL, comme introduite par O'Hearn en 2004, ajoute des règles de raisonnement sur les sections critiques permettant à plusieurs processus d'accéder à des ressources partagées à condition que ces accès s'effectuent en exclusion mutuelle. Les ressources partagées sont décrites par des formules de logique de séparation qui doivent être invariantes en dehors des sections critiques. Cela permet de décrire non seulement de nombreux idiomes de synchronisation entre processus, mais aussi les transferts de ressources qui s'effectuent implicitement lors de ces synchronisations.Nous avons défini une CSL pour le petit langage du précédent cours enrichi de constructions décrivant le parallélisme et les instructions atomiques. Nous avons montré comment construire sur ce langage et cette logique des sémaphores binaires, des sections critiques, et des schémas producteur-consommateur. Enfin, nous avons montré la correction sémantique de cette CSL en reprenant une démonstration publiée par Vafeiadis en 2011.

Om Podcasten

Écrire un petit programme informatique est facile. Concevoir et réaliser un logiciel complet qui soit fiable, pérenne et résistant aux attaques reste extraordinairement difficile. C'est le but des sciences du logiciel que de concevoir et développer les principes, les formalismes mathématiques, les techniques empiriques et les outils informatiques nécessaires pour concevoir, programmer et vérifier des logiciels fiables et sécurisés.L'enseignement de la chaire Sciences du logiciel vise à explorer cette problématique et à présenter la recherche contemporaine dans ce domaine. Le cours privilégie les approches dites « formelles », par opposition à l'empirisme souvent de mise en génie logiciel. Ces approches s'appuient sur des fondements mathématiquement rigoureux, connus ou en émergence : sémantiques formelles, logiques de programmes, systèmes déductifs, équivalences de programmes, calculs de processus… Historiquement, ces concepts ont émergé de considérations de programmation très terre-à-terre avant de se parer de rigueur mathématique. Le cours s'efforce de retracer ce cheminement des idées en partant de l'intuition du programmeur et en allant jusqu'à la mécanisation de ces approches formelles.Les premières années de cet enseignement auraient pu s'intituler « Programmer, démontrer », car ils ont exploré plusieurs modes d'interaction entre la programmation de logiciels et la démonstration d'énoncés mathématiques : programmer puis démontrer, comme dans les logiques de programmes pour la vérification déductive ; programmer pour démontrer, comme dans les logiques constructives et l'assistant à la démonstration Coq ; enfin, programmer égale démontrer, comme dans la féconde correspondance de Curry-Howard, objet de la première année du cours.La recherche de la chaire Sciences du logiciel s'effectue dans le cadre de l'équipe-projet Cambium, commune avec l'Inria. Les travaux de l'équipe visent à améliorer la fiabilité, la sûreté et la sécurité du logiciel en faisant progresser les langages de programmation et les méthodes de vérification formelle de programmes. Les principaux thèmes de recherche sont les systèmes de types et les algorithmes d'inférence de types, la vérification déductive de programmes, le parallélisme à mémoire partagée, et les modèles mémoires faiblement cohérents. L'équipe conçoit et développe deux grands logiciels de recherche qui intègrent et font passer dans la pratique bon nombre de ses résultats : OCaml, un langage de programmation fonctionnel statiquement typé et son implémentation, et CompCert, un compilateur formellement vérifié pour logiciels embarqués critiques.