CASH

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.