Soutenance mémoire
Vers un solveur SAT efficace en OCaml
Bien que le solveur SAT historique d’Alt-Ergo ait été perfectionné au fur et à mesure des années, grâce au retour en arrière non chronologique et à une forme d’apprentissage lors des conflits, il n’utilise toujours pas de technique performante concernant le BCP. Des expérimentations préliminaires à cette thèse sur le solveur SAT d’AltErgo, nous ont permis de capitaliser sur les conclusions existantes pour guider nos premiers travaux. Ces travaux ont consisté en l’implémentation d’un solveur SAT CDCL [69] basé sur le solveur de référence Minisat [40] au sein d’Alt-Ergo. Cette implémentation a montré de moins bons résultats que le solveur historique d’Alt-Ergo par méthode des tableaux sur des exemples issus de la preuve de programme.
Méthodologie de comparaison
Notre but a été de comparer deux implémentations du solveur Minisat dans deux langages différents, le langage C++ et le langage OCaml. Le but étant de comparer les performances des deux langages, nous utiliserons les structures de données fournies par OCaml et gérées par son GC pour implémenter la version en OCaml. Les deux implémentations sont identiques en termes d’algorithme, et ne diffèrent que par le langage utilisé. Nous présenterons les différents points de comparaison ainsi que les paramètres et outils utilisés.
Trace de décision
Le premier point de comparaison fut celui des résultats des deux implémentations. Tel qu’énoncé auparavant, nous avons utilisé le même algorithme pour les deux implémentations afin d’avoir la comparaison la plus viable possible. Minisat étant principalement implémenté avec des structures bas niveau tel que des tableaux, il nous a été possible d’utiliser les mêmes structures de données offertes par OCaml pour implémenter la version en OCaml sans devoir apporter de modification à l’algorithme original. Pour nous assurer que ces deux implémentations fournissaient les mêmes résultats, nous avons utilisé des traces de résolution. Ces traces enregistrent les variables assignées par décision lors de l’exécution. Elles se présentent sous forme de fichier : la figure 3.1 est un exemple de fichier représentant une résolution où il y a eu cinq décisions. Le 1 représente la valeur de vérité vrai et 0 représente faux. Ces traces nous permettent de garantir que les deux algorithmes se comportent et produisent les mêmes résultats par comparaison de leurs fichiers de traces de décisions.
Consommation spatiale et temporelle
Le second point de comparaison est la différence de consommation spatiale et temporelle des deux implémentations. Nous présenterons les outils que nous allons utiliser pour analyser ces consommations avant de rappeler l’importance d’une bonne gestion du cache processeur.
Consommation temporelle
Pour comparer nos deux implémentations en termes de consommation temporelle, nous allons utiliser la commande time qui nous permettra d’obtenir le temps mis par les différentes implémentations pour résoudre des problèmes donnés. Cette commande time permet de donner un temps précis sans alourdir l’exécution de la commande à mesurer.
Consommation mémoire
Pour la consommation spatiale, nous allons analyser les poids en RAM de nos implémentations. Un plus gros poids mémoire peut être synonyme de moins bonnes performances. Pour mesurer ces poids nous utiliserons l’outil Massif de Valgrind , il nous permettra de connaître la taille en mémoire au fur et à mesure de la résolution. Le graphique 3.2 nous présente une telle consommation avec l’outil Massif-visualizer. Cet outil nous permet d’analyser de manière graphique la consommation mémoire enregistrée par Massif. Le graphique renvoyé correspond à la consommation en mémoire par rapport au temps mesuré ici en intervalle entre chaque enregistrement des données par Massif. Une légende nous permet de différencier les courbes correspondant aux parties allouant le plus de mémoire au cours de l’exécution. Le graphique nous permet ici aussi de connaître l’instant où le maximum de mémoire a été consommé, 45,6 Mb.
Cache mémoire
Le cache mémoire est un espace de stockage de données tampon situé entre les registres du processeur et la RAM. Il permet de stocker des données récemment chargées depuis la RAM pour accélérer leur réutilisation. La figure 3.3 ² représente les différentes mémoires utilisées par un programme. Le haut de la pyramide représente les mémoires les plus rapides, les registres (Reg) et les caches mémoires. Les registres sont extrêmement rapides (de l’ordre du cycle machine) mais sont présents en nombre très réduit. Sur les architectures modernes il y a généralement trois niveaux de cache, le plus petit (L1) ne contient que 32 Ko de données et 32 Ko de code. C’est le seul stockage qui sépare code et données. Le deuxième niveau contient 256 Ko et le troisième peut contenir quant à lui un espace de l’ordre du méga-octet. Les temps d’accès de ces trois niveaux sont proches de 4 cycles pour le L1, 12 cycles pour le L2 et 40 cycles pour le L3 [50]. Les niveaux inférieurs de la pyramide présentent des mémoires de plus en plus volumineuses et de plus en plus lentes. On considère que le temps d’accès en RAM est de l’ordre d’une centaine de cycles.
Les chargements dans les caches s’effectuent par ligne (intervalles) de 64 octets (sur des architecture récentes) [50]. Dans le cas d’un chargement de la donnée à l’indice n d’un tableau d’entiers il y a de fortes chances que les cases adjacentes soient elles aussi présentes dans la ligne de cache. Le chargement d’une donnée en mémoire peut ainsi permettre de charger des données qui seront ultérieurement utiles (prefetch). Dans un souci de performances, il est donc intéressant que des données, qui seront utiles dans un laps de temps rapproché, soient proches au sein de la mémoire pour être chargées en même temps (localité). Pour l’analyse des performances des caches mémoire nous utiliserons des outils comme Perf et l’outil Cachegrind de Valgrind . Perf permet d’enregistrer les actions du processeur durant l’exécution d’un programme et d’obtenir un rapport de la forme présentée en figure 3.4. Ces résultats étant dépendants de la charge du CPU au moment de l’exécution, ils peuvent varier d’une exécution à l’autre (le cache de niveau L3 est partagé entre les applications). Nous utiliserons des moyennes sur plusieurs exécutions pour amortir les erreurs statistiques. Sur la figure 3.4 nous pouvons remarquer une liste d’événements ayant eu lieu au cours de l’exécution d’un programme. De haut en bas nous avons tout d’abord les lectures et les erreurs de lecture depuis le cache d’instruction, puis, depuis le cache de données. Pour le cache de données viennent s’ajouter les statistiques concernant l’écriture dans le cache. Ensuite nous avons ces mêmes statistiques sur le cache de plus haut niveau (LLC), ici un cache L3. On appelle erreur de cache tout chargement d’une donnée depuis un cache qui échoue car elle n’y est pas présente. Cela entraîne un chargement depuis le niveau de cache supérieur et ainsi de suite. Viennent ensuite les statistiques concernant le temps d’exécution, le nombre de cycles, le nombre d’instructions, les branchements et les erreurs de branchement sur les conditions.
Valgrind contrairement à Perf simule l’exécution du programme à analyser, permettant d’obtenir un résultat théorique précis au détriment du temps d’exécution ( 50 fois plus lent). À la fin de son exécution l’outil Cachegrind de Valgrind retourne à la manière de Perf un rapport concernant l’utilisation des caches mémoire . On y trouve les informations sur les chargements du cache d’instructions, puis celui de donnée au niveau L1 et enfin ceux sur le niveau de cache maximum, LL. rd et wr représentent respectivement les accès en lecture et écriture aux caches. Il enregistre aussi ce rapport sous forme d’un fichier qui peut être relu de manière graphique grâce au programme KCachgrind, comme sur la figure 3.6. On peut ainsi connaître l’utilisation des caches par fonctions, comme sur la figure 3.6, où les statistiques sont triées par fichier d’origine puis par fonction contenue dans ces fichiers. Le fichier et la fonction dont les erreurs de cache du dernier niveau sont analysées sont major_gc.c et mark_slice.
Paramètres
Compilateurs
Nous avons aussi décidé de paramétrer nos comparaisons grâce à différentes options de compilation offertes par les compilateurs des langages. Nous utiliserons pour cela le compilateur GCC pour le langage C++ et le compilateur de la distribution standard pour OCaml. Ces deux compilateurs proposent différents niveaux d’optimisation pouvant faire varier grandement les résultats. Bien qu’il ne fut pas développé pour obtenir les meilleures performances possibles mais plutôt la portabilité (système d’exploitation et architecture), GCC a au fil des années gagné en performance pour offrir aujourd’hui un code optimisé offrant d’excellentes performances. Les efforts d’optimisation du compilateur d’OCaml sont plus récents et moins avancés (projet Flambda) et il reste encore beaucoup de travail d’optimisation.
|
Table des matières
1 Introduction
1 Satisfiabilité booléenne
1.1 Résolution et exploration
1.2 Méthode des tableaux analytiques
2 Satisfiabilité Modulo Théories
2.1 Le solveur SMT Alt-Ergo
2.2 Le standard SMT-LIB 2
3 Contributions de la thèse
3.1 Étude des performances d’un solveur CDCL en OCaml
3.2 Intégration efficace d’un solveur CDCL dans un solveur SMT
3.3 Extension du standard SMT-LIB 2 avec du polymorphisme
3.4 Participation à la compétition SMT-COMP
4 Plan de la thèse
2 Le solveur Alt-Ergo
1 Architecture
1.1 Gestion paresseuse de la CNF
1.2 Solveur SAT historique d’Alt-Ergo
1.3 Gestion des théories et des termes quantifiés dans AltErgo
2 Le langage natif d’Alt-Ergo
I SAT et SMT solveur
3 Vers un solveur SAT efficace en OCaml
1 Méthodologie de comparaison
1.1 Trace de décision
1.2 Consommation spatiale et temporelle
1.3 Paramètres
2 Résultats expérimentaux
2.1 Impact du langage OCaml sur les performances
2.2 Pistes d’optimisation
2.3 SatML vs solveur historique d’Alt-Ergo
3 Conclusion
4 Intégration efficace d’un solveur CDCL dans Alt-Ergo
1 Première approche : assister le solveur historique d’Alt-Ergo
avec un solveur CDCL
2 CDCL(λ(T)) : CDCL modulo Tableau(T)
2.1 Réduction du modèle booléen par méthode des Tableaux
2.2 Formalisme
2.3 Terminaison, Correction, Complétude
3 Implémentation
3.1 Calcul paresseux de la pertinence
3.2 Calcul de pertinence par frontière
3.3 Gestion du modèle pour l’instanciation
4 Résultats expérimentaux
4.1 Comparaison des différents solveurs SAT
4.2 Impact du calcul de pertinence des littéraux
5 Conclusion
II SMT-LIB et SMT-COMP
5 Extension du standard SMT-LIB2 avec du polymorphisme
1 Extension polymorphe
1.1 Syntaxe
1.2 Typage
2 Implémentation
2.1 Création d’une bibliothèque “frontend” pour le langage
2.2 Intégration à Alt-Ergo
3 Résultats expérimentaux
3.1 Génération de bancs de tests avec l’outil Why3
3.2 Impact du polymorphisme
3.3 Alt-Ergo et les autres solveurs SMT
3.4 Conclusion
6 Participation à la compétition SMT-COMP
1 SMT-COMP
1.1 Les théories et logiques de la SMT-LIB 2
1.2 Bancs de tests de la communauté SMT
1.3 Règles de la compétition
2 Préparation pour la compétition
2.1 Amélioration des heuristiques
2.2 Implémentation d’une version distribuée d’Alt-Ergo
3 Résultats
4 Conclusion
7 Conclusion
Télécharger le rapport complet
