...
 
Commits (3)
This diff is collapsed.
% 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]
......
......@@ -42,7 +42,7 @@ At the top of the figure are an arbitrary number of processors, each containing:
\end{itemize}
All processors are directly connected to the machine's shared memory, referred to as \texttt{heap}, 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}.
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{ref:Intel, ref:AMD}.
\subsection{Instructions}
......@@ -244,5 +244,8 @@ Scheduling is generally performed non-deterministically under the following cons
\begin{enumerate}
\item A processor can execute a read, modify or control operation at any time.
\item A processor can voluntarily flush its store buffer to memory only if it is full.
\item A processor can execute a write, atomic or barrier operation only if it's store buffer is empty.
\item A processor can execute a write or barrier operation only if it's store buffer is empty.
\end{enumerate}
\todo[inline]{block while waiting for checkpoints?}
\todo[inline]{prevent scheduling of halted threads?}
@article{ref:BMC,
title={Bounded model checking.},
author={Biere, Armin and Cimatti, Alessandro and Clarke, Edmund M and Strichman, Ofer and Zhu, Yunshan and others},
journal={Advances in computers},
volume={58},
number={11},
pages={117--148},
year={2003}
}
@article{ref:McKenney17,
author = {Paul E. McKenney},
title = {Is Parallel Programming Hard, And, If So, What Can You Do About It? (v2017.01.02a)},
......@@ -7,24 +17,34 @@
}
@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}
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}
}
@inproceedings{ref:Sinz,
author = {Carsten Sinz},
title = {Towards an Optimal {CNF} Encoding of Boolean Cardinality Constraints},
booktitle = {Proc.\ of the 11th Intl.\ Conf.\ on Principles and Practice of Constraint Programming ({CP 2005})},
year = 2005,
month = Oct,
address = {Sitges, Spain},
pages = {827--831}
}
@article{intel,
@techreport{ref:Intel,
author = {Intel Corporation},
title = {Intel 64 and IA-32 Architectures Software Developer's Manual, rev. 63},
month = {October},
......@@ -32,7 +52,7 @@ numpages = {9}
url = {https://software.intel.com/en-us/articles/intel-sdm},
}
@article{amd,
@techreport{ref:AMD,
author = {Advanced Micro Devices},
title = {AMD64 Architecture Programmer's Manual Volume 2: System Programming, rev 3.32},
month = {October},
......@@ -40,7 +60,7 @@ numpages = {9}
url = {https://www.amd.com/system/files/TechDocs/24593.pdf},
}
@inproceedings{btor2,
@inproceedings{ref:BTOR2,
author = {Aina Niemetz and
Mathias Preiner and
Clifford Wolf and
......@@ -53,3 +73,11 @@ numpages = {9}
publisher = {Springer},
year = {2018}
}
@techreport{ref:SMT-Lib,
author = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
title = {{The SMT-LIB Standard: Version 2.6}},
institution = {Department of Computer Science, The University of Iowa},
year = 2017,
note = {Available at {\tt www.SMT-LIB.org}}
}
......@@ -22,6 +22,9 @@
% tables
\usepackage{tabu}
\usepackage{longtable}
\usepackage{caption}
% \captionsetup[longtable]{skip=0.5\baselineskip}
% code
\usepackage{listings}
......@@ -62,6 +65,7 @@
% tikz
\usepackage{tikz}
\usetikzlibrary{positioning}
\tikzset{>=latex}
% grammars
......@@ -71,6 +75,11 @@
% sideways
\usepackage{rotating}
% todos
\setlength{\marginparwidth}{2cm}
\usepackage{todonotes}
\setuptodonotes{size=\footnotesize, shadow}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% commands
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -100,12 +109,16 @@
\newcommand{\BVSORT}[1][16]{\mathcal{B}^{#1}}
% todos
\newcommand{\todo}[1]{
\begin{flushleft}
\color{red}
$\rightarrow$ #1
\end{flushleft}
}
% \newcommand{\todo}[1]{
% \begin{flushleft}
% \color{red}
% $\rightarrow$ #1
% \end{flushleft}
% }
% \newcommand{\todonote}[1]{
% $^{\color{red}#1}$
% }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% document
......@@ -146,4 +159,8 @@
\bibliographystyle{plain}
\bibliography{references}
\newpage
\listoftodos
\end{document}