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.
 
 
 
 
 

46 lines
7.3 KiB

\section{Travail effectué durant le stage}
\subsection{Contexte scientifique du stage}
Ce stage s'inscrit dans le cadre du projet \href{http://www.agence-nationale-recherche.fr/?Projet=ANR-15-CE39-0009}{\bsc{d}ata\bsc{c}ert} de l'\href{http://www.agence-nationale-recherche.fr/}{\bsc{anr}}. Un des objectifs de ce projet est d'appliquer des méthodes formelles aux différents outils utilisés en informatique traitant principalement des \emph{données}. En effet, jusqu'à présent, peu de travaux impliquant les méthodes formelles ont été effectués sur les deux outils principaux utilisés pour gérer des données en informatique, à savoir, les \bsc{s}ystèmes de \bsc{g}estion de \bsc{b}ases de \bsc{d}onnées (\bsc{sgbd}) et le langage principal utilisé pour communiquer avec eux depuis un autre programme: \bsc{sql}. Pourtant, \href{https://www.domo.com/blog/data-never-sleeps-4-0/}{le volume de données échangé dans le monde ne cesse de croître}.
\subsection{\bsc{sql}}
Le langage \bsc{sql} a été le point de départ du stage. Il a tout d'abord fallu écrire un \emph{parser} \bsc{sql} en \bsc{oc}aml, tout d'abord avec \href{https://caml.inria.fr/pub/docs/manual-ocaml/lexyacc.html#sec296}{\bsc{oc}amllex} et \href{http://gallium.inria.fr/~fpottier/menhir/}{\bsc{m}enhir}.
Ensuite, il a suffi de modifier quelques lignes pour pouvoir utiliser le générateur de parser certifié intégré à \bsc{m}enhir, utilisé dans \href{http://compcert.inria.fr/}{\bsc{c}omp\bsc{c}ert}, lequel a été initialement écrit par \href{https://jhjourdan.mketjh.fr/}{Jacques-Henri \bsc{Jourdan}}. Nous avons ainsi obtenu automatiquement un parser en \bsc{c}oq avec la preuve de correction — si le parser réussit, alors la phrase parsée
fait partie de la grammaire — et la preuve de complétude — si la grammaire n'est pas ambiguë, alors, si une phrase fait partie de la grammaire, le parser doit réussir.
Finalement, grâce à un code \bsc{oc}aml, il a été possible de modifier automatiquement l'\bsc{ast} obtenu pour qu'il corresponde à la syntaxe utilisée dans \bsc{sqlc}oq, une bibliothèque formalisant la sémantique de \bsc{sql} en \bsc{c}oq.
\subsection{Les plans d'exécution}
Interviennent alors les \emph{plans d'exécution}. En effet, \bsc{sql} étant un langage déclaratif — on décrit ce que l'on veut obtenir et non pas comment l'obtenir, contrairement à des langages tels que \bsc{c}, \bsc{j}ava ou \bsc{oc}aml — il est généralement utilisé conjointement avec un \bsc{sgbd}. Pour une requête \bsc{sql} donnée, c'est le \bsc{sgbd} qui va décider des algorithmes à utiliser pour aller récupérer sur le disque les données qui nous intéressent. On peut demander au \bsc{sgbd} de nous fournir un plan d'exécution de la requête, c'est-à-dire de nous indiquer les algorithmes qu'il va utiliser pour exécuter la requête. Par exemple, pour la requête \bsc{sql} suivante: % TODO: trouver un exemple où on voit mieux la différence entre sémantique de la requête et algorithmes utilisés pour l'exécuter...
\inputminted[bgcolor=darkBackground]
{sql}
{movie_01.sql}
On pourrait obtenir un plan comme celui-ci:
\inputminted[bgcolor=darkBackground]
{xml}
{movie_01.xml}
Cependant, il n'existe pas de standard portant sur les plans d'exécution, les \bsc{sgbd} les présentent de façon différente, utilisent leurs propres algorithmes, utilisent un nom différent pour un même algorithme, ne donnent pas la même quantité d'informations etc.
Après avoir étudié quelques plans fournis par quatre \bsc{sgbd}, à savoir \href{https://www.mysql.com/}{\bsc{m}y\bsc{sql}}, \href{https://www.sqlite.org/}{\bsc{sql}ite}, \href{https://www.oracle.com/index.html}{\bsc{o}racle \bsc{d}atabase} et \href{https://www.postgresql.org/}{\bsc{p}ostgre\bsc{sql}}, nous avons remarqué que seuls deux d'entre eux fournissaient des plans suffisamment complets pour pouvoir être utilisés ensuite, il s'agit d'\bsc{o}racle \bsc{d}atabase et de \bsc{p}ostgre\bsc{sql}.
J'ai alors dû écrire un parser pour les plans d'exécution fournis par \bsc{p}ostgre\bsc{sql} tandis qu'une autre personne faisait la même chose pour \bsc{o}racle \bsc{d}atabase. Ensuite, je me suis chargé de définir un format \emph{unifié} permettant de décrire les plans fournis par ces deux \bsc{sgbd} de la même façon. Il a ensuite fallu écrire deux programmes permettant de passer des \bsc{ast} obtenus en parsant les plans à ce nouveau format unifié ; ainsi qu'un parser pour les nouveaux plans respectant ce format unifié.
Ainsi, à partir d'une même requête \bsc{sql}, il est possible de la faire traiter par deux \bsc{sgbd} différents et d'obtenir deux plans d'exécution, parfois différents, mais respectant une syntaxe commune de description des plans.
\subsection{\bsc{e}xt\bsc{a}lg}
La sémantique d'une requête \bsc{sql} peut être exprimée au moyen de l'algèbre relationnelle. Avec \bsc{sqlc}oq, il est possible de relier une requête \bsc{sql} non pas à son équivalent en algèbre relationnelle, mais à son équivalent dans une algèbre étendue, appelée \bsc{e}xt\bsc{a}lg. Ainsi, pour pouvoir vérifier qu'un \bsc{sgbd}, lorsqu'il exécute une requête, préserve la sémantique de celle-ci, il fallait pouvoir comparer le plan engendré par celle-ci à son équivalent en \bsc{e}xt\bsc{a}lg. J'ai donc écrit un programme \bsc{oc}aml qui, à partir d'un plan, produit une expression d'\bsc{e}xt\bsc{a}lg lui correspondant. Dès lors, si l'on arrive à montrer l'équivalence entre l'expression fournie par \bsc{sqlc}oq à partir de la requête et l'expression obtenue à partir du plan fourni par le \bsc{sgbd}, on sait que le \bsc{sgbd} a bien préservé la sémantique de la requête. Un exemple de requête \bsc{sql}, du plan obtenu à partir de celle-ci et d'expression algébrique obtenue à partir du plan est donné dans l'annexe \hyperref[exemple-complet]{exemple complet}.
\bsc{E}xt\bsc{a}lg, tout comme l'algèbre relationnelle, manipule des relations, sur lesquelles on peut appliquer notamment le produit cartésien et l'opérateur $\omega$. L'opérateur $\omega$ prend en compte quatre paramètres: les éventuelles partitions, la projection et le renommage, les conditions de sélection et enfin, la relation sur laquelle on l'applique. Il est nécessaire d'ajouter des variables contenant une requête — requête qui n'est pas affichée en sortie pour des raisons de lisibilité — nommées $x_i$. De plus, ici, la requête est annotée avec des \emph{labels} et les noms des algorithmes venant du plan, afin de pouvoir plus tard, simuler l'exécution au moyen d'algorithmes écrits en \bsc{c}oq.
Il faut noter que certains \bsc{sgbd} ne fournissent pas toutes les informations nécessaires, \bsc{p}ostgre\bsc{sql}, par exemple, ne fournit aucune information sur l'équivalent des \emph{projections} dans les plans, ainsi, il a fallu être capable de retrouver l'information à partir de la requête originale, en attendant que le code de \bsc{p}ostgre\bsc{sql} soit modifié afin d'ajouter ces informations aux plans.
Finalement, il restait à prouver l'équivalence entre deux requêtes d'\bsc{e}xt\bsc{a}lg. Pour cela, j'ai commencé l'écriture d'un programme \bsc{oc}aml qui normalise une requête donnée, point de départ nécessaire pour pouvoir prouver l'équivalence de deux requêtes par d'autres équivalences connues et démontrées.