Amélioration de performances pour le solveur SMT Alt-Ergo
Début : automne 2015 |
Axis : ScilEx
Directors : Sylvain CONCHON, Fabrice LE FESSANT, Michel MAUNY
Institutions : LRI / INRIA Saclay / INRIA Rocquencourt / ENSTA - U2IS
Administrator laboratory : ENSTA
Phd Student : Albin COQUEREAU
Defense thesis : march 2019
Beginning : 2015
Scientific productions : Publication Thèse ErgoFast
The automatic SMT (Satisfiability Modulo Theories) solvers are more and more used in the industry and in the academic world. The reason of this success is connected on to the expressiveness of the languages of entrance of these solvers (first order logic with predefined theories), and on their increasing efficiency.
The speed of SMT solvers is mainly connected to the decision-making procedures which they implement (SAT solvers, Simplex, etc.). The data structures used and the memory management mechanisms have an immediate impact on the performances. Also, the programming language and the available optimizations of code in the compiler are very important.
The team VALS of the LRI develops the SMT solver Alt-Ergo. This tool is programmed with the language OCaml and it is mainly used to prove logical formulas from proof of program workshops as Why3, Spark, Frama-C or the B workshop. His direct competitors are z3 (Microsoft), CVC4 (Univ. New York and Iowa) and yices2 (SRI). This Phd aims at improving Alt-Ergo's performances.
Scientific challenge :
Several leads may help improving Alt-Ergo's performances :
- The first one is connected to the data structures used in the solver. For safety reason, the largest part of Alt-Ergo is developed in a purely functional style of programming with persistent structures. However, the efficiency of these structures is generally not as good as than imperative structures.
- The second has to do with the memory management by the Garbage Collector of the language OCaml. Compared with a manual management, engenders numerous movements of memory blocks and probably too many cache miss. The difference between cache memory access and RAM access being of the order of 150 clock cycles, the maximal use of the cache memory is very important for the performances.
- Finally, it should be possible to improve the optimization of the OCaml compiler. The gap from performance between Alt-Ergo and some of his competitors (written mainly in C or C ++) is indeed strongly reduced when we recompiled them by lowering the compiler optimization level.