The OCaml Planet

Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Séminaire du 15 février 2024 : Représentations intermédiaires pour la compilation : s'affranchir du graphe de flot de contrôle Intervenante : Delphine Demange, université de Rennes Le graphe de flot de contrôle est une représentation intermédiaire classique des programmes dans les compilateurs optimisants pour les langages impératifs. Cette représentation a permis de formuler et de développer de nombreuses optimisations de programmes, des plus simples jusqu'aux plus sophistiquées. Dans sa forme originelle, le graphe de flot de contrôle présente toutefois deux inconvénients pour optimiser les programmes. D’une part, beaucoup d'analyses de programmes sont sensibles au nommage des variables du programme. D'autre part, un modèle d’exécution entièrement dirigé par le contrôle rend parfois difficile le réordonnancement des instructions. Dans cet exposé, nous nous intéresserons à des représentations intermédiaires emblématiques qui visent à pallier ces inconvénients. La première, SSA, permet d'exposer, à travers un schéma spécifique de nommage, quelques relations de dépendances entre instructions. La seconde, Sea-of-Nodes, s'appuie sur SSA et relâche certaines contraintes d'ordre d'exécution au sein de régions du graphe. Issues de travaux de recherche, elles sont aujourd'hui utilisées avec succès dans des compilateurs optimisants de référence. Nous présenterons leur modèle d'exécution respectif, ainsi que leurs propriétés sémantiques clefs dans le cadre de l'optimisation de programmes. Enfin, nous présenterons quelques enjeux actuels du domaine, où des représentations intermédiaires similaires sont utilisées pour basculer dans un modèle d'exécution dirigé par les données. Retrouvez les enregistrements audios et vidéos du cycle et son texte de présentation : https://www.college-de-france.fr/fr/agenda/seminaire/structures-de-controle-de-goto-aux-effets-algebriques Chaire Sciences du logiciel Professeur : Xavier Leroy Retrouvez tous les enseignements du Pr Xavier Leroy : https://www.college-de-france.fr/chaire/xavier-leroy-sciences-du-logiciel-chaire-statutaire https://www.youtube.com/playlist?list=PLtimy8tnozICbD45yhB7Ha_zIBJTIK3im Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous. Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France. Découvrez toutes les ressources du Collège de France : https://www.college-de-france.fr Suivez-nous sur : Facebook : https://www.facebook.com/College.de.France Instagram : https://www.instagram.com/collegedefrance X (ex-Twitter) : https://twitter.com/cdf1530 LinkedIn : https://fr.linkedin.com/company/collègedefrance

Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Séminaire du 15 février 2024 : Représentations intermédiaires pour la compilation : s'affranchir du graphe de flot de contrôle Intervenante : Delphine Demange, université de Rennes Le graphe de flot de contrôle est une représentation intermédiaire classique des programmes dans les compilateurs optimisants pour les langages impératifs. Cette représentation a permis de formuler et de développer de nombreuses optimisations de programmes, des plus simples jusqu'aux plus sophistiquées. Dans sa forme originelle, le graphe de flot de contrôle présente toutefois deux inconvénients pour optimiser les programmes. D’une part, beaucoup d'analyses de programmes sont sensibles au nommage des variables du programme. D'autre part, un modèle d’exécution entièrement dirigé par le contrôle rend parfois difficile le réordonnancement des instructions. Dans cet exposé, nous nous intéresserons à des représentations intermédiaires emblématiques qui visent à pallier ces inconvénients. La première, SSA, permet d'exposer, à travers un schéma spécifique de nommage, quelques relations de dépendances entre instructions. La seconde, Sea-of-Nodes, s'appuie sur SSA et relâche certaines contraintes d'ordre d'exécution au sein de régions du graphe. Issues de travaux de recherche, elles sont aujourd'hui utilisées avec succès dans des compilateurs optimisants de référence. Nous présenterons leur modèle d'exécution respectif, ainsi que leurs propriétés sémantiques clefs dans le cadre de l'optimisation de programmes. Enfin, nous présenterons quelques enjeux actuels du domaine, où des représentations intermédiaires similaires sont utilisées pour basculer dans un modèle d'exécution dirigé par les données. Retrouvez les enregistrements audios et vidéos du cycle et son texte de présentation : https://www.college-de-france.fr/fr/agenda/seminaire/structures-de-controle-de-goto-aux-effets-algebriques Chaire Sciences du logiciel Professeur : Xavier Leroy Retrouvez tous les enseignements du Pr Xavier Leroy : https://www.college-de-france.fr/chaire/xavier-leroy-sciences-du-logiciel-chaire-statutaire https://www.youtube.com/playlist?list=PLtimy8tnozICbD45yhB7Ha_zIBJTIK3im Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous. Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France. Découvrez toutes les ressources du Collège de France : https://www.college-de-france.fr Suivez-nous sur : Facebook : https://www.facebook.com/College.de.France Instagram : https://www.instagram.com/collegedefrance X (ex-Twitter) : https://twitter.com/cdf1530 LinkedIn : https://fr.linkedin.com/company/collègedefrance

Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Cours du 15 février 2024 : Programmer ses structures de contrôle : continuations et opérateurs de contrôle Professeur : Xavier Leroy Chaire Sciences du logiciel Le quatrième cours a introduit la notion de continuation d'un point de programme dans un programme impératif, ou d'une sous-expression dans un programme fonctionnel. Il s'agit de la suite des calculs restant à effectuer pour atteindre la fin du programme, représentée soit par un objet du langage de programmation (commande, fonction, ...), soit par un objet mathématique. Dans les travaux de recherche des années 1965–1975 sur la sémantique dénotationnelle, les continuations apparaissent comme moyen de donner une sémantique mathématiquement précise aux branchements «goto» non locaux du langage Algol. Mais c'est dans le cadre des langages de programmation fonctionnelle que les continuations montrent tout leur intérêt : tout d'abord, pour spécifier complètement les stratégies de réductions (comme l'appel par valeur et l'appel par nom) par transformation systématique des programmes, pour les mettre en style à passage de continuations (CPS, Continuation-Passing Style); ensuite, pour programmer manuellement dans ce style à passage de continuations, ce qui permet de définir de nombreuses structures de contrôle avancées (itérateurs, générateurs, coroutines, threads coopératifs) dans le langage même, sous forme de bibliothèques. Enfin, l'ajout d'opérateurs de contrôle à un langage fonctionnel, comme le call/cc du langage Scheme, donne aux programmes de nouveaux moyens pour capturer, réifier et relancer leurs propres continuations, permettant ainsi de définir des structures de contrôle avancées dans le langage tout en gardant le programme en «style direct», sans mise en forme CPS manuelle. Retrouvez les enregistrements audios et vidéos du cycle et son texte de présentation : https://www.college-de-france.fr/fr/agenda/cours/structures-de-controle-de-goto-aux-effets-algebriques Retrouvez tous les enseignements du Pr Xavier Leroy : https://www.college-de-france.fr/chaire/xavier-leroy-sciences-du-logiciel-chaire-statutaire https://www.youtube.com/playlist?list=PLtimy8tnozICbD45yhB7Ha_zIBJTIK3im Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous. Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France. Découvrez toutes les ressources du Collège de France : https://www.college-de-france.fr Suivez-nous sur : Facebook : https://www.facebook.com/College.de.France Instagram : https://www.instagram.com/collegedefrance X (ex-Twitter) : https://twitter.com/cdf1530 LinkedIn : https://fr.linkedin.com/company/collègedefrance

Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Cours du 15 février 2024 : Programmer ses structures de contrôle : continuations et opérateurs de contrôle Professeur : Xavier Leroy Chaire Sciences du logiciel Le quatrième cours a introduit la notion de continuation d'un point de programme dans un programme impératif, ou d'une sous-expression dans un programme fonctionnel. Il s'agit de la suite des calculs restant à effectuer pour atteindre la fin du programme, représentée soit par un objet du langage de programmation (commande, fonction, ...), soit par un objet mathématique. Dans les travaux de recherche des années 1965–1975 sur la sémantique dénotationnelle, les continuations apparaissent comme moyen de donner une sémantique mathématiquement précise aux branchements «goto» non locaux du langage Algol. Mais c'est dans le cadre des langages de programmation fonctionnelle que les continuations montrent tout leur intérêt : tout d'abord, pour spécifier complètement les stratégies de réductions (comme l'appel par valeur et l'appel par nom) par transformation systématique des programmes, pour les mettre en style à passage de continuations (CPS, Continuation-Passing Style); ensuite, pour programmer manuellement dans ce style à passage de continuations, ce qui permet de définir de nombreuses structures de contrôle avancées (itérateurs, générateurs, coroutines, threads coopératifs) dans le langage même, sous forme de bibliothèques. Enfin, l'ajout d'opérateurs de contrôle à un langage fonctionnel, comme le call/cc du langage Scheme, donne aux programmes de nouveaux moyens pour capturer, réifier et relancer leurs propres continuations, permettant ainsi de définir des structures de contrôle avancées dans le langage tout en gardant le programme en «style direct», sans mise en forme CPS manuelle. Retrouvez les enregistrements audios et vidéos du cycle et son texte de présentation : https://www.college-de-france.fr/fr/agenda/cours/structures-de-controle-de-goto-aux-effets-algebriques Retrouvez tous les enseignements du Pr Xavier Leroy : https://www.college-de-france.fr/chaire/xavier-leroy-sciences-du-logiciel-chaire-statutaire https://www.youtube.com/playlist?list=PLtimy8tnozICbD45yhB7Ha_zIBJTIK3im Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous. Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France. Découvrez toutes les ressources du Collège de France : https://www.college-de-france.fr Suivez-nous sur : Facebook : https://www.facebook.com/College.de.France Instagram : https://www.instagram.com/collegedefrance X (ex-Twitter) : https://twitter.com/cdf1530 LinkedIn : https://fr.linkedin.com/company/collègedefrance

Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Séminaire du 8 février 2024 : Comment concilier parallélisme et contrôle ? Approches des architectures de processeurs généralistes et graphiques Intervenante : Caroline Collange, Inria Depuis la machine analytique de Babbage et Lovelace, le langage machine exécuté par les processeurs consiste typiquement en une succession d'instructions dans l'ordre. Mais une mise en œuvre efficace en matériel nécessite d'exécuter des instructions en parallèle. Deux approches sont suivies respectivement dans les processeurs généralistes et les processeurs graphiques pour combler ce fossé. Un cœur d'un processeur actuel maintient l'illusion d'une exécution séquentielle, mais traite en réalité plusieurs centaines d'instructions en vol, et les exécute dans le désordre. Ce jeu d'équilibriste repose sur de nombreux mécanismes matériels, dont la prédiction de branchements et le renommage de registres. Lire la suite : https://www.college-de-france.fr/fr/agenda/seminaire/structures-de-controle-de-goto-aux-effets-algebriques/comment-concilier-parallelisme-et-controle-approches-des-architectures-de-processeurs-generalistes Retrouvez les enregistrements audios et vidéos du cycle et son texte de présentation : https://www.college-de-france.fr/fr/agenda/seminaire/structures-de-controle-de-goto-aux-effets-algebriques Chaire Sciences du logiciel Professeur : Xavier Leroy Retrouvez tous les enseignements du Pr Xavier Leroy : https://www.college-de-france.fr/chaire/xavier-leroy-sciences-du-logiciel-chaire-statutaire https://www.youtube.com/playlist?list=PLtimy8tnozICbD45yhB7Ha_zIBJTIK3im Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous. Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France. Découvrez toutes les ressources du Collège de France : https://www.college-de-france.fr Suivez-nous sur : Facebook : https://www.facebook.com/College.de.France Instagram : https://www.instagram.com/collegedefrance X (ex-Twitter) : https://twitter.com/cdf1530 LinkedIn : https://fr.linkedin.com/company/collègedefrance

Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Séminaire du 8 février 2024 : Comment concilier parallélisme et contrôle ? Approches des architectures de processeurs généralistes et graphiques Intervenante : Caroline Collange, Inria Depuis la machine analytique de Babbage et Lovelace, le langage machine exécuté par les processeurs consiste typiquement en une succession d'instructions dans l'ordre. Mais une mise en œuvre efficace en matériel nécessite d'exécuter des instructions en parallèle. Deux approches sont suivies respectivement dans les processeurs généralistes et les processeurs graphiques pour combler ce fossé. Un cœur d'un processeur actuel maintient l'illusion d'une exécution séquentielle, mais traite en réalité plusieurs centaines d'instructions en vol, et les exécute dans le désordre. Ce jeu d'équilibriste repose sur de nombreux mécanismes matériels, dont la prédiction de branchements et le renommage de registres. Lire la suite : https://www.college-de-france.fr/fr/agenda/seminaire/structures-de-controle-de-goto-aux-effets-algebriques/comment-concilier-parallelisme-et-controle-approches-des-architectures-de-processeurs-generalistes Retrouvez les enregistrements audios et vidéos du cycle et son texte de présentation : https://www.college-de-france.fr/fr/agenda/seminaire/structures-de-controle-de-goto-aux-effets-algebriques Chaire Sciences du logiciel Professeur : Xavier Leroy Retrouvez tous les enseignements du Pr Xavier Leroy : https://www.college-de-france.fr/chaire/xavier-leroy-sciences-du-logiciel-chaire-statutaire https://www.youtube.com/playlist?list=PLtimy8tnozICbD45yhB7Ha_zIBJTIK3im Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous. Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France. Découvrez toutes les ressources du Collège de France : https://www.college-de-france.fr Suivez-nous sur : Facebook : https://www.facebook.com/College.de.France Instagram : https://www.instagram.com/collegedefrance X (ex-Twitter) : https://twitter.com/cdf1530 LinkedIn : https://fr.linkedin.com/company/collègedefrance

Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Cours du 8 février 2024 : Chassez le contrôle... : la programmation déclarative La programmation déclarative s'attache à décrire les résultats attendus du programme sans pour autant expliciter l'enchaînement des étapes de calcul élémentaires qui produisent ces résultats, au contraire de la programmation impérative classique. Avons-nous encore besoin de structures de contrôle dans les programmes déclaratifs ? Le troisième cours a tenté de répondre à cette question en prenant l'exemple de trois paradigmes de programmation déclarative : la programmation réactive synchrone (Lustre), la programmation purement fonctionnelle (Haskell, Scheme pur), et la programmation logique (Prolog). Les sémantiques des programmes écrits dans ces langages reposent sur des principes élégants mais qui ne suffisent pas pour garantir la terminaison et le coût (en temps, en espace) des exécutions d'un programme ; d'où l'importance, même dans un langage déclaratif, de donner aux programmeurs les moyens de contrôler la manière dont leurs programmes sont évalués. Nous avons mentionné trois de ces moyens : ajouter des opérations ad hoc comme la coupure en Prolog, spécifier les stratégies d'évaluation utilisées (comme l'appel par valeur en Scheme et l'appel par nécessité en Haskell), ou encoder la stratégie désirée dans le programme lui-même (par exemple en ajoutant des suspensions dans un programme Scheme). Professeur : Xavier Leroy Chaire Sciences du logiciel Retrouvez les enregistrements audios et vidéos du cycle et son texte de présentation : https://www.college-de-france.fr/fr/agenda/cours/structures-de-controle-de-goto-aux-effets-algebriques Retrouvez tous les enseignements du Pr Xavier Leroy : https://www.college-de-france.fr/chaire/xavier-leroy-sciences-du-logiciel-chaire-statutaire https://www.youtube.com/playlist?list=PLtimy8tnozICbD45yhB7Ha_zIBJTIK3im Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous. Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France. Découvrez toutes les ressources du Collège de France : https://www.college-de-france.fr Suivez-nous sur : Facebook : https://www.facebook.com/College.de.France Instagram : https://www.instagram.com/collegedefrance X (ex-Twitter) : https://twitter.com/cdf1530 LinkedIn : https://fr.linkedin.com/company/collègedefrance

Enseignement 2023-2024 : Structures de contrôle : de « goto » aux effets algébriques Cours du 8 février 2024 : Chassez le contrôle... : la programmation déclarative La programmation déclarative s'attache à décrire les résultats attendus du programme sans pour autant expliciter l'enchaînement des étapes de calcul élémentaires qui produisent ces résultats, au contraire de la programmation impérative classique. Avons-nous encore besoin de structures de contrôle dans les programmes déclaratifs ? Le troisième cours a tenté de répondre à cette question en prenant l'exemple de trois paradigmes de programmation déclarative : la programmation réactive synchrone (Lustre), la programmation purement fonctionnelle (Haskell, Scheme pur), et la programmation logique (Prolog). Les sémantiques des programmes écrits dans ces langages reposent sur des principes élégants mais qui ne suffisent pas pour garantir la terminaison et le coût (en temps, en espace) des exécutions d'un programme ; d'où l'importance, même dans un langage déclaratif, de donner aux programmeurs les moyens de contrôler la manière dont leurs programmes sont évalués. Nous avons mentionné trois de ces moyens : ajouter des opérations ad hoc comme la coupure en Prolog, spécifier les stratégies d'évaluation utilisées (comme l'appel par valeur en Scheme et l'appel par nécessité en Haskell), ou encoder la stratégie désirée dans le programme lui-même (par exemple en ajoutant des suspensions dans un programme Scheme). Professeur : Xavier Leroy Chaire Sciences du logiciel Retrouvez les enregistrements audios et vidéos du cycle et son texte de présentation : https://www.college-de-france.fr/fr/agenda/cours/structures-de-controle-de-goto-aux-effets-algebriques Retrouvez tous les enseignements du Pr Xavier Leroy : https://www.college-de-france.fr/chaire/xavier-leroy-sciences-du-logiciel-chaire-statutaire https://www.youtube.com/playlist?list=PLtimy8tnozICbD45yhB7Ha_zIBJTIK3im Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous. Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France. Découvrez toutes les ressources du Collège de France : https://www.college-de-france.fr Suivez-nous sur : Facebook : https://www.facebook.com/College.de.France Instagram : https://www.instagram.com/collegedefrance X (ex-Twitter) : https://twitter.com/cdf1530 LinkedIn : https://fr.linkedin.com/company/collègedefrance

This is the fourth video in a series about OCaml’s locals. It covers how the compiler infers what variables can be marked as local_ and it gives a glimpse into some compiler output that you can use to see the inferred modes on variables. I also explain how the compiler infers conversions between locals and globals and introduce *mode-crossing*, showing how ints can be both local and global. View instructions to get the compiler I use in this video: https://github.com/janestreet/opam-repository/tree/with-extensions

This is the fourth video in a series about OCaml’s locals. It covers how the compiler infers what variables can be marked as local_ and it gives a glimpse into some compiler output that you can use to see the inferred modes on variables. I also explain how the compiler infers conversions between locals and globals and introduce *mode-crossing*, showing how ints can be both local and global. View instructions to get the compiler I use in this video: https://github.com/janestreet/opam-repository/tree/with-extensions