zapashcanon/poster-jdse-2017
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fix intro, remove text, fix extalg expression, remove line num

Browse Source
This commit is contained in:
zapashcanon 2017-09-13 21:16:49 +02:00
parent d17754ef6b
commit 96f8e6d4aa
Signed by: zapashcanon
GPG Key ID: 8981C3C62D1D28F1
4 changed files with 46 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
img/compilchain.pdf Normal file
View File

Binary file not shown.

2
src/packages.tex
View File

@ -40,4 +40,4 @@
\usepackage[cache=false, draft=false]{minted}
\usemintedstyle{paraiso-dark}
\setminted{bgcolor=lightBackground}
\setminted{linenos, autogobble, breaklines, breakanywhere, breakautoindent, fontseries=m, fontsize=\fontsize{9pt}{7pt}, frame=none, stepnumber=2}
\setminted{autogobble, breaklines, breakanywhere, breakautoindent, fontseries=m, fontsize=\fontsize{9pt}{7pt}, frame=none, stepnumber=2}

51
src/poster-jdse-2017.tex
View File

@ -19,10 +19,19 @@
\makeposter{}
%----------------------------------------
\section{Data and proofs}
\section{Data systems and languages, proofs}
%----------------------------------------
Data is everywhere etc. Proofs and formal methods not often applied to data languages (SQL) or DBMS (postgresql) etc.
Until now there have been little usages of formal methods towards SQL and DBMS, yet, the compilation chain of SQL queries is complex.
\begin{figure}[h!]
\caption{SQL's compilation chain}
\label{sql-compil-chain}
\centering
\begin{center}
\includegraphics[scale=1]{img/compilchain.pdf}\\
\end{center}
\end{figure}
%Le poster est formatté avec LaTeX. Les instructions détaillées sont dans le fichier source et le source de ce poster peut servir d'exemple.
%Le texte peut être formatté en une, deux ou trois colonnes. Ceci est un exemple de texte formatté sur une colonne. Compte tenu de la largeur du poster, il est préférable de limiter ce texte à quelques lignes.
@ -36,7 +45,12 @@ Data is everywhere etc. Proofs and formal methods not often applied to data lang
\inputminted[bgcolor=darkBackground]
{sql}
{src/query_14.sql}
We parse SQL queries using the certified parser generator written by Jacques-Henri Jourdan and used in CompCert. At the end, we have an SQLCoq-compatible representation of the query. SQLCoq is a Coq library formalising SQL.
\begin{itemize}
\item SQL parser in menhir/OCamllex
\item certified using the CompCert parser generator
\item automatic translation into SQLCoq (in OCaml)
\end{itemize}
% We parse SQL queries using the certified parser generator written by Jacques-Henri Jourdan and used in CompCert. At the end, we have an SQLCoq-compatible representation of the query. SQLCoq is a Coq library formalising SQL.
%Pour formatter le texte sur \emph{deux colonnes}, utiliser la macro \verb|\twocolsection{<titre>}| si vous souhaitez un titre de section qui fasse la largeur du poster, ou bien \verb|\twocoltext| pour ne pas afficher de titre.
@ -54,9 +68,13 @@ We parse SQL queries using the certified parser generator written by Jacques-Hen
\section{Involving DBMS, from SQL to unified execution plan}
We give an SQL query to two DBMS (PostgreSQL and Oracle) and get the query execution plan, that is, the algorithms which are going to be used to fetch the data from the disk.
\begin{itemize}
\item PostgreSQL and Oracle query execution plan parser
\item both translated to our own unified plan format
\end{itemize}
%We give an SQL query to two DBMS (PostgreSQL and Oracle) and get the query execution plan, that is, the algorithms which are going to be used to fetch the data from the disk.
Then, we change the plans so they have the same format. We defined an unified execution plan format.
%sThen, we change the plans so they have the same format. We defined an unified execution plan format.
%Les titres de sections sont formattés dans la couleur du thème du poster.
%le trait sous le titre peut être désactivé / réactivé avec les commandes \verb|\titlerulefalse| et \verb|\titleruletrue|.
@ -84,9 +102,14 @@ Then, we change the plans so they have the same format. We defined an unified ex
\columnbreak{}
%........................................
From a given plan, we build an Extended Algebra expression. ExtAlg is similar to Relationnal Algebra but more powerful.
\begin{itemize}
\item Extended Algebra (ExtAlg) is similar to Relationnal Algebra but more powerful
\item translation from an unified plan to an ExtAlg expression
\item automatic annotation of ExtAlg expression with algorithms
\item ability to execute our Coq version of those algorithms
\end{itemize}
Here, the expression is annotated with algorithms. Thus, we'll be able to go further by executing the algorithms which were formalized in Coq.
%Here, the expression is annotated with algorithms. Thus, we'll be able to go further by executing the algorithms which were formalized in Coq.
%Vous pouvez insérer des images avec la commande habituelle \verb|\includegraphics|.
@ -112,7 +135,12 @@ Here, the expression is annotated with algorithms. Thus, we'll be able to go fur
\twocolsection{Equivalence of two ExtAlg queries}
%----------------------------------------
Now we have the ExtAlg expression of the query from the plan the DBMS gave us. We also have the SQLCoq representation of the query. We can get the ExtAlg expression from the SQLCoq representation. We can show the equivalence of the two ExtAlg queries, by using normal forms on logical formulas, or using other Coq-proved equivalence on ExtAlg.
\begin{itemize}
\item translation from SQLCoq to ExtAlg
\item two ExtAlg expressions, one from the DBMS, one from the SQL query/SQLCoq
\item proof that two ExtAlg expression have the same semantic
\end{itemize}
%Now we have the ExtAlg expression of the query from the plan the DBMS gave us. We also have the SQLCoq representation of the query. We can get the ExtAlg expression from the SQLCoq representation. We can show the equivalence of the two ExtAlg queries, by using normal forms on logical formulas, or using other Coq-proved equivalence on ExtAlg.
%\begin{cbox}
%Pour mettre un paragraphe en évidence, vous pouvez utiliser l'environnement \verb|cbox| qui formatte le texte sur un fond de couleur jaune sable.
%\end{cbox}
@ -125,7 +153,12 @@ Now we have the ExtAlg expression of the query from the plan the DBMS gave us. W
\columnbreak{}
%........................................
With the equivalence of the two expressions, we are sure that the algorithms that the DMBS planned to use are corrects and that they won't change the semantic of the SQL query. We still have to prove that algorithms used in DBMS are correct, or to use our own written in Coq.
\begin{itemize}
\item strong guarantees about the fact that the DBMS kept the semantic of the SQL query
\item algorithms used by the DBMS have not been proved yet
\item Coq version of some algorithms
\end{itemize}
%With the equivalence of the two expressions, we are sure that the algorithms that the DMBS planned to use are corrects and that they won't change the semantic of the SQL query. We still have to prove that algorithms used in DBMS are correct, or to use our own written in Coq.
%Il existe trois thèmes de poster : \verb|\redposter|, \verb|\blueposter| et \verb|\greenposter|. La couleur du thème est dans la variable %\verb|\highlightcolor|. Les autres couleurs prédéfinies sont :
%\begin{itemize}

6
src/query_14.extalg
View File

@ -1,9 +1,9 @@
⍵ {
Omega {
_ 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
_ {
⍵ {
Omega {
_ Fine
_ sid → s.sid, sname → s.sname, rating → s.rating, age → s.age
_ ⊤
@ -11,5 +11,5 @@
Seq Scan on sailors
}
}
× (DependentJoin) (Hash Join)
X (DependentJoin) (Hash Join)
...