thesis.tex

\documentclass[11pt,twoside,a4paper]{book}
\usepackage[shorthands=off,english]{babel} % package for multilingual support

\RequirePackage{iftex}
\ifPDFTeX
    \usepackage[utf8]{inputenc} 
    \usepackage[T1]{fontenc}
    % \usepackage{lmodern}
\else
    \RequirePackage{fontspec} % UFT8 fonts for LuaLaTeX
    % \setmainfont{Latin Modern Roman}
\fi
\usepackage{csquotes}

\usepackage[ backend=biber
           , style=alphabetic % numeric
           , sortlocale=en_US
           , bibencoding=UTF8
           , sorting=anyt % explicit label, name, year, title
           , sortlocale=cs_CZ
           , maxnames=100
           , maxalphanames=4
           , maxbibnames=100
           , urldate=long
           ]{biblatex}
\DeclareSourcemap{
    \maps[datatype=bibtex, overwrite]{
        \map{
            \step[fieldset=editor, null]
            \step[fieldset=language, null]
        }
    }
}

\usepackage{xcolor}
\definecolor{dark-red}{rgb}{0.6,0.15,0.15}
\definecolor{dark-green}{rgb}{0.15,0.4,0.15}
\definecolor{medium-blue}{rgb}{0,0,0.5}
\usepackage[ pdfauthor={Vladimir Still}
           , pdftitle={Analysis of Parallel C++ Programs},
           , pdfsubject={PHD Thesis},
           , plainpages=false
           , pdfpagelabels
           , unicode
           , draft=false
           , colorlinks=true
           , linkcolor={dark-red}
           , citecolor={dark-green}
           , urlcolor={medium-blue}
           , unicode=true
           ]{hyperref}

\usepackage{amssymb,amsmath,amsthm}
\usepackage{paralist}
\usepackage{multicol}
% use upquote for straight quotes in verbatim environments
\usepackage{upquote}
\usepackage{minted}

\newminted[cppcode]{cpp}{autogobble,breaklines}
\newminted[cppcodeln]{cpp}{autogobble,breaklines,linenos}
\newmintinline[cpp]{cpp}{}

\newmintinline[java]{java}{}

\newmintinline[llvmcode]{llvm}{autogobble,breaklines}
\newmintedfile[llvminput]{llvm}{breaklines}
\newmintinline[li]{llvm}{}

\usepackage{xspace}
\usepackage{pgf}
\usepackage{tikz}
\usetikzlibrary{arrows,positioning,shapes,automata,backgrounds,petri,fit,matrix,decorations.pathreplacing,calc}
\tikzset{
    *|/.style={
        to path={
            (perpendicular cs: horizontal line through={(\tikztostart)},
                                 vertical line through={(\tikztotarget)})
            % is the same as (\tikztostart -| \tikztotarget)
            % but just to be safe: http://tex.stackexchange.com/a/29781/16595
            -- (\tikztotarget) \tikztonodes
        }
    },
	|*/.style={to path={
		(\tikztostart) -- (perpendicular cs: vertical line through={(\tikztostart)},
											 horizontal line through={(\tikztotarget)})
  	}}
}
\usepackage{pgfplots}
\pgfplotsset{
    compat=1.16,
    every axis/.append style={
        axis on top,
        scatter/classes={ %
            tt={mark=square,thick,green!70!black}, %
            tT={mark=x,thick,green!70!black}, %
            fT={mark=x,thick,blue}, %
            MT={mark=x,thick,black}, %
            TT={mark=x,thick,black}, %
            MM={mark=x,thick,black}, %
            tf={mark=triangle,thick,red}, %
            ft={mark=triangle,thick,red}, %
            ff={mark=o,thick,blue}
        }, scatter src=explicit symbolic, axis equal
    }
}

\usepackage{changepage}

\usepackage{floatpag} % get the \at@float@page hook
\usepackage{float} % after floatpag so H works
\makeatletter
% custom float style, derived from ruled
% - caption is at the bottom
% - spaces before and after figure are larger
% - rules are thinner
% - bottom rule is missing
\newcommand\floatc@botruled[2]{{\@fs@cfont #1} #2\par}
\newcommand\fs@botruled{\def\@fs@cfont{\bfseries}\let\@fs@capt\floatc@botruled%
    \def\@fs@pre{\hrule\kern0.5\abovecaptionskip}%
    \def\@fs@post{}%
    \def\@fs@mid{\kern0.5\abovecaptionskip\hrule\kern0.5\abovecaptionskip}%
\let\@fs@iftopcapt\iffalse}

\gdef\at@float@page{}
\let\thesis@old@at@float@page\relax
\newenvironment{widefigure}{%
    \let\thesis@old@at@float@page\at@float@page%
    \gdef\at@float@page{%
        \let\thesis@float@cpg\clearpage%
        \let\clearpage\relax%
        \widegeom%
        \let\clearpage\thesis@float@cpg%
        \gdef\at@float@page{\thesis@old@at@float@page}
    }%
    \begin{figure}[p]
    \changetext{}{\marginparwidth+\marginparsep}{}{}{}%
  }{\end{figure}}
\makeatother
\floatstyle{botruled}
\restylefloat{figure}
\usepackage[labelfont=bf]{caption}
\usepackage{subcaption}

\usepackage{multirow}
\usepackage{microtype}

\usepackage{tabularx}
\newcolumntype{C}{>{\centering\arraybackslash}X}
\newcolumntype{R}{>{\raggedleft\arraybackslash}X}
\newcolumntype{L}{>{}X}
\usepackage{booktabs}
\usepackage{arydshln}

\hyphenation{DIVINE DiOS LLVM LTL%
             se-quen-tial-iza-tion}

\input{defs}

\newcommand{\note}{\textit{Note:}\xspace}
\newcommand{\fcite}[1]{\emergencystretch 3em\fullcite{#1}~\cite{#1}\medskip}

\renewcommand{\indent}{\mbox{}\ \ \ \ }
\colorlet{frombuf}{green!60!black}
\colorlet{flushed}{yellow!60!red!85!black}

\newtheorem{theorem}{Theorem}[chapter]
\newtheorem{lemma}{Lemma}[chapter]

\newtheoremstyle{mydefstyle}%
  {\topsep}% space above (default)
  {\topsep}% space below (default)
  {}% body font
  {}% indent amount
  {\bf}% theorem head font
  {}% Punctuation after theorem head
  {\newline}% space after theorem head
  {\thmname{#1}\thmnumber{ #2}\thmnote{: #3}}% theorem head spec (empty = normal)
\theoremstyle{mydefstyle}
\newtheorem{definition}{Definition}[chapter]

\addbibresource{thesis.bib}
\addbibresource{my.bib}

\usepackage[a4paper]{geometry}
\newcommand{\geom}[2]{\csname #1geometry\endcsname{
        bindingoffset=1.5cm, inner=1.5cm, outer=1.5cm, top=1.5cm, bottom=2.5cm,
%        headheight=15.2pt, % for the sake of fancyhdr
        includehead, headsep=1cm,
        includemp, % count outer margin outside of the marginpar
        #2
    }}
\newcommand{\widegeom}{\geom{new}{nomarginpar}}
\newcommand{\margingeom}{\geom{new}{marginparsep=0.8cm, marginparwidth=4cm}}
\widegeom % will override later, set here for the sake of headers
\usepackage{fancyhdr}
\fancyhf{}
\fancyhead[LE]{\footnotesize\makebox[\widthof{000}]{\thepage\hfill}~\leftmark}
\fancyhead[RO]{\footnotesize\rightmark~\makebox[\widthof{000}]{\hfill\thepage}}
\renewcommand{\headrulewidth}{0pt} % remove lines after header
\renewcommand{\footrulewidth}{0pt}
% also restyle the chapter start page
\fancypagestyle{plain}{
  \fancyhf{}
  \fancyhead[LE,RO]{\footnotesize\thepage}
  \renewcommand{\headrulewidth}{0pt}
}
% set marks for headers -- chapter mark contains only the chapter name, section
% mark has the dot after the section number removed (to match the actual
% section heading)
\pagestyle{fancy} % initialize before setting marks
\makeatletter
\def\chaptermark#1{%
  \markboth{|\qquad\MakeUppercase{#1}}{}}
\def\sectionmark#1{%
  \markright{\MakeUppercase{%
    \ifnum \c@secnumdepth >\z@
      \thesection \ %
    \fi
    #1\qquad|}}}
\makeatother


\usepackage{setspace}

\usepackage{enumitem}
\providecommand{\tightlist}{%
  \setlength{\itemsep}{0pt}%
  \setlength{\parskip}{0pt}%
  \setlength{\topsep}{0pt}%
  \setlength{\partopsep}{0pt}}

\newcommand{\TODO}[1]{{\bf\color{red}#1}}

% autoref names
\addto\extrasenglish{%
    \renewcommand{\chapterautorefname}{Chapter}%
    \renewcommand{\sectionautorefname}{Section}%
    \renewcommand{\subsectionautorefname}{Section}%
    \def\definitionautorefname{Definition}%
}

\newcommand{\rot}[1]{\rotatebox{90}{#1\hspace*{0.5em}}}

% \setlength{\overfullrule}{5pt} % TODO: remove

% try to avoid overfull lines, taken from \sloppy, but without allowing greater
% tolerance for paragraphs without any problems
% \emergencystretch 3em

\newenvironment{stretched}{\emergencystretch 3em}{}

\setcounter{tocdepth}{1}

%% MARGIN NOTES %%
\usepackage{marginfix}
\usepackage{ragged2e}
\usepackage{ifoddpage}
\newcommand{\raggedoutunsafe}{\ifoddpage\RaggedRight\else\RaggedLeft\fi}
\newcommand{\raggedout}{\checkoddpage\raggedoutunsafe}
\newcounter{mnote}[chapter]
\newcommand{\mnotemark}[1][\arabic{mnote}]{\stepcounter{mnote}\hyperlink{mnote:\thechapter:\themnote}{\textsuperscript{#1}}\xspace}
\newcommand{\mnotetext}[2][\arabic{mnote}]{\marginpar{\raggedout\hypertarget{mnote:\thechapter:\themnote}{\textsuperscript{#1}\,}\footnotesize{}#2}}
\newcommand{\mnote}[2][\arabic{mnote}]{\mnotemark[#1]{}\mnotetext[#1]{#2}}

\newenvironment{marginnote}{%
        \mnotemark%
        \expandafter\newbox\csname marginnotebox:\thechapter:\themnote\endcsname%
        \expandafter\setbox\csname marginnotebox:\thechapter:\themnote\endcsname=\hbox to \marginparwidth\bgroup%
            \noindent%
            \begin{minipage}{\marginparwidth}%
            \RecustomVerbatimEnvironment{Verbatim}{BVerbatim}{}%
            \hypertarget{mnote:\thechapter:\themnote}{${}^{\arabic{mnote}}\,$}%
            \raggedout\footnotesize\noindent%
    }{%
            \end{minipage}%
        \egroup%
        \marginpar{\expandafter\unhbox\csname marginnotebox:\thechapter:\themnote\endcsname{}}
    }

% allows us to use make names in side margin citations link to DOI-based
% publication page
\newbibmacro{string+doi}[1]{%
  \iffieldundef{doi}{%
    \iffieldundef{url}{%
      #1%
    }{%
      \href{\thefield{url}}{#1}%
    }%
  }{%
    \href{http://dx.doi.org/\thefield{doi}}{#1}%
  }%
}
\DeclareFieldFormat{titlelink}{\usebibmacro{string+doi}{``#1''}}

\usepackage{listofitems}
\makeatletter
\newcommand{\mcite}[2][]{%
\checkoddpage% sync page numbers for \oddpage@page (\thepage is wrong)
\readlist*\cilist{#2}%
\foreachitem\ci\in\cilist[]{%
\ifcsname mcite: \oddpage@page : \ci\endcsname%
  \checkoddpage% hack to ensure the number of page marks does now change if we hide a margin citation
\else%
  \expandafter\def\csname mcite: \oddpage@page : \ci\endcsname{}%
  \marginpar{%
    \raggedout\hypertarget{mcite:\oddpage@page:\ci}\footnotesize\cite{\ci} \citeauthor*{\ci}, \citefield{\ci}[titlelink]{title}.%
    % define note is on this page it once more in case we were forced to the next page
    \expandafter\gdef\csname mcite: \oddpage@page : \ci\endcsname{}%
  }%
\fi%
}%
\cite[#1]{#2}%
}
\makeatother

% set space between margin notes -- unofficial, but works (unline \marginskip)
\setlength\marginparpush\bigskipamount
%%

\newcommand{\srcnote}[1]{\emph{#1}}

\usepackage{halloweenmath}
\newif\ifthesis
\thesistrue

\clubpenalty=4000
\widowpenalty=4000

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
% initial pages from Mornfall + modifications
\frontmatter

\begin{titlepage}
\newgeometry{margin=4cm}
\begin{center}
    {\Large \sc \FI, \MU}
    \vskip4em
    \includegraphics[width = 4cm, height = 4cm] {logo_fi.pdf}
    \vskip4em
    \begin{spacing}{1}
        \Huge \bf \thesistitle
    \end{spacing}
    \vskip2em
    {\Large \sc \thesissubtitle}
    \vskip4em
    {\LARGE \bf \thesisauthor}
    \vfill
\end{center}
\textbf{Supervisor:}\\
\thesisadvisor \hfill \thesisYearCity
\end{titlepage}

% set headers by the wide geometry
\pagestyle{fancy}
\margingeom
\cleardoublepage

\section*{Declaration} % from Mornfall
Thereby I declare that this thesis is my original work, which I have
created on my own. All sources and literature used in writing the
thesis, as well as any quoted material, are properly cited, including
full reference to its source.

\bigskip\bigskip
\hfill\thesisauthor

\vfill
\textbf{Supervisor:} \thesisadvisor

\cleardoublepage

\section*{Abstract}
\input{abstract}

%\vfill
\clearpage
\section*{Keywords}
    program analysis,
    software verification,
    C++,
    DIVINE,
    LLVM,
    parallelism,
    concurrency,
    relaxed memory,
    memory models,
    exceptions,
    termination,
    program transformation,
    implementation
\cleardoublepage

\section*{Acknowledgments}
\input{acknowledgements}
\cleardoublepage

\bgroup
\def\markboth#1#2{}
\tableofcontents
\egroup

\mainmatter

\chapter{Introduction}\label{chap:introduction}
\input{intro}

\chapter{Preliminaries}\label{chap:preliminaries}
\input{preliminaries}

\chapter{State of the Art}\label{chap:stateoftheart}
\input{stateoftheart}

\chapter{Improvements in Analysis of Realistic Programs}\label{chap:lang}
\input{realprogs}

\chapter{Analysis of Programs Under the \xtso Relaxed Memory Model}\label{chap:mm}
\input{memorymodels}

\chapter{Local Nontermination analysis for Parallel Programs}\label{chap:lnterm}
\input{termination}

\chapter{Conclusion}\label{chap:conclusion}
\input{conclusion}

\appendix

\chapter{Published Papers}\label{chap:published}
\input{papers}

\widegeom
\chapter{Bibliography}
% \addcontentsline{toc}{chapter}{Bibliography}

{
    \emergencystretch 3em % there is little other fixing possible for bibio
    \printbibliography[heading=none]
}

\end{document}