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
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.
|
|
|