Début : Automne 2015
Axe : SciLex
Sujet : conception d’outils d’analyse, optimisations et structures de données efficaces pour OCaml
Directors : Sylvain CONCHON, Fabrice LE FESSANT, Michel MAUNY
Institution : LRI / Inria Saclay & Rocquencourt / ENSTA – U2IS
Laboratoire gestionnaire : ENSTA
Doctorant : Albin COQUEREAU
Date de soutenance : 2019
Production scientifique :
- Conférence smt2018 : Alt-Ergo 2.2
- Speaker: Albin Coquereau
- Abstract: Alt-Ergo is an SMT solver jointly developed by Université Paris-Sud and the OCamlPro company. The first version was released in 2006. Since then, its architecture has been continuously adapted for proving formulas generated by software development frameworks. As type systems with polymorphism arise naturally is such platforms, the design of Alt-Ergo has been guided (and constrained) by a native — and non SMT-LIB compliant — input language for a polymorphic first-order logic. In this paper, we present the last version of Alt-Ergo, its architecture and main features. The main recent work is a support for a conservative polymorphic extension of the SMT-LIB 2 standard. We measure Alt-Ergo’s performances with this new frontend on a set of benchmarks coming from the deductive program verification systems Frama-C, SPARK 2014, Why3 and Atelier-B, as well as from the SMT-LIB benchmarks library.
Contexte :
Les démonstrateurs automatiques de la famille SMT (Satisfiability Modulo Theories) sont de plus en plus utilisés dans l’industrie et dans le monde académique. La raison de ce succès est liée d’une part à l’expressivité des langages d’entrée de ces solveurs (logique du premier ordre avec de nombreuses théories prédéfinies), et d’autre part, à leur efficacité toujours croissante.
La rapidité de ces solveurs est principalement liée aux procédures de décision qu’ils implémentent, comme les structures de données utilisées et les mécanismes de gestion mémoire. Le langage de programmation choisi et les optimisations de code disponibles dans le compilateur sont également très importants.
L’équipe VALS du LRI développe le solveur SMT Alt-Ergo. Programmé en langage Ocaml, cet outil est principalement utilisé pour prouver des formules logiques issues d’ateliers pour la preuve de programme comme Why3, Spark, Frama-C ou l’Atelier B.
Ce projet a pour objectif d’améliorer les performances du solveur SMT Alt-Ergo.
Objectif scientifique:
Plusieurs pistes devraient permettre d’augmenter les performance d’Alt-Ego.
- La première est liée aux structures de données utilisées dans le solveur. Pour des raisons de sûreté, la plus grande partie d’Alt-Ergo est développée dans un style de programmation purement fonctionnel avec des structures persistantes. Toutefois, l’efficacité de ces structures est en général moins bonne que des structures impératives.
- La deuxième concerne la gestion mémoire par ramasse-miettes du langage Ocaml. Comparée à une gestion manuelle, le ramasse-miette engendre de nombreux déplacements de blocs mémoire et quelques défauts de cache. La différence entre un accès à la mémoire cache d’un ordinateur et un accès à la RAM étant de l’ordre de 150 cycles d’horloge, l’utilisation maximale de la mémoire cache est très importante pour les performances.
- Une dernière possibilité consisterait à optimiser le compilateur OCaml.
Perspectives :
Les deux objectifs principaux sont, d’une part, une plus grande utilisation du démonstrateur Alt-Ergo dans le monde industriel, et d’autre part, la production d’un outil d’analyse de performance pour OCaml, complément à l’outil d’analyse de la mémoire dévelopé par Çagdas Bozman et très attendu par les utilisateurs de ce langage. Par ailleurs, une amélioration significative des performances d’Alt-Ergo permettrait d’envisager une participation à la compétition internationale SMT-Comp.
Albin COQUEREAU 
Albin Coquereau à étudié l’informatique à l’université de Nantes où il a obtenu sa licence puis à L’université de Paris Sud pour son Master.
En 2014 il effectue un semestre d’étude à l’université de Quebec à Montréal. À son retour il effectue un stage au sein de l’Inria sous la direction de Fabrice le Fessant sur l’analyse du graphe mémoire d’application OCaml.
En 2015 il commence sa thèse “ErgoFast Amélioration de performances pour le solveur SMT Alt-Ergo : conception d’outils d’analyse, optimisations et structures de données efficaces pour OCaml” sous la direction de Michel Mauny et de Sylvain Conchon.