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 : 2019
Beginning : 2015
Scientific productions :
- 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.
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.