Master 2013 2014
psar
UnlockSat : vers un solveur SAT parallèle coopératif sur multi-coeurs.


Site :LIP6 Regal
Lieu :UMPC, 4 place Jussieu 75005 PARIS
Encadrant : Julien Sopena (Julien.Sopena@lip6.fr), Souheib Baarir (Souheib.Baarir@lip6.fr) et Julia Lawall (Julia.Lawall@lip6.fr).
Dates :01/02/2014 au 10/05/2014
Mots-clés : Parcours SAR, aussi pour STL


Description

UnlockSat : vers un solveur SAT parallèle coopératif sur multi-coeurs.

Pitch : La résolution de problèmes SAT se prête bien aux nouvelles architectures multi-coeurs, car ces problèmes se décomposent naturellement en sous-problèmes indépendants. Cependant pour obtenir de bonnes performances un solveur parallèle nécessite un mécanisme de partage d’information pour éviter aux différents threads de faire les mêmes erreurs. L’objet de ce stage est de réduire les coûts de synchronisation induit par ce mécanisme de partage, en travaillant tant sur l’implémentation de la synchronisation que sur les informations partagées.

Contexte : Avec l’intégration toujours plus grande, des systèmes informatiques dans des applications critiques (métro, voitures, centrales-nucléaires, blocs opératoires, etc), assurer la correction des programmes devient une nécessité. Si l’utilisation systématique de tests permet d’améliorer grandement la qualité des codes, elle ne peut réellement garantir leur correction. A l’inverse, les techniques dites de model-checking, qui vérifient la validité du workflow applicatif par rapport à une propriété donnée, permettent de garantir la validité des programmes. Parmis les techniques utilisées dans l’industrie, celles bassées sur la théorie de la satisfiabilité booléenne (SAT) tant à s’imposer, notament dans l’aéronotique.

La résolution de promblème SAT sur des modèles toujours plus complexes pose des problèmes de temps de calcul. L’utilisation d’architectures multi-coeurs a très vite semblé prometteuse car le problème se prête très bien à la parallélisation. En effet, en fixant la valeur de l’une des variables booléennes propositionnelles u on obtient deux nouveaux problèmes disjoints : l’un associé à la valeur u=vrai, l’autre découlant de u=faux. Ces deux nouveaux problèmes plus petits (puisque contenant une variable de moins) peuvent alors se résoudre indépendamment.

Cependant, les approches parallèles souffrent d’un problème de partage de l’information. En effet, l’isolation des threads de traîtement dans les parallélisations dites non collaboratives empêche le partage des connaissances. Ces derniers se retrouvent à faire les mêmes "erreurs". À l’opposé dans les approches dite collaboratives, le surcoût de synchronisation engendrée par le partage des structures de données limite l’intérêt de la parallélisation.

L’idée du projet UnlockSat, dans lequel s’inscrit ce stage, est de réaliser un solveur SAT parralèle colaboratif de façon à pouvoir bénéficier des techniques d’apprentissage de clause (clauses-learning) et ainsi à pouvoir concurrencer les solutions séquentielles ou des portfolios (différents solveurs en parallèle).

Objectif : Dans le cadre de ce projet, une permière version d’un solveur multi-threadé à été rélasier. Se basant sur le solveur séquentiel Glucose, elle a été pensée de façon à pouvoir intégrer les derniers algorithme de la littérature mais aussi de façon à limiter l’impact de la synchronisation. Si les résultats brutes se montrent très prometteurs (le prototype se classerai 3ème au dernier concourt international SAT Competition 2013 dans la catégorie Hard-Combinatorial Problems), ces premiers travaux ont aussi été l’occasion de mettre en évidence l’importance du partage des clauses. En effet, les bonnes performances obtenues avec les 8 coeurs de la compétition, ne se maintiennent pas, dès lors que l’on utilise les 40 coeurs de la machine de test.

L’objectif de ce stage est d’intégrer au prototype existant des mécanismes permettant de limiter le coût lié à la synchronisation. Plusieurs approches pourront être mis-en-oeuvre :

  • utilisation de structure wait-free ;
  • retardement du partage des clauses ;
  • selection dynamique des clauses partagées.

Pré-requis : Bon niveau en C++.