
\section{Local Unboxing and Aliasing}


% -------------------------------------------------------------------------------------------------
\label{Aliasing}
It is well known that purely functional programs support more optimising rewrites than their impure counterparts. The great enablers are the let-floating transforms \cite{peyton-jones:let-floating} that allow us to shift definitions into their use sites in order to expose opportunities for further transformation. In the absence of side effects we can arbitrarily change the order of evaluation of a program without changing its meaning. 

The fact that a program uses computational effects does not rule out performing similar optimisations, provided we know which subexpressions have the potential to interfere with others. An important part of this is to be able to reason about the aliasing properties of data.

For example, suppose we are compiling the following function:

\code{	
	\mc{3}{\Lambda r_1~ r_2.~ \Lambda (w_2 : \iMutable~ r_2).~ \lambda (x : \iInt~ r_1).~ \lambda (y : \iInt~ r_2).} \\
	\mc{3}{\kletregion~ r_3~ \kwith~ w_3 = \iMkConst~ r_3~ \kin} \\
	\klet	& (z : \iInt~ r_3)	& = \iadd~ r_1~ r_3~ r_3~ x~ (1~ r_3) \\
		& \_			& = \iupdateInt~ r_2~ r_3~ w_2~ y~ (0~ r_3) \\
	\kin	& \mc{2}{\iadd~ r_1~ r_3~ r_1~ x~ z}
}

Where $\iadd$ and $\iupdateInt$ have the following types:

\code{	
	\iadd	& :: &
		\forall r_1~ r_2~ r_3.~
		\iInt~ r_1 \to \iInt~ r_2 \longtoa{\iRead~ r_1 \lor \iRead~ r_2} \iInt~ r_3
\\
	\iupdateInt 
		& :: & 
		\forall r_1 r_2.~ 
		Mutable~ r_1 
		\To~ Int~ r_1 
		\to~ Int~ r_2 
		\longtoa{Read~ r_2 ~\lor~ Write~ r_1} ()			
}

The above function adds one to its first argument, updates its second, then adds its first argument to the previous result. Now, suppose that we wish to optimise this function by performing the local unboxing transform \cite{leroy:unboxing}. This should allow us to keep the intermediate values in registers, reducing the number of objects we need to store in the heap. We write the type of unboxed integers as $\iInt_\#$, unboxed integer literals like $23_\#$, and use the following primitives:

\code{	
	\ibox		& :: & \forall r_1.~ \iInt_\# 	\to \iInt~ r_1 \\
	\iunbox		& :: & \forall r_1.~ \iInt~ r_1 \longtoa{\iRead~ r_1} \iInt_\#  \\[0.5ex]
	\iadd_\#	& :: & \iInt_\# \to \iInt_\# \to \iInt_\#
}

By design, these primitives do not support the destructive update of unboxed integers. This effectively places the program in SSA form. It also means that $\iInt_\#$ does not need to be annotated with a region variable, as reading values of this type does not cause an effect. Using these primitives we can rewrite our original function as follows --- taking the liberty of passing the unboxed constant $1_\#$ directly to $\iadd$, converting to A-normal form, and annotating each binding with the effect it causes.

\code{	
	\mc{4}{\Lambda r_1~ r_2.~ \Lambda (w_2 : \iMutable~ r_2).~ \lambda (x : \iInt~ r_1).~ \lambda (y : \iInt~ r_2).} \\
	\mc{4}{\kletregion~ r_3~ \kwith~ w_3 = \iMkConst~ r_3~ \kin} \\
	\klet	& (x_1	& \hspace{-1em}: \iInt_\#)
				& = \iunbox~ r_1~ x 
				& \iRead~ r_1
		\\
		& (z_1	& \hspace{-1em}: \iInt_\#)	
				& = \iadd_\#~ x_1~ 1_\# 		
				& \bot 
		\\
		& (z	& \hspace{-1em}: \iInt~ r_3)	
				& = \ibox~ r_3~ z_1 			
				& \bot 
		\\
		& \_	& 	& = \iupdateInt~ r_2~ r_3~ w_2~ y~ (0~ r_3) 
				& \iRead~ r_3 \lor \iWrite~ r_2
		\\
		& (x_2	& \hspace{-1em}: \iInt_\#)
				& = \iunbox~ r_1~ x
				& \iRead~ r_1
		\\
		& (z_2	& \hspace{-1em}: \iInt_\#)
				& = \iunbox~ r_3~ z
				& \iRead~ r_3
		\\
		& (res	& \hspace{-1em}: \iInt_\#)
				& = \iadd_\#~ x_2~ z_2
				& \bot
		\\
	\kin	& \mc{3}{\ibox~ r_1~ res}
				& \bot
}
As the bindings for $z_1$, $z$, and $res$ are manifestly pure, we can float them directly into their use sites. This is also possible for the $z_2$ binding, as $\iRead~ r_3$ is pure because $r_3$ is constant. Doing this exposes an opportunity to use the identity $\forall x~ r.~ \iunbox~ r~ (\ibox~ r~ x) \equiv x$

\code{	
	\mc{4}{\Lambda r_1~ r_2.~ \Lambda (w_2 : \iMutable~ r_2).~ \lambda (x : \iInt~ r_1).~ \lambda (y : \iInt~ r_2).} \\
	\mc{4}{\kletregion~ r_3~ \kwith~ w_3 = \iMkConst~ r_3~ \kin} \\
	\klet	& (x_1	& \hspace{-1em}: \iInt_\#)
				& = \iunbox~ r_1~ x 
				& \iRead~ r_1
		\\
		& \_	& 	& = \iupdateInt~ r_2~ r_3~ w_2~ y~ (0~ r_3) 
				& \iRead~ r_3 \lor \iWrite~ r_2
		\\
		& (x_2	& \hspace{-1em}: \iInt_\#)
				& = \iunbox~ r_1~ x
				& \iRead~ r_1
		\\
	\kin	& \mc{3}{\ibox~ r_1~ (\iadd_\#~ x_2~ (\iunbox~ r_3~ (\ibox~ r_3~ (\iadd_\#~ x_1~ 1_\#))))}
				& \bot
}

Now, although there is still an obvious optimisation opportunity left in this code, we must be mindful of potentially interfering effects. The bindings for $x_1$ and $x_2$ appear to do the same thing, but note the intermediate update of $y$. If $x$ and $y$ were bound to the same heap object, meaning that they were aliases, then the second call to $\iunbox$ would always return zero. On the other hand, if we could guarantee that $x$ and $y$ were \emph{not} aliases, then we could simply set $x_2 = x_1$ and save the second unboxing.

We will consider two ways to achieve this: the first using the witnesses of constancy we have already discussed, and the second using witnesses of distinctness which we will cover in the next section. For the first way, we specialise the function for the case where $r_1$ is constant, by requiring a witness of of constancy:

\code{	
	\mc{5}{\Lambda r_1~ r_2.~ 
		\Lambda (w_1 : \iConst~ r_1).~ 
		\Lambda (w_2 : \iMutable~ r_2).~ 
		\lambda (x : \iInt~ r_1).~ \lambda (y : \iInt~ r_2).} \\
	\mc{4}{\kletregion~ r_3~ \kwith~ w_3 = \iMkConst~ r_3~ \kin} \\
	\klet	& (x_1	& \hspace{-1em}: \iInt_\#)
				& = \iunbox~ r_1~ x 
				& \iRead~ r_1
		\\
		& \_	& 	& = \iupdateInt~ r_2~ r_3~ w_2~ y~ (0~ r_3) 
				& \iRead~ r_3 \lor \iWrite~ r_2
		\\
	\kin	& \mc{3}{\ibox~ r_1~ (\iadd_\#~ x_1~ (\iunbox~ r_3~ (\ibox~ r_3~ (\iadd_\#~ x_1~ 1_\#))))}
				& \bot
}

Note that by requiring $r_1$ to be constant, we have also ensured that $x$ and $y$ cannot be aliases. Or rather, we have ensured that the function cannot be called if $x$ and $y$ are aliases. As discussed in \S\ref{Witnesses-of-Constancy-and-Mutability} our type system ensures that witness of constancy and mutability for the same region cannot be created. If the caller provides a witness of constancy for $r_1$, then if $x$ and $y$ are the same object then there is no way it can also provide a witness of mutability for $r_2$.

One potential disadvantage of this approach is that the witness variable $w_1$ does not occur in the body of the abstraction that binds it. Here, we are using the witness to create a context where a particular transformation is valid, instead of simply passing it to a primitive function like $\iupdate$ or $\isuspend$. During further optimisation we must be mindful not to erase the binders for such witnesses, else the function may be called with arguments that do not meet the properties we assumed when specialising it.


% -------------------------------------------------------------------------------------------------
\clearpage{}
\subsection{Observational Equivalence of Swap}
\begin{flushleft}

We want to prove the following equivalence:
\[	\begin{array}{lcl}
	\klet~ x_1 : \tau_1 = t_1~ \kin &  			& \klet~ x_2 : \tau_2 = t_2~ \kin \\
	\klet~ x_2 : \tau_2 = t_2~ \kin &     ~~\equalsobs~~	& \klet~ x_1 : \tau_1 = t_1~ \kin \\
	t_3				&			& t_3
	\end{array}
\]

Desugaring the above gives:
\[	\begin{array}{rcl}
	  (\lambda (x_1 : \tau_1).~ (\lambda (x_2 : \tau_2).~ t_3)~ t_2)~ t_1
	& ~~\equalsobs~~
	& (\lambda (x_2 : \tau_2).~ (\lambda (x_1 : \tau_1).~ t_3)~ t_1)~ t_2
	\end{array}
\]

Note that this equivalence is symmetric, meaning the reduction of the first implies the reduction of the second, so we only have to prove equivalence in one direction.



% -----------------------------------------------------------------------------
\theorem{Obs. Equiv. of Swap}
\medskip


\statement{
	If~	& $(\un{1})~~ 
			\tyJudgeGS
			{(\lambda (x_1 : \tau_1).~ (\lambda (x_2 : \tau_2).~ t_3)~ t_2)~ t_1}
			{\tau}
			{\sigma}$
\\
	~~and~~	& $(\un{2})~~
			\eiJudge
			{H}	{(\lambda (x_1 : \tau_1).~ (\lambda (x_2 : \tau_2).~ t_3)~ t_2)~ t_1}
			{H'}	{v_3^\circ}
			{B}$
\\
	~~and~~	& $(\un{3})~~ \Sigma \models H$ ~~and~~ $(\un{4})~ \Sigma \vdash H$
\\
	~~and~~	& $(\un{5})~~ x_1 \notin \ifv(t_2)$
\\
	~~and~~	& $(\un{6})~~ \tyJudgeGS{t_1}{\tau_1}{\sigma_1}$
\\
	~~and~~	& $(\un{7})~~ \tyJudgeGS{t_2}{\tau_2}{\sigma_2}$
\\
	~~and~~	& $(\un{8})~~ \rNonInterfering(\Gamma,~ \sigma_1,~ \sigma_2)$
\\
	then	& $\quad ~~~
	 		\tyJudgeGS
			{(\lambda (x_2 : \tau_2).~ (\lambda (x_1 : \tau_1).~ t_3)~ t_1)~ t_2}
			{\tau}
			{\sigma}$
\\
	~~and~~	& $\quad ~~~ 
			\eiJudge
			{H}	{(\lambda (x_1 : \tau_1).~ (\lambda (x_2 : \tau_2).~ t_3)~ t_1)~ t_2}
			{H'}	{v_3^\circ}
			{B}$
}

Start by assuming the antecedent and then applying the usual inversion lemmas to build the proof tree for the evaluation. 


\[	\hspace{19.7em}\vspace{-1em}
	\infer
	{ (16)~~
		\eiJudge
		{H_2}	{t_3[v_1^\circ/x_1][v_2^\circ/x_2]}
		{H_3}	{v_3^\circ}
		{B_3}
		}
	{ \fbox{T3}
	}
\]
\[	\hspace{1.5em}\vspace{-1em}
	\infer[\trm{(Subst.)}]
	{ (11)~~
		\eiJudge
		{H_1}	{((\teLam{x_2}{\tau_2}{t_3})~ t_2)[v_1^\circ/x_1]}
		{H_3}	{v_3^\circ}
		{B_2 \cup B_3}
	}
	{ 	\infer[\pby{EiApp}]
		{ (12)~~
			\eiJudge
			{H_1}	{\un{(\teLam{x_2}{\tau_2}{t_3[v_1^\circ/x_1]})}_{~ (t_4)}~~ 
					t_2[v_1^\circ/x_1]}
			{H_3}	{v_3^\circ}
			{B_2 \cup B_3}
		}
		{ 	\infer
			{ (13)~~
				\eiJudge
				{H_1}	{t_4}
				{H_1}	{t_4}
				{\emptyset}
			}
			{ \trm{(EiVal)}}
		\quad
			\infer[\trm{by}~ (5)]
			{ (14)~~
				\eiJudge
				{H_1}	{t_2[v_1^\circ/x]}
				{H_2}	{v_2^\circ}
				{B_2}
			}
			{ 	\infer
				{ (15)~~
					\eiJudge
					{H_1}	{t_2}
					{H_2}	{v_2^\circ}
					{B_2}
				}
				{ \fbox{T2}}
			}
		\quad
			~~\stackrel{\vdots}{\stackrel{\vdots}{\vdots}} ~~~~~~~~~~~~~~~~~~~
		}
	}
\]
\[	\hspace{-5.5em}
	\infer[\pby{EiApp}]
	{ (\un{2})~
	  \eiJudge
		{H}	{\un{(\lambda (x_1 : \tau_1).~ (\lambda (x_2 : \tau_2).~ t_3)~ t_1)~ t_2}_{~(t_0)}}
		{H'}	{v_3^\circ}
		{B_1 \cup B_2 \cup B_3}}
	{ 	\infer 
		{ (9)~~ \eiJudge
			{H_0}	{t_0}
			{H_0}	{t_0}
			{\emptyset}
		}
		{ \trm{(EiVal)} }
	 \quad
		\infer
		{ (10)~~ \eiJudge
			{H_0}	{t_1}
			{H_1}	{v_1^\circ}
			{B_1}
		}
		{ \fbox{\trm{T1}} }
	\quad
		~\stackrel{\vdots}{\stackrel{\vdots}{\vdots}}~
	}
\]


\clearpage{}

\TODO{commentary} restate (10) and (15).

\tabbedstmts{
(10)		\> $\eiJudge
			{H_0}	{t_1}
			{H_1}	{v_1^\circ}
			{B_1}$
		\> ~~~~(Restate)
\\
(15)		\> $\eiJudge
			{H_1}	{t_2}
			{H_2}	{v_2^\circ}
			{B_2}$
		\> ~~~~(Restate)
}
\TODO{commentary} so our new goals become as follows:

\begin{tabular}{l}
	$\tbf{(G1)}~~ \eiJudge {H_0} {t_2} {H_2'}{v_2^\circ}{B_2}$
\\	$\tbf{(G2)}~~ \eiJudge {H_2'}{t_1} {H_2} {v_1^\circ}{B_1}$
	~~for some $H_2'$
\end{tabular}


% -----------------------------------------------------------------------------
\medskip
To separate the effect of each reduction on the resulting heaps, we rewrite (10) and (15) in terms of residues.

\tabbedstmts{
(19)		\> $H_1 \equiv H_0 \succ \Residue(H_0,H_1)$ for some $\Residue(H_0,H_1)$
		\> ~~~~ (Heap Factoring 10)
\\[1ex]
(20)		\> $H_2 \equiv H_1 \succ \Residue(H_1,H_2)$ for some $\Residue(H_1,H_2)$
		\> ~~~~ (Heap Factoring 15)
\\
(21)		\> $H_2 \equiv H_0 \succ \Residue(H_0,H_1) \succ \Residue(H_1,H_2)$
		\> ~~~~ (19 20)
\\[1ex]
(22)		\> \qq\qq~~~~
		   $\eiJudge
			{H_0}
			{t_1}
			{H_0 \succ \Residue(H_0,H_1)}
			{v_1^\circ}
			{B_1}$
		\> ~~~~ (10 19)
\\[1ex]
(23)		\> $\eiJudge
			{H_0 \succ \Residue(H_0,H_1)}
			{t_2}
			{H_1 \succ \Residue(H_1,H_2)}
			{v_2^\circ}
			{B_2}$
		\> ~~~~ (15 20)
\\
(24)		\> $\eiJudge
			{H_0 \succ \Residue(H_0,H_1)}
			{t_2}
			{H_0 \succ \Residue(H_0,H_1) \succ \Residue(H_1,H_2)}
			{v_2^\circ}
			{B_2}$
		\> ~~~~ (19 23)
}

Now, to get (G1) we need to prove that we can reduce $t_2$ in the initial heap $H_0$ to yield $v_2^\circ ~;~ H_2'$, where $H_0$ is perhaps smaller than the $H_1$ from (10). Conversely, to get (G2) we need to prove that we can reduce $t_1$ in $H_2'$ to yield the original result $H_2 ~;~ v_1^\circ$, where $H_2'$ is perhaps larger than the $H_0$ from (15).

\smallskip
For the first of these, note that by \TODO{lemma}, $t_2$ does not touch any of the elements in $R(H_0,H_1)$, so we have:

\tabbedstmts{
(25)		\> $\neg \trm{Uses}(B_2,~ \Residue(H_0,H_1))$
		\> ~~~~ (NoUsing ...)
\\
		\> \TODO{Try to use commutable actions for above not all the info is in CA stmt used below}
\\
(26)		\> \qq\qq~~~~
		   $\eiJudge
			{H_0}
			{t_2}
			{H_0 \succ \Residue(H_1,H_2)}
			{v_2^\circ}
			{B_2}$
		\> ~~~~ (EvalCut 24 25)
}

This gives us (G1), where $H_2' = H_0 \succ \Residue(H_1,H_2)$. Now, provided the reduction of $t_1$ does not touch any of the elements in $\Residue(H_1,H_2)$, then we can weaken the initial heap in (22) to match $H_2'$

\tabbedstmts{
(26)		\> $\eiJudge
			{H_0 \succ \Residue(H_1,H_2)}
			{t_1}
			{H_0 \succ \Residue(H_1,H_2) \succ \Residue(H_0,H_1)}
			{v_1^\circ}
			{B_1}$
		\> ~~~~ (Weak. Heap. 22)
}

Finally, as the effects of the two reductions are NonInterfering (5), the residues $R(H_1,H_2)$ and $R(H_0,H_1)$ are commutable, so we can swap the updates in (26) to yield (G2). 

\tabbedstmts{
(27)		\> $\trm{CommutableActions}(B_1,~ B_2)$
		\> \hspace{-2.2em} (Comm. Actions ... )
\\
(28)		\> $\trm{CommutableResidues}(\Residue(H_1,H_2),~ \Residue(H_0,H_1))$
		\> \hspace{-2.2em} (Comm. Residues. 22 23 27)
\\
(27)		\> $\eiJudge
			{H_0 \succ \Residue(H_1,H_2)}
			{t_1}
			{H_0 \succ \Residue(H_1,H_2) \succ \Residue(H_0,H_1)}
			{v_1^\circ}
			{B_1}$
		\> ~~~~ (Comute. Upd. 26 28)
}

$\Box$
\end{flushleft}





