Détail d'une fiche   Version PDF

CASH (SR0874DR)

Compilation et Analyse, Logiciel et Matériel

CASH (SR0838ER) →  CASH


Statut: Décision signée

Responsable : Matthieu Moy

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2024" : A2.1. Langages de programmation , A2.1.1. Sémantique des langages de programmation , A2.1.2. Programmation impérative , A2.1.4. Programmation fonctionnelle , A2.1.6. Programmation concurrente , A2.1.7. Programmation distribuée , A2.1.10. Langages dédiés , A2.1.11. Langages de preuve , A2.2. Compilation , A2.2.1. Analyse statique , A2.2.2. Modèles mémoire , A2.2.3. Gestion mémoire , A2.2.4. Architectures parallèles , A2.2.5. Environnements d'exécution , A2.2.6. GPGPU, FPGA... , A2.2.8. Génération de code , A2.3.1. Systèmes embarqués , A2.4. Méthodes formelles pour vérification, sureté, certification , A2.4.1. Analyse , A2.4.2. Model-checking , A2.4.3. Preuves , A2.5.3. Génie logiciel empirique , A2.5.4. Maintenance, évolution , A7.2. Logique , A7.2.1. Procédures de décision , A7.2.3. Assistants de preuve , A7.2.4. Formalisation mécanisée des mathématiques , A8.3. Géométrie, Topologie , A8.4. Calcul formel, calcul algébrique

Mots-clés de "B - Autres sciences et domaines d'application - 2024" : B3.1. Développement durable , B5.4. Microélectronique , B9.5.1. Informatique , B9.5.2. Mathématiques

Domaine : Algorithmique, programmation, logiciels et architectures
Thème : Architecture, langages et compilation

Période : 01/06/2019 -> 31/12/2025
Dates d'évaluation : 19/03/2020 ,

Etablissement(s) de rattachement : U. LYON 1 (UCBL), ENS LYON, CNRS
Laboratoire(s) partenaire(s) : LIP (UMR5668)

CRI : Centre Inria de Lyon
Localisation : Ecole normale supérieure de Lyon - Laboratoire de l'Informatique du Parallélisme (LIP)
Code structure Inria : 121019-0

Numéro RNSR : 201822804N
N° de structure Inria: SR0874DR

Présentation

L'objectif global de l'équipe CASH est de concevoir et de développer des moyens d'améliorer la qualité des logiciels. Nous travaillons à la fois sur des outils qui aident les programmeurs à écrire de meilleurs programmes et sur des compilateurs qui transforment ces programmes en exécutables efficaces. Le champ des applications ciblées est large, des applications HPC spécialisées sur les superordinateurs jusqu'à l'informatique généraliste, des applications massivement parallèles au code séquentiel, des langages fonctionnels au code impératif, etc. Nous nous concentrons principalement sur les logiciels, mais nous considérons également le matériel, à la fois comme une plateforme d'exécution pour les logiciels et comme un sujet de recherche (génération de matériel et analyse de circuits matériels). Ce qui relie toutes nos activités, c'est que notre objet d'étude est le programme informatique.

Par amélioration de la qualité, nous entendons à la fois la sécurité des programmes et l'efficacité de leur exécution. Nous fournissons notamment aux programmeurs de meilleures constructions de langage de programmation pour exprimer leur intention : des constructions qui leur donnent des garanties par construction telles que la sécurité de la mémoire, le déterminisme, etc. Lorsque les garanties ne peuvent pas être obtenues par construction, nous développons également des analyses statiques pour détecter les bogues ou pour prouver les conditions préalables nécessaires à l'application des transformations du programme. Nous utilisons ces garanties pour développer de nouvelles optimisations afin de générer un code efficace. Toutes ces contributions trouvent leur fondement et leur justification dans la sémantique des programmes. En outre, nous fournissons des simulateurs pour exécuter les programmes qui nécessitent une plate-forme d'exécution spécifique.

En ce qui concerne les constructions de programmation de haut niveau pour le parallélisme, nous développons une expertise spécifique dans les calculs asynchrones et l'élimination des conditions de course dans les programmes concurrents. Dans ce domaine, nous proposons de nouveaux paradigmes, mais nous contribuons également à la sémantique de ces programmes. Par exemple, nous concevons des moyens de spécifier la sémantique à l'aide d'interprètes monadiques et nous les utilisons pour étudier la correction des compilateurs.

Nous assurons des garanties de sûreté à la fois par des systèmes de types et des analyses, dans des contextes très différents : de la vérification de circuits électriques à la conception d'un nouveau système de modules pour OCaml. Comme cela est récurrent dans notre travail, nous adaptons de manière pragmatique l'approche à l'application pratique.

Nous concevons des transformations de code pour l'exécution efficace de programmes, en particulier pour le HPC. Nos contributions dans ce domaine étendent le modèle polyédrique pour le rendre applicable à une plus large gamme de programmes, et pour apporter son potentiel d'optimisation à de nouveaux types d'applications (tuiles paramétriques, structures éparses, ...). Nous concevons également des optimisations pour les données structurées telles que les arbres, ou plus généralement les types de données algébriques.


Axes de recherche

  • Conception de langages de programmation. L'équipe travaille sur des constructions de langages de programmation de haut niveau qui peuvent à la fois aider les programmeurs à écrire des programmes sans bogues et aider les compilateurs à générer des codes plus efficaces. Nous nous intéressons particulièrement aux programmes parallèles, mais nous fournissons également des outils pour les codes séquentiels.
  • Sémantique et preuves. Les prouveurs interactifs comme Rocq permettent d'écrire des preuves mathématiques vérifiées par des machines, ainsi que des programmes informatiques certifiés. Nous travaillons à la fois sur des outils pour l'écriture de meilleures preuves ou la formalisation de la sémantique, et sur l'application de ces outils en particulier pour la compilation certifiée.
  • Analyse et vérification de programmes. Nous concevons des analyses statiques expressives et performantes. Les analyses que nous concevons s'appliquent à la fois à l'optimisation des performances (en calculant les invariants utilisés par les compilateurs optimisants) et à la sûreté (en trouvant automatiquement les bogues ou en prouvant les propriétés de correction sur les programmes ou les circuits électriques).
  • Optimisations et transformations de programmes. Nous proposons plusieurs transformations automatiques de programmes afin d'améliorer leurs performances. Un cadre d'intérêt particulier pour l'équipe est le modèle polyédrique qui peut effectuer des optimisations très agressives pour des programmes impératifs réguliers.

Relations industrielles et internationales