Commit e00d43bf authored by phlo's avatar phlo

started thesis

parent 4205c980
$pdf_mode = 1;
$pdf_previewer = 'start zathura';
$pdflatex = 'pdflatex -interaction=nonstopmode';
@default_files = ('thesis.tex');
preview:
latexmk -pvc
%%Andreas Neubauer, May 2016
\documentclass[12pt,a4paper]{article}
\usepackage{graphicx}
\graphicspath{{cover/}}
\textwidth 16.7cm
\textheight 25cm
\topmargin -2.7cm
\oddsidemargin 0.25cm
\parindent 0pt
\pagestyle{empty}
\begin{document}
%
% -------- only change entries beginning here ----------------------------
%
% choose language of coverpage: german or english
\newif\ifeng
\engtrue
%\engfalse
%
%
% enter the title of the thesis
%
\def\title{Title of the thesis}
%
%
% choose type of work: 0 ... Dissertation
% 1 ... Diplomarbeit
% 2 ... Masterarbeit
\def\type{2}
%
%
% enter name of degree, see examples below (as stated in your curriculum)
%
% e.g. Masterstudium
%\def\degree{Diplom-Ingenieur}
%\def\degree{Diplom-Ingenieurin}
\def\degree{Master of Science}
%
% e.g. Diplomstudium Lehramt
%\def\degree{Magister der Naturwissenschaften}
%\def\degree{Magistra der Naturwissenschaften}
%
% e.g. Doktorratsstudium
%\def\degree{Doktor der technischen Wissenschaften}
%\def\degree{Doktorin der technischen Wissenschaften}
%\def\degree{Doktor der Naturwissenschaften}
%\def\degree{Doktorin der Naturwissenschaften}
%
%
% enter the study (Studienrichtung, as stated in your curriculum)
%
% e.g. Diplomstudium:
%\def\study{Lehramt Mathematik}
%
% e.g. Masterstudium:
\def\study{Computer Science}
%
% e.g. Doktorratsstudium
%\def\study{Technische Wissenschaften}
%\def\study{Naturwissenschaften}
%
%
% If the names for the following entries are too long, break them into several
% lines using \\
%
%
% enter the name of the student
%
\def\name{Florian Schr\"ogendorfer}
%
%
% enter the name of the institute (use translation for english version)
% e.g.
%\def\institute{Industrial Mathematics\\ Institute}
%\def\institute{Institut f\"ur\\ Industriemathematik}
%
\def\institute{Institute for Formal Models and Verification}
%
%
% enter the name of the supervisor and first thesis examiner
% only for type 0 (Dissertation) you need a second thesis examiner
%
% for the german version you also have to enter the sex (male or female)
% of the supervisor/examiners
%
\def\supervisor{Armin Biere}
\newif\ifsupvismale
\supvismaletrue
%\supvismalefalse
%
\def\secondexaminer{Name of 2. examiner}
\newif\ifsecexmale
\secexmaletrue
%\secexmalefalse
%
%
% if there has been assistance by a further person uncomment the following line
% and enter the name.
%
\def\assist{Name of assistant}
%
%
% enter month year
% (the month when you brought it to the Prüfungs- und Anerkennungsservice)
%
\def\date{month year}
%
% do not change anything below this line
% -------------------------------------------------------------------------------
%
\def\ifundefined#1{\expandafter\ifx\csname#1\endcsname\relax}
\DeclareFontShape{OT1}{cmss}{m}{n}
{<5><6><7><8><9><10><10.95><12><14.4><17.28><20.74><24.88><29.86><35.83>%
<42.99><51.59><67><77.38>cmss10}{}
\DeclareFontShape{OT1}{cmss}{bx}{n}
{<5><6><7><8><9><10><10.95><12><14.4><17.28><20.74><24.88><29.86><35.83>%
<42.99><51.59><67><77.38>cmssbx10}{}
\makeatletter
\def\Huge{\@setfontsize\Huge{29.86pt}{36}}
\makeatother
%
\unitlength 1cm
\sffamily
\begin{picture}(16.7,0)
\ifeng
\put(11.5,-2.5){\includegraphics[width=5.2cm]{jku_en}}
\else
\put(11.5,-2.5){\includegraphics[width=5.2cm]{jku_de}}
\fi
\put(12.9,-4.2){\begin{minipage}[t]{3.9cm}\footnotesize%
\ifeng
Submitted by\\
\else
Eingereicht von\\
\fi
{\bfseries\name}%
\vskip 4mm%
\ifeng
Submitted at\\
\else
Angefertigt am\\
\fi
{\bfseries\institute}%
\vskip 4mm%
\ifcase\type%
\ifeng
Supervisor and\\ First Examiner\\
\else
\ifsupvismale%
Betreuer und\\ Erstbeurteiler\\
\else
Betreuerin und\\ Erstbeurteilerin\\
\fi
\fi
{\bfseries\supervisor}%
\vskip 4mm%
\ifeng
Second Examiner\\
\else
\ifsecexmale%
Zweitbeurteiler\\
\else
Zweitbeurteilerin\\
\fi
\fi
{\bfseries\secondexaminer}%
\else
\ifeng
Supervisor\\
\else
\ifsupvismale%
Betreuer\\
\else
Betreuerin\\
\fi
\fi
{\bfseries\supervisor}%
\fi
\vskip 4mm%
\ifundefined{assist}\else
\ifeng
Co-Supervisor\\
\else
Mitbetreuung\\
\fi
{\bfseries\assist}%
\vskip 4mm%
\fi
\date
\end{minipage}}
\put(12.9,-25){\begin{minipage}[t]{3.9cm}\footnotesize%
{\bfseries JOHANNES KEPLER\\
\ifeng
UNIVERSITY
\else
UNIVERSIT\"AT
\fi
LINZ}\\
Altenbergerstra{\ss}e 69\\
4040 Linz, \"Osterreich\\
www.jku.at\\
DVR 0093696
\end{minipage}}
\put(0,-12.2){\begin{minipage}[b]{12cm}\Huge\bfseries\title\end{minipage}}
\put(0,-17.2){\includegraphics[width=4.4cm]{arr}}
\put(0,-18.3){\begin{minipage}[t]{12cm}%
\ifeng
{\large\ifcase\type Doctoral \or Diploma \or Master \fi Thesis}%
\vskip 2mm%
to obtain the academic degree of%
\vskip 3mm%
{\large\degree}
\vskip 3mm%
in the \ifcase\type Doctoral \or Diploma \or Master's \fi Program
\else
{\large\ifcase\type Dissertation\or Diplomarbeit\or Masterarbeit\fi}%
\vskip 2mm%
zur Erlangung des akademischen Grades%
\vskip 3mm%
{\large\degree}
\vskip 3mm%
im \ifcase\type Doktoratsstudium \or Diplomstudium\or Masterstudium\fi
\fi
\vskip 3mm%
{\large\study}
\end{minipage}}
\end{picture}
\end{document}
% layers
\pgfdeclarelayer{background}
\pgfdeclarelayer{foreground}
\pgfsetlayers{background, main, foreground}
% styles
\tikzstyle{box} = [draw, text centered, rounded corners]
\tikzstyle{register} = [box, fill=white, minimum height=2em, minimum width=4em]
\tikzstyle{processor} = [draw, fill=blue!10, rounded corners]
\tikzstyle{buffer} = [processor, fill=red!10, dashed]
% distances
\def\blockdist{3}
\def\borderdist{0.2}
\begin{tikzpicture}
% processor 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\path (0, 0) node (title-0) [] {\textbf{Processor 0}};
% store buffer
\path (title-0)+(0, -1) node (sb-0) [] {store buffer};
\path (sb-0)+(0, -1) node (full-0) [register] {full};
\path (full-0)+(0, -1) node (adr-0) [register] {address};
\path (adr-0)+(0, -1) node (val-0) [register] {value};
% registers
\path (val-0)+(-1.1, -1.5) node (accu-0) [register] {accu};
\path (val-0)+(1.1, -1.5) node (mem-0) [register, dashed] {mem};
% paths
\path [draw, <->] (val-0.west) -- (val-0.west -| accu-0.north) -- (accu-0.north);
\path [draw, ->] (val-0.east) -- (val-0.east -| mem-0.north) -- (mem-0.north);
\begin{pgfonlayer}{background}
% bounding box
\path (accu-0.west |- title-0.north)+(-\borderdist, \borderdist) node (a) {};
\path (mem-0.south east)+(\borderdist, -\borderdist) node (b) {};
\path [processor] (a) rectangle (b);
% top left heap coordinate
\path (a |- b)+(0, -1) node (tlh) {};
% store buffer box
\path (sb-0.north west)+(-\borderdist, \borderdist) node (a) {};
\path (val-0.south -| sb-0.east)+(\borderdist, -\borderdist) node (b) {};
\path [buffer] (a) rectangle (b);
\end{pgfonlayer}
% dots %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\path (title-0)+(\blockdist, 0) node (dots) [] {\large $\ldots$};
% processor n %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\path (dots)+(\blockdist, 0) node (title-n) [] {\textbf{Processor n}};
% store buffer
\path (title-n)+(0, -1) node (sb-n) [] {store buffer};
\path (sb-n)+(0, -1) node (full-n) [register] {full};
\path (full-n)+(0, -1) node (adr-n) [register] {address};
\path (adr-n)+(0, -1) node (val-n) [register] {value};
% registers
\path (val-n)+(-1.1, -1.5) node (accu-n) [register] {accu};
\path (val-n)+(1.1, -1.5) node (mem-n) [register, dashed] {mem};
% paths
\path [draw, <->] (val-n.west) -- (val-n.west -| accu-n.north) -- (accu-n.north);
\path [draw, ->] (val-n.east) -- (val-n.east -| mem-n.north) -- (mem-n.north);
\begin{pgfonlayer}{background}
% bounding box
\path (accu-n.west |- title-n.north)+(-\borderdist, \borderdist) node (a) {};
\path (mem-n.south east)+(\borderdist, -\borderdist) node (b) {};
\path [processor] (a) rectangle (b);
% bottom right heap coordinate
\path (b)+(0, -\blockdist) node (brh) {};
% store buffer box
\path (sb-n.north west)+(-\borderdist, \borderdist) node (a) {};
\path (val-n.south -| sb-n.east)+(\borderdist, -\borderdist) node (b) {};
\path [buffer] (a) rectangle (b);
\end{pgfonlayer}
% heap %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\path [box] (tlh) rectangle node (heap) [minimum height=2cm] {shared memory} (brh);
% paths
\path [draw, ->] (val-0) -- (heap.north -| val-0);
\path [draw, <->] (accu-0) -- (heap.north -| accu-0);
\path [draw, <-] (mem-0) -- (heap.north -| mem-0);
\path [draw, ->] (val-n) -- (heap.north -| val-n);
\path [draw, <->] (accu-n) -- (heap.north -| accu-n);
\path [draw, <-] (mem-n) -- (heap.north -| mem-n);
\end{tikzpicture}
% libraries
\usetikzlibrary{positioning}
% styles
\tikzstyle{module} = [draw, fill=blue!10, text centered, rounded corners, minimum height=1cm, minimum width=2.5cm]
\tikzstyle{file} = [module, fill=red!10]
\begin{tikzpicture}[auto]
\node [file] (program) {program};
\node [module] (simulate) [above right=0cm and 1cm of program] {\texttt{simulate}};
\path [draw, ->] (program.east) -- ++(0.5, 0) |- (simulate);
\node [module] (solve) [below right=0cm and 1cm of program] {\texttt{solve}};
\path [draw, ->] (program.east) -- ++(0.5, 0) |- (solve);
\node [file] (trace) [below right=0cm and 1cm of simulate] {trace};
\path [draw, ->] (simulate.east) -- ++(0.5, 0) |- (trace);
\path [draw, ->] (solve.east) -- ++(0.5, 0) |- (trace);
\node [module, dashed] (replay) [right= of trace] {\texttt{replay}} edge [<-, dashed] (trace);
\path [draw, dashed, ->] (replay) -- (replay.north |- simulate) -| (trace.north);
\end{tikzpicture}
\section{Introduction}
\subsection{Toolchain}
\begin{figure}[h]
\centering
\input{figures/toolchain.tex}
\caption{Toolchain}
\end{figure}
\section{Machine Model}
% intro
% Our abstract machine model of a x86 multiprocessor system is illustrated in Figure \ref{fig:machine:overview}.
%We will start by defining an abstract machine model of a multiprocessor system that allows stores to be reordered after loads.
%Since we are only concerned with the machine's behaviour as observed by assembly programs, the internal structure of any real processor's microarchitecture is a highly abstracted.
%To keep the state space of the resulting model checking problems as small as possible, we defined our model on the basis of a 16 bit, 1 register machine.
% consistent with amd/intel litmus tests
% as observed by assembly programs.
% to reduce the state space, while emulating the behaviour of a x86 multiprocessor system.
% * abstract machine model to investigate the interaction of parallel programs through shared memory.
We will start by defining an abstract machine model of a multiprocessor system as observed by assembly programs.
To keep the state space of the resulting model checking problems as small as possible, it is based on a 16 bit architecture, using only a minimal set of registers and a radically reduced instruction set.
\begin{figure}[h]
\centering
\input{figures/architecture.tex}
\caption{Abstract Machine Model}
\label{fig:machine:overview}
\end{figure}
A schematic overview is illustrated in Figure \ref{fig:machine:overview}.
At the top of the figure are an arbitrary number of processors, each containing:
\begin{itemize}
\item \accu: a single 16 bit accumulator register
\item \mem: a special purpose 16 bit register, storing the expected value required by a unary \emph{compare and swap} instruction
% \item a \emph{store buffer} to break sequential consistency by delaying a single write, consisting of:
\item a single element \emph{store buffer}, consisting of:
\begin{itemize}
\item \sbfull: a one bit flag register, signaling that it contains a value and may be flushed
\item \sbadr: a 16 bit address register
\item \sbval: a 16 bit value register
\end{itemize}
\end{itemize}
All processors are directly connected to the machine's shared memory, which will be uninitialized with the exception of any eventual input data.
In terms of memory ordering, the addition of a \emph{store buffer} allows stores to be reordered after loads, making our model consistent with Intel's or AMD's x86 memory ordering model \cite{intel, amd}.
\subsection{Instructions}
To keep things simple, instructions are not stored in memory and labelled using the following attributes:
% Since we are not considering an actual implementation, the stream of instructions can be seen as hardwired to each of the processors.
\begin{itemize}
\item \textbf{accu} -- modifies accumulator contents
\item \textbf{mem} -- modifies CAS memory register contents
\item \textbf{modify} -- modifies a register's content (accu or mem)
\item \textbf{read} -- reads from memory
\item \textbf{write} -- writes to memory
\item \textbf{barrier} -- memory barrier - requires the store buffer to be flushed
\item \textbf{atomic} -- atomic operations (implies barrier)
\item \textbf{control} -- control flow operation
\end{itemize}
\subsubsection{ADDI - Immediate Addition}
\paragraph{Syntax:} \texttt{ADDI val}
\paragraph{Description:} Adds an intermediate value \texttt{val} to \accu.
\begin{tabular}{|l|l|l|}
\hline
\textbf{Symbol} & \textbf{Operand} & \textbf{Description} \\
\hline
\texttt{ADDI} & val & Adds the immediate value val to the accumulator \\
\hline
\end{tabular}
\subsection{Operational Semantics}
\begin{enumerate}
\item thread $t$ can execute a read, modify or control operation at any time
\item thread $t$ can voluntarily flush its store buffer to memory at any time
\item thread $t$ can read value $v$ from it's store buffer for address $a$ only if it contains a write to $a$
\item thread $t$ can read value $v$ directly from memory at address $a$ only if it's store buffer does not contain a write to $a$
\item thread $t$ can write value $v$ for address $a$ to its store buffer only if it is empty and $t$ performs a write operation
\item thread $t$ can write value $v$ directly to memory at address $a$ only if it performs an *atomic* operation
\item thread $t$ can perform an atomic or barrier operation only if its store buffer is empty
\item the machine stops and returns exit code $e$ if any thread $t$ executes an EXIT instruction
\end{enumerate}
@article{ref:McKenney17,
author = {Paul E. McKenney},
title = {Is Parallel Programming Hard, And, If So, What Can You Do About It? (v2017.01.02a)},
journal = {CoRR},
volume = {abs/1701.00854},
year = {2017}
}
@article{ref:Sewell10,
author = {Sewell, Peter and Sarkar, Susmit and Owens, Scott and Nardelli, Francesco Zappa and Myreen, Magnus O.},
title = {X86-TSO: A Rigorous and Usable Programmer’s Model for X86 Multiprocessors},
year = {2010},
issue_date = {July 2010},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {53},
number = {7},
issn = {0001-0782},
url = {https://doi.org/10.1145/1785414.1785443},
doi = {10.1145/1785414.1785443},
journal = {Commun. ACM},
month = jul,
pages = {89–97},
numpages = {9}
}
@article{intel,
author = {Intel Corporation},
title = {Intel 64 and IA-32 Architectures Software Developer's Manual, rev. 63},
month = {October},
year = {2019},
url = {https://software.intel.com/en-us/articles/intel-sdm},
}
@article{amd,
author = {Advanced Micro Devices},
title = {AMD64 Architecture Programmer's Manual Volume 2: System Programming, rev 3.32},
month = {October},
year = {2019},
url = {https://www.amd.com/system/files/TechDocs/24593.pdf},
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% preamble
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[12pt,a4paper]{article}
% character encoding
\usepackage[utf8]{inputenc}
% hyperlinks
\usepackage{hyperref}
% tikz
\usepackage{tikz}
\tikzset{>=latex}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% commands
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% variable names
\newcommand{\accu}{\texttt{accu}}
\newcommand{\mem}{\texttt{mem}}
\newcommand{\sbfull}{\texttt{sb-full}}
\newcommand{\sbadr}{\texttt{sb-adr}}
\newcommand{\sbval}{\texttt{sb-val}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% document
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
% \input{cover/coversheet}
\tableofcontents
\newpage
\listoffigures
\newpage
\input{introduction}
\newpage
\input{machine}
\newpage
\bibliographystyle{plain}
\bibliography{references}
\end{document}
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment