text:
\documentclass{article}

\usepackage{fancyhdr}
\usepackage{extramarks}
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{syntax}
\usepackage{stmaryrd}
\usepackage{mathpartir}
\usepackage{tipa}

%
% Basic Document Settings
%

\topmargin=-0.45in
\evensidemargin=0in
\oddsidemargin=0in
\textwidth=6.5in
\textheight=9.0in
\headsep=0.25in

\linespread{1.1}

\pagestyle{fancy}
\chead{Globally Ordered Type System}
\lfoot{\lastxmark}
\cfoot{\thepage}

\renewcommand\headrulewidth{0.4pt}
\renewcommand\footrulewidth{0.4pt}

\setlength\parindent{30pt}

\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Zt}{$\Z$}

% Create a relational rule
% [#1] - Additional mathpartir arguments
% {#2} - Name of the rule
% {#3} - Premises for the rule
% {#4} - Conclusions for the rule
\newcommand{\relationRule}[4][]{\inferrule*[lab={\sc #2},#1]{#3}{#4}}

\newcommand{\rel}[1]{\ensuremath{\llbracket {#1} \rrbracket}}
\newcommand{\ttt}{\texttt}
\newcommand{\transform}{\rightsquigarrow}
\newcommand{\proj}{\pi}
\newcommand{\ttuple}{(\tau_1, \ldots, \tau_n)}
\newcommand{\etuple}{(e_1,\ldots,e_n)}
\newcommand{\bool}{\mathrm{bool}}
\newcommand{\integer}{\mathrm{int}}
\newcommand{\option}{\mathrm{option}}
\newcommand{\uoption}[1]{(\bool,#1)}
\newcommand{\opt}[1]{\texttt{opt-#1}}
\newcommand{\varOf}[1]{\texttt{varOf}(#1)}

\newcommand{\oktype}{valid}

\begin{document}
\section*{The System}
We begin by defining a grammar of "base types". These are the types which are eligible to be stored in global variables. The particular set of base types is not important, but we believe the following ones give a good overview.

\begin{grammar}
	<$T$ (base types)> ::= Unit | Int | Bool | T * T
\end{grammar}

Everything in the rest of this document is defined with respect to an ordered set $\mathbb{G} = \{g_0, \dots, g_{n-1}\}$ of \emph{global variables}, each of which has an associated base type $T_i$. Our goal is to enforce that $g_0$ is always used before $g_1$, $g_1$ before $g_2$, and so on. For simplicity, we require that each global variable be used; however, we will later relax this restriction by adding subtyping.

In our model, a global variable is not considered \emph{used} until it is actually accessed. Note that this is different from a normal ordered type system, where any appearance of the variable is considered a use. To distinguish appearances from memory accesses, we adopt ref-cell-like syntax for dereferencing or updating global variables. Note that this is different from the user model in actual dpt, where global variables are viewed as simple values. Instead of the ref-cell operators, dpt contains several built-in functions with appropriate type signatures.

The \emph{effects} $\epsilon$ in this system specify which global variables have been used so far. Effects are represented as an integer from $0$ to $n$, where effect $i$ means that all global variables up to but not including $g_i$ have been used so far (that is, we expect to use $g_i$ next).

We will also wish to allow users to define functions which are polymorphic in effect; for example, a function which takes in any global variable, dereferences it, and returns the value. Such a function would have an "effect signature" of something like $\alpha \rightarrow \alpha + 1$. To accommodate this, we will add polymorphic variables and a $+$ operation to our effect grammar.

Our effects are also intertwined with the language's value types $\tau$, in two ways. First, we have a special $\texttt{ref} (T, \epsilon)$ type for representing the value of a global variable. Second, function types must be altered to include their effect on the global variables. We do so by adding input and output effects to function types as well, using the form $(\tau, \epsilon) \rightarrow (\tau, \epsilon)$.

All in all, we have the following grammar of types and effects.

\begin{grammar}
	<$\epsilon$ (effects)> ::= 0 | 2 | \dots | n | $\alpha$ | $\epsilon + \epsilon$

	<$\tau$ (types)> ::= T | ref ($\tau, \epsilon$) | $\forall \overline \alpha.(\tau, \epsilon) \rightarrow (\tau, \epsilon)$
\end{grammar}

Note that we use the convention that when representing effects, $\epsilon$ represents any effect, Latin letters represent only integer effects, and Greek letters represent effect variables.

Next, we define a simple functional language to use this system on:

\begin{grammar}
	<$x$ (variables)> ::= alphanumeric

	<$v$ (values)> ::= () | $\Z$ | True | False | $(v, v)$ | $\texttt{fun}\ [\overline \alpha]\ (x:\tau, \epsilon) \rightarrow e$ | $g_0$ | \dots | $g_{n-1}$

	<$e$ (expressions)> ::= $v$ | $x$ | $e + e$ | $(e,e)$ | fst $e$ | snd $e$ | let $x$ = $e$ in $e$ | if $e$ then $e$ else $e$ | !$e$ | $e := e$ | $e[\overline \epsilon]$ $e$
\end{grammar}

Note that we treat the global variables as values in their own right in this system.

The $\texttt{fun } [\overline \alpha]\ (x : \tau, \epsilon) \rightarrow e$ syntax defines a possibly-polymorphic function within which annotations may reference the universally quantified effect variable $\alpha$. The $e [\overline \epsilon]\ e$ syntax applies a polymorphic function of this form, instantiating $\alpha$ with $\epsilon$.

\clearpage
\section*{Relations on Effects}
\subsection*{Effect Equivalence}
One may notice that our effect grammar allows us to write logically equivalent effects in different ways: for example, $1+1$ or $2$. To avoid this complication, we define an equivalence relation $\equiv$ on effects as follows, using $\oplus$ to represent integer addition:

\begin{mathpar}
	\relationRule{effect-refl}{
		\
	}{
		\epsilon \equiv \epsilon
	}

	\relationRule{effect-sym}{
		\epsilon_2 \equiv \epsilon_1
	}{
		\epsilon_1 \equiv \epsilon_2
	}

	\relationRule{effect-trans}{
		\epsilon_1 \equiv \epsilon_2\\
		\epsilon_2 \equiv \epsilon_3
	}{
		\epsilon_1 \equiv \epsilon_3
	}

	\relationRule{int-plus}{
		i \oplus j = k
	}{
		i+j \equiv k
	}
\\
	\relationRule{plus-comm}{
		\
	}{
		\epsilon_1 + \epsilon_2 \equiv \epsilon_2 + \epsilon_1
	}

	\relationRule{plus-assoc}{
		\
	}{
		(\epsilon_1 + \epsilon_2) + \epsilon_3 \equiv \epsilon_1 + (\epsilon_2 + \epsilon_3)
	}

	\relationRule{plus-cong}{
		\epsilon_1 \equiv \epsilon_3\\
		\epsilon_2 \equiv \epsilon_4
	}{
		\epsilon_1 + \epsilon_2 \equiv \epsilon_3 + \epsilon_4
	}
\end{mathpar}

\subsection*{Effect Substitution}
In order to define our typing relation, we will need to be able to perform substitution on types to eliminate $\alpha$s. To do so, we define a standard capture-avoiding substitution relation $[\epsilon/\alpha]$, defined below.

\begin{align*}
	\alpha[\epsilon/\alpha] & = \epsilon\\
	\beta[\epsilon/\alpha] & = \beta\ (\mbox{if }\beta \neq \alpha)\\
	i[\epsilon/\alpha] & = i\\
	(\epsilon_1 + \epsilon_2)[\epsilon/\alpha] & = \epsilon_1[\epsilon/\alpha] + \epsilon_2[\epsilon/\alpha]
\\\hfill\\
	T[\epsilon/\alpha] & = T\\
	(\tau_1 * \tau_2)[\epsilon/\alpha] & = \tau_1[\epsilon/\alpha] * \tau_2[\epsilon/\alpha]\\
	\texttt{ref } (\tau, \epsilon_1)[\epsilon/\alpha] & = \texttt{ref } (\tau[\epsilon/\alpha], \epsilon_1[\epsilon/\alpha])\\
	\left(\forall \overline \alpha.(\tau_1, \epsilon_1) \rightarrow (\tau_2, \epsilon_2)\right)[\epsilon/\alpha] & = \forall \overline \alpha.(\tau_1, \epsilon_1) \rightarrow (\tau_2, \epsilon_2)\\
	\left(\forall \beta.(\tau_1, \epsilon_1) \rightarrow (\tau_2, \epsilon_2)\right)[\epsilon/\alpha] & = \forall\beta.(\tau_1[\epsilon/\alpha], \epsilon_1[\epsilon/\alpha]) \rightarrow (\tau_2[\epsilon/\alpha], \epsilon_2[\epsilon/\alpha]) \mbox{ (if $\beta \neq \alpha$ and $\beta$ does not appear in $\epsilon$) }
\end{align*}

We define this to operate on effects and types according to the above rules, and extend it to operate on expressions and environments in the obvious way.

\subsection*{Effect Ordering}
We define a standard $\leq$ order on effects so we can compare them, using the $\preceq$ symbol to indicate integer less-than-or-equals.

\begin{mathpar}
	\relationRule{leq-trans}{
		\epsilon_1 \leq \epsilon_2\\
		\epsilon_2 \leq \epsilon_3
	}{
		\epsilon_1 \leq \epsilon_3
	}

	\relationRule{leq-equiv}{
		\epsilon_1 \equiv \epsilon_2
	}{
		\epsilon_1 \leq \epsilon_2
	}

	\relationRule{leq-int}{
		i \preceq j
	}{
		i \leq j
	}

	\relationRule{leq-plus-1}{
		\epsilon_1 \leq \epsilon_3\\
		\epsilon_2 \leq \epsilon_4
	}{
		\epsilon_1 + \epsilon_2 \leq \epsilon_3 + \epsilon_4
	}

	\relationRule{leq-plus-2}{
		\
	}{
		\epsilon_1 \leq \epsilon_1 + \epsilon_2
	}
\end{mathpar}

\section*{The Typing Relation}
Type inference in this system simultaneously reasons about effects and regular types. As a result, the typing relation has an extra input and output, representing the state of the global variables before and after the expression, respectively.

Our typing relation will thus have the form $\Delta, \Gamma, \epsilon \vdash e\ \colon \tau, \epsilon$. As usual, $\Gamma$ represents our current collection of bound variables; we treat it as a map. $\Delta$ represent our current collection of bound effect quantified variables; we treat it as a set. Our goal is that our program $p$ satisfies $\emptyset, \emptyset, 0 \vdash p\ \colon \tau, n$ for some $\tau$.

We will say that an effect $\epsilon$ is \emph{well-typed} with respect to $\Delta$, written $\Delta \vdash \epsilon$ if all free effect variables in $\epsilon$ are contained in $\Delta$. We extend this relation to operate on types and environments in addition to effects in the obvious way.

When writing rules, we use the convention that the metavariable $x$ matches all \emph{non-global} variables. We will always denote global variables using symbols of the form $g_i$. For the rest of these rules we will treat effects as being equal if they are equivalent.
\begin{mathpar}
	\relationRule{int}{
		n \in \Z
	}{
		\Delta, \Gamma, \epsilon \vdash n\ \colon \texttt{Int}, \epsilon
	}

	\relationRule{true}{
		\
	}{
		\Delta, \Gamma, \epsilon \vdash \texttt{True}\ \colon \texttt{Bool}, \epsilon
	}

	\relationRule{false}{
		\
	}{
		\Delta, \Gamma, \epsilon \vdash \texttt{False}\ \colon \texttt{Bool}, \epsilon
	}

	\relationRule{Unit}{
		\
	}{
		\Delta, \Gamma, \epsilon \vdash ()\ \colon \texttt{Unit}, \epsilon
	}

	\relationRule{global variable}{
		\
	}{
		\Delta, \Gamma, \epsilon \vdash g_i\ \colon \texttt{ref}(T_i, i), \epsilon
	}
\end{mathpar}

Now we can write rules for non-value expressions:

\begin{mathpar}
	\relationRule{local variable}{
		\Gamma[x] = \tau
	}{
		\Delta, \Gamma, \epsilon \vdash x\ \colon \tau, \epsilon
	}

	\relationRule{plus}{
		\Delta, \Gamma, \epsilon \vdash e_1\ \colon \texttt{Int}, \epsilon_1\\
		\Delta, \Gamma, \epsilon_1 \vdash e_2\ \colon \texttt{Int}, \epsilon_2
	}{
		\Delta, \Gamma, \epsilon \vdash e_1 + e_2\ \colon \texttt{Int}, \epsilon_2
	}

	\relationRule{pair}{
		\Delta, \Gamma, \epsilon \vdash e_1\ \colon \tau_1, \epsilon_1\\
		\Delta, \Gamma, \epsilon_1 \vdash e_2\ \colon \tau_2, \epsilon_2
	}{
		\Delta, \Gamma, \epsilon \vdash (e_1, e_2)\ \colon \tau_1 * \tau_2, \epsilon_2
	}

	\relationRule{fst}{
		\Delta, \Gamma, \epsilon \vdash e\ \colon \tau_1 * \tau_2, \epsilon_1\\
	}{
		\Delta, \Gamma, \epsilon \vdash \texttt{fst } e\ \colon \tau_1, \epsilon_1
	}

	\relationRule{snd}{
		\Delta, \Gamma, \epsilon \vdash e\ \colon \tau_1 * \tau_2, \epsilon_1\\
	}{
		\Delta, \Gamma, \epsilon \vdash \texttt{snd } e\ \colon \tau_2, \epsilon_1
	}

	\relationRule{let}{
		\Delta, \Gamma, \epsilon \vdash e_1\ \colon \tau_1, \epsilon_1\\
		\Delta, \Gamma[x := \tau_1], \epsilon_1 \vdash e_2\ \colon \tau_2, \epsilon_2
	}{
		\Delta, \Gamma, \epsilon \vdash \texttt{let } x = e_1 \texttt{ in } e_2\ \colon \tau_2, \epsilon_2
	}

	\relationRule{if}{
		\Delta, \Gamma, \epsilon \vdash e_1\ \colon \texttt{Bool}, \epsilon_1\\
		\Delta, \Gamma, \epsilon_1 \vdash e_2\ \colon \tau, \epsilon_2\\
		\Delta, \Gamma, \epsilon_1 \vdash e_3\ \colon \tau, \epsilon_2
	}{
		\Delta, \Gamma, \epsilon \vdash \texttt{if } e_1 \texttt{ then } e_2 \texttt{ else } e_3\ \colon \tau, \epsilon_2
	}
\end{mathpar}

Now let's finally write some rules that actually change $\epsilon$.

\begin{mathpar}
	\relationRule{deref}{
		\Delta, \Gamma, \epsilon \vdash e\ \colon \texttt{ref}(\tau, \epsilon_1), \epsilon_1
	}{
		\Delta, \Gamma, \epsilon \vdash\ !e\ \colon \tau, \epsilon_1+1
	}

\relationRule{update}{
	\Delta, \Gamma, \epsilon \vdash e_1\ \colon \tau, \epsilon_1\\
	\Delta, \Gamma, \epsilon_1 \vdash e_2\ \colon \texttt{ref}(\tau, \epsilon_2), \epsilon_2
}{
	\Delta, \Gamma, \epsilon \vdash e_2 := e_1\ \colon \texttt{Unit}, \epsilon_2+1
}
\end{mathpar}

And finally, the function rules:
\begin{mathpar}
	\relationRule{abs}{
		\Delta' = \Delta \cup \{\overline \alpha\}\\
		\Delta' \vdash \tau_{in}\\
		\Delta' \vdash \epsilon_{in}\\
		\Delta', \Gamma[x := \tau_{in}], \epsilon_{in} \vdash e\ \colon \tau_{out}, \epsilon_{out}
	}{
		\Delta, \Gamma, \epsilon \vdash \texttt{fun } [\overline \alpha]\ (x : \tau_{in}, \epsilon_{in}) \rightarrow e\ \colon \forall \overline \alpha.(\tau_{in}, \epsilon_{in}) \rightarrow (\tau_{out}, \epsilon_{out}), \epsilon
	}

	\relationRule{app}{
		\Delta, \Gamma, \epsilon \vdash e_1\ \colon \forall \overline \alpha.(\tau_{in}, \epsilon_{in}) \rightarrow (\tau_{out}, \epsilon_{out}), \epsilon_1\\
		\Delta \vdash \overline{\epsilon_\alpha}\\
		\Delta, \Gamma, \epsilon_1 \vdash e_2\ \colon \tau_{in}[\overline{\epsilon_\alpha/\alpha}], \epsilon_{in}[\overline{\epsilon_\alpha/\alpha}]\\
	}{
		\Delta, \Gamma, \epsilon \vdash e_1[\overline {\epsilon_\alpha}]\ e_2\ \colon \tau_{out}[\overline{\epsilon_\alpha/\alpha}], \epsilon_{out}[\overline{\epsilon_\alpha/\alpha}]
	}
\end{mathpar}

\subsection*{Skipping Variables}
In practice, the requirement that we \emph{must} use each global variable more restrictive than we would like. We would like to programs in which some global variables are skipped. We do this by adding a subtyping relation on effects and types.

\begin{mathpar}
	\relationRule{sub-refl}{
		\
	}{
		\tau <: \tau
	}

	\relationRule{sub-pair}{
		\tau_1 <: \tau_3\\
		\tau_2 <: \tau_4\\
	}{
		(\tau_1, \tau_2) <: (\tau_3, \tau_4)
	}

	\relationRule{sub-function}{
		\tau_1' <: \tau_1\\
		\tau_2 <: \tau_2'\\
		\epsilon_1' \leq \epsilon_1\\
		\epsilon_2 \leq \epsilon_2'
	}{
		\forall \overline \alpha.(\tau_1, \epsilon_1) \rightarrow (\tau_2, \epsilon_2) <: \forall \overline \alpha.(\tau_1', \epsilon_1') \rightarrow (\tau_2', \epsilon_2')
	}
\end{mathpar}

Finally, we augment our typing relation with the single rule
\begin{mathpar}
	\relationRule{subtyping}{
		\tau_1 <: \tau_2\\
		\epsilon_1 \leq \epsilon_2\\
		\Delta \vdash \tau_2\\
		\Delta \vdash \epsilon_2\\
		\Delta, \Gamma, \epsilon \vdash e\ \colon \tau_1, \epsilon_1
	}{
		\Delta, \Gamma, \epsilon \vdash e\ \colon \tau_2, \epsilon_2
	}
\end{mathpar}

Note that we only really have two uses for this new typing rule: replacing functions, and incrementing the effect.

\section*{Properties of the Typing Relation}

\subsection*{Transitivity of subtyping}
Theorem: If $\tau_1 <: \tau_2$ and $\tau_2 <: \tau_3$ then $\tau_1 <: \tau_3$.
\\

\noindent Proof: Straightforward structural induction on the proof that $\tau_1 <: \tau_2$, using inversion on the proof that $\tau_2 <: \tau_3$.

\subsection*{Well-typedness}
Lemma WT-1: If $\Delta \cup \{\alpha\} \vdash \epsilon$ if and only if $\Delta \vdash \epsilon'$ implies $\Delta \vdash \epsilon[\epsilon'/\alpha]$.
\\

\noindent Proof: Straightforward induction on $\epsilon$. The $\beta$ case is the tricky one in both instances. In the forward direction we note that since $\Delta \cup \{\overline\alpha\} \vdash \epsilon = \beta$, $\beta$ must be in $\Delta$. In the reverse direction we instantiate $\epsilon'$ with a constant $i$ to get $\Delta \vdash \beta[i/\alpha] = \beta$.
\\

\noindent Lemma WT-2: $\Delta \cup \{\alpha\} \vdash \tau$ if and only if $\Delta \vdash \epsilon'$ implies $\Delta \vdash \tau[\epsilon'/\alpha]$.
\\

\noindent Proof: Straightforward induction on $\tau$.
\\

\noindent Lemma WT-3: $\Delta \vdash \forall \overline \alpha.(\tau_1, \epsilon_1) \rightarrow (\tau_2, \epsilon_2)$  if and only if $\tau_1, \tau_2, \epsilon_1, \epsilon_2$ are all well-typed with respect to $\Delta \cup \{\overline \alpha\}$
\\

\noindent Proof: We prove the contrapositive. The function type is not well-typed iff it contains a free variable $\beta \notin \Delta$, and certainly $\beta \neq \alpha$ since all occurrences of $\alpha$ in the function type are bound. This can happen iff one of the sub-parts contains $\beta$, meaning that one of the sub-parts is not well-typed.
\\

\noindent Theorem: If $\Delta, \Gamma, \epsilon \vdash e\ \colon \tau, \epsilon'$, where $\Delta \vdash \Gamma$ and $\Delta \vdash \epsilon$, then $\Delta \vdash \tau$ and $\Delta \vdash \epsilon'$.
\\

\noindent Proof: Structural induction on the typing derivation. In the LOCAL VARIABLE case, we use the fact that $\Delta \vdash \Gamma$. In the LET case we argue inductively that $\Delta \vdash \tau_1$, so that $\Delta \vdash \Gamma[x := \tau_1]$. In the ABS case we know that the input type and effect are well-typed with respect to $\Delta \cup \{\overline\alpha\}$, so by Lemma WT-3 the output is well-typed with respect to $\Delta$. In the APP case we use both Lemmas WT-2 and WT-3.

\subsection*{Well-typed lemmas}
Lemma WTL-1: If $\Delta \vdash \epsilon$ and $\epsilon' \leq \epsilon$ then $\Delta \vdash \epsilon'$.
Proof: Induction on the $\leq$ derivation.
\\

\noindent Lemma WTL-2: If $\emptyset \vdash \epsilon$ then $\epsilon \in \Z$. Proof: Induction on $\epsilon$.

\subsection*{Effect Weakening}
Lemma W-1: If $\Delta, \Gamma, \epsilon_1 \vdash e\ \colon \tau, \epsilon_2$ and $\epsilon_1' \leq \epsilon_1$ then $\Delta, \Gamma, \epsilon_1' \vdash e\ \colon \tau, \epsilon_2'$ for some $\epsilon_2' \leq \epsilon_2$.
\\

\noindent Proof: Straightforward structural induction on the typing derivation. We have to use subtyping in the DEREF, UPDATE and APP cases.
\\

\noindent Theorem: $\Delta, \Gamma, \epsilon_1 \vdash e\ \colon \tau, \epsilon_2$, $\epsilon_1' \leq \epsilon_1$ and $\epsilon_2 \leq \epsilon_2'$ and $\Delta \vdash \epsilon_2'$ then $\Delta, \Gamma, \epsilon_1' \vdash e\ \colon \tau, \epsilon_2'$.
\\

\noindent Proof: Apply Lemma W-1 then use transitivity of $\leq$ to apply SUBTYPING.

\subsection*{Environment Weakening}
Theorem: If $\Delta, \Gamma, \epsilon \vdash e\ \colon \tau, \epsilon'$ and $z \notin \Gamma$, then for all $\tau$, $\Gamma[z := \tau], \Delta, \epsilon \vdash e\ \colon \tau, \epsilon'$.
\\

\noindent Proof: Straightforward structural induction on the typing derivation. In the LOCAL VARIABLE case we use the fact that $z \notin \Gamma$ to show that $\Gamma[z := \tau][x] = \Gamma[z]$. In the LET case, either $z = x$ in which case $\Gamma[z := \tau][x := \tau_1] = \Gamma[x := \tau_1]$ and so the original premise still works, or $z <> x$ in which case $z \notin \Gamma[x := \tau_1]$ and $\Gamma[x := \tau_1][z := \tau] = \Gamma[z := \tau][x := \tau_1]$ and induction gives us the result. We do the same in the ABS case.

\subsection*{Delta-Weakening}
\noindent Lemma DW-1: If $\Delta \vdash \epsilon$ then for all $\alpha$, $\Delta \cup \{\alpha\} \vdash \epsilon$, and similarly if we replace $\epsilon$ with $\tau$ or $\Gamma$.
\\

\noindent Proof: Immediate from the definition well-typedness.
\\

\noindent Theorem: If $\Delta, \Gamma, \epsilon \vdash e\ \colon \tau, \epsilon'$ then for all $\alpha$, $\Gamma, (\Delta \cup \{\alpha\}), \epsilon \vdash e\ \colon \tau, \epsilon'$.
\\

\noindent Proof: Straightforward structural induction on the typing derivation, applying Lemma DW-1 as needed.

\subsection*{A shorthand for values}
Definition: We will write $v : \tau$ as shorthand for $\forall \epsilon. \emptyset, \emptyset, \epsilon \vdash v\ \colon \tau, \epsilon$.
\\

\noindent Theorem V-1: If $v : \tau$ then $\forall \Delta, \Gamma, \epsilon. \Delta, \Gamma, \epsilon \vdash v\ \colon \tau, \epsilon$.
\\

\noindent Proof: Inductive application of Environment and Delta Weakening.
\\

\noindent Theorem V-2: If $\emptyset, \emptyset, \epsilon \vdash v\ \colon \tau, \epsilon'$ then $v : \tau$ and $\epsilon \leq \epsilon'$.
\\

\noindent Proof: Straightforward structural induction on the typing derivation.

\subsection*{Canonical Forms}
Lemma C-1: If $\tau_1 <: \tau_2$, then:
\begin{itemize}
	\item If either $\tau_1$ or $\tau_2$ is a base type or $\texttt{ref}$ type then $\tau_1 = \tau_2$
	\item If either $\tau_1$ or $\tau_2$ is a pair type, then $\tau_1 = (\tau_a, \tau_b)$ and $\tau_2 = (\tau_c, \tau_d)$ where $\tau_a <: \tau_c$ and $\tau_b <: \tau_d$.
	\item If either $\tau_1$ or $\tau_2$ is a function type, then $\tau_1 = \forall \overline \alpha. (\tau_a, \epsilon_a) \rightarrow (\tau_b, \epsilon_b)$ and $\tau_2 = \forall \overline \alpha. (\tau_c, \epsilon_c) \rightarrow (\tau_d, \epsilon_d)$ where $\tau_c <: \tau_a$, $\tau_b <: \tau_d$, $\epsilon_a \leq \epsilon_c$ and $\epsilon_b \leq \epsilon_d$.
\end{itemize}

\noindent Proof: Inversion of the subtyping relation.
\\

\noindent Theorem: For all values $v$, if $v\ \colon \tau$ then
\begin{itemize}
	\item If $\tau = \texttt{Int}$ then $v \in \Z$
	\item If $\tau = \texttt{Bool}$ then $v = \texttt{True}$ or $v = \texttt{False}$
	\item If $\tau = \texttt{Unit}$ then $v = ()$
	\item If $\tau = \tau_1 * \tau_2$ then $v = (v_1, v_2)$ where $v_1 : \tau_1$ and $v_2 : \tau_2$.
	\item If $\tau = \texttt{ref} (\tau_1, \epsilon)$ then $\epsilon = i \in \Z$, $v = g_i$ and $\tau_1 = T_i$.
	\item If $\tau = \forall \overline \alpha.(\tau_1, \epsilon_1) \rightarrow (\tau_2, \epsilon_2)$ then $v = \texttt{fun } [\overline \alpha]\ (x : \tau_{in}, \epsilon_{in}) \rightarrow e$ where $\tau_1 <: \tau_{in}$ and $\epsilon_1 \leq \epsilon_{in}$, and $\{x := \tau_{in}\}, \{\overline\alpha\}, \epsilon_{in} \vdash e\ \colon \tau_{out}, \epsilon_{out}$, where $\tau_{out} <: \tau_2$ and $\epsilon_{out} \leq \epsilon_2$.
\end{itemize}

\noindent Proof: Induction on the proof that $v$ has type $\tau$ for some arbitrary $\Gamma, \epsilon$. Each $\tau$ has only two (or three, for booleans) that apply to a value and produce it: the base rules, and the subtyping rule. In the subtyping cases, we use Lemma C-1. In the pair case, we use induction and theorem V-2, and in the case where $\tau$ is a pair type and the subtyping rule was used, we Lemma C-1 twice in addition to induction, and similarly when $\tau$ is a function type.

\subsection*{The Substitution Lemma for Values}

\noindent Definition: If $\Gamma$ is a map, let $\Gamma \backslash x$ indicate the map which is identical to $\Gamma$ but contains no binding for $x$.
\\

\noindent Definition: Let $e[v/x]$ be the standard capture-avoiding substitution relation. It differs from the effect one in that it operates on values/variables instead of effects and effect variables.
\\

\noindent Theorem: If $\Gamma[x] = \tau$ and $v : \tau$ and $\Delta, \Gamma, \epsilon \vdash e\ \colon \tau', \epsilon'$, then $\Gamma\backslash x, \Delta, \epsilon \vdash e[v/x]\ \colon \tau', \epsilon'$

\noindent Proof: Structural induction on the typing proof. The interesting cases are:

\begin{itemize}
	\item In the VAR case $e = z$, either $z = x$ in which case $e[v/x] = v$ and the premise $v : \tau$ solves it (using theorem V-1), or $z <> x$ in which case $z \in \Gamma\backslash x$ and we simply use the VAR rule.
	\item In the LET case $e = \texttt{let } z = e_1 \texttt{ in }e_2$, either $z = x$ in which case $\Gamma\backslash z[x := \tau_1] = \Gamma[x := \tau_1]$ and we do not substitute in $e_2$, or $z <> x$ in which case $\Gamma\backslash z[x := \tau_1] = \Gamma[x := \tau_1]\backslash z$ and we do substitute in $e_2$. In either case the result follows immediately.
	\item Similar reasoning works for the ABS case.
	\item The subtyping case is immediate, but it bears noting that we don't change any of the types or effects that appear in the original derivation.
\end{itemize}

\subsection*{The Substitution Lemma for Effects}

\noindent Definition: If $\Delta$ is a set, let $\Delta \backslash \alpha$ indicate the set which is identical to $\Delta$ but does not contain $\alpha$.
\\

\noindent Lemma SE-1: For all $\epsilon, \epsilon_1, \epsilon_2, \alpha$, if $\epsilon_1 \equiv \epsilon_2$, then $\epsilon_1[\epsilon/\alpha] \equiv \epsilon_2[\epsilon/\alpha]$
\\

\noindent Proof: Straightforward structural induction on the proof that $\epsilon_1 \equiv \epsilon_2$.
\\

\noindent Lemma SE-2: For all $\epsilon, \epsilon_1, \epsilon_2, \alpha$, if $\epsilon_1 \leq \epsilon_2$, then $\epsilon_1[\epsilon/\alpha] \leq \epsilon_2[\epsilon/\alpha]$
\\

\noindent Proof: Straightforward structural induction on the proof that $\epsilon_1 \leq \epsilon_2$, using lemma SE-1 in the \texttt{leq-equiv} case.
\\

\noindent Lemma SE-3: If $\tau_1 <: \tau_2$ then for all $\epsilon, \alpha$ $\tau_1[\epsilon/\alpha] <: \tau_2[\epsilon/\alpha]$.
\\

\noindent Proof: Straightforward structural induction on the proof that $\tau_1 <: \tau_2$.
\\

\noindent Theorem: (If $\Delta \vdash \Gamma$ and $\Delta \vdash \epsilon$ then) If $\Delta\backslash \alpha \vdash \epsilon_\alpha$, and $\Delta, \Gamma, \epsilon \vdash e\ \colon \tau', \epsilon'$, then $\Gamma[\epsilon_\alpha/\alpha], \Delta\backslash \alpha, \epsilon[\epsilon_\alpha/\alpha] \vdash e[\epsilon_\alpha/\alpha]\ \colon \tau'[\epsilon_\alpha/\alpha], \epsilon'[\epsilon_\alpha/\alpha]$

\noindent Proof: Structural induction on the typing proof. The interesting cases are:

\begin{itemize}
	\item In the ABS case $e = \texttt{fun } [\beta] ...$, we have two cases. If $\beta = \alpha$ then $\Delta\backslash \alpha \cup \{\beta\} = \Delta \cup \{\beta\}$, and we did not change the expression when substituting, so the original premises suffice. Otherwise, by induction we can show what we need starting from $(\Delta \cup \{\beta\})\backslash \alpha$, and since $\beta \neq \alpha$ this is equal to $\Delta\backslash \alpha \cup \{\beta\}$, and the rest is easy. Note that we also use Lemma WT-2.
	\item In the APP case we have a similar situation to the above. Note that in both cases we could just use alpha-equivalence to only consider the case where $\beta \neq \alpha$.
	\item The subtyping case uses the induction hypothesis and Lemmas WT-2, SE-2 and SE-3.
\end{itemize}

\section*{Operational Semantics}

Now we'll define an operational semantics for our language. We are modeling a situation in which global variables are ordered in a pipeline, such that each global variable must be accessed after the ones before it in the pipeline.

As such, our operational semantics relation will have the form $(G, i, e) \rightarrow (G', i', e')$, where $G$ is an array $[v_0; \dots; v_{n-1}]$ of the current values for each global variable, $i$ is an integer indicating the current pipeline stage, and $e$ is the expression to be evaluated. We treat $G$ as a map from integers to values, so $G[0] = v_0$, etc. We say $G$ is well-typed if $G[i] : T_i$ for $0 \leq i \leq {n-1}$.

As usual, the metavariable $v$ will refer exclusively to values, while $e$ represents any expression. We use $\oplus$ to denote regular integer addition.

\clearpage
\begin{mathpar}
	\relationRule{plus-1}{
		(G, i, e_1) \rightarrow (G', i', e_1')
	}{
		(G, i, e_1 + e_2) \rightarrow (G', i', e_1' + e_2)
	}

	\relationRule{plus-2}{
		(G, i, e_2) \rightarrow (G', i', e_2')
	}{
		(G, i, v + e_2) \rightarrow (G', i', v + e_2')
	}

	\relationRule{plus-3}{
		v_1, v_2 \in \Z\\
	}{
		(G, i, v_1 + v_2) \rightarrow (G, i, v_1 \oplus v_2)
	}
\end{mathpar}

\begin{mathpar}
	\relationRule{pair-1}{
		(G, i, e_1) \rightarrow (G', i', e_1')
	}{
		(G, i, (e_1, e_2)) \rightarrow (G', i', (e_1', e_2))
	}

	\relationRule{pair-2}{
		(G, i, e_2) \rightarrow (G', i', e_2')
	}{
		(G, i, (v, e_2)) \rightarrow (G', i', (v, e_2'))
	}
\end{mathpar}

\begin{mathpar}
	\relationRule{fst-1}{
		(G, i, e) \rightarrow (G', i', e')
	}{
		(G, i, \texttt{fst } e) \rightarrow (G', i', \texttt{fst } e')
	}

	\relationRule{fst-2}{
		\
	}{
		(G, i, \texttt{fst } (v_1, v_2)) \rightarrow (G, i, v_1)
	}
\end{mathpar}

\begin{mathpar}
	\relationRule{snd-1}{
		(G, i, e) \rightarrow (G', i', e')
	}{
		(G, i, \texttt{snd } e) \rightarrow (G', i', \texttt{fst } e')
	}

	\relationRule{snd-2}{
		\
	}{
		(G, i, \texttt{snd } (v_1, v_2)) \rightarrow (G, i, v_2)
	}
\end{mathpar}

\begin{mathpar}
	\relationRule{let-1}{
		(G, i, e_1) \rightarrow (G', i', e_1')
	}{
		(G, i, \texttt{let } x = e_1 \texttt{ in } e_2) \rightarrow (G', i', \texttt{let } x = e_1' \texttt{ in } e_2)
	}

	\relationRule{let-2}{
		\
	}{
		(G, i, \texttt{let } x = v \texttt{ in } e_2) \rightarrow (G, i, e_2[v/x])
	}
\end{mathpar}

\begin{mathpar}
	\relationRule{if-1}{
		(G, i, e_1) \rightarrow (G', i', e_1')
	}{
		(G, i, \texttt{if } e_1 \texttt{ then } e_2 \texttt{ else } e_3) \rightarrow (G', i', \texttt{if } e_1' \texttt{ then } e_2 \texttt{ else } e_3)
	}

	\relationRule{if-true}{
		\
	}{
		(G, i, \texttt{if } \texttt{True} \texttt{ then } e_2 \texttt{ else } e_3) \rightarrow (G, i, e_2)
	}

	\relationRule{if-false}{
		\
	}{
		(G, i, \texttt{if } \texttt{False} \texttt{ then } e_2 \texttt{ else } e_3) \rightarrow (G, i, e_3)
	}
\end{mathpar}

\begin{mathpar}
	\relationRule{deref-1}{
		(G, i, e) \rightarrow (G', i', e')
	}{
		(G, i, !e) \rightarrow (G', i', !e')
	}

	\relationRule{deref-2}{
		i \leq j
	}{
		(G, i, !g_j) \rightarrow (G, j+1, G[j])
	}
\end{mathpar}

\begin{mathpar}
	\relationRule{update-1}{
		(G, i, e_1) \rightarrow (G', i', e_1')
	}{
		(G, i, e_2 := e_1) \rightarrow (G', i', e_2 := e_1')
	}

	\relationRule{update-2}{
		(G, i, e_2) \rightarrow (G', i', e_2')
	}{
		(G, i, e_2 := v) \rightarrow (G', i', e_2' := v)
	}

	\relationRule{update-3}{
		i \leq j
	}{
		(G, i, g_j := v) \rightarrow (G[j := v], j+1, ())
	}
\end{mathpar}

\begin{mathpar}
	\relationRule{app-1}{
		(G, i, e_1) \rightarrow (G', i', e_1')
	}{
		(G, i, e_1 [\overline{\epsilon_\alpha}]\ e_2) \rightarrow (G', i', e_1'[\overline{\epsilon_\alpha}]\ e_2)
	}

	\relationRule{app-2}{
		(G, i, e_2) \rightarrow (G', i', e_2')
	}{
		(G, i, v[\overline{\epsilon_\alpha}]\ e_2) \rightarrow (G', i', v[\overline{\epsilon_\alpha}]\ e_2')
	}

	\relationRule{app-3}{
		v_1 = \texttt{fun } [\overline \alpha]\ (x : \tau, \epsilon) \rightarrow e
	}{
		(G, i, v_1[\overline{\epsilon_\alpha}]\ v_2) \rightarrow (G, i, e[\overline{\epsilon_\alpha/\alpha}][v_2/x])
	}
\end{mathpar}

\subsection*{Evaluation weakening}
\noindent Theorem: If $(G, i, e) \rightarrow (G', i', v)$ and $j \leq i$ then $(G, j, e) \rightarrow (G', j', v)$ for some $j' \leq i'$.
\\

\noindent Proof: Straightforward induction on the proof of evaluation. The only mildly interesting cases are DEREF and UPDATE, where we use transitivity and reflexivity of $\leq$.

\subsection*{Monotonicity}
Theorem: if $(G, i, e) \rightarrow (G', i', e')$ then $i \leq i'$.
\\

\noindent Proof: Straightforward induction on the proof of evaluation.
\\

\noindent Corollary: If $(G, i, e) \rightarrow^* (G', i', e')$, then for all $j$, at the DEREF-2 and UPDATE-3 rules are used at most once (total, not each) on $g_j$. Furthermore, they are use only after any such rules are used on $g_k$ for all $k \leq j$.
\\

\noindent Proof: Each rule can only be used if the current state is at most $j$, and immediately sets the state to $j+1 > j$. By monotonicity, the state will remain above $j$ for the rest of the evaluation, so neither rule may be used again.

\subsection*{Progress}
Theorem: If $\emptyset, \emptyset, i \vdash e\ \colon \tau, j$, then either $e$ is a value or for all well-typed $G$ there exist some $G', j', e'$ such that $(G, i, e) \rightarrow (G', j', e')$.
\\

\noindent Proof: Structural induction on the typing derivation.
\\

Case INT/TRUE/FALSE/UNIT/GLOBAL VARIABLE/ABS: In these cases $e$ was already a value, so the result is trivial.
\\

Case LOCAL VARIABLE: Contradiction, since the environment is empty.
\\

\clearpage
Case PLUS: We know that
\begin{itemize}
	\item INV1:	$e = e_1 + e_2$
	\item PLUS: $\emptyset, \emptyset, i \vdash e_1 + e_2\ \colon \texttt{Int}, j$
	\item INV2: $\emptyset, \emptyset, i \vdash e_1\ \colon \texttt{Int}, \epsilon_1$
	\item INV3: $\emptyset, \emptyset, \epsilon_1 \vdash e_2\ \colon \texttt{Int}, j$
	\item IND1: $e_1$ is a value OR $\forall G.\exists G_1, j_1.(G, i, e_1) \rightarrow (G_1, j_1, e_1')$
	\item IND2: $e_2$ is a value OR $\forall G.\exists G_2, j_2.(G, \epsilon_1, e_2) \rightarrow (G_2, j_2, e_2')$
\end{itemize}
Note that by well-typedness and INV2, $\emptyset \vdash \epsilon_1$, so by Lemma WTL-2 $\epsilon_1 \in \Z$. Hence it is valid to use it in the second place of the evaluation relation in IND2.

Now we have three cases:
\begin{itemize}
	\item $e_1$ steps. We may then use IND1 and PLUS-1 to show that $(G, i, e_1 + e_2) \rightarrow (G_1, j_1, e_1'+e_2)$.
	\item $e_1$ is a value and $e_2$ steps. We first use INV2 and Theorem V-2 to show that $i \leq \epsilon_1$. We may then use evaluation weakening on IND2 to show that $(G, i, e_2) \rightarrow (G_2, j_2', e_2')$ for some $j_2' \leq j_2$. Finally we apply PLUS-2 to show that $(G, i, e_1+e_2) \rightarrow (G_2, j_2', e_1+e_2')$.
	\item Both $e_1$ and $e_2$ are values. Then by canonical forms we may conclude that $e_1, e_2 \in \Z$, so we may apply PLUS-3.
\end{itemize}

Case PAIR: Analogous to PLUS, but in the final case $e$ itself is already a value.
\\

Case FST: Here $e = \texttt{fst }e_1$. By induction, either $e_1$ is a value or $(G, i, e_1) \rightarrow (G', i', e_1')$. In the first case, canonical forms tells us that $e = (v_1, v_2)$, so we may use FST-2; otherwise, we may use FST-1.
\\

Case SND: Analogous to FST.
\\

Case LET: Here $e = \texttt{let } x = e_1 \texttt{ in } e_2$. By induction, either $e_1$ is a value or $(G, i, e_1) \rightarrow (G', i', e_1')$. In the former case we may apply LET-2; otherwise, we apply LET-1.
\\

Case IF: If $e_1$ steps then we use IF-1; otherwise, by canonical forms $e_1$ is either true or false. We then use Theorem V-2 to reduce $\epsilon_1$ to $i$ in the appropriate induction hypothesis, and apply IF-TRUE or IF-FALSE respectively.
\\

CASE DEREF: Here $e = !e_1$. By induction we conclude that either $e_1$ steps or it is a value. In the former case we apply DEREF-1. If it is a value, then by canonical forms $e_1 = g_j$. We then use theorem V-2 to conclude that $i \leq j$, so we may apply DEREF-2.
\\

CASE UPDATE: Here $e = e_2 := e_1$; the only interesting case is when both are values. We use theorem V-2 twice to show that $e \leq \epsilon_1$ and $\epsilon_1 \leq j$, and use canonical forms to show that $e_2 = g_j$. Thus we may apply UPDATE-3.
\\

CASE APP: Analogous to PLUS.
\\

CASE SUBTYPING: The result is immediate from induction on the typing judgement in the premises.

\subsection*{Preservation}
Theorem: If $\emptyset, \emptyset, i \vdash e\ \colon \tau, j$, $G$ is well-typed and $(G, i', e) \rightarrow (G', j', e')$ where $i' \leq i$, then $G'$ is well-typed and $\emptyset, \emptyset, j' \vdash e'\ \colon \tau, j$.

\noindent Proof: Structural induction on the typing derivation.
\\

Case INT/TRUE/FALSE/UNIT/GLOBAL VARIABLE/ABS: In these cases $e$ is a value, so it cannot step; hence these cases cannot occur.
\\

Case LOCAL VARIABLE: This case also cannot occur, because the environment is empty.
\\

Case PLUS: We have $e = e_1 + e_2$, so the proof that $e$ steps must have been PLUS-1, PLUS-2, or PLUS-3. We also know that $\emptyset, \emptyset, i \vdash e_1\ \colon \texttt{Int}, \epsilon_1$ and $\emptyset, \emptyset, \epsilon_1 \vdash e_2\ \colon \texttt{Int}, j$.
\begin{itemize}
	\item If we used PLUS-1, then $(G, i', e_1) \rightarrow (G', j', e_1')$, so by induction $G'$ is well-typed and $\emptyset, \emptyset, j' \vdash e_1'\ \colon \texttt{Int}, \epsilon_1$. We may then combine this with the other premise to show that $\emptyset, \emptyset, j' \vdash e_1' + e_2\ \colon \texttt{Int}, j$.
	\item If we used PLUS-2, then $e_1$ is a value and $(G, i', e_2) \rightarrow (G', j', e_2')$ where $i' \leq i$. Since $e_1$ is a value, by $i \leq \epsilon_1$ by Theorem V-2. Hence $i' \leq \epsilon_1$, so by induction $\emptyset, \emptyset, j' \vdash e_2'\ \colon \texttt{Int}, j$.

	Since $e_1$ is a value, we may use theorem V-2 on the first premise to show that $e_1 : \texttt{Int}$, so in particular $\emptyset, \emptyset, j' \vdash e_1\ \colon \texttt{Int}, j'$. We may combine this with the result of our induction to show that $\emptyset, \emptyset, j' \vdash e_1 + e_2'\ \colon \texttt{Int}, j$.
	\item If we use PLUS-3, then both $e_1$ and $e_2$ are integer values, $j' = i'$, and $G' = G$ is well-typed. We may then immediately show $\emptyset, \emptyset, j' \vdash e_1 \oplus e_2\ \colon \texttt{Int}, j'$ using the INT rule. Finally, we apply Theorem V-2 to our two premises to conclude that $i \leq \epsilon_1 \leq j$, so since $j' = i' \leq i$ we may use SUBTYPING to show that $\emptyset, \emptyset, j' \vdash e_1 \oplus e_2\ \colon \texttt{Int}, j$
\end{itemize}

Case PAIR: Analogous to the first two cases of PLUS
\\

Case FST: Analogous to the first and last cases of PLUS. In the latter case we also use canonical forms to show $v_1 : \tau_1$ instead of the INT rule.
\\

Case SND: Analogous to FST
\\

Case LET: The LET-1 case is analogous to previous cases. In the LET-2, case we get that $e_1$ is a value, $G' = G$ is well-typed, and $j' = i'$. From the typing proof, we also know that $\emptyset, \emptyset, i \vdash e_1\ \colon \tau_1, \epsilon_1$ and $\emptyset[x := \tau_1], \emptyset, \epsilon_1 \vdash e_2\ \colon \tau_2, j$. Since $e_1$ is a value, we immediately conclude $e_1 : \tau_1$ by Theorem V-2. Hence by the substitution lemma for values, $\emptyset, \emptyset, \epsilon_1 \vdash e_2[e_1/x]\ \colon \tau_2, \epsilon_2$. Using Theorem V-2 on the first premise we show that $i \leq \epsilon_1$, and since $i' \leq i$ we may use effect weakening to show that $\emptyset, \emptyset, i' \vdash e_2[e_1/x]\ \colon \tau_2, j$ as desired.
\\

Case IF: Analogous to previous cases.
\\

Case DEREF: We have $e =\ !e_1$ and $\emptyset, \emptyset, i \vdash e\ \colon \texttt{ref}(\tau, k), k$ where $k+1 = j$. We must have stepped using either DEREF-1 or DEREF-2. In the first case, we know that $(G, i', e_1) \rightarrow (G', j', e_1')$ and $i' \leq i$, so by induction $G'$ is well-typed and $\emptyset, \emptyset, j' \vdash e_1'\ \colon \texttt{ref}(\tau, k), k$. This is enough to show that $\emptyset, \emptyset, j' \vdash\ !e_1'\ \colon \tau, j$.

In the second case, we know that $e_1 = g_k$, $G' = G$, $j' = k+1 = j$, and $e' = G[k]$. Now note that $\tau = T_k$ by canonical forms, and since $G$ is well-typed, $G[k] : T_k$. If we instantiate the previous proof with $\epsilon = j$, we have what we wished to show.
\\

Case UPDATE: We have $e = e_2 := e_1$ and $\emptyset, \emptyset, i \vdash e\ \colon \tau, \epsilon_1$ and $\emptyset, \emptyset, \epsilon_1 \vdash e_2\ \colon \texttt{ref}(\tau, j), j$. Note also that by well-typedness $\emptyset \vdash \epsilon_1$, so by Lemma WTL-2 $\epsilon_1 \in \Z$. Hence it is valid to use $\epsilon_1$ in the step relation. We have three cases for which evaluation rule we used:
\begin{itemize}
	\item UPDATE-1: Then $(G, i', e_1) \rightarrow (G', j', e_1')$ and $i' \leq i$, so by induction $G'$ is well-typed and $\emptyset, \emptyset, j' \vdash e_1'\ \colon \tau, \epsilon_1$. We can combine this with the other premise to show that $\emptyset, \emptyset, j' \vdash e_2 := e_1'\ \colon \texttt{Unit}, j$ as required.
	\item UPDATE-2: In this case, we know that $(G, i', e_2) \rightarrow (G', j', e_2')$ and $i' \leq i$. We also know that $e_1$ is a value, so by Theorem V-2 $i \leq \epsilon_1$. Hence by induction $G'$ is well-typed and $\emptyset, \emptyset, j' \vdash e_2'\ \colon \texttt{ref}(\tau, j), j$.

	Next, we use Theorem V-2 on the first premise to show that $e_1 : \tau$, and so in particular $\emptyset, \emptyset, j' \vdash e_1\ \colon \tau, j'$. Now, finally, we may use these two premises to show that $\emptyset, \emptyset, j' \vdash e_2 := e_1'\ \colon \texttt{Unit}, j$ as required.

	\item UPDATE-3: In this case, $e' = ()$, $j' = j$, $e_1$ is a value and $e_2 = g_k$, where $k+1 = j$. Hence by the first premise $e_1 : \tau$ and by canonical forms, $\tau = T_k$, so $G[j := e_1]$ remains well-typed. Finally, $\emptyset, \emptyset, j' \vdash e'\ \colon \texttt{Unit}, j$ it is immediate with the UNIT rule.
\end{itemize}
\hfill

Case APP: We have $e = e_1[\overline{\epsilon_\alpha}]\ e_2$ and know that $\emptyset, \emptyset, i \vdash e_1\ \colon \forall \overline \alpha.(\tau_{in}, \epsilon_{in}) \rightarrow (\tau_{out}, \epsilon_{out}), \epsilon_1$ and $\emptyset, \emptyset, \epsilon_1 \vdash e_2\ \colon \tau_{in}[\overline{\epsilon_\alpha/\alpha}], \epsilon_{in}[\overline{\epsilon_\alpha/\alpha}]$ and $(G, i', e) \rightarrow (G', j', e')$ where $i' \leq i$. We also know that $\emptyset \vdash \overline{\epsilon_\alpha}$. We have three cases:
\begin{itemize}
	\item Case APP-1: We then know that $(G, i', e_1) \rightarrow (G', j', e_1')$. Hence by induction $\emptyset, \emptyset, j' \vdash e_1'\ \colon \forall \overline \alpha.(\tau_{in}, \epsilon_{in}) \rightarrow (\tau_{out}, \epsilon_{out})$, which can be directly combined with our other premise to prove the conclusion.
	\item Case APP-2. We then know that $e_1$ is a value, and $(G, i', e_2) \rightarrow (G', j', e_2')$. By Theorem V-2 on the first premise, $i \leq \epsilon_1$. Hence $i' \leq \epsilon_1$, so by induction $\emptyset, \emptyset, j' \vdash e_2'\ \colon \tau_{in}[\overline{\epsilon_\alpha/\alpha}], \epsilon_{in}[\overline{\epsilon_\alpha/\alpha}]$. We then again use Theorem V-2 on the first premise to show that $\emptyset, \emptyset, j' \vdash e_1\ \colon \forall \overline \alpha.(\tau_{in}, \epsilon_{in}) \rightarrow (\tau_{out}, \epsilon_{out})$, which may be combined with the above derivation to show our conclusion.
	\item Case APP-3. We know that $G' = G$ is well-typed, and $j' = i'$ and $e_1 = \texttt{fun } [\overline \alpha]\ (x : \tau_{in}', \epsilon_{in}') \rightarrow e_{body}$ and $e_2$ is a value.
	We need to show that
	$$\emptyset, \emptyset, i' \vdash e_{body}[\overline{\epsilon_\alpha/\alpha}][e_2/x]\ \colon \tau_{out}[\overline{\epsilon_\alpha/\alpha}], \epsilon_{out}[\overline{\epsilon_\alpha/\alpha}].$$

	By canonical forms, we know that $\tau_{in} <: \tau_{in}'$ and $\epsilon_{in} \leq \epsilon_{in}'$ and $$\{x := \tau_{in}'\}, \{\overline\alpha\}, \epsilon_{in}' \vdash e_{body}\ \colon \tau_{out}', \epsilon_{out}'$$ where $\tau_{out}' <: \tau_{out}$ and $\epsilon_{out}' \leq \epsilon_{out}$.
	We will first use SUBTYPING to change the above derivation into
	$$\{x := \tau_{in}'\}, \{\overline\alpha\}, \epsilon_{in}' \vdash e_{body}\ \colon \tau_{out}, \epsilon_{out}$$

	and then apply the substitution lemma for effects to show that
	$$\{x := \tau_{in}'[\overline{\epsilon_\alpha/\alpha}]\}, \emptyset, \epsilon_{in}'[\overline{\epsilon_\alpha/\alpha}] \vdash e_{body}[\overline{\epsilon_\alpha/\alpha}]\ \colon \tau_{out}[\overline{\epsilon_\alpha/\alpha}], \epsilon_{out}[\overline{\epsilon_\alpha/\alpha}].$$

	Next, since $e_2$ is a value, we conclude that $e_2 : \tau_{in}[\epsilon_\alpha/\alpha]$ by Theorem V-2, and thus by Lemma SE-3 $e_2 : \tau_{in}'[\overline{\epsilon_\alpha/\alpha}]$. So we may apply the substitution lemma for values to show that
	$$\emptyset, \emptyset, \epsilon_{in}'[\overline{\epsilon_\alpha/\alpha}] \vdash e_{body}[\overline{\epsilon_\alpha/\alpha}][e_2/x]\ \colon \tau_{out}[\overline{\epsilon_\alpha/\alpha}], \epsilon_{out}[\overline{\epsilon_\alpha/\alpha}].$$

	Finally, we need only show that $i' \leq \epsilon_{in}'[\overline{\epsilon_\alpha/\alpha}]$ so that we may apply effect weakening. This follows from two applications of theorem V-2 on our original premises, the fact that $\epsilon_{in} \leq \epsilon_{in}'$, the fact that $i'[\overline{\epsilon_\alpha/\alpha}] = i'$, and lemma SE-2.
\end{itemize}

\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:

max_stars_repo_path: notes/global typing small step.tex

max_stars_repo_name: DanielBentleyMacLeod/lucid

max_issues_repo_path: notes/global typing small step.tex

max_issues_repo_name: DanielBentleyMacLeod/lucid

max_forks_repo_path: notes/global typing small step.tex

max_forks_repo_name: DanielBentleyMacLeod/lucid


text:
In this Section we present some experimental results on the case study presented in Section \ref{sec:case_study}. We want to check if \emph{Property 1} is verified on the program of Figure \ref{lst:casestudy} and, in particular, we want to know which subset of starting values brings to verify it.
We implemented our analysis in the \FSharp\ language with Visual Studio 2012. We ran the analysis on an Intel Core i5 CPU 1.60 GHz with 4 GB of RAM, running Windows 8 and the \FSharp\ runtime 4.0 under .NET 4.0.

We set the initial widths associated to all variables to $100.0$ and the minimum width allowed to $5.0$. As for \emph{Property 1}, we set $T = 5$, i.e., we want to verify if the ball is surely out of the screen within $5$ seconds from its generation. Since $dt=0.05$, a simulation during $5$ seconds corresponds to $5/0.05 = 100$ iterations of the \statement{while} loop. To verify this property, we apply trace partitioning \cite{MR05} to track one abstract state per loop iteration until the 100-th iteration (we do not need to track precise information after the 100th iteration). The position which corresponds to the exiting from the screen is $100.0$: if after $100$ iterations the position \statement{px} is surely greater than $100.0$, then \emph{Property 1} is verified. The whole of these values (starting variables values and widths, minimum width allowed, number of iterations, position to reach) make up our \emph{standard workbench data}. We will experiment to study how efficiency and precision change when modifying some parameters of the analysis.
%, and for each test we will specify only the values which are different with respect to the standard workbench data.
%We will start by running the analysis on the standard workbench data, and then we will experiment by changing one value at a time to study how the efficiency and precision change\footnote{}.

%For example, we will start by showing how precision and performance are affected by changing the minimum width allowed. After that, we will concentrate on the horizontal velocity variable and we will show how we can use our analysis as a form of \textquotedblleft assisted debugging\textquotedblright\ to understand which starting values of a variable bring to verify the property and which not.

For each test, the analysis returns three sets of starting hypercubes: the initial values of the variables which satisfy the property (\textit{yes} set), which surely do not satisfy the property (\textit{no} set), and which may or not satisfy the property (\textit{maybe} set). To make the results more immediate and clearer, we computed for each \emph{yes} and \emph{no} set the corresponding volume covered in the space by their hypercubes. We also consider the \emph{total} volume of the variable space, i.e., the volume covered by all possible values with which the program variables are initialized. In the case of the standard workbench data, the \emph{total} volume is $10.0 \times 50.0 \times 60.0 \times 5.0 = 150000$. Dividing the sum of \emph{yes} and \emph{no} volumes by the \emph{total} volume, we obtain the percentage of the cases for which the analysis gives a definite answer. We will call this percentage the precision of the analysis.

%Note that the \emph{total} volume refers to the initial variable space, i.e., to the space defined by the intervals assigned to the variables at the beginning of the program. The \emph{yes}, \emph{maybe}, and \emph{no} volumes refer to the same space, since they are defined in terms of \emph{starting} hypercubes. These volumes are all finite, since we suppose that all the variables are initialized by a bound interval, and this is always the case in Computer Games Software.

\subsubsection{Varying the minimum width allowed}
First of all, we run the analysis modifying the \emph{minimum width allowed} (MWA) parameter and we reported the results of these tests in Table \ref{table:minWidthAllowed}. We can clearly see the trade-off between performance and precision. %that the performance decreases when we set small widths, and it is instead very good on bigger ones. On the other hand, by decreasing the MWA we also gain more precision.

\vspace{-15pt}
\begin{table}[ht]
\scriptsize
\caption{Varying the minimum width allowed (MWA)}
\centering
\begin{tabular}{| c | c | c | c |}
\hline
MWA & Time (sec.) & \emph{yes+no} volume & Precision \\ \hline
3 & 530 & 131934 & 88\%  \\ %\hline
5 & 77 & 99219 & 66\%  \\ %\hline
12 & 11 & 40625 & 27\%  \\ %\hline
24 & 1 & 25000 & 17\% \\ %\hline
45 & 0.2 & 0 & 0\% \\ \hline
\end{tabular}
\label{table:minWidthAllowed}
\end{table}
\vspace{-30pt}

%\begin{figure}
%\begin{center}
%\includegraphics[scale=0.6]{Pics/varyingMWA.png}
%\caption{Varying the minimum width allowed - Plots}
%\label{fig:minWidthAllowed}
%\end{center}
%\end{figure}

%From these results,  For instance, when MWA = 45 we do not have any certain answer, while with MWA = 3 the certain answers cover the 88\% of the volume space, a quite precise result.

\subsubsection{Finding appropriate starting values}

In Table \ref{table:velocityX} we reported the results of a series of successive tests obtained by changing the horizontal velocity of the ball (\statement{vx}). In particular, we made up a series of tests simulating the behavior of a developer using our analysis to debug his code. Let us suppose that we wrongly inserted a starting interval of negative values (between -120 and 0) for the horizontal velocity. The first test (\# 1) shows us that the program does not work correctly, since the \emph{no} volume is 100\%. Also, to give this answer, the analysis is very quick because a low MWA (45) suffices. After that, we try (test \# 2) with very high positive velocities (between 60 and 120) and we obtain (also very quickly) a 100\% of positive answer: we know for sure that with these velocities the program works correctly. Now it remains to verify what happens with velocities between 0 and 60, and we try this in test \# 3, where we decrease the MWA because we need more precision (the results with greater MWA were presented by the previous Section). Some values of \statement{vx} (i.e., $\geq 31.25$) ensure that the property is verified, some other values (i.e., $\leq 12.5$) ensure that the property is not verified, but the ones in between are uncertain. Tests \# 4 and \# 5 are just double checks.
%To do a double check about this data, we execute also tests \# 4 and \# 5, where we keep, respectively, only the low (between 0 and 15) and the high (between 30 and 60) values: in both cases the analysis is fairly quick in confirming the 100\% \emph{no} and 100\% \emph{yes}.
So we try with a smaller MWA (3) in test \# 6 on the interval $[15..30]$: about a quarter of the starting values produces \emph{yes} and another quarter produces \emph{no}. The \emph{no} derives from low values (smaller than 18) and we confirm this in test \# 7. %, where (with a MWA of 5 and quick execution time) we obtain a 100\% of \emph{no} answers.
As for medium-high values, test \# 6 shows that, with a velocity greater than 25, the answer is \emph{almost} always \emph{yes}. It is not always yes because, with this range of velocities, the values of other variables become important to verify the property. Test \# 8, in fact, shows us that velocities within 25 and 30 produce an 82\% of \emph{yes}, but a 18\% of \emph{maybe} remains. Finally, in test \# 9 we modify also other two variables (with values chosen looking at the results from test \# 6 and \# 8)
%: in particular, we set the horizontal position (\statement{px}) between 5 and 10, and the vertical position (\statement{py}) between 40 and 50.
and, with such values, the answers are 100\% \emph{yes}.

After these tests, the developer of the case study is sure that horizontal velocities below 18 will certainly not make the program work. On the other hand, values greater than 30 certainly make the program work. For values between 25 and 30, other variable values must be changed (\statement{px} and \statement{py}) to make the program work correctly. Making some other tests, we could also explore what happens with values between 18 and 25.

\begin{table}[ht]
\scriptsize
\caption{Varying the horizontal velocity (\statement{vx})}
\centering
\begin{tabular}{| l | c | c | c | l | p{5cm} |}
\hline
Test & \statement{vx} interval & MWA & Time (sec) & Answer & Comment \\ \hline
\# 1 & [-120 .. 0] & 45 & 1 & \emph{no} = 100\% & With negative values the answer is always no. \\ \hline
\# 2 & [60 .. 120] & 45 & 0.2 & \emph{yes} = 100\% & With very high positive values the answer is always yes. \\ \hline
\# 3 & [0 .. 60] & 5 & 77 &
$\begin{array}{l}
\emph{yes} = 45\%\\
\emph{no}  = 21\%
\end{array}$ & Uncertainty. High values ($\geq$ 31.25) imply \emph{yes}, low values ($\leq$ 12.5) imply \emph{no}. \\ \hline
\# 4 & [0 .. 15] & 24 & 0.5 & \emph{no} = 100\% & Double check on low values: answer always no. \\ \hline
\# 5 & [30 .. 60] & 5 & 30 & \emph{yes} = 100\% & Double check on medium-high values: answer always yes. \\ \hline
\# 6 & [15 .. 30] & 3 & 526 &
$\begin{array}{l}
\emph{yes} = 27\%\\
\emph{no} = 25\%
\end{array}$ & Uncertainty. Low values ($\leq$ 18) imply \emph{no}, for high values ($\geq$ 25) depends also on other variables. \\ \hline
\# 7 & [15 .. 18] & 5 & 7 & \emph{no} = 100\% & Double check on medium-low values: answer always no. \\ \hline
\# 8 & [25 .. 30] & 3 & 164 &
$\begin{array}{l}
\emph{yes} = 82\%\\
\emph{maybe} = 18\%
\end{array}$ & Double check on medium-high values: answer almost always yes. In this case, also values of other variables influence the result. \\ \hline
\# 9 & [25 .. 30] & 5 & 1 & \emph{yes} = 100\% & Modified also py ([40 .. 50]) and px ([5 .. 10]). Answer always yes. \\ \hline
\end{tabular}
\label{table:velocityX}
\end{table}
\vspace{-10pt}

\subsubsection{Discussion}
In this scenario, we ran the analysis by manually changing the initial values of program variables. Notice that this process could be automatized.
%In particular, instead of providing a program that initializes all the variables, and checking if a given property holds, a user could give only the \statement{while} loop that performs the physics simulation, and then try wide ranges of initial values for the variables. This will obviously lead to an analysis that, even with large widths, could quickly give definite answers for a wide part of the given starting intervals.
This process can be highly interactive, since the tool could show to the user even partial results while it is automatically improving the precision by adopting narrower intervals on the \emph{maybe} portion as described by Algorithm \ref{alg:widthAdjusting}. In this way, the user could iterate the process until it finds suitable initial values.

The execution times obtained so far underline that the analysis is efficient enough to be the basis of practical tools. Moreover, the analysis could be parallelized by running in parallel the computation of the semantics for each initial hypercube: exploiting several cores or even running the analysis in the cloud, we could further improve the efficiency of the overall analysis.
%. In this way, when we choose a narrow width, we could exploit several cores or even run the analysis in the cloud, thus improving the efficiency of the overall analysis.

ext: tex

max_stars_repo_name: vs-team/Papers

max_issues_repo_name: vs-team/Papers

max_forks_repo_name: vs-team/Papers


text:
\documentclass{article}

\usepackage{graphicx}
\usepackage{verbatim}

\begin{document}

\section{Parallellizing the thickness algorithm}

\noindent 1) Explain Thickness of Knot

\noindent 2) Explain Thickness Algo

Now we would like to compute the thickness in parallel using
more than a single CPU. This is natural since the bisections
are done on a per arc pair basis. Once we have a set of candidate
arc pairs the only remaining thing to do is computing the minimal
distance on arcs containing a double critical point. The smallest
of these values is the thickness of the knot.

Every child process gets a few candidate
arc pairs and computes the minimal distance on double critical
arcs, if it exists. The master handles in a client server way
the communication with the child processes by sending new arc
pairs and the currently best thickness value. If a child reports
to be done with its work it sends back the distance found. If the
computed distance is either larger than the one received from
the master or there are no double critical points found, then the
distance value send back to the master is simply a large number.

In what follows we'll discuss the tasks for master and child processes,
present the details of the complete algorithm, go into implementation
issues and present some benchmark results. The last part points out
possible improvements.

\subsection{Client/server, master/children}

The master or root process initializes the knot and computes a first
set of candidate arc pairs. Now it has to send one or more pairs to
every available child, which will compute the shortest distance on the
pairs. Once every child has gotten its first workload, the master cycles through
them and waits for children done with their task. The child reports back
the computed distance and the master immediatly sends the next arc pair (or more
than one) to constantly keep the children busy. Every time the master
receives a distance value from a child, it updates the thickness
and sends this value in future jobs. As soon as all the arc pairs are processed,
the master notifies the child processes that their work is done and
ends.

\begin{comment}
\begin{figure}[p]
\includegraphics[width=\textwidth]{parallel_algo_flowchart.pdf}
\caption{XXX Explain chart! \label{fig:parallel_algo_flowchart} }
\end{figure}
\end{comment}

\subsection{MPI: A Message-Passing Interface Standard}

The MPI API specification is a standart for MIMD parallel computing
that defines how different processes with separate memory spaces
communicate to fullfill a computation or program execution. The
communication is done with a message passing protocol between the
various processes running in parallel. The communication between
processes can be point-to-point (blocking) or asynchronous (non-blocking).
A point-to-point communication is considered to be finished when
the sender and receiver exchanged the data. For the non-blocking
case the sender does not wait until the data has been received
by its communication partner.

Different computer and cluster manifacturers have different
implementations of the MPI interface tailored to their hardware.
A relatively widespread implementation is MPICH, which has
as well been used as a bases for MPI implementations.
LAM or openMPI are other implementations of this interface standard.

We will not present the entire list of MPI functions. As an example
we start with a minimal program.

\begin{verbatim}
#include <stdio.h>
#include <mpi.h>

int main (int argc, char *argv[]) {
  int rank, size,

  MPI_Init(&argc, &argv);

  MPI_Comm_rank(MPI_COMM_WORLD, &rank);
  MPI_Comm_size(MPI_COMM_WORLD, &size);

  printf("Process %d of %d\n", rank, size );

  MPI_Finalize();

  return 0;
}
\end{verbatim}

In the program listing we use \verb+MPI_Init+ to intialize
the MPI environment and \verb+MPI_Finalize+ to end the
execution. The function \verb+MPI_Comm_rank+ asks what
processor number this process has and
\verb+MPI_Comm_size+ requests information about how many
CPUs are available.

Running MPI programs in a parallel environment such as
a computing cluster depend on the different implementations.
A sample invocation using $4$ CPUs would be the following

\begin{verbatim}
mpirun -machinefile machines -np 4 program
\end{verbatim}

where the file \verb+machines+ contains information about
the cluster like node hostnames and number of processors per
host.

Two other routines are worth mentioning since they are
the basis of every parallel program for sending and
receiving messages.

\begin{verbatim}
int MPI_Send( void *buf, int count, MPI_Datatype datatype, int dest,
              int tag, MPI_Comm comm )
int MPI_Recv( void *buf, int count, MPI_Datatype datatype, int source,
              int tag, MPI_Comm comm, MPI_Status *status )
\end{verbatim}

The various arguments are \verb+buf+, a pointer to the data to be
sent or received - \verb+count+, the size of the data of type
\verb+datatype+. The integers \verb+dest+ and \verb+source+ define
the rank of the partner process, \verb+tag+ is a message identification
and \verb+MPI_Comm+ is a communication handle. A common handle is
\verb+MPI_COMM_WORLD+ which includes all the available processes.
It is possible to define other communicators depending on the
network and computation topology implemented in the program.

Collective communication is possible as well. A broadcast sends
a message to all the processes, scatter and reduce sends one task
to all the processes in a group or reduces values on all processes to a
single value on one process.

\subsection{Custom datatypes}

The MPI standard defines a series of datatypes like \verb+MPI_INT+ or
\verb+MPI_DOUBLE+. In this algorithm we have to send information concerning
the candidate arc pairs to the computing children. Every message passed from one
process to another must have a specified datatype. We want to send a message
containing enough information for the child processes to be able to compute the
minimal distance. That's why a new MPI datatype was necessary. It is possible
to define an entire structure as a new MPI datatype, which in our case would be
the \verb+Candi<Vector>+ class. However, the size of this structure is $248$ bytes,
which would cause considerable communication overhead. In order to compute the
minimal distance we only need the bezier points ($9+9$ double) for the arc pair,
error information ($2+2$ double) associated with each arc and the currently best
minimal distance ($1$ double) for the subdivision process. This is a total of $23$
doubles adding up to $184$ bytes, which is better than sending the whole struct.
We add one more double used as signal. Implementing signals floating point values
is usually a bad idea due to rounding errors, but here we set this value larger
than $0$ if we want the receiving process to compute the distance and smaller than
$0$ if we want to inform the process that it can exit. An alternative could be a
MPI mixed data type, where we would use a single bit as a signal and the $23$ doubles.
The implementation is easier with only doubles and with a single bit alignement
problems could occur due to fixed buffer lengths in the sending and receiving process.

The new datatype is therefore an array of $24$ doubles, initialized at the beginning
of the MPI program with

\begin{verbatim}
MPI_Datatype MPI_Candi;
MPI_Type_contiguous(24, MPI_DOUBLE, &MPI_Candi);
MPI_Type_commit(&MPI_Candi);
\end{verbatim}

This datatype can then be used just like \verb+MPI_INT+ or \verb+MPI_DOUBLE+.
The next thing to do is prepare the data to be sent to the child processes.
For that purpose we have the two following two routines

\begin{verbatim}
void pack_candidate(const Candi<Vector3> &c, const double curr_min, double res[24]);
void unpack_candidate(const double res[24], Candi<Vector3>* c, double *curr_min);
\end{verbatim}

The function \verb+pack_candidate+ fills an array of doubles with the information
needed from \verb+Candi<Vector3>+ and \verb+unpack_candidate+ initializes the
\verb+Candi<Vector3>+ from \verb+res+. Since the master process has a list
of candidates to process, it packs the data in an array of doubles and sends it to
the child process, which then unpacks it into a \verb+Candi<Vector3>+ object.
The minimal distance gets computed and only this double value is sent back to
the master.

\subsection{Batching candidates}

Subdivision on one arc pair can finish very quickly depending on how close
we alredy are to the final thickness value. The consequence is that the child
processes will ask for new candidate pairs and the master might become a bottleneck
if he's only busy sending out new candidates to the children. To reduce this
communication overhead we can play with the number of arc pairs we send at once.
This is called batching and needs more memory to store all the arc pairs, but then
the children simply process the whole list and only when finished, they ask for
new pairs. This is implemented like

\begin{verbatim}
MPI_Send(serial, BATCH, MPI_Candi, i, TAG, MPI_COMM_WORLD);
MPI_Recv(serial, BATCH, MPI_Candi, 0, TAG, MPI_COMM_WORLD, &stat);
\end{verbatim}

where \verb+serial+ is the send/receive buffer, \verb+BATCH+ the number of arc
pairs, $i=1,\ldots, \#CPUs-1$ is the child process rank ($0$ for the master). Whether
batching speeds up the computation depends on various parameters like the number
of arc pairs, the knot shape, local curvature active, etc.

\subsection{Code snippets showing the algo implementation}

\subsection{Discussion}

% time vs cpus
In what follows we use an approximately ideal trefoil to test the program. Everything
has been computed on an Intel "Woodcrest" cluster with one master and $14$ bi-dual nodes.
Figure \ref{fig:time_vs_cpus} shows the time needed to compute the thickness in function
of the number of CPUs. Up to $10$ CPUs, the speed improvement can seams reasonnable. For more
than $10$ CPUs the gain flattens out and is no longer useful. The master can no longer
serve the children at full speed, since there are too many, and slows down the whole computation.

% time vs nodes
The next experiment is shown in Figure \ref{fig:time_vs_nodes}, where we vary the number of
knot data points, keeping the number of CPUs at $8$ for all the runs. Compare this to the
standard thickness computation on a single CPU. We can see a more or less linear behaviour with
a slope visibly smaller for the multi CPU case. Parallelization becomes interesting if we
have to compute with extremely refined knot shapes as it is the case at the so called end-game.

% time vs batch size
Earlier we discussed that the master could send more than a single candidate pair to the
child processes. Figure \ref{fig:time_vs_batch} plots the time versus the number of arc
pairs we send in a row. The knot shape has $512$ data points and we vary the batch size
between $1$ and $100$. The computation gets faster the more candidates we send at once.
The resulting communication overhead seems negligeable compared to the speed we win by giving a
lot of work to the child processes. A batch size larger than $100$ slows the computations
down, here is where the communication overhead starts to interfer. The master's minimal distance
value allows us to discard a lot of candidates early on, but this is no longer the case if
we send batches to each child process.

% time vs various knots
Another delicate point is the actual shape. Different shapes might lead to completely different
timings depending on how close various parts are to the final thickness. If a knot has several
"good" regions it will take much longer to converge on a single processor. All the subdivisions
have to be carried out until the relative tolerance is reached and only then can the master
compare the various values and compute the smallest one. sequentially, then . The computations
in Figure \ref{fig:time_vs_knots} show that the speed-up can be significantly different from
one knot shape to another. For the knots where the time of a single CPU comes very close to the $8$
processor run could be explained by this worst case scenario : In parallel we compute $7$ arc pairs
and the master receives $7$ distance answers, where the smallest is used for the next $7$ arc pairs.
If we would follow these $7$ candidates in the single CPU case it might happen, that the first
pair is already the smallest out of the $7$ and the next $6$ are rejected since they can not yield
a lower value. If this is true for almost every block of $7$ pairs, then the times for the single
and multi processor runs have to be close.

\begin{comment}
\begin{figure}
\includegraphics[width=\textwidth]{time_vs_cpus.pdf}
\caption{XXX Explain \label{fig:time_vs_cpus}}
\end{figure}

\begin{figure}
\includegraphics[width=\textwidth]{time_vs_nodes.pdf}
\caption{XXX Explain \label{fig:time_vs_nodes}}
\end{figure}

\begin{figure}
\includegraphics[width=\textwidth]{time_vs_knots.pdf}
\caption{XXX Explain \label{fig:time_vs_knots}}
\end{figure}

\begin{figure}
\includegraphics[width=\textwidth]{time_vs_batch.pdf}
\caption{XXX Explain \label{fig:time_vs_batch}}
\end{figure}
\end{comment}

\subsection{Timing master/slaves}

%We now adress the time for the master and the slaves.
%XXX Continue, make plots, for trefoil and 3.1 (3.1 master is 50% of total time)

A different analysis, compared to the various parameters discussed above, is
the time the master needs to do the initial setup and preliminary computations.
Table \ref{tab:master_slave_timing} summarizes this for the first knot of every knots
with a number of crossings up to $9$. The knot $j3.1$ has been computed by \cite{XXX}
and is a very good approximation for an ideal trefoil knot. These times indicate,
that the master spends a lot of time at the beginning. For the $k3.1$ the master
needs the same time as the children, for the $k5.1$ the children do basically
nothing compared to the master. On the other side there is the $j3.1$, where
the initialization step takes only a fraction of the afterwards following
computation by the child processes. A more in depth analysis has shown that
the masters spends most of the time to set up the inital candidate arc pairs.
Note that the batch size has been set to $1$ for these computations.

\begin{comment}
\begin{figure}
\begin{center}
\begin{tabular}{lclll}
knot & data points & master (sec) & children (sec) & total (sec) \\
j3.1 & 512 & 0.165336 & 2.092650 & 2.258000 \\
k3.1 & 160 & 0.016368 & 0.016206 & 0.032578 \\
k4.1 & 208 & 0.024819 & 0.018046 & 0.042868 \\
k5.1 & 232 & 0.031302 & 0.000165 & 0.031471 \\
k6.1 & 280 & 0.042829 & 0.000162 & 0.042995 \\
k7.1 & 304 & 0.052276 & 0.013455 & 0.065735 \\
k8.1 & 352 & 0.067262 & 0.012944 & 0.080209 \\
k9.1 & 376 & 0.067325 & 0.000118 & 0.067447
\end{tabular}
\end{center}
\caption{XXX caption \label{tab:master_slave_timing} }
\end{figure}
\end{comment}

\subsection{Possible improvements}

The above analysis of the various parts and parameters of the algorithm
points out a few weak points and ideas for optimizations. The master might
have a lot to do with interprocess communication if the children finish
rapidly their computations, however if this is not the case, then the
master is idel, waiting for child processes to send back their values,
when it could compute as well some candidate pairs. If we make the master
compute as well, then some of the children might have to wait until the
master answers again the phone, waisting precious time. This issue could
be surmounted by implementing an interrupt system, where the children
stop the master in its computation, send the value and receive new pairs.
XXX However we do not know if MPI supports this type of communication.
The master's minimal distance value is important to quickly discard
pairs if they can not achieve better. Keeping the children up to date
by sending them a new distance value whenever the master receives a
better thickness (for example by broadcasting) would deal with that problem.
Table \ref{tab:master_slave_timing} pointed out that the master
spends a lot of time in the initialization step, mainly by setting up the
arc pairs and the first double critical filter. Delegating part of this
first filtering to the children would reduce the master's work. Considering
the underlying implementation the initial filtering is based on, this
would require quite a few changes.

\end{document}

max_stars_repo_name: mcarlen/libbiarc

max_issues_repo_name: mcarlen/libbiarc

max_forks_repo_name: mcarlen/libbiarc