Commit c48820e5 authored by Andreas Zwinkau's avatar Andreas Zwinkau
Browse files

initial

parents
thesis/build
thesis/thesis.pdf
[submodule "Slicing"]
path = Slicing
url = ssh-pp.ipd.kit.edu:/ben/local/GIT/Isabelle/Slicing.git
Basics for writing a thesis at IPD Snelting.
Put your code into the "code" directory. Use git submodule or subtree to
include external repositories.
Write your thesis with LaTeX. A template is provided in the "thesis" directory.
Prepare your presentation in the "present" directory. A template is provided
there.
Add you code here or use repos which already exist.
../document/mathpartir.sty
\ No newline at end of file
This diff is collapsed.
BUILD=build
BASE=thesis
DEPS=$(wildcard *.tex) $(wildcard *.sty)
default: $(BASE).pdf
$(BUILD)/$(BASE).pdf: $(BASE).tex $(DEPS)
mkdir -p $(BUILD)
latexmk -f -pdf -outdir=build $<
$(BASE).pdf: $(BUILD)/$(BASE).pdf
mv $< $@ # atomic update
cp $@ $<
.PHONY: show clean
show: $(BASE).pdf
gnome-open $< || open $<
clean:
rm -rf build
\section{Grundlagen und Verwandte Arbeiten}\label{sec:basics}
In diesem Kapitel landet alles,
was nicht vom Autor selbst erfunden wurde.
Einerseits Grundlagen,
die für das Verständnis der Arbeit notwendig sind.
Andererseits verwandte Arbeiten,
wobei bei diesen klar gemacht werden soll,
inwiefern diese Arbeit darauf aufbaut bzw. etwas anders macht.
Beispiel wäre ein Standardwerk in Sachen SSA-Form~\cite{cytron91}
welches bei uns häufig zitiert wird.
Es soll klar werden,
dass dem Studenten der Stand der Technik bewusst war
und keine redundante Arbeit gemacht wurde.
@inproceedings{braun13cc,
title = {Simple and Efficient Construction of Static Single Assignment Form},
booktitle = {Compiler Construction},
year = {2013},
publisher = {Springer},
volume = {7791},
pages = {102--122},
author = {Matthias Braun and Sebastian Buchwald and Sebastian Hack and Roland Lei{\ss}a and Christoph Mallon and Andreas Zwinkau},
editor = {Jhala, Ranjit and Bosschere, Koen},
series = {Lecture Notes in Computer Science},
url = {http://dx.doi.org/10.1007/978-3-642-37051-9\_6},
doi = {10.1007/978-3-642-37051-9_6},
}
@article{cytron91,
author = {Cytron, Ron and Ferrante, Jeanne and Rosen, Barry K. and Wegman, Mark N. and Zadeck, F. Kenneth},
title = {Efficiently computing static single assignment form and the control dependence graph},
journal = {ACM Transactions on Programming Languages and Systems},
issue_date = {Oct. 1991},
volume = {13},
number = {4},
month = oct,
year = {1991},
issn = {0164-0925},
pages = {451--490},
numpages = {40},
url = {http://doi.acm.org/10.1145/115372.115320},
doi = {10.1145/115372.115320},
acmid = {115320},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {control dependence, control flow graph, def-use chain, dominator, optimizing compilers},
}
@misc{kohlmeyer12bachelorarbeit,
title = {{F}unktionale {K}onstruktion und {V}erifikation von {K}ontrollflussgraphen},
year = {2012},
month = aug,
author = {Kevin-Simon Kohlmeyer},
school = {Karlsruher Institut f{\"u}r Technologie (KIT)},
note = {Bachelor's Thesis}
}
@InProceedings{LLVM,
author = {Lattner, Chris and Adve, Vikram},
title = {{LLVM}: A Compilation Framework for Lifelong Program Analysis \& Transformation},
booktitle = {Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization},
series = {CGO '04},
year = {2004},
isbn = {0-7695-2102-9},
location = {Palo Alto, California},
pages = {75--},
url = {http://dl.acm.org/citation.cfm?id=977395.977673},
acmid = {977673},
publisher = {IEEE Computer Society},
}
@techreport{libfirm,
title = {{libFIRM} -- A Library for Compiler Optimization Research Implementing {FIRM}},
year = {2002},
month = sep,
publisher = {Universit{\"a}t Karlsruhe, Fakult{\"a}t f{\"u}r Informatik},
number = {2002-5},
pages = {75},
chapter = {9},
author = {G{\"o}tz Lindenmaier},
url = {http://www.info.uni-karlsruhe.de/papers/Lind\_02-firm\_tutorial.ps},
}
@article{hotspot,
author = {Kotzmann, Thomas and Wimmer, Christian and M\"{o}ssenb\"{o}ck, Hanspeter and Rodriguez, Thomas and Russell, Kenneth and Cox, David},
title = {Design of the {Java HotSpot\texttrademark~client compiler for Java 6}},
journal = {ACM Transactions on Architecture and Code Optimization},
issue_date = {May 2008},
volume = {5},
number = {1},
month = may,
year = {2008},
issn = {1544-3566},
pages = {7:1--7:32},
articleno = {7},
numpages = {32},
url = {http://doi.acm.org/10.1145/1369396.1370017},
doi = {10.1145/1369396.1370017},
acmid = {1370017},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Java, compiler, deoptimization, intermediate representation, just-in-time compilation, optimization, register allocation},
}
@inproceedings{alpern,
author = {Alpern, B. and Wegman, M. N. and Zadeck, F. K.},
title = {Detecting equality of variables in programs},
booktitle = {Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
series = {POPL '88},
year = {1988},
isbn = {0-89791-252-7},
location = {San Diego, California, USA},
pages = {1--11},
numpages = {11},
url = {http://doi.acm.org/10.1145/73560.73561},
doi = {10.1145/73560.73561},
acmid = {73561},
publisher = {ACM},
}
@article{locales,
year={2013},
issn={0168-7433},
journal={Journal of Automated Reasoning},
doi={10.1007/s10817-013-9284-7},
title={Locales: A Module System for Mathematical Theories},
url={http://dx.doi.org/10.1007/s10817-013-9284-7},
publisher={Springer},
keywords={Theorem prover; Module system; Theory hierarchy; Theory interpretation; Isabelle},
author={Ballarin, Clemens},
pages={1-31},
language={English}
}
@incollection{mansky2010framework,
year={2010},
isbn={978-3-642-14051-8},
booktitle={Interactive Theorem Proving},
volume={6172},
series={Lecture Notes in Computer Science},
doi={10.1007/978-3-642-14052-5_26},
title={A Framework for Formal Verification of Compiler Optimizations},
url={http://dx.doi.org/10.1007/978-3-642-14052-5_26},
publisher={Springer},
keywords={optimizing compilers; theorem proving; program transformations; temporal logic},
author={Mansky, William and Gunter, Elsa},
pages={371-386}
}
@inproceedings{zhao2013formal,
author = {Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M.K. and Zdancewic, Steve},
title = {{Formal verification of SSA-based optimizations for LLVM}},
booktitle = {Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation},
series = {PLDI '13},
year = {2013},
isbn = {978-1-4503-2014-6},
location = {Seattle, Washington, USA},
pages = {175--186},
numpages = {12},
url = {http://doi.acm.org/10.1145/2491956.2462164},
doi = {10.1145/2491956.2462164},
acmid = {2462164},
publisher = {ACM},
keywords = {coq, llvm, single static assignment},
}
@incollection{aycock2000simple,
year={2000},
isbn={978-3-540-67263-0},
booktitle={Compiler Construction},
volume={1781},
series={Lecture Notes in Computer Science},
doi={10.1007/3-540-46423-9_8},
title={Simple Generation of Static Single-Assignment Form},
url={http://dx.doi.org/10.1007/3-540-46423-9_8},
publisher={Springer},
author={Aycock, John and Horspool, Nigel},
pages={110-125},
language={English}
}
@inproceedings{zhao2012formalizing,
author = {Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M.K. and Zdancewic, Steve},
title = {Formalizing the {LLVM} intermediate representation for verified program transformations},
booktitle = {Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
series = {POPL '12},
year = {2012},
isbn = {978-1-4503-1083-3},
location = {Philadelphia, PA, USA},
pages = {427--440},
numpages = {14},
url = {http://doi.acm.org/10.1145/2103656.2103709},
doi = {10.1145/2103656.2103709},
acmid = {2103709},
publisher = {ACM},
keywords = {Coq, LLVM, memory safety},
}
@article{kalvala2009program,
author = {Kalvala, Sara and Warburton, Richard and Lacey, David},
title = {Program transformations using temporal logic side conditions},
journal = {ACM Transactions on Programming Languages and Systems},
issue_date = {May 2009},
volume = {31},
number = {4},
month = may,
year = {2009},
issn = {0164-0925},
pages = {14:1--14:48},
articleno = {14},
numpages = {48},
url = {http://doi.acm.org/10.1145/1516507.1516509},
doi = {10.1145/1516507.1516509},
acmid = {1516509},
publisher = {ACM},
keywords = {Optimizing compilers, program transformation, rewriting, temporal logic},
}
@inproceedings{huffman2012lifting,
title={Lifting and Transfer: A Modular Design for Quotients in {Isabelle/HOL}},
author={Huffman, Brian and Kun{\v{c}}ar, Ond{\v{r}}ej}
}
@article{paulson2000foundation,
author = {Paulson, L. C.},
title = {The foundation of a generic theorem prover},
journal = {Journal of Automated Reasoning},
issue_date = {September 1989},
volume = {5},
number = {3},
month = sep,
year = {1989},
issn = {0168-7433},
pages = {363--397},
numpages = {35},
url = {http://dx.doi.org/10.1007/BF00248324},
doi = {10.1007/BF00248324},
acmid = {67178},
publisher = {Springer},
address = {Secaucus, NJ, USA},
}
@inproceedings{choi1991automatic,
author = {Choi, Jong-Deok and Cytron, Ron and Ferrante, Jeanne},
title = {Automatic construction of sparse data flow evaluation graphs},
booktitle = {Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
series = {POPL '91},
year = {1991},
isbn = {0-89791-419-8},
location = {Orlando, Florida, USA},
pages = {55--66},
numpages = {12},
url = {http://doi.acm.org/10.1145/99583.99594},
doi = {10.1145/99583.99594},
acmid = {99594},
publisher = {ACM},
}
@inproceedings{sreedhar1995linear,
author = {Sreedhar, Vugranam C. and Gao, Guang R.},
title = {A linear time algorithm for placing $\phi$-nodes},
booktitle = {Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
series = {POPL '95},
year = {1995},
isbn = {0-89791-692-1},
location = {San Francisco, California, USA},
pages = {62--73},
numpages = {12},
url = {http://doi.acm.org/10.1145/199448.199464},
doi = {10.1145/199448.199464},
acmid = {199464},
publisher = {ACM},
}
@inproceedings{rosen1988global,
author = {Rosen, B. K. and Wegman, M. N. and Zadeck, F. K.},
title = {Global value numbers and redundant computations},
booktitle = {Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
series = {POPL '88},
year = {1988},
isbn = {0-89791-252-7},
location = {San Diego, California, USA},
pages = {12--27},
numpages = {16},
url = {http://doi.acm.org/10.1145/73560.73562},
doi = {10.1145/73560.73562},
acmid = {73562},
publisher = {ACM},
}
@article{bilardi2003algorithms,
author = {Bilardi, Gianfranco and Pingali, Keshav},
title = {Algorithms for computing the static single assignment form},
journal = {ACM Transactions on Computational Logic},
issue_date = {May 2003},
volume = {50},
number = {3},
month = may,
year = {2003},
issn = {0004-5411},
pages = {375--425},
numpages = {51},
url = {http://doi.acm.org/10.1145/765568.765573},
doi = {10.1145/765568.765573},
acmid = {765573},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Control dependence, optimizing compilers, program optimization, program transformation, static single assignment form},
}
@misc{gcc-ssa,
title = {The {GCC} Internals Documentation},
howpublished = {\url{http://gcc.gnu.org/onlinedocs/gccint/SSA.html}},
note = {Retrieved: 23 Oct. 2013}
}
@misc{llvm-sreedhar,
title = {Source code of The {LLVM} Compiler Infrastructure},
howpublished = {\url{http://llvm.org/viewvc/llvm-project/llvm/trunk/lib/Transforms/Utils/PromoteMemoryToRegister.cpp?revision=189169&view=markup}},
note = {Revision 189169, 24 Aug.\ 2013}
}
@Manual{Coq:manual,
title = {The Coq proof assistant reference manual},
author = {\mbox{The Coq development team}},
organization = {LogiCal Project},
note = {Version 8.0},
year = {2004},
url = "http://coq.inria.fr"
}
@article{afp-dfs,
author = {Toshiaki Nishihara and Yasuhiko Minamide},
title = {Depth First Search},
journal = {Archive of Formal Proofs},
month = jun,
year = 2004,
note = {\url{http://afp.sf.net/entries/Depth-First-Search.shtml},
Formal proof development},
ISSN = {2150-914x},
}
\section{Fazit und Ausblick}\label{sec:conclusion}
Was bedeuten also die Zahlen aus der Evaluation?
In welchen Situationen ist die vorgestellte Lösung empfehlenswert?
Als Ausblick dürfen offene Fragen genannt werden.
Aus Zeitgründen bleiben üblicherweise einige interessante Fragen unbeantwortet.
Womit könnten spätere Studenten sich beschäftigen?
In diesem Kapitel sind ein bischen persönliche Meinung
und Überzeugungen erlaubt.
Der Rest der Arbeit sollte so objektiv wie möglich sein.
\section{Evaluation}\label{sec:eval}
Hier wird nun das Ergebnis des vorherigen Kapitels kritisch betrachtet.
Verbesserungen werden anhand von konkreten Experimenten und Zahlen belegt.
Eine saubere statistische Auswertung ist das Ziel.
Für schöne Tabellen ist das \enquote{booktabs} package zu empfehlen.
Ein Beispiel ist in \autoref{fig:example_table} zu sehen.
\begin{figure}[hb]
\begin{center}
\begin{tabular}{lrr}
\toprule
Fach & xkcd Comics & Spaß \\
\midrule
Informatik & 1325 & 100\% \\
Physik & 1324,31 & 87\% \\
Geologie & 123 & 23\% \\
Wirtschaft & 5 & 4\% \\
Deutsch & 0 & 101 \\
\midrule
& 743 & 63\% \\
\bottomrule
\end{tabular}
\end{center}
\caption{Eine Beispieltabelle.
Man beachte, dass zwischen Datenzeilen keine Linien sind.
Außerdem ist der Beschreibungstext hier sehr ausführlich,
damit der Leser nicht den zugehörigen Abschnitt im Fließtext finden muss.
}
\label{fig:example_table}
\end{figure}
\section{Entwurf und Implementierung}\label{sec:impl}
Hier wird die eigene Lösung des Problems vorgestellt,
sowie interessante Details der Implementierung.
Was also wurde praktisch in dieser Arbeit geleistet?
\section{Einführung}\label{sec:intro}
In diesem Kapitel wird das Problem vorgestellt, das diese Arbeit löst.
Es sollte verständlich sein (anschauliches Beispiel?).
Das Problem sollte wichtig sein,
denn das motiviert weiterzulesen.
Bestenfalls ist dieses Kapitel auch für Laien verständlich.
\usepackage{lmodern}
\usepackage[german]{babel}
\usepackage{tikz}
\usetikzlibrary{positioning,calc,arrows}
\usepackage{listings}
\usepackage{titling}
\newcommand{\thesistype}[1]{\newcommand{\thethesistype}{#1}}
\newcommand{\zweitgutachter}[1]{\newcommand{\thezweitgutachter}{#1}}
\newcommand{\betreuer}[1]{\newcommand{\thebetreuer}{#1}}
\newcommand{\coverimage}[1]{\newcommand{\thecoverimage}{#1}}
\usepackage{csquotes}
\usepackage{amsmath}
\usepackage[labelformat=simple]{subfig}
\usepackage[font={sf},margin=10pt,labelfont=bf]{caption}
\usepackage{booktabs}
\usepackage[colorlinks=false]{hyperref}
\usepackage{fancyhdr}
\pagestyle{fancy}
\fancyhead{} % clear all header fields
\fancyhead[LE,RO]{\slshape \rightmark}
\fancyfoot{} % clear all footer fields
\fancyfoot[LE,RO]{\thepage}
\definecolor{todo}{rgb}{0.8,0,0}
\newcommand\tod[1]{\texttt{\textcolor{todo}{#1}}}
\newcommand\todo[1]{\par\texttt{\textcolor{todo}{#1}}\par}
\newcommand{\mytitlepage}{
\begin{titlepage}
\begin{tikzpicture}[remember picture,overlay]
% Seitenrahmen zeichnen.
\draw[semithick,rounded corners=0.5cm]
($(current page.north west) + ( 1cm,-1cm)$) --
($(current page.north east) + (-1cm,-1cm)$) --
($(current page.south east) + (-1cm, 1.5cm)$);
\draw[semithick,rounded corners=0.5cm]
($(current page.south east) + (-1cm, 1.5cm)$) --
($(current page.south west) + ( 1cm, 1.5cm)$) --
($(current page.north west) + ( 1cm,-1cm)$);
% Logo einbinden.
\node[anchor=north west] (logo) at ($(current page.north west) + (1.75cm,-1.5cm)$)
{
\includegraphics[width=4cm]{KITLogo}
};
% Institut / Lehrstuhl.
\node[anchor=east] at ($(current page.east |- logo.east) + (-1.75cm,0cm)$)
{
\begin{minipage}{5.2cm}
\begin{flushleft}
\footnotesize{}Institut für Programmstrukturen und Datenorganisation (IPD) \\
\vspace{6pt}
Lehrstuhl Prof.\ Dr.-Ing.\ Snelting
\end{flushleft}
\end{minipage}
};
\node (title) at ($(current page.center |- logo.south) + (0cm, -4cm)$)
{
% Korrekter Zeilenabstand etc. durch Minipage.
\begin{minipage}{12cm}
\begin{center}
\huge\textbf{\thetitle}
\end{center}
\end{minipage}
};
\node[below=1.05cm of title.south] (prename) { \thethesistype\ von };
\node[below=0.75cm of prename.south] (name) { \Large{}\textbf{\theauthor} };
\node[below=0.8cm of name.south] (postname) { an der Fakultät für Informatik };
\node[below=0.5cm of postname.south] (bildchen) { \includegraphics[width=0.8\textwidth]{\thecoverimage}
};
\node[below=0.4cm of bildchen.south] (table)
{
\begin{tabular}{ll}
\textbf{Erstgutachter:} & Prof.\ Dr.-Ing.\ Gregor Snelting \\[5pt]
\textbf{Zweitgutachter:} & \thezweitgutachter\\[5pt]
\textbf{Betreuende Mitarbeiter:} & \thebetreuer \\
\end{tabular}
};
\node[below=1.3cm of table.south] (time)
{
\begin{tabular}{ll}
\textbf{Bearbeitungszeit:} & 4. Juli 2013 -- \thedate
\end{tabular}
};
% Fußzeile, unten zentriert.
\node[anchor=south] (footnote) at ($(current page.center |- current page.south) + (0cm, 0.65cm)$)
{
\tiny{}KIT -- Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft
\hspace{0.5cm}
\Large{}\textbf{www.kit.edu}
};
\end{tikzpicture}
\end{titlepage}
}
\documentclass[12pt,a4paper,twoside]{scrartcl}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{studarbeit}
\title{Evaluation of Randomized Algorithms}
\author{Alice Müller}
\date{\today}
\thesistype{Bachelorarbeit}
\zweitgutachter{Prof. Dr. Bernhard Beckert}% for verification stuff
%\zweitgutachter{Prof. Dr. Jörg Henkel}% for compiler stuff
\betreuer{Sebastian Mohr}
\coverimage{4665389330_d09f3d6b75_z.jpg}
\begin{document}
\mytitlepage
\clearpage
\section*{Zusammenfassung}
\vfill
\begin{abstract}
Konsistentes Hashen und Voice-over-IP
wurde bisher nicht als robust angesehen,
obwohl sie theoretisch essentiell sind.
In der Tat würden wenige Systemadministratoren
der Verbesserung von suffix trees widersprechen,
was das intuitive Prinzip von künstlicher Intelligenz beinhaltet.
Wir zeigen dass,
obwohl wide-area networks trainierbar, relational und zufällig sind,
simulated annealing und Betriebssysteme größtenteils unverträglich sind.
\end{abstract}
\vfill
\begin{abstract}
Consistent hashing and voice-over-IP, while essential in theory, have not until recently been considered robust. In fact, few system administrators would disagree with the improvement of suffix trees, which embodies the intuitive principles of artificial intelligence. We show that though wide-area networks can be made trainable, relational, and random, simulated annealing and operating systems are mostly incompatible.
\end{abstract}
\vfill
\todo{Das Titelbild ist von
\url{http://www.flickr.com/photos/x-ray_delta_one/4665389330/}
und muss durch ein zum Thema passendes Motiv ausgetauscht werden.}
\cleardoublepage
\tableofcontents
\cleardoublepage
\input{intro.tex}
\input{basics.tex}
\input{impl.tex}
\input{eval.tex}
\input{conclusion.tex}
\cleardoublepage
\bibliographystyle{abbrv}
\bibliography{bib}
\cleardoublepage
\pagestyle{empty}
\section*{Erklärung}
\vspace{20mm}
Hiermit erkläre ich, \theauthor, dass ich die vorliegende Bachelorarbeit selbst\-ständig
verfasst habe und keine anderen als die angegebenen Quellen und Hilfsmittel
benutzt habe, die wörtlich oder inhaltlich übernommenen Stellen als solche kenntlich gemacht und
die Satzung des KIT zur Sicherung guter wissenschaftlicher Praxis beachtet habe.
\vspace{20mm}
\begin{tabbing}
\rule{4cm}{.4pt}\hspace{1cm} \= \rule{7cm}{.4pt} \\
Ort, Datum \> Unterschrift
\end{tabbing}
\cleardoublepage