Browse Source

First commit

master
zapashcanon 4 years ago
commit
2acc75caa7
Signed by: zapashcanon GPG Key ID: 8981C3C62D1D28F1
  1. 8
      .gitignore
  2. 0
      CHANGELOG.md
  3. 16
      LICENSE.md
  4. 13
      Makefile
  5. 0
      README.md
  6. 13
      scripts/build.sh
  7. 9
      scripts/clean.sh
  8. 9
      scripts/mrproper.sh
  9. 16
      scripts/test.sh
  10. 5
      src/abstract.tex
  11. 30
      src/biblio.bib
  12. 2
      src/cakeml.tex
  13. 8
      src/content.tex
  14. 7
      src/contexte_du_stage.tex
  15. 3
      src/intro.tex
  16. 2
      src/lambda_lifting.tex
  17. 6
      src/lambda_lifting_algorithms.tex
  18. 29
      src/main.tex
  19. 2
      src/méthodes_formelles.tex
  20. 58
      src/packages.tex
  21. 5
      src/title.tex

8
.gitignore

@ -0,0 +1,8 @@
*.pdf
*.bbl
*.bcf
*.blg
*.log
*.run.xml
*.aux
*.out

0
CHANGELOG.md

16
LICENSE.md

@ -0,0 +1,16 @@
The ISC License (ISC)
=====================
Copyright (c) 2018, 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.

13
Makefile

@ -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
README.md

13
scripts/build.sh

@ -0,0 +1,13 @@
#!/usr/bin/env sh
set -eu
( cd "$(dirname "$0")"/../src
xelatex -shell-escape main.tex
biber main
# xelatex -shell-escape src/main.tex
xelatex -shell-escape main.tex
xelatex -shell-escape main.tex
mv main.pdf ../main.pdf
)

9
scripts/clean.sh

@ -0,0 +1,9 @@
#!/usr/bin/env sh
set -eu
( cd "$(dirname "$0")"/../src/
rm -f ./*.log ./*.tuc ./*.out ./*.aux ./*.toc ./*.pyg ./*.bbl ./*.bcf ./*.blg ./*.run.xml
)

9
scripts/mrproper.sh

@ -0,0 +1,9 @@
#!/usr/bin/env sh
set -eu
( cd "$(dirname "$0")"/../
rm -f ./*.pdf
)

16
scripts/test.sh

@ -0,0 +1,16 @@
#!/usr/bin/env sh
set -eu
(
cd "$(dirname "$0")"/../
# Testing scripts
# shellcheck disable=SC2185
find -O3 . -type f -name '*.sh' -exec shellcheck {} \;
cd src/
# 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...
)

5
src/abstract.tex

@ -0,0 +1,5 @@
\begin{abstract}
Ce document est un rapport de mon stage \emph{Implémentation et vérification du lambda-lifting dans le compilateur \bsc{CakeML}}, effectué dans le cadre de ma formation en Master 1 Jacques Herbrand à l'École Normale Supérieure Paris-Saclay. Ce stage s'est déroulé sous la direction conjointe de \href{https://www.cs.kent.ac.uk/people/staff/sao/}{Scott \bsc{Owens}} et de \href{https://www.cs.kent.ac.uk/people/staff/hf216/}{Hugo \bsc{Férée}}.
\end{abstract}

30
src/biblio.bib

@ -0,0 +1,30 @@
@article{BOUAJJANI1999211,
title = "Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations",
journal = "Theoretical Computer Science",
volume = "221",
number = "1",
pages = "211 - 250",
year = "1999",
issn = "0304-3975",
doi = "https://doi.org/10.1016/S0304-3975(99)00033-X",
url = "http://www.sciencedirect.com/science/article/pii/S030439759900033X",
author = "Ahmed Bouajjani and Peter Habermehl",
keywords = "Verification, Infinite-state systems, FIFO-channel systems, Symbolic reachability analysis, Non-regular sets, Automata, Linear constraints"
}
@Inbook{Fischer1998,
author="Fischer, Michael J.
and Rabin, Michael O.",
editor="Caviness, Bob F.
and Johnson, Jeremy R.",
title="Super-Exponential Complexity of Presburger Arithmetic",
bookTitle="Quantifier Elimination and Cylindrical Algebraic Decomposition",
year="1998",
publisher="Springer Vienna",
address="Vienna",
pages="122--135",
abstract="Lower bounds are established on the computational complexity of the decision problem and on the inherent lengths of proofs for two classical decidable theories of logic: the first-order theory of the real numbers under addition, and Presburger arithmetic --- the first-order theory of addition on the natural numbers. There is a fixed constant c > 0 such that for every (nondeterministic) decision procedure for determining the truth of sentences of real addition and for all sufficiently large n, there is a sentence of length n for which the decision procedure runs for more than 2 cn steps. In the case of Presburger arithmetic, the corresponding bound is {\$}{\$}{\{}2^{\{}{\{}2^{\{}cn{\}}{\}}{\}}{\}}{\$}{\$} . These bounds apply also to the minimal lengths of proofs for any complete axiomatization in which the axioms are easily recognized.",
isbn="978-3-7091-9459-1",
doi="10.1007/978-3-7091-9459-1_5",
url="https://doi.org/10.1007/978-3-7091-9459-1_5"
}

2
src/cakeml.tex

@ -0,0 +1,2 @@
\section{CakeML}
CakeML c'est bien parce que y'a des preuves. C'est plus compliqué à faire. On rend des choses simples compliquées, pour les rendre simples.

8
src/content.tex

@ -0,0 +1,8 @@
\paragraph{}
La vérification de protocoles revient en partie à vérifier des propriétés sur des \emph{Communicating Finite State Machines} (CFSM). Un moyen de représenter ces CFSM, est d'utiliser des \emph{Constrained Queue Decision Diagram} (CQDD), qui possèdent de nombreuses propriétés intéressantes pour effectuer de l'analyse d'atteignabilité. Les contraintes des CQDD sont des formules de l'arithmétique de Presburger, qui est une logique décidable\cite{BOUAJJANI1999211}.
\paragraph{}
Il peut alors sembler légitime de se demander s'il est possible de trouver une logique \emph{minimale} permettant de représenter les contraintes d'un CQDD et qui soit telle que ce CQDD soit toujours suffisant pour calculer l'effet de n'importe quel cycle dans le graphe de contrôle d'un CFSM\@. Il a été montré que l'arithmétique de Presburger est suffisante\cite{BOUAJJANI1999211}, cependant, il a aussi été montré que la décidabilité d'une formule de l'arithmétique de Presburger est un problème 2EXPTIME-dur\cite{Fischer1998}, il serait donc intéressant d'utiliser une logique moins expressive afin d'essayer d'obtenir une meilleure complexité. Une des raisons qui laissent penser qu'il est possible de faire mieux est le fait que la quantification universelle de l'arithmétique de Presburger n'est jamais utilisée dans les contraintes d'un CQDD\cite{BOUAJJANI1999211}.
\paragraph{}
Une approche pour tenter de répondre à cette question serait de commencer par enlever la quantification universelle: on sait déjà qu'elle n'est pas nécessaire ; puis, de chercher à savoir si le problème de décision est toujours 2EXPTIME-dur. On pourrait ensuite regarder s'il est possible d'exprimer les contraintes de telle sorte qu'on puisse réduire encore notre logique et réitérer le processus de savoir si cela améliore la complexité. On peut aussi montrer que des parties de la logique sont absolument nécessaires et ainsi, savoir qu'on ne pourra faire mieux que ce que l'on fait déjà et que pour vérifier des systèmes trop gros, il faudra se tourner vers d'autres méthodes et non pas seulement attendre que des algorithmes plus efficaces apparaissent.
\paragraph{}
Ainsi, on devrait pouvoir vérifier des protocoles en utilisant les mêmes méthodes, mais en moins de temps. La vérification de programme est importante puisqu'en effet, on sait pas a priori, si un programme est correct. Dans de nombreux cas, le fait de détecter les problèmes une fois qu'ils surviennent n'aura pas de graves conséquences, mais il y a des domaines où cela n'est pas souhaitable: énergie, transport, médecine etc. La vérification de programmes au moyen de preuves mathématiques est donc utile. Cependant, dans des approches telles que le \emph{model checking}, cela n'est pas toujours possible puisque la vérification du programme prend trop de temps. Le fait de réduire le temps de calcul des problèmes d'atteignabilité permet donc d'accélérer la vérification et lorsqu'on change de classe de complexité, la différence est sensible.

7
src/contexte_du_stage.tex

@ -0,0 +1,7 @@
\section{Contexte du stage}
\paragraph{}
Ce stage s'inscrit dans le cadre de ma formation à l'\href{http://www.ens-cachan.fr/}{École Normale Supérieure Paris-Saclay}. L'École Normale Supérieure Paris-Saclay a, entre autres, pour but de former ses étudiants \emph{par la recherche, pour la recherche} ; ainsi, en tant qu'étudiant du \href{https://www.masters-herbrand.fr/}{Master 1 Jacques \bsc{Herbrand}}, il est obligatoire d'effectuer un stage de recherche à l'étranger durant l'été. Il est possible d'effectuer un stage plus long, qui couvre alors aussi le second semestre: c'est le choix que j'ai fait.
\paragraph{}
Le stage a eu lieu à l'\href{https://www.kent.ac.uk/}{université du Kent}, au sein de la \href{https://www.cs.kent.ac.uk/}{School of Computing} située à \href{https://fr.wikipedia.org/wiki/Canterbury}{Canterbury} et constituée de plusieurs équipes de recherche. J'ai travaillé au sein de l'équipe \href{https://www.cs.kent.ac.uk/research/groups/plas/}{Programming Languages and Systems}.
\paragraph{}
TODO: L'équipe PLAS c'est très bien. Ils font des choses autour des langages et des méthodes formelles.

3
src/intro.tex

@ -0,0 +1,3 @@
\section{Introduction}
We assume you're working on a Debian system.

2
src/lambda_lifting.tex

@ -0,0 +1,2 @@
\section{Le lambda-lifting}
Le lambda-lifting c'est bien.

6
src/lambda_lifting_algorithms.tex

@ -0,0 +1,6 @@
\section{Les algorithmes existant pour le lambda-lifting}
1: $O(n^3)$, pas optimal
2: $O(n^2)$, pas optimal
3: $O(n^3)$, optimal
4: $O(n^2)$, optimal
On va faire le 4ème pck on est forts.

29
src/main.tex

@ -0,0 +1,29 @@
\documentclass[a4paper,11pt]{article}
\input{packages.tex}
\bibliography{biblio}
\begin{document}
\input{title.tex}
\maketitle
\input{abstract.tex}
\tableofcontents
\input{contexte_du_stage.tex}
\input{méthodes_formelles.tex}
\input{cakeml.tex}
\input{lambda_lifting.tex}
\input{lambda_lifting_algorithms.tex}
\printbibliography{}
\end{document}

2
src/méthodes_formelles.tex

@ -0,0 +1,2 @@
\section{À propos des langages et des méthodes formelles}
Les langages c'est bien, mais parfois non. Les compilateurs aussi. C'est mieux avec des méthodes formelles.

58
src/packages.tex

@ -0,0 +1,58 @@
\usepackage[french]{babel}
\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 ...
\usepackage[
backend=biber, % choix de l'outil de traitement
babel=hyphen, % environnement linguistique dédié aux entrées en langues alternatives (utilise l'attribut « hyphenation »)
backref=true, % liens dans la bibliographie pour remonter dans le texte
backrefstyle=none, % afficher toutes les utilisations de la référence
bibstyle=alphabetic, % style pour les clés des références dans la bibliographie : [initialesAnnée]
citestyle=alphabetic, % style pour les clés des références dans le texte : [initialesAnnée]
sorting=none, % bibliographie triée par ordre d'utilisation des références
]{biblatex} % support des bibliographies

5
src/title.tex

@ -0,0 +1,5 @@
\title{Rapport de stage: implémentation et vérification du lambda-lifting dans le compilateur \bsc{CakeML}}
\author{\href{mailto:leo@ndrs.fr}{Léo \bsc{Andrès}}}
\date{\today}
Loading…
Cancel
Save