zapashcanon
6 years ago
commit
38a370c798
27 changed files with 404 additions and 0 deletions
@ -0,0 +1,16 @@ |
|||
The ISC License (ISC) |
|||
===================== |
|||
|
|||
Copyright (c) 2017, Léo Andrès |
|||
|
|||
Permission to use, copy, modify, and/or distribute this software for any |
|||
purpose with or without fee is hereby granted, provided that the above |
|||
copyright notice and this permission notice appear in all copies. |
|||
|
|||
THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES |
|||
WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF |
|||
MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR |
|||
ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES |
|||
WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN |
|||
ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF |
|||
OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. |
|||
@ -0,0 +1,13 @@ |
|||
default: build clean |
|||
|
|||
build: |
|||
scripts/build.sh |
|||
|
|||
clean: |
|||
scripts/clean.sh |
|||
|
|||
test: |
|||
scripts/test.sh |
|||
|
|||
mrproper: clean |
|||
scripts/mrproper.sh |
|||
@ -0,0 +1,10 @@ |
|||
#!/usr/bin/env sh |
|||
|
|||
set -eu |
|||
|
|||
( cd "$(dirname "$0")"/../ |
|||
|
|||
xelatex -shell-escape src/internship-report-datacert.tex |
|||
xelatex -shell-escape src/internship-report-datacert.tex |
|||
xelatex -shell-escape src/internship-report-datacert.tex |
|||
) |
|||
@ -0,0 +1,9 @@ |
|||
#!/usr/bin/env sh |
|||
|
|||
set -eu |
|||
|
|||
( cd "$(dirname "$0")"/../ |
|||
|
|||
rm -f ./*.log ./*.tuc ./*.out ./*.aux ./*.toc ./*.pyg |
|||
|
|||
) |
|||
@ -0,0 +1,9 @@ |
|||
#!/usr/bin/env sh |
|||
|
|||
set -eu |
|||
|
|||
( cd "$(dirname "$0")"/../ |
|||
|
|||
rm -f ./*.pdf |
|||
|
|||
) |
|||
@ -0,0 +1,15 @@ |
|||
#!/usr/bin/env sh |
|||
|
|||
set -eu |
|||
|
|||
( |
|||
cd "$(dirname "$0")"/../ |
|||
|
|||
# Testing scripts |
|||
# shellcheck disable=SC2185 |
|||
find -O3 . -type f -name '*.sh' -exec shellcheck {} \; |
|||
# shellcheck disable=SC2185 |
|||
find -O3 . -type f -name '*.tex' -exec chktex -q --nowarn 26 --nowarn 15 --nowarn 17 {} \; |
|||
## shellcheck disable=SC2185 |
|||
# find -O3 . -type f -name '*.tex' -exec lacheck {} \; # TODO: fix lacheck so it's possible to disable some warnings which are incorrects... |
|||
) |
|||
@ -0,0 +1,65 @@ |
|||
\section{À propos des méthodes formelles} |
|||
|
|||
\subsection{Trouver l'erreur} |
|||
|
|||
Lorsqu'on exécute un programme informatique que l'on vient d'écrire, il est courant que le résultat ne soit pas celui que l'on souhaitait. Le plus souvent, cela est dû à une erreur dans le code source du programme, parfois dans les bibliothèques que l'on utilise, rarement dans le compilateur et presque jamais dans le matériel. |
|||
|
|||
Cela peut s'expliquer en partie par le fait que le compilateur est utilisé par un plus grand nombre d'utilisateurs que les bibliothèques, lesquelles sont elles-mêmes plus utilisées que notre programme. |
|||
|
|||
Faut-il alors attendre qu'un utilisateur de notre programme remarque un bug pour pouvoir le corriger ? Dans le cas des systèmes critiques — transports, énergie, santé etc. — il est impératif de pouvoir détecter les problèmes avant qu'ils ne se manifestent ; dans le cas des autres logiciels, on préfère aussi que cela soit le cas même si ce n'est pas une condition nécessaire. |
|||
|
|||
\subsection{Tests manuels et unitaires} |
|||
|
|||
Un des moyens de détecter les bugs, est tout simplement de \emph{tester} les programmes. Cela peut se faire à la main, mais cette façon de faire devient très vite fastidieuse dans le cas de gros programmes. On peut donc automatiser les tests. Les tests unitaires sont un exemple de tests automatisés, il s'agit par exemple d'écrire un ensemble de tests pour chacune des fonctions de notre programme. Une fois les tests écrits, on peut ainsi vérifier rapidement que le programme passe les tests, ce qui s'avère pratique lorsque l'on modifie le code du programme par exemple. |
|||
|
|||
Cependant, avec cette méthode, si l'on oublie un cas particulier dans nos tests, on aura l'impression que le programme est correct, alors qu'il ne l'est pas. Prenons par exemple cet algorithme écrit en \href{https://ocaml.org/index.fr.html}{\bsc{oc}aml} qui recherche l'entier maximum d'une liste supposée non-vide: |
|||
|
|||
\inputminted[bgcolor=darkBackground] |
|||
{ocaml} |
|||
{src/max_in_list.ml} |
|||
|
|||
Supposons que l'on ait écrit les tests suivants pour notre algorithme: |
|||
|
|||
\inputminted[bgcolor=darkBackground] |
|||
{ocaml} |
|||
{src/test_max_in_list.ml} |
|||
|
|||
Notre algorithme ne va échouer sur aucun des tests et l'on pourrait alors croire qu'il est correct. Ce n'est bien évidemment pas le cas. Si notre liste n'est composée que de nombres entiers négatifs, l'algorithme renverra $0$ dans tous les cas\textellipsis\ Le test suivant aurait pu détecter cela: |
|||
|
|||
\inputminted[bgcolor=darkBackground] |
|||
{ocaml} |
|||
{src/test_max_in_list_bis.ml} |
|||
|
|||
Une version correcte de l'algorithme serait: |
|||
|
|||
\inputminted[bgcolor=darkBackground] |
|||
{ocaml} |
|||
{src/max_in_list_correct.ml} |
|||
|
|||
On voit bien alors une des faiblesses des tests: on ne peut jamais être certain d'avoir pensé à tous les cas et on ne peut généralement pas tous les tester lorsqu'il y en a une infinité ou qu'ils sont trop nombreux. |
|||
|
|||
\subsection{Un exemple de méthode formelle} |
|||
|
|||
Il existe un autre ensemble de façons de procéder, que l'on appelle méthodes formelles. Ces méthodes permettent de vérifier que pour n'importe quel cas, on aura bien le comportement attendu. On peut par exemple exprimer le résultat attendu sous forme de formules logiques, puis, laisser un outil analyser notre programme et nous dire s'il satisfait bien ces formules. Le fait de décrire le comportement attendu sous forme de formules logiques est appelé la \emph{spécification}. |
|||
|
|||
Prenons l'exemple de recherche du maximum dans une liste d'entiers supposée non-vide. Avec $l$ la liste passée à notre fonction et $r$ son résultat, la spécification pourrait être la suivante: |
|||
|
|||
\[ \forall x \in l, r \geq x \] |
|||
|
|||
Si l'outil chargé de vérifier que notre programme satisfait bien cette formule nous affirme que la spécification est respectée, on a alors de fortes garanties sur la \emph{correction} de celui-ci, puisqu'en effet, on reste très général sur notre liste: on ne se réduit pas à quelques cas comme précédemment avec les tests. |
|||
|
|||
Cependant, si on y regarde de plus près, on s'aperçoit que le programme suivant satisfait aussi cette formule: |
|||
|
|||
\inputminted[bgcolor=darkBackground] |
|||
{ocaml} |
|||
{src/max_in_list_plus_one.ml} |
|||
|
|||
Ici, le problème n'est donc plus celui des cas particuliers, mais celui de la spécification : ici, on a oublié de préciser que la valeur renvoyée par notre fonction doit être présente dans la liste. Cela pourrait s'exprimer ainsi: |
|||
|
|||
\[ r \in l \] |
|||
|
|||
Il est intéressant de noter que le fait que l'algorithme précédent est incorrect aurait été détecté très facilement avec un test. |
|||
|
|||
\subsection{Les différents aspects des méthodes formelles} |
|||
|
|||
Les méthodes formelles ne se limitent pas à la vérification d'une spécification pour un algorithme. On peut aussi prouver des propriétés diverses sur des langages, garantir que les états d'un système respectent des contraintes, démontrer des théorèmes mathématiques. Tout cela implique de nombreux travaux tels que le développement de langages de spécification adaptés à des langages particuliers, de solveurs, la formalisation de la sémantique de langages etc. % TODO: reformuler ça % |
|||
@ -0,0 +1,5 @@ |
|||
\begin{abstract} |
|||
|
|||
Ce document est un rapport de mon stage \emph{Vérification de compilation de requêtes \bsc{sql} à base de traces}, effectué dans le cadre de ma formation en Magistère 1 à l'Université Paris-Sud. Ce stage s'est déroulé sous la direction conjointe de \href{https://www.lri.fr/~benzaken/}{Véronique \bsc{Benzaken}}, \href{https://www.lri.fr/~contejea/}{Évelyne \bsc{Contejean}} et \href{https://www.lri.fr/~keller/}{Chantal \bsc{Keller}}. |
|||
|
|||
\end{abstract} |
|||
@ -0,0 +1,23 @@ |
|||
\section{Exemple complet}\label{exemple-complet} |
|||
|
|||
\inputminted[bgcolor=darkBackground] |
|||
{sql} |
|||
{src/query_14.sql} |
|||
|
|||
\inputminted[bgcolor=darkBackground] |
|||
{xml} |
|||
{src/query_14.xml} |
|||
|
|||
{\setmonofont{Everson Mono} |
|||
\inputminted[bgcolor=darkBackground] |
|||
{ocaml} |
|||
{src/query_14.extalg} |
|||
} |
|||
|
|||
La ligne $27$ indique un \emph{Seq Scan} sur la relation \emph{reserves}, si l'on enlève l'indication de l'algorithme utilisé, cela revient à simplement parler de la relation \emph{reserves}. Sur les lignes $22$ à $29$, on utilise $\omega$ sur cette relation avec des paramètres particuliers. La ligne $23$ nous indique qu'il n'y a aucune partition, ce qui se note \emph{Fine}. La ligne $24$ nous indique qu'on va sélectionner les attributs \emph{sid}, \emph{bid} et \emph{dday} de la relation, et qu'on les renomme respectivement en \emph{r.sid}, \emph{r.bid} et \emph{r.dday}. La ligne $25$ indique quant à elle que l'on va filtrer le résultat en ne gardant que les lignes respectant la condition $bid = 103$. L'écriture mathématique de cette expression, en faisant abstraction des variables notées $x_i$, serait la suivante: |
|||
|
|||
\[ \omega_{\text{Fine},\text{r.sid → r.sid, r.bid → r.bid, r.dday → r.dday},\text{bid} = 103}(\text{reserves}) \] |
|||
|
|||
Les variables notées $x_i$ servent à conserver des informations parfois nécessaires ailleurs alors qu'elles ne sont pas disponible. En effet, le \bsc{sgbd}, afin d'optimiser l'exécution des requêtes, va parfois appliquer un filtre en fonction de la valeur d'un attribut qui n'est pas disponible sur les relations qu'il est en train de traiter, il faut donc enregistrer certaines informations pour pouvoir retrouver ces valeurs. |
|||
|
|||
On peut aussi noter qu'à la ligne $14$, il y a: \emph{× (DependentJoin) (Hash Join)}, \emph{Hash Join} est simplement l'algorithme qui va être utilisé, il ne fait pas partie de l'algèbre étendue. Cependant, il est intéressant de noter que le \emph{Join} est dit \emph{Dependent}, en effet, là aussi, le \bsc{sgbd} va souvent avoir besoin du résultat d'une des deux relations composant la jointure pour pouvoir calculer l'autre. Ainsi, on note par défaut toutes les jointures comme étant des \emph{DependentJoin} et ce n'est que lors de la phase de normalisation que l'on détectera si le \emph{Dependent} est vraiment nécessaire ou non — ici, ça n'est par exemple pas le cas. |
|||
@ -0,0 +1,27 @@ |
|||
\documentclass[a4paper,11pt]{article} |
|||
|
|||
\input{src/packages.tex} |
|||
|
|||
\begin{document} |
|||
|
|||
\input{src/title.tex} |
|||
|
|||
\maketitle |
|||
|
|||
\input{src/abstract.tex} |
|||
|
|||
\tableofcontents |
|||
|
|||
\input{src/lri.tex} |
|||
|
|||
\input{src/about_verification.tex} |
|||
|
|||
\input{src/work.tex} |
|||
|
|||
\input{src/lesson.tex} |
|||
|
|||
\appendix |
|||
|
|||
\input{src/appendix.tex} |
|||
|
|||
\end{document} |
|||
@ -0,0 +1,5 @@ |
|||
\section{Leçons} |
|||
|
|||
Ce stage m'a permis d'approfondir mes connaissances dans plusieurs domaines. Tout d'abord, l'écriture de parser, chose que je n'avais jamais réalisée avant. De plus, j'ai eu l'occasion d'approfondir mes connaissances du langage \bsc{sql}, des différents \bsc{sgbd}, mais surtout, de la façon dont ces derniers fonctionnent : les algorithmes courants, leur lien avec l'algèbre relationnelle etc. |
|||
|
|||
Au-delà de l'aspect informatique, cela a surtout été l'occasion de découvrir le monde de la recherche et d'être, grâce à cela, sûr, dorénavant, de vouloir m'orienter vers la recherche. En effet, cela a été à la fois très enrichissant et stimulant. Pour arriver à résoudre les problèmes que l'on rencontre, il n'est plus question de procéder comme lorsque l'on suit un \bsc{tp} en cours d'informatique ; il n'y a plus une liste linéaire de questions intermédiaires nous guidant directement au résultat et qu'il suffit de résoudre une par une. Il s'agit plutôt de comprendre suffisamment le problème afin de trouver soi-même cette liste d'étapes que l'on va devoir franchir pour arriver au résultat souhaité, sans garantie sur le fait de partir dans la bonne direction. On se trouve alors dans une situation où l'on effectue un travail conscient, technique, dans une direction jusqu'à rencontrer un nouveau problème ou réaliser que cette direction n'était pas la bonne. Parfois, aucune solution n'apparaît clairement, jusqu'à ce que quelques heures, voire quelques jours plus tard, elle nous apparaisse subitement ; une autre possibilité est la discussion du problème avec les autres chercheurs, chose très courante d'après mon expérience de stage, car souvent, une autre personne envisagera le problème d'une autre façon et saura trouver comment le contourner. D'autre part, l'échange avec les autres chercheurs est toujours présent, même avec ceux avec qui l'on ne travaille pas directement, permettant ainsi de toujours avoir l'occasion de réfléchir sur nombre de sujets en permanence. Tout cela rend le travail quotidien très intéressant, agréable et est par la même occasion très formateur. Ainsi, je tiens à remercier Véronique \bsc{Benzaken}, Évelyne \bsc{Contejean} et Chantal \bsc{Keller} pour m'avoir confié des problèmes intéressants, d'avoir pris le temps de m'expliquer les problématiques en profondeur, de m'avoir toujours guidé lorsque cela était nécessaire, mais surtout, de s'être toujours montrées très compréhensives et amicales, rendant par là ma première expérience de recherche extrêmement satisfaisante. |
|||
@ -0,0 +1,5 @@ |
|||
\section{Le Laboratoire de Recherche en Informatique} |
|||
|
|||
Le \href{https://www.lri.fr}{\bsc{l}aboratoire de \bsc{r}echerche en \bsc{i}nformatique} (\bsc{lri}) est une \href{https://fr.wikipedia.org/wiki/Unit%C3%A9_mixte_de_recherche}{\bsc{u}nité \bsc{m}ixte de \bsc{r}echerche} (\bsc{umr}) associant l'\href{http://www.u-psud.fr}{Université Paris-Sud} et le \href{http://www.cnrs.fr/}{\bsc{cnrs}}. |
|||
|
|||
Le \bsc{lri} est composé de plusieurs équipes, parmi lesquelles, l'équipe \href{https://vals.lri.fr/}{\bsc{v}érification d'\bsc{a}lgorithmes, \bsc{l}angages et \bsc{s}ystèmes} (\bsc{vals}) au sein de laquelle s'est déroulé ce stage. L'équipe \bsc{vals} est particulièrement orientée vers la recherche dans le domaine des méthodes formelles. |
|||
@ -0,0 +1,2 @@ |
|||
let max_in_list = function |
|||
List.fold_left (fun max el -> if el > max then el else max) 0 |
|||
@ -0,0 +1,3 @@ |
|||
let max_in_list = function |
|||
| [x] -> x |
|||
| x::s -> List.fold_left (fun max el -> if el > max then el else max) x s |
|||
@ -0,0 +1,3 @@ |
|||
let max_in_list = function |
|||
| [x] -> x + 1 |
|||
| x::s -> List.fold_left (fun max el -> if el > max then el + 1 else max) (x + 1) s |
|||
@ -0,0 +1 @@ |
|||
SELECT mid, title FROM movie WHERE mid > 2500; |
|||
@ -0,0 +1,6 @@ |
|||
<Plan> |
|||
<Node> Seq Scan </Node> |
|||
<Relation> movie </Relation> |
|||
<Projection> mid, title </Projection> |
|||
<Filter> (mid > 2500) </Filter> |
|||
</Plan> |
|||
@ -0,0 +1,50 @@ |
|||
\usepackage[english,french]{babel} % french typo |
|||
\frenchbsetup{StandardLists=true} % avoid conflict between frenchbabel and enumitem |
|||
|
|||
\usepackage{euler} |
|||
|
|||
\usepackage{fontspec} % encoding |
|||
\setmainfont{Linux Libertine O} |
|||
\setsansfont{Linux Biolinum O} |
|||
\setmonofont{Source Code Pro} |
|||
\newfontfamily\unicodemonofont{Everson Mono} |
|||
|
|||
\usepackage{graphicx} % to include img |
|||
\usepackage{enumitem} % powerful lists |
|||
\usepackage{xspace} % correct quotes printing |
|||
\usepackage[np]{numprint} % correct numbers printing |
|||
\usepackage{amsmath} % maths and better typo |
|||
\usepackage{amssymb} % more maths |
|||
\usepackage{dsfont} % and even more maths |
|||
\usepackage{color} % color power |
|||
\usepackage[dvipsnames]{xcolor} % more color power |
|||
\definecolor{darkBackground}{HTML}{282c34} % source code background |
|||
\definecolor{darkBackgroundHighlight}{HTML}{2c323c} % source code background |
|||
\definecolor{lightBackground}{HTML}{D7D3CB} % source code background |
|||
\usepackage{microtype} % better typo |
|||
|
|||
\usepackage{hyperref} % internal and external links (e.g. mail, www) |
|||
\usepackage{cleveref} |
|||
|
|||
\newcommand\myshade{85} |
|||
\colorlet{mylinkcolor}{violet} |
|||
\colorlet{mycitecolor}{YellowOrange} |
|||
\colorlet{myurlcolor}{Aquamarine} |
|||
|
|||
\usepackage[cache=false, draft=false]{minted} % source code |
|||
\usemintedstyle{paraiso-dark} |
|||
\setminted{bgcolor=lightBackground} |
|||
\setminted{linenos, autogobble, breaklines, breakanywhere, breakautoindent, fontseries=m, fontsize=\fontsize{9pt}{7pt}, frame=none, stepnumber=2} |
|||
|
|||
\usepackage{placeins} % float displaying |
|||
\usepackage{tikz} % .tex figures (e.g. from Dia) |
|||
|
|||
\hypersetup{ |
|||
linkcolor = mylinkcolor!\myshade!black, |
|||
citecolor = mycitecolor!\myshade!black, |
|||
urlcolor = myurlcolor!\myshade!black, |
|||
colorlinks = true, |
|||
pdfstartview=FitH |
|||
} |
|||
|
|||
\usepackage{ellipsis} % correct ... |
|||
@ -0,0 +1,33 @@ |
|||
⍵ { |
|||
_ Fine |
|||
_ r.dday → r.dday, r.bid → r.bid, r.sid → r.sid, s.age → s.age, s.rating → s.rating, s.sname → s.sname, s.sid → s.sid |
|||
_ x_0.s.sid = x_0.r.sid |
|||
_ { |
|||
⍵ { |
|||
_ Fine |
|||
_ sid → s.sid, sname → s.sname, rating → s.rating, age → s.age |
|||
_ ⊤ |
|||
_ { |
|||
Seq Scan on sailors |
|||
} |
|||
} |
|||
× (DependentJoin) (Hash Join) |
|||
Label: Hash |
|||
⍵ { |
|||
_ Partition (x_0.r.sid) |
|||
_ r.sid → r.sid, r.bid → r.bid, r.dday → r.dday |
|||
_ ⊤ |
|||
_ { |
|||
Label: Aggregate |
|||
⍵ { |
|||
_ Fine |
|||
_ sid → r.sid, bid → r.bid, dday → r.dday |
|||
_ x_0.bid = 103 |
|||
_ { |
|||
Seq Scan on reserves |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1 @@ |
|||
select s.sname from sailors s where exists (select * from reserves r where r.bid = 103 and s.sid = r.sid); |
|||
@ -0,0 +1,41 @@ |
|||
<?xml version="1.0"?> |
|||
<explain> |
|||
<Query> |
|||
<Plan> |
|||
<Node-Type>Hash Join</Node-Type> |
|||
<Join-Type>Inner</Join-Type> |
|||
<Hash-Cond>(s.sid = r.sid)</Hash-Cond> |
|||
<Plans> |
|||
<Plan> |
|||
<Node-Type>Seq Scan</Node-Type> |
|||
<Parent-Relationship>Outer</Parent-Relationship> |
|||
<Relation-Name>sailors</Relation-Name> |
|||
<Alias>s</Alias> |
|||
</Plan> |
|||
<Plan> |
|||
<Node-Type>Hash</Node-Type> |
|||
<Parent-Relationship>Inner</Parent-Relationship> |
|||
<Plans> |
|||
<Plan> |
|||
<Node-Type>Aggregate</Node-Type> |
|||
<Strategy>Hashed</Strategy> |
|||
<Parent-Relationship>Outer</Parent-Relationship> |
|||
<Group-Key> |
|||
<Item>r.sid</Item> |
|||
</Group-Key> |
|||
<Plans> |
|||
<Plan> |
|||
<Node-Type>Seq Scan</Node-Type> |
|||
<Parent-Relationship>Outer</Parent-Relationship> |
|||
<Relation-Name>reserves</Relation-Name> |
|||
<Alias>r</Alias> |
|||
<Filter>(bid = 103)</Filter> |
|||
</Plan> |
|||
</Plans> |
|||
</Plan> |
|||
</Plans> |
|||
</Plan> |
|||
</Plans> |
|||
</Plan> |
|||
</Query> |
|||
</explain> |
|||
@ -0,0 +1,8 @@ |
|||
(* on suppose que notre framework de test contient une fonction assert_equal qui lève une exception si ses deux paramètres sont différents *) |
|||
|
|||
let test_max_in_list () = |
|||
|
|||
assert_equal 0 (max_in_list [0]); |
|||
assert_equal 73 (max_in_list [73]); |
|||
assert_equal 3 (max_in_list [0; 1; 2; 3]); |
|||
assert_equal 1357 (max_in_list [549; 0; 1; 2; 64; 1035; 1357; 10; 1345]) |
|||
@ -0,0 +1 @@ |
|||
assert_equal -1 (max_in_list [-1]); |
|||
@ -0,0 +1,7 @@ |
|||
\title{Rapport de Stage\\ |
|||
Vérification de compilation de requêtes \bsc{sql} à base de traces |
|||
} |
|||
|
|||
\author{\href{mailto:leo@ndrs.fr}{Léo \bsc{Andrès}}} |
|||
|
|||
\date{\today} |
|||
@ -0,0 +1,46 @@ |
|||
\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} |
|||
{src/movie_01.sql} |
|||
|
|||
On pourrait obtenir un plan comme celui-ci: |
|||
|
|||
\inputminted[bgcolor=darkBackground] |
|||
{xml} |
|||
{src/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. |
|||
Loading…
Reference in new issue