Skip to Main content Skip to Navigation
Theses

[ErgoFast] Amélioration de performances du solveur SMT Alt-Ergo grâce à l’intégration d’un solveur SAT efficace

Abstract : 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. In the team VALS of the LRI, we develop 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). In spite of our efforts in the design and the optimization of the implanted decision-making procedures, it appears that Alt-Ergo is slower than his competitors on certain benchmarks. The reasons are multiple. We identified three important causes. - The first one seems to be 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. But, the efficiency of these structures is generally worse than imperative structures. - The second seems to be connected to the memory management by the Garbage Collector of the language OCaml, which, 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, the third seems to be connected to the lack of optimizations of the OCaml compiler. Indeed, we noticed that the gap from performance between Alt-Ergo and some of his competitors (written mainly in C or C ++) was strongly reduced when we recompiled them by lowering the compiler optimization level.
Document type :
Theses
Complete list of metadatas

Cited literature [75 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/tel-02504894
Contributor : Abes Star :  Contact
Submitted on : Wednesday, March 11, 2020 - 10:14:07 AM
Last modification on : Monday, May 11, 2020 - 12:29:38 PM
Long-term archiving on: : Friday, June 12, 2020 - 2:04:03 PM

File

72492_COQUEREAU_2019_archivage...
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-02504894, version 1

Collections

Citation

Albin Coquereau. [ErgoFast] Amélioration de performances du solveur SMT Alt-Ergo grâce à l’intégration d’un solveur SAT efficace. Informatique et langage [cs.CL]. Université Paris-Saclay, 2019. Français. ⟨NNT : 2019SACLY007⟩. ⟨tel-02504894⟩

Share

Metrics

Record views

114

Files downloads

455