Explorez tous les épisodes du podcast Sciences du logiciel - Xavier Leroy
| Titre | Date | Durée | |
|---|---|---|---|
| Séminaire - Daan Leijen : Design and Compilation of Efficient Effect Handlers in the Koka Language | 14 Mar 2024 | 00:55:15 | |
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 Séminaire - Daan Leijen : Design and Compilation of Efficient Effect Handlers in the Koka Language Daan Leijen Microsoft Research | |||
| 08 - Structures de contrôle : de « goto » aux effets algébriques : 08 - Structures de contrôle : de « goto » aux effets algébriques : Logiques de programmes pour le contrôle et les effets | 14 Mar 2024 | 01:22:02 | |
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 08 - Structures de contrôle : de « goto » aux effets algébriques : 08 - Structures de contrôle : de « goto » aux effets algébriques : Logiques de programmes pour le contrôle et les effets | |||
| Séminaire - Caroline Collange : Comment concilier parallélisme et contrôle ? Approches des architectures de processeurs généralistes et graphiques | 08 Feb 2024 | 00:51:51 | |
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 Séminaire - Caroline Collange : Comment concilier parallélisme et contrôle ? Approches des architectures de processeurs généralistes et graphiques Caroline Collange Inria | |||
| 03 - Structures de contrôle : de « goto » aux effets algébriques : Chassez le contrôle... : la programmation déclarative | 08 Feb 2024 | 01:24:14 | |
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 03 - Structures de contrôle : de « goto » aux effets algébriques : Chassez le contrôle... : la programmation déclarative | |||
| 02 - Structures de contrôle : de « goto » aux effets algébriques : Structures de contrôle avancées : des subroutines aux coroutines et au parallélisme | 01 Feb 2024 | 01:15:22 | |
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 02 - Structures de contrôle : de « goto » aux effets algébriques : Structures de contrôle avancées : des subroutines aux coroutines et au parallélisme | |||
| 01 - Structures de contrôle : de « goto » aux effets algébriques : Naissance des structures de contrôle : du « goto » à la programmation structurée | 25 Jan 2024 | 01:19:00 | |
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 01 - Structures de contrôle : de « goto » aux effets algébriques : Naissance des structures de contrôle : du « goto » à la programmation structurée | |||
| Séminaire - Pierre-Etienne Meunier : Une algèbre de modifications, ou : le contrôle de versions pour tous | 20 Apr 2023 | 01:00:30 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Séminaire - Pierre-Etienne Meunier : Une algèbre de modifications, ou : le contrôle de versions pour tous | |||
| 07 - Structures de données persistantes : À la recherche du vecteur perdu : limites théoriques et conclusions | 20 Apr 2023 | 01:25:35 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes À la recherche du vecteur perdu : limites théoriques et conclusions Jusqu'à quel point une structure de données persistante peut être efficace ? Y a-t-il forcément un surcoût par rapport à une structure transiente ? Le dernier cours essaiera de répondre à ces questions, d'abord en passant en revue les meilleures implémentations connues des tableaux persistants, purement fonctionnelles ou non, puis en étudiant les bornes inférieures sur l'efficacité des modèles de calcul « LISP pur » et « LISP impur » établies par Ben-Armarm, Galil, et Pippenger. | |||
| Séminaire - Arthur Charguéraud : Comment allier persistance et performance | 13 Apr 2023 | 00:49:43 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Séminaire - Arthur Charguéraud : Comment allier persistance et performance Cet exposé explore trois approches permettant d'optimiser les performances de programmes exploitant des structures persistantes. La première approche consiste à optimiser les structures purement fonctionnelles en augmentant l'arité des feuilles et des nœuds des arbres. La deuxième approche consiste à exploiter les effets de bords pour réaliser la persistance. La troisième approche consiste à modifier l'interface en autorisant des versions transitoires non persistantes, selon la technique dite de « transience ». Je montrerai comment mettre en pratique ces trois approches sur des diverses structures : piles, files, tableaux, et séquences sécables et concaténables. | |||
| 06 - Structures de données persistantes : De la dérivation formelle à la navigation dans une structure : contextes, zippers, index, etc. | 13 Apr 2023 | 01:17:58 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes De la dérivation formelle à la navigation dans une structure : contextes, zippers, index, etc. Il est souvent utile de pouvoir désigner une partie d'une structure de données (par exemple, un sous-arbre d'un arbre) et opérer sur cette partie de manière locale. Dans les algèbres de termes, cela se modélise à l'aide de contextes. Cependant, les « zippers » de Huet, une présentation duale des contextes, permet de se déplacer dans un terme de manière algorithmiquement efficace. Nous verrons comment les types des contextes et des zippers s'obtiennent systématiquement à partir d'un type algébrique en utilisant les mêmes règles que pour la dérivation de fonctions à une variable. Nous ferons ensuite le lien entre zippers et index (« fingers »), une technique algorithmique classique pour tenir à jour des pointeurs à l'intérieur d'un arbre. | |||
| Séminaire - KC Sivaramakrishnan : Mergeable Replicated Data Types | 07 Apr 2023 | 00:53:36 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Séminaire - KC Sivaramakrishnan : Mergeable Replicated Data Types Replicated data types (RDTs) are specialised data structures that allow for concurrent modification of multiple replicas, even when they are geographically dispersed, without requiring coordination between them. However, constructing efficient and correct RDTs is challenging due to the complexity involved in reasoning about independently evolving states of replicas and resolving conflicts between them. In this talk, I will introduce Mergeable Replicated Data Types (MRDTs), a practical approach to constructing and verifying RDTs that is both efficient and correct. MRDTs build on the concept of a distributed version control system like Git, but extend it to arbitrary data types rather than just files. The key idea is to make sequential data types suitable for distribution by equipping them with a three-way merge function that reconciles conflicting versions. I will discuss how this merge function captures the complexities of distribution, simplifying both implementation and verification. Furthermore, I will discuss the critical role played by persistent data structures in MRDTs, as well as the inherent trade-off between persistence and efficiency in distributed data stores. | |||
| 05 - Structures de données persistantes : Systèmes de numération et types non réguliers | 07 Apr 2023 | 01:16:49 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Systèmes de numération et types non réguliers Un système de numération permet de représenter efficacement de grands nombres en donnant des poids différents aux chiffres successifs (par exemple, 1, 10, 100, 1 000, etc.). Cette idée inspire aussi la conception de structures persistantes remarquablement efficaces, notamment pour les listes à accès direct et les files de priorité. Nous décrirons ensuite l'utilisation de types algébriques non réguliers pour implémenter de telles structures de manière plus simple et mieux contrôlée par le typage. Nous terminerons par l'étude des « finger trees » de Hinze et Paterson, une structure polyvalente qui applique plusieurs de ces techniques. | |||
| Séminaire - Matija Pretnar : Effect handlers and mathematically inspired language constructs | 07 Mar 2024 | 01:03:47 | |
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 Séminaire - Matija Pretnar : Effect handlers and mathematically inspired language constructs Matija Pretnar Université de Ljubljana | |||
| Séminaire - Jean-Christophe Filliatre : Structures de données semi-persistantes | 30 Mar 2023 | 00:50:01 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Séminaire - Jean-Christophe Filliatre : Structures de données semi-persistantes | |||
| 04 - Structures de données persistantes : Comment rendre persistante une structure impérative ? | 30 Mar 2023 | 01:17:05 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Concilier amortissement et persistance : de l'importance de la paresse Dans ce cours, nous nous intéresserons aux structures de données persistantes dont l'implémentation utilise « sous le capot » des structures impératives et de la mutation en place, tout en préservant une interface purement fonctionnelle. Nous partirons des tableaux fonctionnels de Baker, qui combinent un tableau impératif et des liste de différences, puis introduirons progressivement la technique des « fat nodes » de Driscoll, Sarnak, Sleator et Tarjan, qui donne un procédé systématique pour rendre persistante une structure d'arbre impérative. | |||
| Séminaire - Tobias Nipkow : Verification of functional data structures: Correctness and complexity | 23 Mar 2023 | 00:50:26 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Séminaire - Tobias Nipkow : Verification of functional data structures: Correctness and complexity The talk gives a brief overview of our book "Functional Algorithms, Verified!" and its approach to verifying not just correctness but also running time of a large collection of functional algorithms. Then, two examples are presented in more detail: real time queues and double-ended queues that are implemented purely functionally with the help of stacks and whose operations have guaranteed constant running time. | |||
| 03 - Structures de données persistantes : Concilier amortissement et persistance : de l'importance de la paresse | 23 Mar 2023 | 01:17:22 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Concilier amortissement et persistance : de l'importance de la paresse L'amortissement est un principe de conception de structures de données qui vise à garantir un coût moyen par opération sur toute séquence d'opérations, le coût élevé de certaines opérations étant amorti par le coût faible d'opérations précédentes. Après un rappel des principes de l'amortissement et de l'analyse en temps amorti, le cours montrera des exemples de structures de données persistantes qui ont une complexité O(1) à condition d'être utilisées de manière linéaire. Nous étudierons ensuite l'approche d'Okasaki pour concilier amortissement et persistance générale (non linéaire), utilisant l'évaluation paresseuse (à la demande) de certains calculs. | |||
| 02 - Structures de données persistantes : Arbres équilibrés + copie de branches = persistance | 16 Mar 2023 | 01:24:38 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Arbres équilibrés + copie de branches = persistance Copier et modifier une branche d'un arbre équilibré, tout en partageant les sous-arbres non modifiés avec l'arbre d'origine, est une technique simple et générale pour construire de nombreuses structures de données persistantes ayant des complexités O(log n). Le cours montrera cette technique à l'œuvre sur des structures de type « dictionnaire » : arbres de recherche, arbres préfixes, arbres préfixes avec hachage (HAMT), arbres de Braun, etc. | |||
| 01 - Structures de données persistantes : Introduction aux structures persistantes et à la programmation purement fonctionnelle | 09 Mar 2023 | 01:17:41 | |
Xavier Leroy Collège de France Science du logiciel Année 2022-2023 Structures de données persistantes Introduction aux structures persistantes et à la programmation purement fonctionnelle Ce premier cours décrira l'émergence des structures de données persistantes dans deux contextes historiques différents : l'émergence des langages de programmation purement fonctionnels et de leurs approches équationnelles de dérivation et de vérification des programmes, d'une part, et de l'autre l'apparition de besoins nouveaux, notamment en algorithmique géométrique, de partager efficacement les représentations en mémoire de plusieurs structures de données qui diffèrent en peu de points. Nous verrons au passage nos premiers exemples de structures persistantes, à base de listes, d'arbres binaires, ou de tableaux avec historiques de modifications. | |||
| 07 - Sécurité du logiciel : quel rôle pour les langages de programmation ? | 21 Apr 2022 | 01:04:07 | |
Xavier Leroy Collège de France Science du logiciel Année 2021-2022 Sécurité du logiciel : quel rôle pour les langages de programmation ? Compiler un programme source en code machine peut être l'occasion de le rendre plus résistant à certaines attaques. Cependant, de nombreuses optimisations de compilation, pourtant sémantiquement correctes, peuvent affaiblir la sécurité du programme. Nous verrons comment caractériser ces différences de sécurité entre un fragment de programme source et son code compilé à l'aide d'outils sémantiques classiques : l'équivalence observationnelle et le problème de la full abstraction. Nous présenterons quelques approches qui ont été proposées pour compiler tout en préservant les équivalences observationnelles. | |||
| 06 - Sécurité du logiciel : quel rôle pour les langages de programmation ? | 14 Apr 2022 | 01:18:48 | |
Xavier Leroy Collège de France Science du logiciel Année 2021-2022 Sécurité du logiciel : quel rôle pour les langages de programmation ? Compiler un programme source en code machine peut être l'occasion de le rendre plus résistant à certaines attaques. Cependant, de nombreuses optimisations de compilation, pourtant sémantiquement correctes, peuvent affaiblir la sécurité du programme. Nous verrons comment caractériser ces différences de sécurité entre un fragment de programme source et son code compilé à l'aide d'outils sémantiques classiques : l'équivalence observationnelle et le problème de la full abstraction. Nous présenterons quelques approches qui ont été proposées pour compiler tout en préservant les équivalences observationnelles. | |||
| 05 - Sécurité du logiciel : quel rôle pour les langages de programmation ? | 07 Apr 2022 | 01:24:58 | |
Xavier Leroy Collège de France Science du logiciel Année 2021-2022 Sécurité du logiciel : quel rôle pour les langages de programmation ? Qu'il soit vérifié dynamiquement (pendant l'exécution) ou statiquement (par analyse préalable), le typage est un aspect essentiel des langages de programmation de haut niveau. Dans ce cours, nous étudierons les contributions du typage à la sécurité des logiciels, des garanties de base (sûreté des valeurs et de la mémoire) indispensables pour l'isolation logicielle à des garanties d'intégrité plus fines s'appuyant sur l'abstraction de types et l'encapsulation procédurale des valeurs. Nous parlerons aussi des ownership types et des assertions en logique de séparation, et de leurs utilisations possibles pour la sécurité. | |||
| 04 - Sécurité du logiciel : quel rôle pour les langages de programmation ? | 31 Mar 2022 | 01:09:58 | |
Xavier Leroy Collège de France Science du logiciel Année 2021-2022 Sécurité du logiciel : quel rôle pour les langages de programmation ? L'isolation d'un logiciel possiblement malveillant ou compromis est nécessaire pour qu'il ne puisse pas compromettre d'autres logiciels s'exécutant dans le même environnement et encore moins les mécanismes de sécurité du système d'exploitation et du matériel. Nous passerons en revue plusieurs mécanismes d'isolation : mémoire virtuelle, software fault isolation (SFI), sandboxing, et contrôle d'accès au niveau des interfaces logicielles (API). | |||
| 07 - Structures de contrôle : de « goto » aux effets algébriques : Typage et analyse statique des effets | 07 Mar 2024 | 01:19:07 | |
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 07 - Structures de contrôle : de « goto » aux effets algébriques : Typage et analyse statique des effets | |||
| 03 - Sécurité du logiciel : quel rôle pour les langages de programmation ? | 24 Mar 2022 | 01:20:25 | |
Xavier Leroy Collège de France Science du logiciel Année 2021-2022 Sécurité du logiciel : quel rôle pour les langages de programmation ? L'isolation d'un logiciel possiblement malveillant ou compromis est nécessaire pour qu'il ne puisse pas compromettre d'autres logiciels s'exécutant dans le même environnement et encore moins les mécanismes de sécurité du système d'exploitation et du matériel. Nous passerons en revue plusieurs mécanismes d'isolation : mémoire virtuelle, software fault isolation (SFI), sandboxing, et contrôle d'accès au niveau des interfaces logicielles (API). | |||
| 02 - Sécurité du logiciel : quel rôle pour les langages de programmation ? | 17 Mar 2022 | 01:06:30 | |
Xavier Leroy Collège de France Science du logiciel Année 2021-2022 Sécurité du logiciel : quel rôle pour les langages de programmation ? Certaines informations sont plus confidentielles que d'autres, ou plus digne de confiance que d'autres. Après une introduction aux politiques de confidentialité de Bell-Lapadula et d'intégrité de Biba, nous étudierons comment contrôler les flux d'information à travers un programme, ou bien dynamiquement, ou bien statiquement à l'aide de systèmes de types ou de logiques de programmes. | |||
| 01 - Sécurité du logiciel : quel rôle pour les langages de programmation ? | 10 Mar 2022 | 01:20:21 | |
Xavier Leroy Collège de France Science du logiciel Année 2021-2022 Sécurité du logiciel : quel rôle pour les langages de programmation ? Comment rendre un logiciel résistant non seulement aux « bugs » et aux pannes involontaires, mais aussi aux attaques et à l'utilisation malveillante ? C'est le problème général de la sécurité du logiciel, que nous introduirons dans ce premier cours. Nous étudierons ensuite quelques attaques récentes et les vulnérabilités logicielles qu'elles exploitent. | |||
| 07 - Logiques de programmes : quand la machine raisonne sur ses logiciels | 15 Apr 2021 | 01:18:35 | |
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. | |||
| 06 - Logiques de programmes : quand la machine raisonne sur ses logiciels | 08 Apr 2021 | 01:29:00 | |
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. | |||
| 05 - Logiques de programmes : quand la machine raisonne sur ses logiciels | 01 Apr 2021 | 01:22:27 | |
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. | |||
| 04 - Logiques de programmes : quand la machine raisonne sur ses logiciels | 25 Mar 2021 | 01:21:15 | |
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. | |||
| 03 - Logiques de programmes : quand la machine raisonne sur ses logiciels | 18 Mar 2021 | 01:25:53 | |
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 troisième cours, nous avons étudié les structures de données et la vérification de programmes qui les manipulent. Les tableaux sont la plus ancienne des structures de données. Une extension simple de la logique de Hoare avec une règle pour l'affectation à un élément d'un tableau permet de spécifier et de vérifier de nombreux programmes utilisant des tableaux, comme par exemple les tris en place. Les pointeurs, aussi appelés références, permettent de représenter de nombreuses structures de données : graphes, listes chaînées, arbres... Un codage des pointeurs en termes de tableaux globaux, comme proposé par R. Burstall (1972) et développé par R. Bornat (2000), se révèle efficace pour vérifier des algorithmes opérant sur des graphes, mais très lourd pour les algorithmes sur les listes et autres structures chaînées. En effet, il est difficile d'éviter les situations de partage, d'alias et d'interférence qui peuvent invalider ces structures. C'est en cherchant à décrire et maîtriser ces phénomènes d'interférence que J. C. Reynolds, rejoint ensuite par P. O'Hearn et H. Yang, invente entre 1997 et 2001 la logique de séparation. Cette logique met en avant l'importance du raisonnement local et des règles d'encadrement associées, le besoin d'associer une empreinte mémoire à chaque assertion, et le concept de conjonction séparante entre assertions. Nous avons illustré l'approche en développant une logique de séparation pour un petit langage fonctionnel et impératif doté de variables immuables et de pointeurs vers des cases mémoires mutables. Cette logique de séparation permet de décrire très précisément de nombreuses structures de données par des prédicats de représentation : listes simplement ou doublement chaînées, listes circulaires, arbres, etc., et de spécifier et vérifier leurs principales opérations. Enfin, nous avons esquissé deux démonstrations de la correction sémantique de cette logique de séparation, l'une reposant sur une propriété de non-déterminisme de l'allocation mémoire ; l'autre, sur une quantification sur tous les encadrements possibles. | |||
| 02 - Logiques de programmes : quand la machine raisonne sur ses logiciels | 11 Mar 2021 | 01:22:36 | |
Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Le deuxième cours a été consacré à l'étude approfondie des « logiques de Hoare », c'est-à-dire des logiques de programmes qui suivent l'approche introduite par C. A. R. Hoare en 1969. Nous avons défini une telle logique de programmes pour le langage IMP, un petit langage impératif à contrôle structuré que nous avions déjà étudié dans le cours 2019-2020 « Sémantiques mécanisées ». Nous avons ensuite développé diverses extensions de cette logique : règles de raisonnement dérivées ou admissibles, non-déterminisme, erreurs dynamiques, contrôle non structuré, etc. La suite du cours a étudié les liens entre la logique de programmes et la sémantique opérationnelle du langage IMP. Nous avons défini et démontré la correction sémantique de la logique : toutes les propriétés d'un programme dérivables par les règles de la logique sont bien vérifiées par toutes les exécutions concrètes du programme. Plusieurs techniques de démonstration ont été esquissées : inductives, co-inductives, ou encore par comptage de pas (step-indexing). La complétude est la propriété réciproque de la correction sémantique : toute propriété vraie de toutes les exécutions d'un programme peut-elle s'exprimer comme un triplet de Hoare et se dériver par règles de la logique ? Une logique complète permettrait de décider le problème de l'arrêt. La complétude absolue est donc impossible pour un langage Turing-complet. En revanche, la logique de Hoare satisfait une propriété de complétude relative montrant qu'elle est aussi expressive qu'un raisonnement direct sur les exécutions des programmes, à logique ambiante fixée. Enfin, nous avons discuté des possibilités d'automatiser une vérification déductive à base de logique de Hoare. À condition de fournir manuellement les invariants des boucles, un calcul de plus faible précondition, ou de plus forte postcondition, permet de réduire la vérification d'un programme en logique de Hoare à la vérification d'un ensemble d'implications en logique du premier ordre, tâche qui peut être confiée à des démonstrateurs automatiques ou assistés. | |||
| 01 - Logiques de programmes : quand la machine raisonne sur ses logiciels | 04 Mar 2021 | 01:14:46 | |
Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Résumé Comment s'assurer qu'un logiciel fait ce qu'il est censé faire ? Les méthodes classiques de vérification et de validation du logiciel, reposant sur le test, les revues et les analyses, ne suffisent pas toujours. La vérification déductive permet d'aller plus loin en établissant des propriétés vraies de toutes les exécutions possibles d'un programme, via des raisonnements formels au sein d'une logique appropriée : une logique de programmes. Le premier cours a illustré cette approche par la vérification déductive d'une fonction de recherche dichotomique dans un tableau trié, un algorithme très utilisé et souvent implémenté de manière incorrecte. Ensuite, le cours a retracé l'émergence de la vérification déductive et des logiques de programmes via trois publications fondatrices. La brève communication d'Alan Turing en 1949, intitulée « Checking a large routine », introduit deux idées majeures : les assertions logiques et les ordres de terminaison, et les illustre sur la vérification d'un petit programme exprimé par un organigramme. Trop en avance sur son temps, et jamais publié formellement, ce texte précurseur tombe dans l'oubli jusqu'en 1984. L'article de Robert W. Floyd de 1967, « Assigning meanings to programs », réinvente l'approche de Turing et l'approfondit considérablement, avec une formalisation complète des conditions de vérification qui garantissent qu'un programme est correctement annoté, et l'observation, révolutionnaire pour l'époque, qu'une telle formalisation constitue une sémantique formelle du langage de programmation utilisé. Enfin, l'article de C. A. R. Hoare de 1969, intitulé « An axiomatic basis for computer programming », constitue le manifeste de la vérification déductive moderne. L'article étend les résultats de Floyd à un langage à contrôle structuré (séquences, conditionnelles, boucles) et introduit des notations toujours utilisées aujourd'hui (les « triplets de Hoare »). Mais, au-delà des contributions techniques, cet article est visionnaire tant par son approche purement axiomatique de la vérification déductive que par son analyse lucide de l'intérêt pratique de cette approche. | |||
| Séminaire - Olivier Danvy : Les continuations : cinq minutes pour les apprendre, toute une vie pour les comprendre | 29 Feb 2024 | 00:58:48 | |
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 Séminaire - Olivier Danvy : Les continuations : cinq minutes pour les apprendre, toute une vie pour les comprendre Olivier Danvy National University of Singapore | |||
| 08 - Sémantiques mécanisées : quand la machine raisonne sur ses langages | 13 Feb 2020 | 01:11:02 | |
Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages | |||
| 07 - Sémantiques mécanisées : quand la machine raisonne sur ses langages | 06 Feb 2020 | 01:25:41 | |
Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages | |||
| 06 - Sémantiques mécanisées : quand la machine raisonne sur ses langages | 30 Jan 2020 | 01:16:42 | |
Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages | |||
| 05 - Sémantiques mécanisées : quand la machine raisonne sur ses langages | 16 Jan 2020 | 01:20:18 | |
Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages | |||
| 04 - Sémantiques mécanisées : quand la machine raisonne sur ses langages | 09 Jan 2020 | 01:57:58 | |
Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages | |||
| 03 - Sémantiques mécanisées : quand la machine raisonne sur ses langages | 19 Dec 2019 | 01:22:36 | |
Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages | |||
| 02 - Sémantiques mécanisées : quand la machine raisonne sur ses langages | 12 Dec 2019 | 01:20:43 | |
Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages | |||
| 01 - Sémantiques mécanisées : quand la machine raisonne sur ses langages | 28 Nov 2019 | 01:49:12 | |
Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages | |||
| 11 - Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | 30 Jan 2019 | 01:01:39 | |
Xavier Leroy Collège de France Science du logiciel Année 2018-2019 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | |||
| 10 - Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | 23 Jan 2019 | 01:07:55 | |
Xavier Leroy Collège de France Science du logiciel Année 2018-2019 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | |||
| 06 - Structures de contrôle : de « goto » aux effets algébriques : Théorie des effets : des monades aux effets algébriques | 29 Feb 2024 | 01:16:12 | |
Xavier Leroy Collège de France Science du logiciel Année 2023-2024 06 - Structures de contrôle : de « goto » aux effets algébriques : Théorie des effets : des monades aux effets algébriques | |||
| 09 - Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | 16 Jan 2019 | 01:08:57 | |
Xavier Leroy Collège de France Science du logiciel Année 2018-2019 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | |||
| 08 - Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | 09 Jan 2019 | 01:00:59 | |
Xavier Leroy Collège de France Science du logiciel Année 2018-2019 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | |||
| 07 - Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | 09 Jan 2019 | 01:00:14 | |
Xavier Leroy Collège de France Science du logiciel Année 2018-2019 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | |||
| 06 - Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | 19 Dec 2018 | 01:06:54 | |
Xavier Leroy Collège de France Science du logiciel Année 2018-2019 Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui | |||