72 episodes

Xavier Leroy a étudié les mathématiques puis l'informatique à l'École Normale Supérieure et à l'Université Paris Diderot. Après un doctorat en informatique fondamentale en 1992 et un postdoctorat à l'Université Stanford, il devient chargé de recherche à l'Inria en 1994, puis directeur de recherche en 2000. Il y a dirige aujourd’hui l'équipe de recherche GALLIUM. De 1999 à 2004, il participe à la start-up Trusted Logic. Il est nommé Professeur au Collège de France en mai 2018 et devient le titulaire de la chaire Sciences du logiciel.

Les travaux de recherche de Xavier Leroy portent d'une part sur les nouveaux langages et outils de programmation, et d’autre part sur la vérification formelle de logiciels critiques afin de garantir leur sûreté et leur sécurité. Il est l'architecte et l’un des principaux développeurs du langage de programmation fonctionnelle OCaml et du compilateur C formellement vérifié CompCert, deux grands logiciels issus de la recherche.

Sciences du logiciel - Collège de France Collège de France

    • Education

Xavier Leroy a étudié les mathématiques puis l'informatique à l'École Normale Supérieure et à l'Université Paris Diderot. Après un doctorat en informatique fondamentale en 1992 et un postdoctorat à l'Université Stanford, il devient chargé de recherche à l'Inria en 1994, puis directeur de recherche en 2000. Il y a dirige aujourd’hui l'équipe de recherche GALLIUM. De 1999 à 2004, il participe à la start-up Trusted Logic. Il est nommé Professeur au Collège de France en mai 2018 et devient le titulaire de la chaire Sciences du logiciel.

Les travaux de recherche de Xavier Leroy portent d'une part sur les nouveaux langages et outils de programmation, et d’autre part sur la vérification formelle de logiciels critiques afin de garantir leur sûreté et leur sécurité. Il est l'architecte et l’un des principaux développeurs du langage de programmation fonctionnelle OCaml et du compilateur C formellement vérifié CompCert, deux grands logiciels issus de la recherche.

    • video
    06 - Logiques de programmes : quand la machine raisonne sur ses logiciels - VIDEO

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

    Xavier Leroy
    Collège de France
    Science du logiciel
    Année 2020-2021
    Logiques de programmes : quand la machine raisonne sur ses logiciels

    Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes.

    La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.

    La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.

    Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.

    La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.

    Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

    • 1 hr 29 min
    06 - Logiques de programmes : quand la machine raisonne sur ses logiciels

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

    Xavier Leroy
    Collège de France
    Science du logiciel
    Année 2020-2021
    Logiques de programmes : quand la machine raisonne sur ses logiciels

    Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes.

    La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.

    La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.

    Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.

    La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.

    Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

    • 1 hr 29 min
    • video
    05 - Logiques de programmes : quand la machine raisonne sur ses logiciels - VIDEO

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

    Xavier Leroy
    Collège de France
    Science du logiciel
    Année 2020-2021
    Logiques de programmes : quand la machine raisonne sur ses logiciels

    Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes.

    La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.

    La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.

    Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.

    La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.

    Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

    • 1 hr 22 min
    05 - Logiques de programmes : quand la machine raisonne sur ses logiciels

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

    Xavier Leroy
    Collège de France
    Science du logiciel
    Année 2020-2021
    Logiques de programmes : quand la machine raisonne sur ses logiciels

    Dans le cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes.

    La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint de la conjonction séparante, au même titre que l'implication usuelle est l'adjoint de la conjonction usuelle. Cette « baguette magique » facilite le raisonnement en logique de séparation, notamment via la règle de conséquence ramifiée ou via un calcul de plus faibles préconditions.

    La deuxième extension permet de vérifier des processus qui partagent des données mais y accèdent en lecture seule, sans modifications. Il s'agit d'associer des permissions aux cellules de la mémoire, ces permissions pouvant être partielles (permettant uniquement la lecture) ou complètes (permettant aussi l'écriture et la libération). Deux modèles bien connus de permissions partielles sont les permissions fractionnaires et les permissions comptées. Nous avons illustré l'utilisation de ces dernières pour vérifier un verrou à lecteurs multiples implémenté par deux sémaphores.

    Le « code fantôme » est la troisième technique étudiée dans cette séance. Il s'agit de commandes qui ne sont pas exécutées dans le programme final, mais contribuent à définir des « variables fantômes » qui simplifient la vérification. Dans le cadre du calcul parallèle, code et variables fantômes permettent de garder trace des calculs faits par chacun des processus et comment ces calculs individuels contribuent à l'exécution globale du programme.

    La dernière extension que nous avons décrite permet de stocker en mémoire des verrous et leur invariant de ressources, tout comme les données protégées par ces verrous. Cela permet de spécifier et de vérifier des algorithmes parallèles à grain fin, comme nous l'avons illustré avec une structure de liste simplement chaînée avec verrouillage couplé.

    Aussi disparates qu'elles peuvent sembler, ces extensions et bien d'autres sont des cas particuliers d'un petit nombre de notions plus générales, comme le montre l'infrastructure logique Iris.

    • 1 hr 22 min
    • video
    04 - Logiques de programmes : quand la machine raisonne sur ses logiciels - VIDEO

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

    Xavier Leroy
    Collège de France
    Science du logiciel
    Année 2020-2021
    Logiques de programmes : quand la machine raisonne sur ses logiciels

    Les 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.

    • 1 hr 21 min
    04 - Logiques de programmes : quand la machine raisonne sur ses logiciels

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

    Xavier Leroy
    Collège de France
    Science du logiciel
    Année 2020-2021
    Logiques de programmes : quand la machine raisonne sur ses logiciels

    Les 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.

    • 1 hr 21 min

Top Podcasts In Education

Listeners Also Subscribed To

More by Collège de France