text:
% !TeX program = lualatex -synctex=1 -interaction=nonstopmode --shell-escape %.tex

\documentclass[_international_finance_p1.tex]{subfiles}
\beamertemplatenavigationsymbolsempty

%\newcommand{\onslidecell}[2]{\onslide<#1->{#2}}
\newcommand{\aheader}[2]{\action<#1-|alert@#1>{#2}}
\begin{document}
\section{Binomial Options Pricing Model (BOPM)}
\subsection{Market Volatility}
\setbeamercovered{transparent}
\begin{frame}{Binomial Options Pricing Model (BOPM)}
\begin{itemize}[<+->]
\item
Buyer and seller always have different opinions on the underlying instrument price direction
\item
At each step, it is assumed that the underlying instrument will move up or down by a specific factor ($u$ or $d$) per step of the tree (where, by definition, $u \ge 1$ and $0 < d \le 1 )$.
\item
The up and down factors are calculated using the underlying volatility, $\sigma$, and the time duration of a step, $t$, measured in time intervals (days, months, years).
\item
Binomial Options Pricing Model says nothing about the underlying instrument up or down price movements probability.
\end{itemize}
\end{frame}
\begin{frame}{}
\begin{itemize}[<+->]
\item
At each final node of the tree — i.e. at expiration of the option — the option value is simply its intrinsic, or exercise, value.

    $Max [ (S_n-K), 0 ]$, for a call option

    $Max [ (K – S_n), 0 ]$, for a put option:

Where $K$ is the strike price and $S_n$ is the spot price of the underlying asset at the $n^{th}$ period.
\item
The binomial pricing model traces the evolution of the option`s key underlying variables in discrete-time. This is done by means of a binomial lattice (tree), for a number of time steps between the valuation and expiration dates. Each node in the lattice represents a possible price of the underlying at a given point in time.
\end{itemize}
\end{frame}
\setbeamercovered{invisible}
\begin{frame}[shrink=15]{USDRUB quotes changes from 01.10.2013 to 01.10.2014}
\begin{center}
% Table generated by Excel2LaTeX from sheet 'USDRUB'
\begin{table}[htbp]
  \centering
    \begin{tabular}{>{\onslide<1->}c
    				>{\onslide<1->}c
    				>{\onslide<2->}c}
    \toprule
    \multicolumn{1}{c}{Date} & \multicolumn{1}{c}{Close price} & \multicolumn{1}{c}{$\Delta,\%$} \\
    \midrule
    01.10.2013 & 32,0973 &  \\
    01.11.2013 & 33,0852 & 3,08\% \\
    01.12.2013 & 32,8311 & -0,77\% \\
    01.01.2014 & 35,2523 & 7,37\% \\
    01.02.2014 & 35,9238 & 1,90\% \\
    01.03.2014 & 35,1707 & -2,10\% \\
    01.04.2014 & 35,6287 & 1,30\% \\
    01.05.2014 & 34,8855 & -2,09\% \\
    01.06.2014 & 33,9675 & -2,63\% \\
    01.07.2014 & 35,705 & 5,12\% \\
    01.08.2014 & 37,1041 & 3,92\% \\
    01.09.2014 & 39,5562 & 6,61\% \\
    01.10.2014 & 42,9913 & 8,68\% \\
    \bottomrule
    \end{tabular}%
  \label{tab:addlabel}%
\end{table}%
\end{center}
\end{frame}
\begin{frame}{Monthly USDRUB quotes graph}
\begin{center}
\includegraphics[scale=0.7]{img/usdrubquoteschart}
\end{center}
\end{frame}
\begin{frame}{Monthly USDRUB quote percentage change}
\begin{center}
\includegraphics[scale=0.8]{img/usdrubdeltaperc}
\end{center}
\end{frame}
\begin{frame}{USDRUB quotes percentage change intervals}
\begin{center}
\includegraphics[scale=0.8]{img/usdrubquotesintervals}
\end{center}
\end{frame}
\setbeamercovered{transparent}
\begin{frame}{Formulas for the average return and the standard deviation of return}
\begin{itemize}[<+->]
\item
The average return:
$$m=\frac{\sum_{i=1}^n x_i}{n}$$
where $x_i$ – observed value;

$n$ – number of values.
\item
The standard deviation of return:
$$s=\sqrt{\frac{\sum_{i=1}^n (m-x_i)^2}{n-1}}$$
\end{itemize}
\end{frame}
\setbeamercovered{invisible}
\begin{frame}[shrink=15]{Monthly USDRUB average return and its standard deviation}
% Table generated by Excel2LaTeX from sheet 'Расчет m и s'
\begin{table}[htbp]
  \centering
    \begin{tabular}{cccc}
    \toprule
    & $x_i$    & $m-x_i$  & $(m-x_i)^2$ \\
    \midrule
1 & 3,08\% & \hiddencell{4}{-0,54\%} & \hiddencell{5}{0,30} \\
2 & -0,77\% & \hiddencell{4}{3,30\%} & \hiddencell{5}{10,90} \\
3 & 7,37\% & \hiddencell{4}{-4,84\%} & \hiddencell{5}{23,44} \\
4 & 1,90\% & \hiddencell{4}{0,63\%} & \hiddencell{5}{0,40} \\
5 & -2,10\% & \hiddencell{4}{4,63\%} & \hiddencell{5}{21,44} \\
6 & 1,30\% & \hiddencell{4}{1,23\%} & \hiddencell{5}{1,52} \\
7 & -2,09\% & \hiddencell{4}{4,62\%} & \hiddencell{5}{21,34} \\
8 & -2,63\% & \hiddencell{4}{5,17\%} & \hiddencell{5}{26,68} \\
9 & 5,12\% & \hiddencell{4}{-2,58\%} & \hiddencell{5}{6,66} \\
10 & 3,92\% & \hiddencell{4}{-1,38\%} & \hiddencell{5}{1,92} \\
11 & 6,61\% & \hiddencell{4}{-4,08\%} & \hiddencell{5}{16,61} \\
12 & 8,68\% & \hiddencell{4}{-6,15\%} & \hiddencell{5}{37,83} \\
    \midrule
    $\Sigma$& \hiddencell{2}{30,40\%}
    &  -
    & \onslide<6->{169,02} \\
    \textbf{m}
    & \hiddencell{3}{\textit{\textbf{2,5337\%}}}
    & \textbf{s}
    & \hiddencell{7}{\textit{\textbf{3,9199\%}}} \\
    \bottomrule
    \end{tabular}%
  \label{tab:addlabel}%
\end{table}%

\end{frame}
\begin{frame}{Monthly USDRUB average return and its standard deviation}
\begin{center}

% Table generated by Excel2LaTeX from sheet 'Расчет m и s'
\begin{table}[htbp]
  \centering
    \begin{tabular}{lr}
    \toprule
    m     & 2,5337\% \\
    s     & 3,9199\% \\
    \midrule
    m+s   & 6,4535\% \\
    m-s   & -1,3862\% \\
    \midrule
    u     & 1,0645 \\
    d     & 0,9861 \\
    \bottomrule
    \end{tabular}%
  \label{tab:addlabel}%
\end{table}%
\end{center}
\end{frame}
\subsection{Binomial price tree}
\begin{frame}{Create the binomial price tree}
{Options call and put parameters}
\begin{center}
% Table generated by Excel2LaTeX from sheet 'Модель'
\begin{table}[htbp]
  \centering
    \begin{tabular}{lrr}
    \toprule
    & \multicolumn{2}{c}{Option type} \\  \cmidrule{2-3}
    & Call & Put \\
    \midrule
    Option price & 45,00 ~₽ & 45,00 ~₽ \\
    Term & 2 month & 2 month \\
    USD rate, \% annual & 1\% & 1\% \\
    RUB rate, \% annual & 8,00\% & 8,00\% \\
    USD rate, \% monthly & 0,08\% & 0,08\% \\
    RUB rate, \% monthly & 0,67\% & 0,67\% \\
    \bottomrule
    \end{tabular}%
  \label{tab:addlabel}%
\end{table}%
\end{center}
\end{frame}

\setbeamercovered{invisible}
\begin{frame}[fragile,shrink=35]{The binomial price tree}
\begin{center}

\end{center}
\end{frame}
\newcommand{\optionpicturescale}{1.2}
\begin{frame}[fragile,shrink=35]{The binomial price tree}
\begin{figure}
	\center
	\begin{overprint}
		\forloop{slideno}{1}{\value{slideno} < 7}{%
			\only<\value{slideno}>{
				\includegraphics[page=\value{slideno},
				scale=\optionpicturescale
				% trim={<left> <lower> <right> <upper>}
				,trim={0cm 2cm 0cm 0cm}
				,clip]
				{tikz/price_binary_tree}}}
	\end{overprint}
	\caption{The binomial price tree}
\end{figure}

\end{frame}
\subsection{Intermediate Option Value}
\setbeamercovered{transparent}
\begin{frame}{}
\begin{itemize}[<+->]
\item
The option value for each earlier node is found, starting at the penultimate time step, and working back to the first node of the tree (the valuation date) where the calculated result is the value of the option.
\item
The "arbitrage free" approach creates a position that has an identical value in either state – the cash flow in one period is therefore known, and arbitrage pricing is applicable.
\end{itemize}
\end{frame}
\begin{frame}{}
\begin{itemize}[<+->]
\item
In case of an option the equivalent position consists of some amount of the base and quoted currency (one long and the other short) which has the value identical to the option price at the each moment.
\item
Under the risk neutrality assumption, today's fair price of a derivative is equal to the expected value of its future payoff discounted by the risk free rate. Therefore, expected value is calculated using the option values from the later two nodes.
\end{itemize}
\end{frame}

\begin{frame}{}
\begin{itemize}[<+->]
\item
The expected value is then discounted at r, the risk free rate corresponding to the life of the option.
\item
Long position in one currency yields interest revenue
\item
Short position in the other currency cause interest cost
\item
Usually the interest revenue/expenses are calculated on the basis of the risk free rate (e.g. LIBOR).
\end{itemize}
\end{frame}
\setbeamercovered{invisible}
\begin{frame}[shrink=10]{Option value at earlier nodes calculation example}
\begin{align*}
\begin{cases}
\onslide<2->{z_1 = 45,7658 \cdot x_1 + y_1}\\
\onslide<3->{3,7193 = 48,7193 \cdot x_1 \cdot (1 + \frac{r_{USD}}{n}) + y_1 \cdot (1 + \frac{r_{RUB}}{n})}\\
\onslide<4->{0,1314 = 45,1314 \cdot x_1 \cdot (1 + \frac{r_{USD}}{n}) + y_1 (1 + \cdot \frac{r_{RUB}}{n})}
\end{cases}
\end{align*}
$z_1$ – the option value at each intermediate node;

$x_1$ – base currency position amount, negative value means short position;

$y_1$ – quoted currency position amount, negative value means short position;

$r_{USD},r_{RUB}$ – risk free deposit/lending rate, in the base and quoted currency respectively, annual

$n$ - interest rate compounding frequency (number of compounding periods per year, e.g. 12 months).
\end{frame}
\setbeamercovered{transparent}
\begin{frame}{}
\begin{itemize}[<+->]
\item
Call and put options pricing is the same. The difference is only in options pricing at the final periods.
\item
If exercise is permitted at the node, then the model takes the greater of binomial and exercise value at the node.
\end{itemize}
\end{frame}
\setbeamercovered{invisible}
\subsection{Call and Put Options}
\begin{frame}[fragile,shrink=35]{Call option}
\begin{figure}
	\center
	\begin{overprint}
		\forloop{slideno}{1}{\value{slideno} < 6}{%
			\only<\value{slideno}>{
				\includegraphics[page=\value{slideno},
				scale=\optionpicturescale
				% trim={<left> <lower> <right> <upper>}
				,trim={0cm 2cm 0cm 0cm}
				,clip]
				{tikz/option_call}}}
	\end{overprint}
	\caption{Option call}
\end{figure}
\end{frame}
\begin{frame}[fragile,shrink=35]{Put option}
\begin{figure}
	\center
	\begin{overprint}
		\forloop{slideno}{1}{\value{slideno} < 8}{%
			\only<\value{slideno}>{
				\includegraphics[page=\value{slideno},
				scale=\optionpicturescale
				% trim={<left> <lower> <right> <upper>}
				,trim={0cm 2cm 0cm 0cm}
				,clip]
				{tikz/option_put}}}
	\end{overprint}
	\caption{Option put}
\end{figure}
\end{frame}
\subsection{Binary options}
\begin{frame}{Binary options pricing}
{Binary options parameters}
\begin{center}

% Table generated by Excel2LaTeX from sheet 'Модель'
\begin{table}[htbp]
  \centering
    \begin{tabular}{lrr}
    \toprule
    & \multicolumn{2}{c}{Option type} \\  \cmidrule{2-3}
    & One touch & No touch \\
    \midrule
    Barrier price & 48,00 ~₽ & 42,50 ~₽ \\
    Payoff & \$1 000 & \$1 000 \\
    Term & 2 months & 2 months \\
    USD rate, \% annual & 1\% & 1\% \\
    RUB rate, \% annual & 8,00\% & 8,00\% \\
    USD rate, \% monthly & 0,08\% & 0,08\% \\
    RUB rate, \% monthly & 0,67\% & 0,67\% \\
    \bottomrule
    \end{tabular}%
  \label{tab:addlabel}%
\end{table}%
\end{center}
\end{frame}
\begin{frame}[fragile,shrink=35]{One touch option}
\begin{figure}
	\center
	\begin{overprint}
		\forloop{slideno}{1}{\value{slideno} < 9}{%
			\only<\value{slideno}>{
				\includegraphics[page=\value{slideno},
				scale=\optionpicturescale
				% trim={<left> <lower> <right> <upper>}
				,trim={0cm 2cm 0cm 0cm}
				,clip]
				{tikz/option_one_touch}}}
	\end{overprint}
	\caption{One touch option}
\end{figure}
\end{frame}
\begin{frame}[fragile,shrink=35]{No touch option}
\begin{figure}
	\center
	\begin{overprint}
		\forloop{slideno}{1}{\value{slideno} < 9}{%
			\only<\value{slideno}>{
				\includegraphics[page=\value{slideno},
				scale=\optionpicturescale
				% trim={<left> <lower> <right> <upper>}
				,trim={0cm 2cm 0cm 0cm}
				,clip]
				{tikz/option_no_touch}}}
	\end{overprint}
	\caption{No touch option}
\end{figure}
\end{frame}
\setbeamercovered{transparent}
\subsection{General one period model}
\begin{frame}[shrink=15]{General one period model}
\begin{figure}
	\center
	\begin{overprint}
		\forloop{slideno}{1}{\value{slideno} < 2}{%
			\only<\value{slideno}>{
				\includegraphics[page=\value{slideno},
				scale=\optionpicturescale
				% trim={<left> <lower> <right> <upper>}
				,trim={0cm 7cm 0cm 0cm}
				,clip]
				{tikz/option_general_model}}}
	\end{overprint}
	\caption{General one period model}
\end{figure}

where

$S$ - undelying asset current price;

$E$ - options execution price.
\begin{align}
C_u = \begin{cases} u \cdot S - E, & \mbox{for } u \cdot S > E \\
0, & \mbox{for } u \cdot S \leq E \end{cases}\\
C_d = \begin{cases} d \cdot S - E, & \mbox{for } d \cdot S > E \\
0, & \mbox{for } d \cdot S \leq E \end{cases}
\end{align}
\end{frame}
\begin{frame}[shrink=15]{System of equations for one period model}{and its solution}
\begin{align}
\begin{cases}
C = S \cdot x + y\\
C_u = u \cdot S \cdot x \cdot r_{USD} + y \cdot r_{RUB}\\
C_d = d \cdot S \cdot x \cdot r_{USD} + y \cdot r_{RUB}
\end{cases}\\[12pt]
x=\frac{C_u-C_d}{(u-d)\cdot S \cdot r_{USD}}
y=\frac{u \cdot C_d-d \cdot C_u}{(u-d) \cdot r_{RUB}}
\end{align}
\begin{align}
C = S \cdot x + y
\end{align}

where

$x, y$ - position amounts in dollars and rouble, respectively;

$r_{USD},r_{RUB}$ - deposit/lending rates for time period \textit{T} in dollars and roubles, respectively.
\end{frame}

\end{document}

max_stars_repo_name: aabor/textbooks

max_issues_repo_name: aabor/textbooks

max_forks_repo_name: aabor/textbooks


text:
\documentclass{cv}

\title{CV example}
\author{Jing Li}
\date{April 2019}

\begin{document}

\section*{Richard Hendricks}

\begin{personalinfo}
  \personalinfoitem{\faHome}{5230 Newell Road, Palo Alto, CA, USA}
  \personalinfoitem{\faPhone}{+1-202-000-1111}
  \personalinfoitem{\faEnvelope}{\href{mailto:r.hendricks@piedpiper.com}{r.hendricks@piedpiper.com}}
  \personalinfoitem{\faLinkedin}{\textbf{LinkedIn}: \href{https://www.linkedin.com/in/richard-hendriks-148b7796/}{Richard Hendriks}}
  \personalinfoitem{\faTwitter}{\textbf{Twitter}: \href{https://twitter.com/siliconhbo/}{siliconhbo}}
  \personalinfoitem{\faStackOverflow}{\href{https://stackoverflow.com/}{\textbf{StackOverflow}}}
  \personalinfoitem{\faGithub}{\href{https://api.github.com/zen}{\textbf{GitHub}}}
  \personalinfoitem{\faInternetExplorer}{\href{http://www.piedpiper.com/}{\textbf{Pied Piper}}}
\end{personalinfo}

\section*{Professional Experience}

\begin{workexperience}{Pied Piper}{CEO}{Apr 2014 - Present}{company_logo_pied_piper.png}{0.4in}
  \workexperienceitem{Created a revolutionary data compression platform}
  \workexperienceitem{Worked on a decentralized, peer-to-peer internet}
  \workexperienceitem{Built a cryptocurrency for Pied Piper}
  \workexperienceitem{Garners funding from investors}
  \workexperienceitem{Hires engineers to strengthen the team}
\end{workexperience}

\begin{workexperience}{Hooli}{Programmer}{2013 - May 2014}{company_logo_hooli.png}{0.2in}
  \workexperienceitem{Performed quality assurance for mobile messaging}
\end{workexperience}

\section*{Education Background}

\educationbackground{Stanford University}{BS}{Computer Science}{2010 - 2013}

\section*{Awards and Honors}

\award{TechCrunch Disrupt Startup Battlefield Winner}{2015}

\section*{Skills}

\codingskills{Java}{JavaScript}{Python}{Ruby}{C}{C++}

\languageproficiency{English/Native}{French/Intermediate}

\section*{Conference Talks}

\conftalk{TechCrunch Disrupt}{NY}{2014}{https://youtu.be/wW49cy61PM4}

\conftalk{Talks at Google}{California}{2017}{https://youtu.be/QOXup8chEoY}

\section*{Publications}

\publication{A Beginners Guide to Decentralization}{978-6-9729-3379-9}{http://www.piedpiper.com/\#decentralization-guide}

\section*{Side Projects}

\project{Not Hotdog Android app}{https://play.google.com/store/apps/details?id=com.seefoodtechnologies.nothotdog}{10,000+ Installs \& 4.8\faStar}

\project{Not Hotdog iOS app}{https://itunes.apple.com/us/app/not-hotdog/id1212457521}{4.7\faStar}

\end{document}

ext: tex

max_stars_repo_name: thyrlian/CurriculumVitae

max_issues_repo_name: thyrlian/CurriculumVitae

max_forks_repo_name: thyrlian/CurriculumVitae


text:
% Due Date: 7/4/14

\chapter{Distributed Execution}
\label{chapter:distributed}
The third stage %(or second depending on mapping decisions)
of the Legion task pipeline is the distribution stage.
The distribution stage entails moving
a task and any necessary meta-data to the target node
on which the task is assigned to run by the mapper
that owns the task. The collection of mappers that own
a task also have control over whether the task is mapped
{\em locally} (on the node on which the task originated)
or {\em remotely} (on the target node).  This decision
determines the ordering of the mapping and distribution
stages  of the pipeline. If a task is assigned to a remote
node, the decision also determines what meta-data
must be moved in conjunction with the task.

In order to facilitate the distributed execution of
Legion tasks, the runtime must operate similarly to
a distributed system that is capable of reasoning
about partitioned meta-data structures. In this
chapter, we describe the algorithms necessary for
allowing the Legion runtime to support distributed
execution of Legion applications (with the caveat
that we omit discussion of resiliency to
Chapter~\ref{chapter:resilience}).  We begin
in Section~\ref{sec:messaging} by describing
the way messages are communicated between nodes
and the invariants supported by the communication
model. Section~\ref{sec:taskdist} describes how
both individual and index space tasks perform
the distribution stage of the task pipeline.
In Section~\ref{sec:distshape} we detail
how region tree data structures are migrated
through a distributed address space.  Finally,
we cover the details of how Legion supports
distributed physical contexts for parallel
mapping of non-interfering tasks in
Section~\ref{sec:distctx}.

\section{Messaging Interface}
\label{sec:messaging}
The Legion high-level runtime operates on top of
the low-level runtime, therefore there is no
explicit mechanism for the high-level runtime to
send messages between two nodes.  Instead data
can be moved in one of two ways: explicit copies
or task launches on remote processors. Explicit copies
are done  between physical instances and are optimized
for moving data structures in bulk. The low-level
runtime implements these copies efficiently using
asynchronous one-sided RDMA transfers. Alternatively,
task launches on remote processors can be
accompanied with an un-typed buffer of data that
is copied along with the task to the remote node.
In general, the un-typed buffer is only used for
capturing task arguments and should be relatively
small. The low-level runtime implements remote
task launches using asynchronous active messages
supported by the GASNet API\cite{GASNet02}. The
size of the buffer determines the size of the active
message required: either small (less than 128B),
medium (less than about 8KB depending on hardware),
or large (anything greater than the medium size).
Pre-allocated buffers of pinned memory is maintained
by GASNet for small and medium active messages, making
them considerably faster and lighter-weight than long
active messages.

The Legion programming model encourages bulk transfers
of data and therefore all application data is always
moved by copies between physical instances. However,
determining the best approach for moving meta-data
is not as obvious. Region tree data structures are
large and could therefore benefit from being moved
in bulk.  However, in practice, our implementation
of distributed region trees (described in
Sections~\ref{sec:distshape} and \ref{sec:distctx})
rely on an eventual consistency model that
maintains persistent state on all nodes and relies
on sending fewer small updates instead of
re-sending large bulk data structures each time
they are needed on a remote node. The Legion high-level
runtime therefore relies on sending tasks to remote
processors as the primary communication mechanism
for internal meta-data.

\subsection{Ordered Channels}
\label{subsec:channels}
While the Legion runtime uses remote task launch
as its primary communication mechanism, it does
so in a disciplined way.  Specifically, we create
the abstraction of an {\em ordered channel} for all
messages between a pair of nodes.  Ordering all
messages between a pair of nodes provides a useful
invariant for reasoning about the coherence of distributed
data structures.  In the case of the Legion runtime,
by knowing that all messages from one node to another
are ordered, we will be able to develop a novel algorithm
for distributed garbage collection of physical instances
in Chapter~\ref{chapter:garbage}.

To implement our ordered channels, we create
{\em message manager} objects on each node for
sending messages to destination nodes.  Message
managers provide a thread safe interface that
serializes all message requests from any thread running
on a node. In order to serialize messages to the
remote node, each message manager remembers the
termination event of the most recent message.
This event serves as the
precondition for the next message to be run.
Message managers also handle all incoming messages
from the remote node that it is responsible
for managing.

In order for Legion to remain scalable, message managers
are lazily instantiated.  In the worst case, every node
in the system will attempt to talk to every other node
in the system.  If there are $N$ nodes in the system,
this will require each node to instantiate $N$ message
managers, ultimately requiring $N^2$ message managers
across all nodes.  Since message managers maintain some
state and a buffer for sending messages, this can result
in a significant cost of memory.  In practice,
most nodes only talk to a subset of other nodes in the
machine.  Therefore, the Legion runtime only instantiates
a message manager for a destination node when either
it is requested as a target, or it receives a message
from the remote node.

\subsection{Deferred Sends}
\label{subsec:deferredsends}

While many of the messages sent by Legion are small
update messages, it is possible to defer many messages
for a short period of time and to aggregate many small
messages into larger messages that gain back some
of the efficiency of bulk data movement. The message
manager interface allows other components of the Legion
runtime to send messages and to indicate whether these
messages must be {\em flushed} (sent immediately) or
whether they can be deferred for a short period of
time. The message manager maintains a small buffer
for aggregating messages.  This buffer is intentionally
sized to target the maximum size of GASNet medium
active messages (usually between 8KB and 16KB).
The message manager attempts to aggregate as many
message as possible into this buffer until either
the buffer fills up or a message that needs to be
flushed is requested, at which point the aggregate
message is sent. On the remote node, the message
manager that receives the aggregate message then
unpacks the smaller messages and invokes the
proper handler.

The message manager API is also intelligent
enough to handle message requests that are bigger
than its buffer size, breaking them up into smaller
messages that fit into GASNet medium active
messages. By breaking up larger active messages
into slightly smaller ones, we can get data
moving through the network earlier, both reducing
latency and improving communication parallelism.
Note that even though messages are serialized
by low-level event dependences, those dependences
are handled by the remote node, meaning that the
active messages for those tasks can be in-flight
in the network simultaneously. Ultimately, the
message manager interface allows the Legion runtime
to strike a good balance between optimizing for
message throughput and latency by targeting
GASNet medium sized active messages. The message manager
interface also simplifies the implementation of other
runtime components, allowing them the illusion
of sending many small messages, that are ultimately
aggregated into larger messages.

\section{Task Distribution}
\label{sec:taskdist}
In practice, the mapping stage of the task pipeline
can actually be thought of as two separate
stages: the premapping stage and the actual
mapping stage (see Chapter~\ref{chapter:physical}).
The premapping stage must always be done on the
origin node where a task was created. However, the
actual mapping can be performed either on the
node where the task was created (locally) or on
the node where the task is going to be run (remotely).
In this section we discuss the implications of the
how both individual (Section~\ref{subsec:singledist})
and index space (Section~\ref{subsec:indexdist}) tasks
are distributed and actually mapped. In
Section~\ref{subsec:stealdist}, we discuss how task
stealing is incorporated into task distribution.

\subsection{Single Task Distribution}
\label{subsec:singledist}
For single tasks, the distribution stage is fairly
straightforward.  Figure~\ref{fig:singletaskdist}
shows the distribution pipeline for an individual task
launch including the extra detail of physical traversals
from Chapter~\ref{chapter:physical}. After the task
is finished premapping all of its regions, it first
checks to see the mapper has selected for it to be
locally or remotely mapped.  If the task is to be
locally mapped, then the mapping is performed, the
mapped regions are recorded, and the task is sent
to the target node where it is launched onto the
specified processor. If the task is to be remotely
mapped, then the task is sent to the
target node. If the task is not eligible for stealing
(see Section~\ref{subsec:stealdist}), then the
physical region tree state necessary for mapping
the task is eagerly sent along with the task. If
the task is eligible for stealing we defer sending
the region tree meta-data until we know for sure that
a task will attempt to map on a specific node.
(We discuss the movement of physical region tree
data in further detail in Section~\ref{sec:distctx}.)
When the task arrives on the target node, it is
placed in the ready queue for its intended processor.

\begin{figure}
\centering
\includegraphics[scale=0.7]{figs/IndividualTaskPipeline.pdf}
\caption{Individual Task Pipeline\label{fig:singletaskdist}}
\end{figure}

Once a task is placed in the ready queue for the
target processor, then the mapper associated with
that processor can decide to either map the task
or to send it to another processor to be mapped.
If the mapper decides to map the task, then the runtime
first checks to see if the necessary meta-data
is resident.  If the region tree meta-data is not
local, then a request is sent to the owner node of
the task for the necessary state. The owner node
handles these requests and replies with the necessary
region tree meta-data. Once the meta-data arrives
the task can be mapped. If the meta-data is already
resident, the task is immediately added to the list
of tasks to map.

Alternatively, a mapper may also decide to continue
forwarding a task on to an additional processor.
A mapper might choose to make this decision if the
processor that it is managing is overloaded and it
knows of other processors with less work to perform.
Under these circumstances, even if the task has
been marked not eligible for stealing, the remote
state information is not automatically forwarded.
While it is useful to forward state eagerly the
first time to reduce latency, if a task is moved
multiple times before being mapped, then the
cost of moving the state outweighs the latency
savings. When the task ultimately does map, it
will first need to request the necessary region
tree meta-data from the owner node. While this
does add latency, it does reduce the overhead
of moving the task multiple times as the meta-data
only needs to be moved once from the owner node
to the node where the task is ultimately mapped.

\subsection{Index Space Task Distribution}
\label{subsec:indexdist}
Figure~\ref{fig:indextaskdist} shows the more detailed
pipeline for the stages of an index space task launch.
Index task distribution is more complicated than
for single tasks.  The reason for this is that
index space task launches create many sub-tasks
with a single call. To handle all of these tasks,
the distribution stage for index space tasks
contains a sub-stage called {\em slicing}. Slicing
allows the mapper to break apart an index space
task launch into {\em slices} that describe a
subset of tasks in the original index space task
launch. Slices are created by the {\tt slice\_domain}
mapper call, which queries the mapper object
to break apart an index space task into subsets of
tasks (although the mapper is not required to break
apart an index space, and can create a single slice
that describes the entire set of tasks). Slices
act as the unit of reasoning about distribution
for index space task launches, with all tasks
within a slice being moved together. By grouping
tasks into slices, the runtime can deduplicate
much of the meta-data necessary for moving sets
of tasks between nodes.

\begin{figure}
\centering
\includegraphics[scale=0.57]{figs/IndexTaskPipeline.pdf}
\caption{Index Task Pipeline\label{fig:indextaskdist}}
\end{figure}

In some cases, index space task launches can
consist of very large numbers of tasks that need
to be distributed throughout an entire machine
that may contain thousands of nodes. To make
this process efficient, the slicing stage
supports hierarchical division.  When a slice
is created, the mapper chooses two values for
the slice object: a target processor and a
boolean value indicating whether the slice
should be recursively sliced. If the mapper
asks for the slice to be recursively divided,
then when the slice arrives on the target
node, the mapper for the target processor is
invoked with the {\tt slice\_domain} call
to perform the recursive slice operation.
Ultimately it is up the mapper objects of
a task to determine how many times and how
finely an index space task is divided.

After slicing is complete, slice objects
are added to the ready queue, similar to
individual tasks. Slices are the operations
that traverse the pipeline, with the original
index task operation waiting to complete
the final three stages of the pipeline until
all of its constituent slices have completed
the equivalent pipeline stages.
Slices behave like individual tasks until
they are ready to be mapped. The mapper that
owns a slice can choose to map it onto its
processor or send it to another process to
be mapped. Slices can also be marked eligible
for stealing, as we will describe in
Section~\ref{subsec:stealdist}. Once a slice
is ready to be mapped, the runtime enumerates
all the points in the slice, and generates
a {\em point task} for each point in the
slice. Each of these point tasks are then
mapped individually using the same routines
as individual tasks.

Similar to individual tasks, an index space
of tasks can also be mapped both locally
and remotely. In the case of local mapping,
slicing is performed first, but none of the
slices are sent remotely until each of the
points within each slice have been mapped.
For remote mappings, slicing is performed
first, allowing slices to be moved throughout
the machine.  Once a slice is ready to be
mapped, it sends a request to the owner
node for the region tree meta-data necessary
to perform the mapping. The owner node
responds with this information, allowing
the slice to be mapped. Note that, unlike
individual tasks, region tree meta-data
is not eagerly sent to any nodes as part
of the slicing process.  The reason for this
is that it is common for slices to be
both recursively sliced and moved; therefore,
we avoid the cost of moving the meta-data
by lazily sending it only when it is
explicitly requested.

\subsection{Distributed Stealing}
\label{subsec:stealdist}
While the distribution phase of the task
execution pipeline allows to tasks to be
pushed to their target processors (as
we described in the previous two sections),
the distribution phase also allows tasks
to be pulled to processors, with little or
no work, through stealing. By supporting both
push and pull models of task migration,
Legion allows mappers sufficient flexibility
for expressing optimal ways of mapping a
particular application onto a target
architecture.

To support stealing, Legion allows mappers
to designate tasks as eligible to be
stolen by setting the {\em spawn} flag
in the {\tt select\_task\_options} mapper
call\footnote{The choice of {\em spawn} as the flag
was inspired by the semantics of the Cilk
language\cite{Cilk98}.}. While stealing in many
other programming models is done implicitly by
the runtime, stealing in Legion is directed by
mappers because it impacts the performance
of an application. Mappers can send steal requests
to  any other mappers with the same ID on
different processors. Note by restricting steal
requests to other mappers with the same ID
we ensure that a task will always be mapped
by the same kind of mapper, albeit on different
processors. Unlike many stealing systems,
a steal request does not guarantee that a
steal will succeed.  Instead of having the
runtime automatically decide which tasks
are stolen by a steal request, the obvious
potential performance impacts mandate that
the decision be made by the mapper object.
Each steal request is therefore converted
by the runtime into a mapper call asking
the target mapper which (if any) of the
eligible tasks that it owns are permitted
to be stolen. The mapper is free to specify
none, all, or a subset of its eligible tasks.
In order to make such a decision the mapper
can introspect information such as the location
of physical instances available for different
tasks that reveal locality information. We
discuss these considerations further
when we describe the full mapping interface
in Chapter~\ref{chapter:mapping}.

One important detail regarding stealing is
that only eligible tasks still in the
ready queue for a specific mapper can be
stolen.  Once a task has been mapped, then
it is guaranteed to execute on the target
processor and it cannot be stolen.  For mappers
that choose to employ stealing as a means
for performing task migration, there exists
a natural tension between mapping tasks
early to get any precondition operations in
flight, and deferring mapping to achieve better
load balance through stealing. To aid
in these decisions, mappers are given detailed
information regarding the number of queued
tasks on each processor allowing them to
make informed decisions about when to map
tasks. Importantly, all such decisions regarding
when to map tasks and when to permit stealing,
are under mapper control, ensuring that there
is no implicit decisions made by the runtime
that may impact performance.

Since stealing in Legion is primarily designed
to migrate tasks between nodes, Legion does
provides some additional support for avoiding
unnecessary steal requests.  When a steal fails,
Legion blacklists the target processor as one in
which a steal has failed from the source processor.
No steal requests from the mapper of the source
processor will be allowed to be sent to the mapper
of the target processor until the mapper on the target
processor receives additional tasks that are
eligible for stealing in its ready queue.  The
runtime also records all the failed steal attempts
at a given processor.  When new tasks that are
eligible for stealing are added to the ready
queue, the runtime sends advertisements to all the
previously failed stealing processors.  These
advertisements remove the processor from the
blacklists of the attempted thieves.

Finally, while stealing in Legion will work between
any pair of processors, it works best between
different nodes, where it is more difficult
to achieve load balance. Task migration between
processors within a node is implemented in a fast
way that requires no copying of data.  However,
it is often more efficient to perform load-balancing
within a node using light-weight processor groups
that we discuss in Chapter~\ref{chapter:mapping}.

\section{Distributed Region Trees}
\label{sec:distshape}
While a Legion application is executing, it is
free to dynamically create index spaces,
field spaces, logical regions, and partitions. Each
of these operations are initially invoked by
a task on a single node, meaning that the
shape of the index space trees, field spaces, and
region trees are initially unknown to other nodes
immediately after creation. When a task is to be
mapped remotely, it is the responsibility of the
runtime to guarantee that the necessary index tree
and region tree shape information exist on the remote
node where the mapping is to be performed. In this section
we describe how the runtime maintains this
guarantee efficiently by lazily moving region
tree shape information.

\subsection{Leveraging Lazy Tree Instantiation}
\label{subsec:lazytree}

In order to map a task remotely, the state
for performing the mapping must be sent to
the target node.  Before the state can be
sent, the runtime first checks to see which
region tree shape information must be sent
to instantiate the necessary region tree
data structures on the remote node for storing
the state information.  For each of the region
requirements requested by a task, the runtime
checks that necessary region tree shapes
can be created on the remote node. The only
traversals that are performed remotely are
the mapping traversal and the instance view
traversal.  Therefore for each region
requirement of the task, the runtime must
ensure that the node corresponding to the
requested logical region and all sub-trees
are sent to the remote node. Additionally,
because some instance view trees for physical
instances may contain views from parent logical
regions, all logical regions that are ancestors
of the requested logical region must also be
sent to the remote node.

While this may initially sound like a
considerable number of region tree nodes
to send, we cut the number of nodes that
must be sent in half by leveraging the
lazy region tree instantiation supported
by the runtime (see
Section~\ref{subsec:logicalshape}).
Instead of having to send both the region
tree nodes as well as their corresponding
index space tree nodes, we only need to
send the necessary nodes from the index space
tree and the root node of the logical
region tree. This is sufficient from
the perspective of the remote node to
instantiate the remaining parts of
the region tree when needed, thereby reducing
the amount of data that must be sent
when moving a region tree to a remote node
by half.

\subsection{Creation and Deletion Sets}
\label{subsec:createsets}

To further reduce the amount of data that
must be sent when moving tasks between
nodes, all index space tree and logical
region tree nodes memoize the set of
other nodes in the machine to which they
have been sent. We call this set the
{\em creation set}, and it records which
nodes in the machine know about the creation
of the index space tree node or region tree
node from the perspective of the local node.
It is possible that this set is stale and
does not accurately represent all the nodes
in the machine that are aware of the existence
of a node. However, this lack of information
can only result in duplicate sends of region
tree and index tree data. In practice these
duplicate sends are rare, and when they do
occur, the sending node is immediately added
to the creation set of all region tree and
index space nodes on the destination node,
to avoid further duplication.

In addition to creation sets, both region
tree nodes and index space tree nodes also
maintain deletion sets for tracking which nodes
have been notified of the deletion of a node.
Since node deletions are deferred
(there may be sub-tasks still using the node),
deletions of nodes in both the index space trees
and region trees do not immediately delete a
node, but instead simply mark it as deleted.
As the deletion propagates and removes privileges
working its way back up the task tree, the
corresponding deletion information is only sent
to the proper nodes and only when the destination
node is unaware of the deletion.

To store both creation and deletion sets the
runtime uses a {\em node mask} data structure
that relies on the same base bit mask
implementation as field masks (see
Section~\ref{subsec:fieldmasks}). However,
the upper bound on the number of entries in a
node masks is determined by the number of nodes
in the machine instead of the maximum number of
fields in a field space. While these node masks
require $O(N)$ memory storage (in bits),
they make checking for elements in the set $O(1)$,
which is important since the common operation is
traversing a tree to see which region tree and
index space tree nodes still need to be sent to
a destination node.

\subsection{Distributed Field Allocation}
\label{subsec:distfields}
The final aspect of maintaining distributed
region tree data structures is handling dynamic
field allocation\footnote{Dynamic allocation of
rows in unstructured index spaces is handled
by the low-level runtime.}. Each runtime instance
statically partitions a space of field names for
each field instance, allowing them to be able to
dynamically allocate field IDs without needing
to communicate with other runtime instances.
When a field is allocated on a specific node
it is given a unique ID, but it is not sent
to any other nodes.  Instead when a field space
is sent to a node, it sends all the field IDs
that it knows about to the target node. If the
field space already exists on the destination
node, only the newly allocated fields are sent.
Upon receipt of an update of newly allocated
fields, the runtime always checks that the
upper bound on the maximum number of fields
in a field space has not been exceeded (see
Section~\ref{subsec:fieldspace} for a description
of the upper bound).

The difficult part of this distributed allocation
scheme is maintaining a mapping of field IDs
in a field space to indexes in the field masks.
Each node maintains its own mapping. All nodes
coordinate on a scheme in which they attempt to
allocate fields at indexes that are equal to their
node number modulo the number of nodes in the entire
machine. When these locations are exhausted they
progress to their neighbors locations. Ultimately the
goal is to maintain the same mapping across all nodes
so field masks can be directly unpacked and not
require a transformation when they are sent from
one node to another.

In some cases though, different fields will
be allocated to the same index in different nodes.
To handle this case, each field space maintains
a permutation vector for every other node in the
machine that describes the necessary transformation
that must be applied to unpacked field masks
received from every other node. Permutations are
also stored as field masks and are implemented
efficiently using the sheep and goats algorithm
from \cite{HackersDelight}. In practice most of
these permutations are the identity function.
The runtime tracks whether a permutation is the
identity function or not so that the identity
case can be easily skipped.

\section{Distributed Contexts}
\label{sec:distctx}
One of the options afforded to the mapper of a
task is to map the task remotely. To map remotely,
the necessary region tree state for performing the
mapping, registration, and instance view traversals
from Chapter~\ref{chapter:physical} must be available
on the remote node. To satisfy this requirement
the Legion runtime must provide a distributed
implementation of the region tree meta-data for a
physical context. In a distributed environment where
many tasks can be mutating the state of a physical
context in parallel on different nodes, maintaining
the consistency of the physical state is challenging.
In this section we detail the approach that enables
Legion to support distributed physical contexts on
multiple nodes in a consistent manner.

\subsection{Eventual Consistency}
\label{subsec:eventual}
In order to support distributed mappings of non-interfering
tasks within the same context on different nodes, Legion
permits the physical context from the owner node to be
replicated on remote nodes.  This allows non-interfering
tasks to map in parallel on remote nodes. The challenging
aspect to this approach is that tasks mapping in parallel
may mutate the state of a physical context in different
ways. To be safe, we need a mechanism to guarantee that
these independent mutations can be reconciled at a later
point in time. This deferred reconciliation of data
structures at a later point in time is called
{\em eventual consistency} in the distributed systems
community literature.

The primary requirement for supporting eventual consistency
is that the types of data being stored are instances
of convergent replicated datatypes (CRDTs) \cite{CRDT09}.
A CRDT is a type that is defined by a set of (possibly
unbounded) instances and a meet operator.  The meet
operator is required to be associative, commutative,
and idempotent. The crucial insight for supporting
eventual consistency for distributed region tree contexts
is that the set of possibles states for
sub-trees open in either read-only or reduce mode
represent instances of a CRDT.

For example, consider a region tree (or sub-tree) rooted
by a logical region $R$ in a context. For a given field,
the state of the region tree can take on many potential
values defined by the valid instances and open parts of
the sub-tree. These different states of the tree rooted
at $R$ define the different elements in the CRDT. The
meet operator is then defined to be the union operator
that unifies any two states for the sub-tree rooted
at $R$. It is important to note that this union operator
only works if the state of the tree rooted in $R$ is
open in read-only or reduce mode, as these privilege
modes can only open parts of the sub-tree or add new
valid instances.  Read-write privileges do not have
this property as they can close sub-trees and remove
valid instances which invalidates the commutativity
of the union operator. Defined in this way, Legion can
permit multiple distributed nodes to be mapped in parallel
on distinct nodes for trees open in read-only and reduce
mode and later be able to reconcile the state of the
physical context.

\subsection{Sending Remote State}
\label{subsec:sendstate}

State of a physical region tree for a physical
context is sent to a remote node in one of two
cases. First, it can be sent eagerly when an
individual task that is not eligible for stealing
is sent to a remote node (see
Section~\ref{subsec:singledist}). The second,
and more common case, is that a request is received
from a remote node for the physical state
meta-data necessary for mapping either an
individual task or a slice of an index space
task. When these requests occur, the runtime
locates the meta-data for the requesting task
(this data is always resident because requests
are only handled by the owner node where the task
was originally created). For each of the region
requirements for these tasks, the runtime traverses
the region tree from the region on which
privileges were requested through all open
sub-trees for the requested fields. This traversal
ensures that all the meta-data necessary for performing
the mapping, registration, and instance view
traversals will be resident on the remote node.

During the traversal, the state of each node in
the region tree is sent to the target node including
the dirty fields, valid physical instances, and open
sub-trees. Only state for the fields being requested
by the region requirement are sent. Each state is
sent as a separate message that can be deferred
allowing the message managers (described in
Section~\ref{subsec:channels}) to aggregate the
smaller messages into larger ones. The traversal
also keeps track of the necessary instance views
and instance managers that must be sent to the
remote node for performing the traversal. After
the entire traversal is finished, the instance
view and instance managers are also sent to the
remote node.  Instance managers are always
sent in full, while instance views only need to
send the members of the epoch lists for the
fields being requested by the region requirement.

On the remote node, the messages are handled and
unpacked into another physical context serves as a
clone of the physical context on the owner
node (note this context does not need to remain
a clone and can diverge from the owner node under
the conditions of CRDTs). Each message contains the
logical region node for the state that is being unpacked,
allowing the state to be updated directly. It is
important to note that unpacking state is merged
into the existing state rather than overwriting
it as the context may already contain valid
data for other fields from another task that
mapped on the same remote node (see
Section~\ref{subsec:persistence} for a detailed
description of persistent remote contexts).
The remote node also handles messages for
instance view and instance managers. Instance
managers and instance views are either updated
or created by the runtime to ensure that
there exists a unique one on the node\footnote{
Instance managers are unique on a node,
while instance views are unique within a
context on a node.}.

After the traversal of all the region requirements
in the physical state has been completed, the owner
node replies to the requesting remote node with a
message indicating that all of the physical state
data has been sent.  This message is marked as being
unable to be deferred, which causes the message
manager to flush the ordered channel to the remote
node. Since all messages between a pair of nodes
are both sent and received in order, by the time
the remote node observes the notification, all of
the necessary physical state has already been unpacked
in its region tree.  The runtime on the remote node
can then resume the mapping process for the task.

\subsection{Receiving Remote State Updates}
\label{subsec:receivestate}

When a task has finished mapping, it returns the
updated state of the region tree back to the origin
node of the task\footnote{There is an important interaction
with virtual mappings here: tasks with virtual
mappings cannot return their state until they have
finished mapping all their child operations.}. While
eagerly flushing meta-data back to the origin node
is not strictly necessary
(we could have opted to employ a distributed coherence
mechanism for tracking which nodes had valid state
for a specific fields of each region tree node), we
decided on this approach in order to ensure a
simpler implementation\footnote{The analogy to modern
processors is the difference between a write-back
and a write-through cache. Eagerly flushing data is
like writing through the cache back to main memory.}.

To return the meta-data state back to the origin
node, the runtime traverses the sub-trees for
all regions on which the task held privileges, and
sends back the state of these nodes. We currently
send back the entire state as it is relatively cheap
to represent.  Upon receiving the remote state on
the origin node, one of two operations is performed.
If the state is coming from a region requirement that
requested read-only or reduce privileges, the state
is unioned with the existing state on the owner node.
Performing a union is possible because the state of
the region tree under read-only or reduce privileges
is a CRDT (see Section~\ref{subsec:eventual}), allowing
states from distributed nodes to be safely merged.
Alternatively, if the state is returning from a sub-tree
on which the remote task had read-write privileges,
then the existing state on the owner node is first
invalidated, and then the returning state is
written as the new state. Read-write privileges
guarantee that there is only ever at most one task
mutating the state of that sub-tree at a time,
and the canonical version of that state is therefore
always the most recently written one.

In addition to returning state for region tree
nodes, state for the epoch user lists of instance
view objects is also returned.  Similar to returning
state for region tree nodes, whether or not the
state is merged or overwritten depends on the privilege
context under which it is being returned. If the
added users are being returned within a read-only
or reduce privilege context, then they are merged
with the existing set of users.  Otherwise, the
current epoch lists are invalidated for the fields
being returned, and the new users are added to the
lists as the new version of the epoch lists for
the returned fields.

\subsection{Persistence of Remote Contexts}
\label{subsec:persistence}

One important optimization implemented by the runtime
is deduplication of remote physical contexts. In
many cases, multiple sub-tasks from the same parent
task are sent to the same remote node to be mapped.
Often, these sub-tasks will request some of the same
state in order to map their regions. Under such
circumstances, it is inefficient for the runtime to
send multiple copies of the same physical state to
a remote node. Instead, the runtime deduplicates
these requests by ensuring that at most a single
copy of any physical context exists on any remote node.

On each node, the runtime tracks all of the physical
contexts that have been allocated, as well as
whether the allocated contexts are for a task running
on the local node, or whether the contexts are remote
versions of a context from a different node. If a context
is a remote version, then the runtime also tracks the
identity of the parent task on the owner node associated
with the remote clone context. When a task is
received to be executed and mapped remotely on a
node, the runtime first checks to see if an existing
remote context has been allocated for the parent
task. If it has, the child task is told of the appropriate
context so that it can use it as the target of any
remote state requests that are sent to the owner node.
If no such context exists, then a new remote clone
context is allocated and registered.  Any future
tasks that are sent to the node with the same parent
task are then guaranteed to re-use the same context.

The parent task on the owner node also tracks the
set of remote clone contexts that exist on remote nodes.
Individual region tree nodes in the context on the owner
node track the validity of state information for
different fields on remote nodes. We discuss the
protocol for maintaining this validity in
Section~\ref{subsec:invalidate}. When the parent task
commits on the owner node, it is safe to infer that
there is no longer a need for the remote clone contexts
to be maintained.  At this point, the owner node sends
messages to all of the nodes that contain remote clone
contexts, instructing them to invalidate the remote contexts
and recycle them so that can be re-used for future tasks.

\subsection{Invalidate Protocol for Remote Context Coherence}
\label{subsec:invalidate}

Maintaining coherence of the distributed region tree
state is a challenging problem. Not surprisingly, this
problem has a natural analog in modern hardware processors:
maintaining cache coherence. Modern hardware processors
support replication of cache lines whenever possible for different
processors in the same chip while still guaranteeing a
total order on writes to the cache line. Legion relies on
a similar approach for maintaining coherence of the region
tree state within a physical context that have been replicated
throughout the nodes of a machine.

We considered two potential adaptations of cache coherence
protocols on which to base our Legion implementation.  Our
initial approach was based on an update protocol.  In an
update protocol, data initially resides on a single node.
As other nodes request data, they become subscribers. Any
updates to the data are eagerly flushed out to all of the
subscribers.  Our initial implementation based on an
update protocol maintained a set of subscribers for each
region tree node.  While the update protocol performed well
at small node counts, it failed to perform well at larger
node counts.  At larger node counts, there are many
unnecessary update messages sent that ultimately are
not used for mapping any future tasks in a specific
part of the region tree.

Our second design is based on an invalidation cache
coherence protocol. In an invalidation protocol, remote
copies of the data are invalidated, and requests are
generated by the remote node to pull data from the owner
node (which always has a valid copy) to the requesting
node. Invalidation protocols scale better because they
move data lazily, which ensures that data is only moved
when it is actually going to be used. In our Legion
implementation, each region tree node on the owner node
maintains a {\em directory} object (similar to the directory
maintained by distributed memory cache coherence protocols).
The directory stores two kinds of information for each field:
the {\em mode} it is in and for each field, the set of
nodes that contain valid versions of the state. Each
field within a state can be in one of three modes
corresponding to the different region privileges:
read-only, read-write, and reduce.  The read-only and
reduce modes permit multiple nodes to have valid copies
of the data simultaneously, while the read-write mode
permits at most a single other node to maintain a valid
copy of the state.

Whenever a state transition takes place for a node within
a field, all outstanding remote copies are invalidated.
The invalidation is both recorded on the owner node and
on the remote nodes by messages sent from the owner node.
It is important to node that the owner node always maintains
a valid copy of the state for all fields of all nodes
within a context because all tasks eagerly flush changes
to the region tree back to the owner node. In many ways
this approach is similar to write-through caches that always
flush data back to the backing memory so that the directory
owner always has a valid copy of the data. Remote nodes
can then request updated versions of the state for any
set of region tree nodes when necessary.

\subsection{Distributed Futures}
\label{subsec:distfutures}

The final piece of distributed state within a context that
must be considered are futures.  Futures are local to the
context of the parent task in which they are created.
However, sub-tasks can request future values as arguments.
If these tasks are mapped to processors on remote nodes,
it is the responsibility of the runtime to ensure that the
value of the future is propagated to the remote node
when the future completes.

To support this feature, the runtime implements {\em distributed
futures}.  Distributed futures operate in a similar manner
to instance managers (see Section~\ref{subsec:instmanagers}).
There is an owner distributed future created on the owner
node and clones can be created on remote nodes. Each
distributed future remembers the nodes where versions already
exist as well as the node that contains the original owner
node.  Distributed futures are registered with the runtime
to ensure that they are deduplicated within a node (guaranteeing
that at most one distributed future exists on each node).
Each remote distributed future registers itself with the
owner version on the owner node. When the owner distributed
future completes, it broadcasts out the value associated
for the future with any registered waiters on remote nodes.
If the owner distributed future receives any requests after
it has already completed, it immediately replies with the
value of the future. When remote nodes receive the values
for the future, they also complete immediately and notify
any tasks that may have been waiting on them that they
are complete (usually done with low-level runtime events).
Distributed futures are reclaimed with the same garbage
collection algorithm as instance managers which is discussed
in detail in Chapter~\ref{chapter:garbage}.

max_stars_repo_name: lightsighter/Thesis

max_issues_repo_name: lightsighter/Thesis

max_forks_repo_name: lightsighter/Thesis


text:
\section{\module{mimetools} ---
         Tools for parsing MIME messages}

\declaremodule{standard}{mimetools}
\modulesynopsis{Tools for parsing MIME-style message bodies.}

\deprecated{2.3}{The \refmodule{email} package should be used in
                 preference to the \module{mimetools} module.  This
                 module is present only to maintain backward
                 compatibility.}

This module defines a subclass of the
\refmodule{rfc822}\refstmodindex{rfc822} module's
\class{Message} class and a number of utility functions that are
useful for the manipulation for MIME multipart or encoded message.

It defines the following items:

\begin{classdesc}{Message}{fp\optional{, seekable}}
Return a new instance of the \class{Message} class.  This is a
subclass of the \class{rfc822.Message} class, with some additional
methods (see below).  The \var{seekable} argument has the same meaning
as for \class{rfc822.Message}.
\end{classdesc}

\begin{funcdesc}{choose_boundary}{}
Return a unique string that has a high likelihood of being usable as a
part boundary.  The string has the form
\code{'\var{hostipaddr}.\var{uid}.\var{pid}.\var{timestamp}.\var{random}'}.
\end{funcdesc}

\begin{funcdesc}{decode}{input, output, encoding}
Read data encoded using the allowed MIME \var{encoding} from open file
object \var{input} and write the decoded data to open file object
\var{output}.  Valid values for \var{encoding} include
\code{'base64'}, \code{'quoted-printable'}, \code{'uuencode'},
\code{'x-uuencode'}, \code{'uue'}, \code{'x-uue'}, \code{'7bit'}, and
\code{'8bit'}.  Decoding messages encoded in \code{'7bit'} or \code{'8bit'}
has no effect.  The input is simply copied to the output.
\end{funcdesc}

\begin{funcdesc}{encode}{input, output, encoding}
Read data from open file object \var{input} and write it encoded using
the allowed MIME \var{encoding} to open file object \var{output}.
Valid values for \var{encoding} are the same as for \method{decode()}.
\end{funcdesc}

\begin{funcdesc}{copyliteral}{input, output}
Read lines from open file \var{input} until \EOF{} and write them to
open file \var{output}.
\end{funcdesc}

\begin{funcdesc}{copybinary}{input, output}
Read blocks until \EOF{} from open file \var{input} and write them to
open file \var{output}.  The block size is currently fixed at 8192.
\end{funcdesc}

\begin{seealso}
  \seemodule{email}{Comprehensive email handling package; supersedes
                    the \module{mimetools} module.}
  \seemodule{rfc822}{Provides the base class for
                     \class{mimetools.Message}.}
  \seemodule{multifile}{Support for reading files which contain
                        distinct parts, such as MIME data.}
  \seeurl{http://www.cs.uu.nl/wais/html/na-dir/mail/mime-faq/.html}{
          The MIME Frequently Asked Questions document.  For an
          overview of MIME, see the answer to question 1.1 in Part 1
          of this document.}
\end{seealso}

\subsection{Additional Methods of Message Objects
            \label{mimetools-message-objects}}

The \class{Message} class defines the following methods in
addition to the \class{rfc822.Message} methods:

\begin{methoddesc}{getplist}{}
Return the parameter list of the \mailheader{Content-Type} header.
This is a list of strings.  For parameters of the form
\samp{\var{key}=\var{value}}, \var{key} is converted to lower case but
\var{value} is not.  For example, if the message contains the header
\samp{Content-type: text/html; spam=1; Spam=2; Spam} then
\method{getplist()} will return the Python list \code{['spam=1',
'spam=2', 'Spam']}.
\end{methoddesc}

\begin{methoddesc}{getparam}{name}
Return the \var{value} of the first parameter (as returned by
\method{getplist()}) of the form \samp{\var{name}=\var{value}} for the
given \var{name}.  If \var{value} is surrounded by quotes of the form
`\code{<}...\code{>}' or `\code{"}...\code{"}', these are removed.
\end{methoddesc}

\begin{methoddesc}{getencoding}{}
Return the encoding specified in the
\mailheader{Content-Transfer-Encoding} message header.  If no such
header exists, return \code{'7bit'}.  The encoding is converted to
lower case.
\end{methoddesc}

\begin{methoddesc}{gettype}{}
Return the message type (of the form \samp{\var{type}/\var{subtype}})
as specified in the \mailheader{Content-Type} header.  If no such
header exists, return \code{'text/plain'}.  The type is converted to
lower case.
\end{methoddesc}

\begin{methoddesc}{getmaintype}{}
Return the main type as specified in the \mailheader{Content-Type}
header.  If no such header exists, return \code{'text'}.  The main
type is converted to lower case.
\end{methoddesc}

\begin{methoddesc}{getsubtype}{}
Return the subtype as specified in the \mailheader{Content-Type}
header.  If no such header exists, return \code{'plain'}.  The subtype
is converted to lower case.
\end{methoddesc}


text:
\documentclass[a4paper,11pt, oneside, openany]{book}% note: a4paper - not a4 If you don't use, it will leave margin for printing
\usepackage[hmarginratio=1:1]{geometry}% equal left and right margins
\usepackage[linktocpage, pdftex,
pdfauthor={Rohit Suratekar},
pdftitle={Conference Schedule}]{hyperref} %References and hyperlinks
\usepackage{fixltx2e} %Removes in paragraph warnings
\usepackage{standalone} % load only in the main file
\usepackage{graphicx, float}%Graphics related
\usepackage{titlesec} %To customize titles
\usepackage{fancyhdr} %For header
\usepackage{microtype} %For justify text in block
\usepackage{caption, tabularx} %Tables related
\usepackage{multirow, hhline, longtable} % Table related
\usepackage[table]{xcolor} %Coloring
%\usepackage{afterpage}
%\usepackage[T1]{fontenc}
\pagestyle{fancy}
\fancypagestyle{MyStyle}{%
    \fancyhead{} %Clean headers
    \fancyhead[RO]{\leftmark}
    \fancyhead[LE]{\leftmark}
    \renewcommand{\chaptermark}[1]{\markboth{{\slshape{##1}}}{}}
}
\usepackage{tocloft} %Need this for proper section no space
\setlength{\cftchapnumwidth}{3em}

\usepackage{mathptmx}
\usepackage{amsmath}
\def\permille{\ensuremath{{}^\text{o}\mkern-5mu/\mkern-3mu_\text{oo}}}

\usepackage[normalem]{ulem} % For underline

% Formatting underline
\setcounter{errorcontextlines}{999}
\usepackage{soul} % For proper underline
\makeatletter
\newcommand*{\whiten}[1]{\llap{\textcolor{white}{{\the\SOUL@token}}\hspace{#1pt}}}
\DeclareRobustCommand*\myul{%
	\def\SOUL@everyspace{\underline{\space}\kern\z@}
	\def\SOUL@everytoken{%
		\setbox0=\hbox{\the\SOUL@token}%
		\ifdim\dp0>\z@
		\the\SOUL@token
		\else
		\underline{\the\SOUL@token}%
		\fi}
	\SOUL@}
\makeatother
\titleformat{\chapter}[display]
{\normalfont\huge\bfseries}{}{0pt}{\Huge}
\titlespacing*{\chapter} {0pt}{20pt}{40pt}

%For skipping subchapter
\DeclareRobustCommand{\gobblefour}[4]{}
\newcommand*{\SkipTocEntry}{\addtocontents{toc}{\gobblefour}}
\setcounter{tocdepth}{0}

\begin{document}
\frontmatter
%\input{sections/front_page}
\input{sections/cover_page}
\tableofcontents
\mainmatter
\pagestyle{MyStyle}
\renewcommand{\thesection}{\arabic{section}}
\input{sections/useful_info}
\input{sections/schedule}
\newgeometry{left=1in, right=1in, top=1in, bottom=1in}
\chapter{Talk Abstracts}
\begingroup
\titleformat{\section}[block]{\bfseries\filcenter}{}{1em}{}
\renewcommand*{\thesection}{}
\input{all_speakers}
\endgroup
\chapter{Poster Abstracts}
\renewcommand{\thesection}{\arabic{section}}
\input{all_abstracts}
\input{sections/end_matter}
\end{document}

max_stars_repo_name: rohitsuratekar/AbstractBook

max_issues_repo_name: rohitsuratekar/AbstractBook

max_forks_repo_name: rohitsuratekar/AbstractBook


text:
\subsubsection{\stid{1.09} Distributed Tasking at Exascale: PaRSEC}

\paragraph{Overview}

The PaRSEC Environment provides a runtime component to dynamically execute on
heterogeneous distributed systems, and a productivity toolbox that comprises a
development framework for the support of multiple domain specific languages
(DSLs) and extensions, with debugging, trace collection, and analysis tools.
%
The PaRSEC project team is dedicated to solving two challenging and
interdependent problems facing the ECP developer community: First, how we create
an execution model that enables developers to express as much parallelism as
possible in their applications, so that those applications effectively utilize
the massive collection of heterogeneous devices that ECP machines will deploy.
Second, how we ensure that that execution model is flexible and portable enough
to actually increase the scientific productivity of those same application
developers, not only for the ECP target environments but for the foreseeable
future.
\begin{wrapfigure}{l}{.6\linewidth}
  \includegraphics[scale=0.35]{projects/2.3.1-PMR/2.3.1.09-ParSEC/PaRSEC-diagram.png}
  \caption{PaRSEC architecture\label{fig:parsec}}
\end{wrapfigure}
%
PaRSEC is an open source, community-based implementation of a generic task-based
runtime that is freely available, and used by an increasing number of software
libraries.
%  The PARSEC development team is mainly comprised of research staff at % UTK,
%  but regular contributions from the community are provided via our presence %
%  on GitHub and Bitbucket.
The project focuses on prototyping different approaches to define task-based
languages that will be able to exploit the full range of capabilities of
Exascale platforms. Without such a project, and based on the current state of
task-based runtimes, potential users will be stuck either in fixed programming
boundaries, or with particular programming languages. The DTE project provides
means to maintain a high competitiveness in the field leading to more innovation
on addressing the challenges we are facing toward scalable, performant and
Exascale ready programming paradigms.

\paragraph{Key  Challenges}
%\textit{Describe what is hard to do, why it is challenging.}

As we approach Exascale, a number of aspects of the hardware and software
environment pose challenges. First and foremost, keeping pace with the
architectural changes on current and future machines requires changes not only
on how we take advantage of the hardware capabilities, but how we reshape our
algorithms and applications to expose enough parallelism to maximize the use of
the underlying hardware. The number of nodes, threads per node, memory
hierarchies and support for increased computational capabilities (accelerators)
will continue to increase, while the currently available programming paradigms
are still struggling with parallelism at the node level.

\paragraph{Solution Strategy}
%\textit{Describe your basic strategy for addressing the challenges.}
The approach followed in PaRSEC is to provide a low-level, flexible and dynamic
runtime able not only to schedule tasks at the node level, but to handle data
transfers between different memory (both inter and intra nodes), memory
hierarchies, heterogeneous architectures with support for accelerators with a
simple programming scheme. The proposed approach envisions a middle-ground
solution, addressing both hardware and software challenges. At the hardware
level a team of dedicated developers extends PaRSEC to map it's capabilities to
the hardware and to improve it's scalability and performance. At the upper level
the interaction with the users is through building Domain Specific Languages
with the target domain scientists in mind, that will facilitate the expression
of algorithmic parallelism with familiar constructs mapped on the exposed
low-level capabilities. To facilitate the integration of PaRSEC-driven libraries
into larger and complex applications, PaRSEC natively interoperate with other
programming paradigms, including some target of the ECP PMR support, such as
PGAS, MPI, OpenMP and Kokkos. This integration provides a smooth transition for
library developers that embrace the PaRSEC runtime, providing a platform where a
shift to a new programming paradigms can be done in stages of increased
complexity.
% In this model, PaRSEC remains in full control of data tracking and
% allocation on the managed accelerator.

\paragraph{Recent Progress}

\begin{wrapfigure}{l}{.45\linewidth}
  \centering\includegraphics[scale=0.55]{projects/2.3.1-PMR/2.3.1.09-ParSEC/cc_abcd.pdf}
  \caption{Strong-scaling performance of the ABCD term in the coupled-cluster doubles equation for $(H_2O)_{12}$ in aug-cc-pVDZ basis set.\label{fig:MPQC}}
\end{wrapfigure}
The DTE GPU support engine has been refactored, enabling unprecedented
performance on distributed, multi-GPU platforms for real applications,
like MPQC, which is part of the NWChemEx chemistry
package. Figure~\ref{fig:MPQC} shows a strong scaling performance of
MPQC using PaRSEC to power the most compute intensive operation of the
tensor contraction, and compares it with native MPQC. This
integration illustrates inter-runtimes cooperation, as the
vast majority of MPQC remains supported by its current runtime
system, and only a tensor contraction, runs over
the PaRSEC runtime.
% Both runtime systems thus collaborate to the general progress of the application.
The refactoring of the GPU engine in PaRSEC, and the task system programming
approach, however, allow to support multiple GPUs without code modification,
while the native MPQC implementation does not. PaRSEC supported DTE shows an
efficient strong scaling, even with multiple accelerators.

An important aspect of the DTE project is to define and prototype scalable
domain specific languages that enable a productive expression of parallelism for
end-user communities. PaRSEC presents multiple programming interfaces
(Parameterized Task Graphs for maximum parallelism, the popular serial task
insertion dataflow model to provide direct access to the runtime). In addition
the DTE team is in close contact with application teams to define parallel
abstractions that are suitable for their domain usage. Notably, the PaRSEC team
has ongoing collaboration with the SLATE linear algebra package and NWChemEx
chemistry package teams.
The PaRSEC development team did the first step toward the integration
of their framework into the SLATE (2.3.3.09) in the context of the
shared milestone (STPM11-23). The first prototype of the application
ran in a distributed environment and showed the capability of the
SLATE library using a modern fully capable runtime system. This work
involved enhancing the insert task interface available in the ParSEC
runtime to map onto the logic of a SLATE algorithm.

\begin{wrapfigure}[16]{l}{.45\linewidth}
  \vspace*{-1em}\centering\includegraphics[scale=0.55]{projects/2.3.1-PMR/2.3.1.09-ParSEC/SLATE_inital_result_phicluster_scalapack.pdf}
  \caption{Comparison of DPLASMA and SLATE Cholesky factorization over PaRSEC with
           SLATE and ScaLAPACK on 64 nodes 12 cores each\label{fig:slate-parsec}}
\end{wrapfigure}
%
In figure~\ref{fig:slate-parsec}, we compare the integration of SLATE
and PaRSEC against the state of the art. First against the two legacy
domain specific languages that have the capability to do linear
algebra; then against the regular SLATE using OpenMP for intra-node
parallelism, and MPI for communication; and finally against ScaLAPACK,
which is the reference for distributed linear algebra.

On the software quality side, the PaRSEC runtime has been evaluated and amended
to compile and run on all major target pre-Exascale platforms (ALCF Mira, Theta; OLCF
Titan, Summit-dev). In particular the detection of architecture specific
features on NVIDIA V100 accelerators and Power processors has been improved.
PaRSEC now includes a Spack definition file to ease the deployment on future
target systems as part of the system software SDK effort.

\paragraph{Next Steps}
%\textit{Describe what you are working on next.}
% Improve DTE accelerator support and interoperability with other
% programming models
To provide programmers with more supervision over how accelerators are
integrated and used by the runtime, a need to provide finer control of the
resource usage by the runtime system has arisen. We are developing new APIs to
allow the programmers to advise the runtime system with respect to data
placement, prefetching, and management of cache.
%
Programming interoperability should not be limited to node-level programming
models but should extend to distributed programming. Execution modes where part
of the application is expressed in native MPI (including communicating tasks)
and other parts using PaRSEC DSLs, running above the task system in a tightly
coupled manner, are being developed.

% Facilitate DSL integration

% Provide better libraries and tools integration
The set of tools that come with the PaRSEC runtime environment to
assess performance, find bottlenecks, improve scheduling and debug the
task-based application are being improved to expose the information
in a format compatible with TAU, Score-P and other
tools that are already familiar to ECP users.


text:
\chapter{Compositional Modeling and Abstraction}
\label{ch:compositional}

This chapter describes \uclid{}'s features for compositional and modular verification, and the use of abstraction.

We will use a running example of a CPU model constructed in \uclid{} and use bounded unrolling of the model's transition relation to prove that the execution of this CPU is deterministic: i.e. we show that given two identical instruction memories, the state updates performed by this CPU will be identical.

\section{Common Type Definitions Across Modules}

Example~\ref{ex:cpu-common} shows a module that defines only type synonyms. Such a module can be used to share type definitions across other modules. The types declared in Example~\ref{ex:cpu-common} are \emph{imported} in lines~2-5 of module \codelike{cpu} declared in Example~\ref{ex:cpu-cpu}.

\label{sec:cpu-model}
\begin{uclidlisting}[htbp]
%\begin{lstlisting}[language=uclid,style=uclidstyle]
    \lstinputlisting[language=uclid,style=uclidstyle]{../examples/tutorial/ex3.1-cpu.ucl}
    \caption{Module \codelike{common} of the CPU model}
    \label{ex:cpu-common}
\end{uclidlisting}

\begin{uclidlisting}[htbp]
    \lstinputlisting[language=uclid,style=uclidstyle]{../examples/tutorial/ex3.2-cpu.ucl}
    \caption{The \codelike{cpu} module in the CPU model}
    \label{ex:cpu-cpu}
\end{uclidlisting}

\begin{uclidlisting}[htbp]
    \lstinputlisting[language=uclid,style=uclidstyle]{../examples/tutorial/ex3.3-cpu.ucl}
    \caption{Module \codelike{main} in the CPU model}
    \label{ex:cpu-main}
\end{uclidlisting}

Isolating commonly used types into a single module in this manner allows the construction of large models parameterized by this types. These common types can be changed and the ramifications of these changes on the model's behavior can be studied easily.

\section{Uninterpreted Functions and Types}
A convenient mechanism for abstraction in \uclid{} is through the use of uninterpreted functions and types. This is one of the novel modeling
aspects for transition systems introduced by the original UCLID system~\cite{bryant-cav02}.

\subsection{Uninterpreted Types}
Example~\ref{ex:cpu-cpu} shows the use of the \emph{uninterpreted type}: \codelike{regindex_t} on line~6. The index type to the register is an \emph{abstract} type, as opposed to a specific type (e.g. \codelike{bv3}). This allows us to reason about an abstract register file that has an undefined (and unbounded) number of entries, as opposed to proving facts about some specific register file implementation, potentially enabling more general proofs about system behavior.

\subsection{Uninterpreted Functions}
Values belonging to an uninterpreted type can be created using \emph{uninterpreted functions}. The functions \codelike{inst2op}, \codelike{inst2reg0}, \codelike{inst2reg1}, \codelike{inst2imm} and \codelike{inst2addr} on lines~15-19 of Example~\ref{ex:cpu-cpu} are all examples of uninterpreted functions. An uninterpreted function $f$ is a symbol about which we know nothing, except that it is a function; i.e. $\forall x_1, x_2.~ x_1 = x_2 \implies f(x_1) = f(x_2)$.

As an example, in the context of processor verification,
uninterpreted functions allow us to reason about an abstract CPU model without considering specific instruction encodings or decoder models. This could potentially lead to more general proofs as well as more scalable automated proofs.

\section{Module Instantiation and Scheduling}

Modules are instantiated using the \keyword{instance} keyword. Lines 14~and~15 of Example~\ref{ex:cpu-main} show two instantiations of the module \codelike{cpu}. For each instance, the module input \codelike{imem} is mapped to the state variable \codelike{imem} of module \codelike{main}.

Scheduling of instantiated modules is explicit and synchronous. The two \keyword{next} statements on lines 22~and~23 of Example~\ref{ex:cpu-main} invoke the next state transitions of the two instances of the \codelike{cpu} module.

Asynchronous and partially synchronous composition can be
modeled by explicitly encoding a scheduler into the \uclid{} model
that specifies when the \codelike{next} block of each module
is executed.

\subsection{Accessing Members of Instances}

The state variables, types, etc. of an instantiated module are accessed using the \codelike{.} operator. The four invariants on lines 27-32 of Example~\ref{ex:cpu-main}, refer to the registers, memory, pc and instruction variables of the two instantiated modules. These invariants state that both instances must have identical values for these state variables.

\section{Running \uclid{}}

Executing \uclid{} on the complete CPU model shows that CPU is in fact deterministic.

\begin{Verbatim}[frame=single, samepage=true]
$ uclid ex3.1-cpu.ucl ex3.2-cpu.ucl ex3.3-cpu.ucl
Successfully parsed 3 and instantiated 1 module(s).
16 assertions passed.
0 assertions failed.
0 assertions indeterminate.
Finished execution for module: main.
\end{Verbatim}

Note the files \codelike{ex3.1-cpu.ucl}, \codelike{ex3.2-cpu.ucl} and \codelike{ex3.3-cpu.ucl} contains three modules. Each of these modules could potentially have \keyword{control} blocks. Which \uclid{} is invoked on this model, it executes only the \keyword{control} block of the \codelike{main} module.  If we had included a \keyword{control} block for the \codelike{alu} module and wished to verify properties of this module, we would have to invoke \uclid{} on this specific module using the \codelike{--main} command-line option.

% Moved to next chapter
%\subsection{Exercise: Inductive Proof of CPU model}
%Prove determinism of the CPU model using induction rather than bounded model checking. You will need to add strengthening inductive invariants relating the two CPU instances.

max_stars_repo_name: kkmc/uclid

max_issues_repo_name: kkmc/uclid

max_forks_repo_name: kkmc/uclid


text:
\subsection{The Eager and the Lazy approaches}

\begin{frame}
  \frametitle{The Eager and Lazy Approaches}

  Recall that in our reduction to SAT we need to encode
  \begin{enumerate}[$(i)$]
    \item incompatible relations between \tatoms exhaustively
    \item the structure of $\varphi$
  \end{enumerate}
  \pause
  \vfill
  Condition $(ii)$ is easy to encode. The critical condition is $(i)$.
  If we have 3 \tatoms $a, b, c$, then we need to check whether
  \begin{itemize}
    \item $a$ and $b$ are incompatible
    \item $a$ and $\neg b$ are incompatible
    \item \ldots
    \item $a$ and $b$ and $c$ are incompatible
    \item \ldots
  \end{itemize}
  \pause
  \vfill
  Potentially, this leads to checking $O(2^n)$ relations, if $n$
  \tatoms are in the formula

\end{frame}

\begin{frame}
  \frametitle{The Eager and Lazy Approaches}

  There are (at least) two ways to discover incompatibilities
  \begin{itemize}
    \item {\bf eagerly} adding them before calling a \satsolver (eager approach)
	  \begin{description}
	    \item[$+$] Easy to implement: \satsolver used as black-box
	    \item[$+$] Good for bit-vectors theories
	    \item[$-$] Potentially generates too big encoding: needs heuristics
	               to make it efficient
	    \item[$-$] Bad for arithmetic theories
	  \end{description} \pause
    \item {\bf lazily}, by adding them during the \satsolver's search (lazy approach)
	  \begin{description}
	    \item[$+$] Generates smaller encodings
	    \item[$+$] Good for arithmetic theories
	    \item[$+$] Modular approach: allows easy theory combination
	    \item[$-$] Trickier to implement: \satsolver has to be ``openen''
	  \end{description}
  \end{itemize}
  \vfill
  \pause
  Most of this course will be devoted to the lazy approach,
  which is nowadays the most successful technique available

\end{frame}

\begin{frame}
  \frametitle{The Eager Approach}

  \begin{center}
  \scalebox{.5}{\input{eager.pdf_t}}
  \end{center}

\end{frame}

\begin{frame}
  \frametitle{The Lazy Approach}

  \begin{center}
  \scalebox{.5}{\input{lazy.pdf_t}}
  \end{center}

\end{frame}

\begin{frame}
  \frametitle{Plan of (the rest of) the course}

  \begin{itemize}
    \item The eager approach: solving bit-vectors
    \vfill
    \item Modern SAT-solvers: conflict analysis, clause learning, and heuristics
    \vfill
    \item The Lazy approach: generalities
    \vfill
    \item A theory-solver for \Idl
    \vfill
    \item A theory-solver for \Uf
    \vfill
    \item A theory-solver for \Lra
    \vfill
    \item (see if there is time left)
  \end{itemize}

\end{frame}

max_stars_repo_name: formalmethods/smtlectures

max_issues_repo_name: formalmethods/smtlectures

max_forks_repo_name: formalmethods/smtlectures


text:
% LaTeX template for Artifact Evaluation V20180713
%
% Prepared by
% * Grigori Fursin (cTuning foundation, France and dividiti, UK) 2014-2019
% * Bruce Childers (University of Pittsburgh, USA) 2014
%
% See example of this Artifact Appendix in
%  * SC'17 paper: https://dl.acm.org/citation.cfm?id=3126948
%  * CGO'17 paper: https://www.cl.cam.ac.uk/~sa614/papers/Software-Prefetching-CGO2017.pdf
%  * ACM ReQuEST-ASPLOS'18 paper: https://dl.acm.org/citation.cfm?doid=3229762.3229763
%
% (C)opyright 2014-2019
%
% CC BY 4.0 license
%

\documentclass{sigplanconf}

\PassOptionsToPackage{hyphens}{url}\usepackage{hyperref}

\usepackage{framed}

\begin{document}

\special{papersize=8.5in,11in}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% When adding this appendix to your paper,
% please remove above part
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\appendix
\section{Artifact Appendix}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Abstract}

The artifact contains all the JARs of version 0.12 of the DataSketches
library, before it moved into Apache (Incubating), as well as configurations
and shell scripts to run our tests.. It can support the results found in
Section XXX of our PPoPP'2020 paper Fast Concurrent Data Sketches. To
validate the results, run the test scripts and check the results piped
in the according text output files.

\subsection{Artifact check-list (meta-information)}

{\em Obligatory. Use just a few informal keywords in all fields applicable to your artifacts
and remove the rest. This information is needed to find appropriate reviewers and gradually
unify artifact meta information in Digital Libraries.}

{\small
\begin{itemize}
  \item {\bf Algorithm: HLL $\Theta$ Sketch}
  \item {\bf Program: Java code}
  \item {\bf Compilation: JDK 8, and each package is compiled using maven}
  \item {\bf Binary: Java executables}
  \item {\bf Run-time environment: Java}
  \item {\bf Hardware: Ubuntu on 12 core server and 32 core server with hyperthreading disabled}
  \item {\bf Execution: }
  \item {\bf Metrics: Throughput and accuracy}
  \item {\bf Output: Runtime throughputs, and runtime accuracy}
  \item {\bf Experiments: }
  \item {\bf How much disk space required (approximately)?: }
  \item {\bf How much time is needed to prepare workflow (approximately)?: Using precomipled packages, none.}
  \item {\bf How much time is needed to complete experiments (approximately)?: 10 hours}
  \item {\bf Publicly available?: Yes.}
  \item {\bf Code licenses (if publicly available)?: Apache License 2.0}
  \item {\bf Data licenses (if publicly available)?: }
  \item {\bf Workflow framework used?: }
  \item {\bf Archived (provide DOI)?: }
\end{itemize}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Description}

\subsubsection{How delivered}

{\em Obligatory}
The Apache DataSketches (Incubating) library is an open source project
under Apache License 2.0, and is hosted with code, API specifications,
build instructions, and design documentations on Github.

\subsubsection{Hardware dependencies}
Our tests require a 12 core server and 32 core machine with hyper-threading disabled

\subsubsection{Software dependencies}
The Apache DataSketches (Incubating) library has been tested on Ubuntu 12.04/14.04,
and is expected to run correctly under other Linux distributions. Building the JAR
files requires JDK 8; the files don't compile otherwise.

\subsubsection{Data sets}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Installation}

{\em Obligatory}

First, clone the repository:

\begin{framed}

\$ git clone \url{https://github.com/ArikRinberg/FastConcurrentDataSketchesArtifact}

\end{framed}

\noindent We have provided the necessary JAR files for recreating our experiment.

\paragraph{\textbf{Custom compilation.}}
Alternatively, follow the build instructions on Apache DataSketches (Incubating) apache
page (https://datasketches.apache.org/), in order to building the above mentioned
JAR files, now called:
\begin{itemize}
  \item incubator-datasketches-java (https://github.com/apache/incubator-datasketches-java)
  \item incubator-datasketches-memory (https://github.com/apache/incubator-datasketches-memory)
  \item incubator-datasketches-characterization (https://github.com/apache/incubator-datasketches-characterization)
\end{itemize}

\noindent The version number of incubator-datasketches-java
and incubator-datasketches-memory must comply with the version numbers required by incubator-datasketches-characterization.
The characterization JAR file is an unsupported open-source code base, and
does not pretend to have the same level of quality as the primary repositories.
These characterization tests are often long running (some can run for days) and very resource intensive, which makes
them unsuitable for including in unit tests. The code in this repository are some of
the test suites we use to create some of the plots on our website and provide evidence for our speed and accuracy claims.

For convenience we have included these repositories as modules in our main repository along with specific branches and commit id's
that are known to compile. To compile the jar files:
\begin{framed}

\$ git clone \url{https://github.com/ArikRinberg/FastConcurrentDataSketchesArtifact}

\$ cd FastConcurrentDataSketchesArtifact

\$ source customCompile.sh

\end{framed}

\noindent The shell script takes care of initialising the submodules, building the source files, and copying the correct
JAR files to the current directory.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Experiment workflow}

\paragraph{\textbf{Workflow for precompiled JAR files.}}
For convenience, we provide the JAR files required and the configurations
used to run our tests.

\begin{enumerate}
  \item After cloning the repository:

  \hrulefill

  \$ cd FastConcurrentDataSketchesArtifact

  \hrulefill

  \noindent In the current working directory, there should either be the following JAR files:
  \begin{itemize}
    \item memory-0.12.1.jar
    \item sketches-core-0.12.1-SNAPSHOT.jar
    \item characterization-0.1.0-SNAPSHOT.jar
  \end{itemize}

  \item Next, run the tests:

  \hrulefill

  \$ java -cp "./*" com.yahoo.sketches.characterization.Job \${FigureXX}JobTest.conf

  \hrulefill

  \noindent where FIGURE-XX is the figure that you wish to recreate. The results per
  experiment are in a file called \${FigureXX}Profile*.txt.

\end{enumerate}

TODO:
Command line:
java -cp "./*" com.yahoo.sketches.characterization.Job test.conf

\paragraph{\textbf{Workflow for custom JAR files.}}

\begin{enumerate}
  \item After cloning the repository:

  \hrulefill

  \$ cd FastConcurrentDataSketchesArtifact

  \hrulefill

  \noindent In the current working directory, there should either be the following JAR files:

  \begin{itemize}
    \item datasketches-memory-1.1.0-incubating.jar
    \item datasketches-java-1.1.0-incubating.jar
    \item datasketches-characterization-1.0.0-incubating-SNAPSHOT.jar
  \end{itemize}

\end{enumerate}

TODO:
Command line :
java -cp "./*" org.apache.datasketches.Job test.conf
(mention that JobProfile needs to be altered.)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Evaluation and expected result}

For Figures X,Y and Z, the expected results are runtime throughput in nanoseconds
per update. These figures show updates per second, therefore a conversion is needed;
if the result is $x$, then the data-point is $1000/x$. For Figures A and B, the
expected results are accuracy.

{\em Obligatory}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Experiment customization}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Notes}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Methodology}

Submission, reviewing and badging methodology:

\begin{itemize}
  \item \url{http://cTuning.org/ae/submission-20190109.html}
  \item \url{http://cTuning.org/ae/reviewing-20190109.html}
  \item \url{https://www.acm.org/publications/policies/artifact-review-badging}
\end{itemize}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% When adding this appendix to your paper,
% please remove below part
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\end{document}


text:
\documentclass[10pt,letter]{article}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{setspace}
\usepackage{fullpage}
\renewcommand{\arraystretch}{2}
\usepackage{braket}
\usepackage{hyperref}

\usepackage{algorithm}
\usepackage{algpseudocode}

\begin{document}

\title{One dimensional adaptive mesh refinement}
\author{Justin Ripley
	\\Princeton University}
\date{\today}

\maketitle

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
	Berger-Oliger style adaptive mesh refinement \cite{Berger:1984zza},
with implementation of delayed solution technique of \cite{Pretorius:2005ua}
to also solve ordinary differential equation constraints along with PDE.

       A lot of the basic implementation ideas come from the AMRD/PAMR
library written by Frans Pretorius
(with addtions by Will East and Branson Stevens).

	As it stands, the code can handle one dimensional PDE, with only
one refinement grid per level. The code can also handle excision, and
be configured to run with fixed mesh refinement.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Basic algorithms}

	The basic algorithm. See also \cite{Berger:1984zza,Pretorius:2005ua}.

\begin{algorithm}
\caption{Evolve grid hierarchy (recursive)}\label{alg:time_step}
\begin{algorithmic}[1]
\Procedure{Evolve}{grid,times}
	\For{$t\gets1,times$}
		\State{$grid.time\gets grid.time+1$}
		\If{$\texttt{time to regrid}$}
			\State\Call{Regrid\_All\_Finer\_Grids}{$grid$}
		\EndIf
		\If{$\texttt{grid is interior}$}
			\State{\Call{Interpolate\_Boundary\_Conditions}{$grid.parent,grid$}}
		\EndIf
		\State{\Call{Solve\_PDE\_Step}{$grid$}}
		\If{$\texttt{not finest grid}$}
			\State{\Call{Evolve}{$grid.child,\texttt{refinement}$}}
		\EndIf
	\EndFor
	\If{$\texttt{not coarsest grid}$}
		\State{\Call{Compute\_Truncation\_Error}{$grid.parent,grid$}}
		\State{\Call{Inject}{$grid.parent,grid$}}
	\EndIf
\EndProcedure
\end{algorithmic}
\end{algorithm}

\bibliography{localbib}
\bibliographystyle{alpha}

\end{document}