You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
206 lines
18 KiB
206 lines
18 KiB
\section{Implémentation}
|
|
|
|
Toute notre implémentation s'est faite en utilisant le langage OCaml. On supposera ici que le lecteur est familier de ce langage.
|
|
|
|
\subsection{Implémentation naïve}
|
|
\subsubsection{Types}
|
|
On commence par se donner un type représentant les diagrammes de décision binaires:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/naive_type.ml}
|
|
|
|
Un diagramme de décision binaire est soit \texttt{True} soit \texttt{False} soit un noeud étiqueté par un entier et ayant deux fils qui sont eux-mêmes des diagrammes de décision binaire.
|
|
\subsubsection{Ordre sur les variables}
|
|
On se donne un ordre sur les variables:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/naive_order.ml}
|
|
|
|
Pour comparer deux diagrammes de décision binaire, on se contentera ensuite de récupérer leur image par \texttt{get\_order} et d'utiliser la comparaison sur les entiers d'OCaml.
|
|
\subsubsection{Smart constructor, fonctions auxiliaires et constantes}
|
|
On introduit ensuite un \emph{smart constructor} permettant de créer un nouveau sommet:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/naive_node.ml}
|
|
|
|
On garantit à travers lui le respect de l'ordre et la non-redondance.
|
|
|
|
On va introduire des fonctions \texttt{view} et \texttt{fview}, inutiles pour le moment, mais que l'on modifiera ensuite, cela permettra de ne pas avoir à redéfinir d'autres fonctions.
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/naive_view.ml}
|
|
|
|
On définit deux constantes correspondant à $\top$ et $\bot$:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/naive_truefalse.ml}
|
|
|
|
\subsubsection{Fonctions sur les diagrammes}
|
|
On peut alors ensuite définir l'équivalent des fonctions propositionnelles sur nos diagrammes de décision binaires, par exemple la négation:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/naive_neg.ml}
|
|
|
|
Pour les fonctions $\mathbb{B}^2 \rightarrow \mathbb{B}$, on va commencer par définir des fonctions d'ordre supérieur \texttt{comb\_comm} et \texttt{comb} qui permettent de définir un opérateur respectivement commutatif et quelconque à partir d'une fonction booléenne d'OCaml, seul le code de la version commutative est donné ici, l'autre ne servant que pour définir l'implication:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/naive_comb.ml}
|
|
|
|
On peut alors facilement définir plusieurs des opérateurs de la logique propositionnelle:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/naive_defop.ml}
|
|
|
|
On a donc de quoi construire des diagrammes ordonnés et non-redondants. Il reste alors à implémenter la propriété d'unicité.
|
|
|
|
\subsection{Implémentation du partage physique}
|
|
|
|
La démarche expliquée ici repose sur celle présentée dans \cite{ConchonFilliatre06}. Le concept principal est celui du \emph{hashconsing}, ou partage maximal.
|
|
|
|
Elle est surtout utile lorsqu'on a affaire à des structures de données récursives. Le but est d'être capable de ne jamais recréer deux fois la même valeur en mémoire, tout en préservant la sûreté des types d'OCaml et en utilisant une approche modulaire.
|
|
|
|
L'idée principale est la suivante. Lorsque l'on veut créer une valeur, on regarde si on a déjà une valeur équivalente en mémoire et si oui, on réutilise cette dernière.
|
|
|
|
\subsubsection{Modèle d'exécution d'OCaml}
|
|
En OCaml, les valeurs sont soit des entiers, soit des pointeurs vers des entiers, c'est par exemple aussi le cas en Java. Les entiers permettent en effet d'encoder divers types. Ainsi, contrairement à ce qui peut se faire en C, une structure ou une valeur d'un type récursif ne sont jamais copiés entièrement lors de l'appel d'une fonction, on ne passe qu'un pointeur vers notre valeur, ou bien la valeur elle-même si l'ensemble des valeurs qu'elle peut prendre peut être encodé sur un seul entier.
|
|
|
|
Pour notre type de diagramme de décision binaire, on peut par exemple imaginer que la valeur \texttt{False} est un entier valant $0$, \texttt{True} un entier valant $1$ et \texttt{Node (v, l, h)} un pointeur vers une structure contenant successivement un pointeur vers les trois valeurs $v$, $l$ et $h$.
|
|
|
|
Pour distinguer si une valeur est un pointeur ou non, OCaml utilise une technique quelque peu particulière. En fait, les valeurs ne sont pas codées sur $32$ ou $64$ bits, mais sur $31$ ou $63$, le bit restant servant à distinguer les pointeurs.
|
|
\subsubsection{Hashconsing basique}
|
|
On commence par définir une fonction \texttt{hc} qui va regarder si on a déjà construit une valeur. Si oui, on renverra donc cette valeur déjà construite. Sinon, on l'ajoute à la table et l'on renvoie cette valeur. L'égalité utilisée est celle par défaut, c'est-à-dire l'égalité structurelle d'OCaml, il en va de même pour la fonction de hachage, une fonction générique fournie par OCaml est utilisée.
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/hc.ml}
|
|
|
|
Ainsi, on peut redéfinir les fonctions définies précedemment afin de garantir que toutes nos valeurs passent par notre fonction \texttt{hc}:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/hc_node.ml}
|
|
|
|
Ce faisant, on peut garantir que pour deux valeurs $x$ et $y$ auxquelles on a appliqué le hashconsing, on a:
|
|
|
|
\[ x = y \Leftrightarrow x == y \]
|
|
|
|
On pourrait alors maintenant remplacer l'égalité structurelle par l'égalité physique dans notre fonction \texttt{hc}, le temps de comparaison ne dépendrait alors plus de la taille de notre valeur - c'est un type récursif - mais serait constant.
|
|
|
|
OCaml permet de faire cela simplement, il suffit d'instancier un module en utilisant le foncteur de table de hachages fourni par OCaml:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/hc_phy_eq.ml}
|
|
|
|
La ligne avec le commentaire \texttt{(1)} n'est pas valide en OCaml, il faudrait simplement utiliser un autre nom pour le type, seulement, pour des raisons de clarté, on garde le même ici, le type \texttt{t} du côté droit faisant référence à celui définit précédemment. On redéfinit ensuite notre fonction \texttt{hc} ainsi:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/hc_bis.ml}
|
|
\subsubsection{Surêté du typage}
|
|
Si l'on travaille sur un type \texttt{t}, on veut pouvoir parler du type \texttt{t} sur lequel on a appliqué le \emph{hashconsing} comme étant un type différent. Une des raisons à cela est de s'assurer que le typechecker d'OCaml ne nous laisse pas mélanger des valeurs hashconsées avec d'autres qui ne le sont pas, ce qui signifierait qu'on aurait oublié d'appliquer le hashconsing à un endroit.
|
|
|
|
On va commencer par définir un type polymorphe \texttt{'a hash\_consed}:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/hc_type.ml}
|
|
|
|
Ainsi, une valeur $v$ de type $t$ après \emph{hashconsing} sera simplement l'enregistrement OCaml ayant son champ \texttt{node} valant $v$ et dotée d'un champ \texttt{tag} supplémentaire, lequel enregistrement aura le type $t~hash\_consed$. Le but du champ \texttt{tag} est donné ci-après.
|
|
\subsubsection{Hashconsing fonctorisé}
|
|
Pour pouvoir réutiliser notre implémentation du hashconsing et en faire une bibliothèque plutôt qu'un \emph{design pattern}, on va définir un foncteur \texttt{Make}, qui à partir d'un module ayant la signature \texttt{Hashtbl.HashedType} va produire un module ayant la signature suivante:
|
|
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/hc_sig.ml}
|
|
|
|
La fonction \texttt{create} permet à l'utilisateur de créer une nouvelle \enquote{table de hashconsing}, qui appliquée à la fonction \texttt{hashcons} produira une fonction permettant d'obtenir la version hashconsée de n'importe quelle valeur de type \texttt{H.t}.
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/hc_fonct.ml}
|
|
|
|
On en profite pour attribuer au champs \texttt{tag} une valeur unique, qu'on utilisera plus tard. Il faut aussi noter qu'on n'utilise plus deux fois \texttt{v}, mais une seule: en tant que valeur associée à une clé. On place notre type \texttt{'a hash\_consed} et notre foncteur \texttt{Make} dans un module appelé \texttt{Hashcons}. On peut alors obtenir une version hashconsée de nos diagrammes:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/hbdd.ml}
|
|
|
|
On a utilisé le champ \texttt{tag} pour fournir une fonction de hachage en temps constant ! Désormais, le hashconsing d'un diagramme se fait en temps constant. On peut alors redéfinir nos fonctions \texttt{view} et \texttt{hc} de la manière suivante:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/hc_hashcons.ml}
|
|
|
|
Toutes nos anciennes fonctions sur les diagrammes restent alors correctes !
|
|
|
|
\subsubsection{Hashconsing avec éphéméron}
|
|
|
|
En OCaml, la mémoire n'est pas gérée par le programmeur, mais par le \emph{garbage collector}. L'un des rôles du \emph{garbage collector} est de désallouer la mémoire lorsqu'elle n'est plus utilisée. Pour cela, l'une des techniques les plus simples\footnote{Qui n'est pas celle employée par le garbage collector d'OCaml.} il peut par exemple compter le nombre de pointeurs vers une valeur afin de savoir si celle-ci est toujours utilisée. Cela a l'avantage d'éviter de faire de nombreuses erreurs: fuites mémoires, double libération de pointeurs et autres réjouissances. Cela se fait au prix d'une baisse des performances.
|
|
|
|
Il y a aussi un second inconvénient au fait de passer par un \emph{garbage collector}. Si l'on crée une table de hachage dont les clés sont des pointeurs pour par exemple implémenter la mémoïsation d'une fonction, le fait d'avoir un pointeur dans notre table empêchera le garbage collector de libérer cette valeur.
|
|
|
|
Notre implémentation du hashconsing présente aussi ce problème ! Si un diagramme peut être libéré, il ne le sera pas parce qu'il est présent dans la table de hashconsing\ldots
|
|
|
|
Pour répondre à ce problème, une structure de donnée a été présentée dans \cite{Hayes97}: les éphémérons. % TODO: explain ephemerons.
|
|
Cette structure est plutôt générale. Ainsi, le cas particulier d'un éphéméron à une seule clé est en fait une \emph{weak hash-table}. Il s'agit d'une table de hachage dont les clés sont des pointeurs faibles. Un pointeur faible est un pointeur traité de manière spéciale par le garbage collector: si une valeur n'est accessible que par des pointeurs faibles, alors, le garbage collector pourra libérer la mémoire occupée par cette valeur. L'entrée correspondante dans la table sera alors supprimée.
|
|
|
|
% TODO: quote F. Bobot and JaneStreet
|
|
Les éphémérons ont été introduits dans OCaml $4.03$. Comme les tables de hachages, il en existe une interface fonctorisée, et il existe même un foncteur pour le cas particulier des \emph{weak hash-table}. On peut très simplement redéfinir notre foncteur \texttt{Hashcons} pour utiliser un éphéméron plutôt qu'une table de hachage:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/ephem.ml}
|
|
|
|
Il nous a suffit de changer quatre lignes pour y parvenir. L'implémentation présentée dans \cite{ConchonFilliatre06} datant d'avant l'introduction des éphémérons dans OCaml, une grande quantité de code y est nécessaire pour arriver au même résultat.
|
|
|
|
% =============== Mémo
|
|
\subsection{Mémoïsation}
|
|
|
|
On a gagné de la place en mémoire, en utilisant le partage physique, mais, on peut en fait faire \emph{beaucoup} mieux, en mémoïsant nos opérations sur les diagrammes.
|
|
|
|
Le concept de la mémoïsation est plutôt simple: avant de calculer le résultat de l'application d'une fonction à des arguments, on regarde si on a déjà appliqué la fonction à ces mêmes arguments, si oui, on utilise ces arguments, si non, on calcule le résultat et on l'ajoute à une table de hachage avec les arguments comme clé.
|
|
|
|
Il est en fait même possible de créer une fonction permettant de mémoïser n'importe quelle fonction, ce qui nous évite d'implémenter la mémoïsation pour chaque fonction.
|
|
|
|
On va donc créer une petite bibliothèque de mémoïsation possédant un foncteur:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/memo.ml}
|
|
|
|
En fait, cela permet à l'utilisateur de mémoïser n'importe quelle fonction mais en plus, en lui permettant de fournir lui-même les fonctions d'égalité et de hachage à utiliser. On ne donne ici que le code pour la version à un argument, le reste étant similaire et disponible dans le code complet. On place ce code dans un module nommé \texttt{MemoFunct}.
|
|
|
|
On peut alors l'instancier pour nos diagrammes:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/memobdd.ml}
|
|
|
|
Ce qui nous permet alors de mémoïser toutes nos fonctions précédentes, par exemple pour la fonction \texttt{neg}:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/neg_memo.ml}
|
|
|
|
Le corps de la fonction reste identique, seul le début change légèrement.
|
|
|
|
Le point intéressant est que la mémoïsation se fait elle aussi en temps constant: on utilise l'égalité physique pour comparer deux valeurs et on se contente de récupérer le champ \texttt{tag} pour hacher une valeur.
|
|
|
|
\subsection{Fonctorisation des implémentations précédentes}
|
|
|
|
Cette section mais surtout, le code associé, fait un usage intensif des foncteurs d'OCaml et de son système de modules. Le lecteur qui n'est pas familier avec ce système peut se reporter vers \cite{Leroy00} qui en fait une présentation détaillée. Il est important de noter que ce système de module est extrêmement puissant et permet beaucoup de choses. Il est d'ailleurs, en théorie, adaptable à n'importe quel langage pour lequel on dispose d'un \emph{typechecker}.
|
|
|
|
Afin de pouvoir mesurer l'impact sur l'usage mémoire et le temps de calcul du hashconsing et de la mémoïsation, on a créé un foncteur \texttt{Bdd.Make} paramétré par un module contenant un module de hashconsing et un module de mémoïsation.
|
|
|
|
On peut alors lui donner des \enquote{faux} modules de mémoïsation et de hashconsing, ou bien des vrais et ainsi obtenir quatre implémentations différentes à partir d'une seule.
|
|
|
|
Le code ne sera pas recopié ici, mais est disponible sur le dépôt du projet.
|
|
|
|
La chose la plus intéressante à noter a été la définition de la signature du module par lequel est paramétré notre foncteur:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/functsighard.ml}
|
|
|
|
On a dû définir le type \texttt{view} comme étant partiellement opaque: il dépend du type \texttt{hidden} mais impose les variants à fournir. Il n'est pas possible de faire autrement, sans quoi, le compilateur n'accepte pas le type, pensant qu'il est cyclique.
|
|
|
|
\subsection{SAT}
|
|
|
|
On peut utiliser nos diagrammes pour implémenter les fonctions classiques proposées par un SAT-solver. Cela se fait en effet de façon extrêment simple et efficace une fois le diagramme construit.
|
|
|
|
\subsubsection{\texttt{is\_sat}}
|
|
La fonction \texttt{is\_sat} qui indique si la formule propositionnelle représentée par un diagramme est satisfiable se fait par exemple en temps constant:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/is_sat.ml}
|
|
|
|
Si le diagramme est réduit à $\bot$, alors, la formule n'est pas satisfiable, sinon, soit il est réduit à $\top$ et est donc toujours satisfiable, soit il existe au moins une assignation des variables propositionnelles atomiques telle que la formule est satisfiable - sinon elle aurait été réduite à $\bot$. Ce problème, lorsqu'appliqué directement aux formules propositionnelles est $NP$-complet. Ici, toute la difficulté a été déportée vers la construction du diagramme.
|
|
|
|
\subsubsection{\texttt{any\_sat}}
|
|
La fonction \texttt{any\_sat} qui donne une assignation quelconque aux variables telle que la formule est vraie se fait aussi très simplement:
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/any_sat.ml}
|
|
|
|
On descend dans notre diagramme en prenant toujours la branche correspondant à l'assignation $\bot$ pour la variable courante. Si on a trouvé une assignation, alors, on l'utilise, sinon, on essaie avec l'autre branche, celle correspondant à $\top$. Si notre diagramme est réduit à $\bot$, alors on aura \texttt{None}, sinon, on aura forcément une assignation correcte.
|
|
|
|
\subsubsection{\texttt{all\_sat}}
|
|
|
|
La fonction \texttt{all\_sat} est identique, sauf qu'on parcourt toutes les branches et on garde l'ensemble des assignations valides.
|
|
|
|
\inputminted[bgcolor=darkBackground]{ocaml}{ml/all_sat.ml}
|
|
|
|
Il faut noter que l'on ne considère que les variables qui apparaissent dans la formule.
|
|
|
|
\subsubsection{\texttt{random\_sat}}
|
|
La fonction \texttt{random\_sat} est elle aussi similaire. Elle calcule la taille des deux sous-diagrammes, et va vers l'un ou l'autre de façon aléatoire avec une probabilité proportionnelle à la taille de chacun.
|
|
|
|
\subsubsection{\texttt{count\_sat}}
|
|
Le cas de \texttt{count\_sat} est un peu plus compliqué car l'utilisateur doit saisir le nombre de variables existantes. On utilise alors le fait que les variables sont ordonnées pour calculer à chaque fois le nombre de variables qui n'apparaissent pas dans la formule, et on multiplie correctement le nombre possible de solutions en faisant un peu d'arithmétique. On a ici aussi dû utiliser de la mémoïsation: en effet un sous-diagramme peut apparaître plusieurs fois dans notre parcours.
|
|
|
|
\subsection{Outils utilisés}
|
|
En plus du langage OCaml, plusieurs outils ont été utilisés pour notre implémentation: le \emph{build system} \href{https://dune.build}{Dune}, le générateur de parser \href{https://gallium.inria.fr/~fpottier/menhir/}{Menhir}, le framework de test \href{https://github.com/mirage/alcotest}{alcotest}, \href{https://github.com/aantron/bisect_ppx}{bisect\_ppx} pour la couverture du code et enfin, \href{https://github.com/LexiFi/landmarks}{landmarks} pour le profilage du code. Merci à leurs auteurs.
|
|
|