Index: /Deliverables/addenda/indexed_labels/report.tex
===================================================================
 /Deliverables/addenda/indexed_labels/report.tex (revision 1673)
+++ /Deliverables/addenda/indexed_labels/report.tex (revision 1674)
@@ 168,5 +168,5 @@
\newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}}
%horizontal thiner line for figures
\newenvironment{figureplr}{\begin{figure}[t] \Figbar}{\Figbar \end{figure}}
+\newenvironment{figureplr}[1][t]{\begin{figure}[#1] \Figbar}{\Figbar \end{figure}}
%environment for figures
% ************Macros for mathematical symbols*************
@@ 572,4 +572,6 @@
\newcommand{\gramm}{\mathrel{::=}}
\newcommand{\ass}{\mathrel{:=}}
+
+\renewcommand{\to}[1][]{\stackrel{#1}{\rightarrow}}
%<<<<<<<<<<<<
\begin{document}
@@ 641,5 +643,5 @@
label. The second, optional but desirable, is \emph{preciseness}: the estimate
is not in fact an estimate but the actual cost. In the labelling approach, this will
true if for every label every possible execution of the compiled code starting
+be true if for every label every possible execution of the compiled code starting
from such a label yields the same cost. In simple architectures such as the 8051
microcontroller this can be guaranteed by having labels at the immediate start of any
@@ 754,14 +756,8 @@
The version of the minimal imperative language \imp that we will present has,
with respect to the barebone usual version, \s{goto}s and labelled statements.
+with respect to the barebone usual version, \s{goto}s and labelled statements.
Break and continue statements can be added at no particular expense. Its syntax
and operational semantics is presented in \autoref{fig:minimp}. The actual
grammar for expressions is not particularily relevant so we do not give a
precise one. For the sake of this presentation we also trat boolean and
arithmetic expressions together (with the usual convention of an expression
being true iff nonzero). We will consistently suppose programs are
\emph{welllabelled}, i.e.\ every label labels at most one occurrence of statement
in the program, and every \s{goto} points to a label actually present in the program.
\begin{figure}
+and operational semantics is presented in \autoref{fig:minimp}.
+\begin{figureplr}
$$\begin{gathered}
\begin{array}{nlBl>(R<)n}
@@ 830,8 +826,17 @@
\caption{The syntax and operational semantics of \imp.}
\label{fig:minimp}
\end{figure}



+\end{figureplr}
+The actual
+grammar for expressions is not particularly relevant so we do not give a
+precise one. For the sake of this presentation we also treat boolean and
+arithmetic expressions together (with the usual convention of an expression
+being true iff nonzero).
+
+We will suppose programs are
+\emph{welllabelled}, i.e.\ every label labels at most one occurrence of statement
+in the program, and every \s{goto} points to a label actually present in the program.
+The \s{find} helper functions has the task of not only finding the labelled
+statement in the program, but also building the correct continuation. The continuation
+built by \s{find} replaces the current continuation in the case of a jump.
\paragraph{Further down the compilation chain.}
@@ 890,4 +895,8 @@
& \text{etc.}
\end{array}$$
+where we identify cost labels $\alpha$ with singleton traces and we use $\varepsilon$
+for the empty trace. We then write $\to[\lambda]\!\!^*$ for the transitive
+closure of the small step semantics which produces by concatenation the trace
+$\lambda$.
\paragraph{Labelling.}
@@ 1140,8 +1149,16 @@
We are ready to update the definition of the operational semantics of
indexed labelled \imp. The emitted cost labels will now be ones indexed by
constant indexings. We add loop index increments as constructors to continuations%
\footnote{This is unneeded if we keep track of active loops (like is necessary
in the presence of \s{continue} and \s{break} statements).}:
$$K,\ldots \gramm \cdots  i_k{\uparrow} \cdot K$$
+constant indexings. We add a special indexed loop construct for continuations
+that keeps track of active indexed loop indexes:
+$$K,\ldots \gramm \cdots  i_k:\sop{while} b \sbin {do} S \sbin{then} K$$
+The difference between the regular stack concatenation
+$i_k:\sop{while}b\sbin{do}S\cdot K$ and the new constructor is that the latter
+indicates the loop is the active one in which we already are, while the former
+is a loop that still needs to be started%
+\footnote{In the presence of \s{continue} and \s{break} statements active
+loops need to be kept track of in any case.}.
+The \s{find} function is updated accordingly with the case
+$$ \s{find}(\ell, i_k:\sop{while}b\sbin{do}S, K) \ass \s{find}(\ell, S, i_k:
+ \sop{while}b\sbin{do}S\sbin{then}K).$$
The state will now be a 4uple
$(S,K,s,C)$ which adds a constant indexing to the 3uple of regular
@@ 1154,11 +1171,25 @@
(i_k:\sop{while}b\sbin{do}S,K,C) &\to[\varepsilon]_P
\begin{cases}
 (S,i_k{\uparrow} \cdot \sop{while}b\sbin{do}S\cdot K,s,C[i_k{\downarrow}0])
 & \text{if $(b,s)\eval v\neq 0$,}\\
 (\s{skip}, K, s, C) & \text{otherwise}
+ (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\downarrow}0])
+ \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\
+ \rlap{(\s{skip}, K, s, C)}\hskip 125pt \text{otherwise}
\end{cases}\\
 (\s{skip},i_k{\uparrow} \cdot K,s,C) &\to[\varepsilon]_P (\s{skip}, K, s, C[i_k{\uparrow}])
+ (\s{skip}, i_k:\sop{while}b\sbin{do}S\sbin{then}K,C) &\to[\varepsilon]_P
+ \begin{cases}
+ (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\uparrow}])
+ \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\
+ \rlap{(\s{skip}, K, s, C)} \hskip 125pt \text{otherwise}
+ \end{cases}
\end{aligned}$$
The starting state with store $s$ for a program $P$ becomes then
+Some explications are in order.
+\begin{itemize}
+ \item Emitting a label always instantiates it with the current indexing.
+ \item Hitting an indexed loop the first time initializes to 0 the corresponding
+ index; continuing the same loop inrements the index as expected.
+ \item The \s{find} function ignores the current indexing: this is correct
+ under the assumption that all indexed loops are single entry ones, so that
+ when we land inside an indexed loop with a \s{goto}, we are sure that its
+ current index is right.
+ \item The starting state with store $s$ for a program $P$ is
$(P,\s{halt},s,(i_0\mapsto 0,\dots,i_{n1}\mapsto 0)$ where $i_0,\ldots,i_{n1}$ cover
all loop indexes of $P$\footnote{For a program which is the indexed labelling of an
@@ 1166,4 +1197,5 @@
avoid computing this value in advance if we define $C[i{\downarrow}0]$ to extend
$C$'s domain as needed, so that the starting constant indexing can be the empty one.}.
+\end{itemize}
\paragraph{Compilation.}
@@ 1433,7 +1465,11 @@
\kappa(\alpha)\circ (I\circ C) = \kappa(\alpha\la I \ra).$$
$C$ represents a snapshot of loop indexes in the compiled code, while
$I\circ C$ is the corresponding snapshot in the source code.

A part from carrying over the proofs, we would like to extend the approach
+$I\circ C$ is the corresponding snapshot in the source code. Semantics preservation
+will make sure that when with snapshot $C$ we emit $\alpha\ra I\la$ (that is,
+we have $\alpha\la I\circ C\ra$ in the trace), this means that $\alpha$ must be
+emitted in the source code with indexing $I\circ C$, so the cost
+$\kappa(\alpha)\circ (I\circ C)$ applies.
+
+Apart from carrying over the proofs, we would like to extend the approach
to more loop transformations. Important examples are loop inversion
(where a for loop is reversed, usually to make iterations appear as truly
@@ 1446,4 +1482,21 @@
guarded loop (the $n$ in the first example).
+Finally, as stated in the introduction, the approach should allow integrating
+some techniques for cache analysis, a possibility that for now has been put aside
+as the standard 8051 architecture targeted by the CerCo project has no cache.
+As possible developments of this line of work without straying from the 8051
+architecture, two possibilities present themselves.
+\begin{enumerate}
+ \item One could extend the development to some 8051 variants, of which some have
+ been produced with a cache.
+ \item One could make the compiler implement its own cache: this cannot
+ apply to RAM accesses of the standard 8051 architecture, as the difference in
+ cost of accessing the two types of RAM is of just 1 clock cycle, which makes
+ any implementation of cache counterproductive. So this possibility should
+ either artificially change the accessing cost of RAM of the model just for the
+ sake of possible future adaptations to other architectures, or otherwise
+ model access to an external memory by means of the serial port.\end{enumerate}
+
+
%
% \newpage