Changeset 1674


Ignore:
Timestamp:
Feb 6, 2012, 12:32:06 PM (6 years ago)
Author:
tranquil
Message:

corrected some faults
still TODO: running example, language corrections

Location:
Deliverables/addenda/indexed_labels
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/addenda/indexed_labels/report.tex

    r1673 r1674  
    168168\newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}}
    169169 %horizontal thiner line for figures
    170 \newenvironment{figureplr}{\begin{figure}[t] \Figbar}{\Figbar \end{figure}}
     170\newenvironment{figureplr}[1][t]{\begin{figure}[#1] \Figbar}{\Figbar \end{figure}}
    171171%environment for figures
    172172%       ************Macros for mathematical symbols*************
     
    572572\newcommand{\gramm}{\mathrel{::=}}
    573573\newcommand{\ass}{\mathrel{:=}}
     574
     575\renewcommand{\to}[1][]{\stackrel{#1}{\rightarrow}}
    574576%<<<<<<<<<<<<
    575577\begin{document}
     
    641643label. The second, optional but desirable, is \emph{preciseness}: the estimate
    642644is not in fact an estimate but the actual cost. In the labelling approach, this will
    643 true if for every label every possible execution of the compiled code starting
     645be true if for every label every possible execution of the compiled code starting
    644646from such a label yields the same cost. In simple architectures such as the 8051
    645647micro-controller this can be guaranteed by having labels at the immediate start of any
     
    754756
    755757The version of the minimal imperative language \imp that we will present has,
    756 with respect to the barebone usual version, \s{goto}s and labelled statements.
     758with respect to the bare-bone usual version, \s{goto}s and labelled statements.
    757759Break and continue statements can be added at no particular expense. Its syntax
    758 and operational semantics is presented in \autoref{fig:minimp}. The actual
    759 grammar for expressions is not particularily relevant so we do not give a
    760 precise one. For the sake of this presentation we also trat boolean and
    761 arithmetic expressions together (with the usual convention of an expression
    762 being true iff non-zero). We will consistently suppose programs are
    763 \emph{well-labelled}, i.e.\ every label labels at most one occurrence of statement
    764 in the program, and every \s{goto} points to a label actually present in the program.
    765 \begin{figure}
     760and operational semantics is presented in \autoref{fig:minimp}.
     761\begin{figureplr}
    766762$$\begin{gathered}
    767763\begin{array}{nlBl>(R<)n}
     
    830826\caption{The syntax and operational semantics of \imp.}
    831827\label{fig:minimp}
    832 \end{figure}
    833 
    834 
    835 
     828\end{figureplr}
     829The actual
     830grammar for expressions is not particularly relevant so we do not give a
     831precise one. For the sake of this presentation we also treat boolean and
     832arithmetic expressions together (with the usual convention of an expression
     833being true iff non-zero).
     834
     835We will suppose programs are
     836\emph{well-labelled}, i.e.\ every label labels at most one occurrence of statement
     837in the program, and every \s{goto} points to a label actually present in the program.
     838The \s{find} helper functions has the task of not only finding the labelled
     839statement in the program, but also building the correct continuation. The continuation
     840built by \s{find} replaces the current continuation in the case of a jump.
    836841
    837842\paragraph{Further down the compilation chain.}
     
    890895& \text{etc.}
    891896\end{array}$$
     897where we identify cost labels $\alpha$ with singleton traces and we use $\varepsilon$
     898for the empty trace. We then write $\to[\lambda]\!\!^*$ for the transitive
     899closure of the small step semantics which produces by concatenation the trace
     900$\lambda$.
    892901
    893902\paragraph{Labelling.}
     
    11401149We are ready to update the definition of the operational semantics of
    11411150indexed labelled \imp. The emitted cost labels will now be ones indexed by
    1142 constant indexings. We add loop index increments as constructors to continuations%
    1143 \footnote{This is unneeded if we keep track of active loops (like is necessary
    1144 in the presence of \s{continue} and \s{break} statements).}:
    1145 $$K,\ldots  \gramm \cdots | i_k{\uparrow} \cdot K$$
     1151constant indexings. We add a special indexed loop construct for continuations
     1152that keeps track of active indexed loop indexes:
     1153$$K,\ldots  \gramm \cdots | i_k:\sop{while} b \sbin {do} S \sbin{then}  K$$
     1154The difference between the regular stack concatenation
     1155$i_k:\sop{while}b\sbin{do}S\cdot K$ and the new constructor is that the latter
     1156indicates the loop is the active one in which we already are, while the former
     1157is a loop that still needs to be started%
     1158\footnote{In the presence of \s{continue} and \s{break} statements active
     1159loops need to be kept track of in any case.}.
     1160The \s{find} function is updated accordingly with the case
     1161$$ \s{find}(\ell, i_k:\sop{while}b\sbin{do}S, K) \ass \s{find}(\ell, S, i_k:
     1162  \sop{while}b\sbin{do}S\sbin{then}K).$$
    11461163The state will now be a 4-uple
    11471164$(S,K,s,C)$ which adds a constant indexing to the 3-uple of regular
     
    11541171   (i_k:\sop{while}b\sbin{do}S,K,C) &\to[\varepsilon]_P
    11551172    \begin{cases}
    1156      (S,i_k{\uparrow} \cdot \sop{while}b\sbin{do}S\cdot K,s,C[i_k{\downarrow}0])
    1157       & \text{if $(b,s)\eval v\neq 0$,}\\
    1158      (\s{skip}, K, s, C) & \text{otherwise}
     1173     (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\downarrow}0])
     1174     \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\
     1175     \rlap{(\s{skip}, K, s, C)}\hskip 125pt \text{otherwise}
    11591176    \end{cases}\\
    1160    (\s{skip},i_k{\uparrow} \cdot K,s,C) &\to[\varepsilon]_P (\s{skip}, K, s, C[i_k{\uparrow}])
     1177   (\s{skip}, i_k:\sop{while}b\sbin{do}S\sbin{then}K,C) &\to[\varepsilon]_P
     1178    \begin{cases}
     1179     (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\uparrow}])
     1180      \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\
     1181     \rlap{(\s{skip}, K, s, C)} \hskip 125pt \text{otherwise}
     1182    \end{cases}
    11611183  \end{aligned}$$
    1162 The starting state with store $s$ for a program $P$ becomes then
     1184Some explications are in order.
     1185\begin{itemize}
     1186 \item Emitting a label always instantiates it with the current indexing.
     1187 \item Hitting an indexed loop the first time initializes to 0 the corresponding
     1188  index; continuing the same loop inrements the index as expected.
     1189 \item The \s{find} function ignores the current indexing: this is correct
     1190  under the assumption that all indexed loops are single entry ones, so that
     1191  when we land inside an indexed loop with a \s{goto}, we are sure that its
     1192  current index is right.
     1193  \item The starting state with store $s$ for a program $P$ is
    11631194$(P,\s{halt},s,(i_0\mapsto 0,\dots,i_{n-1}\mapsto 0)$ where $i_0,\ldots,i_{n-1}$ cover
    11641195all loop indexes of $P$\footnote{For a program which is the indexed labelling of an
     
    11661197avoid computing this value in advance if we define $C[i{\downarrow}0]$ to extend
    11671198$C$'s domain as needed, so that the starting constant indexing can be the empty one.}.
     1199\end{itemize}
    11681200
    11691201\paragraph{Compilation.}
     
    14331465  \kappa(\alpha)\circ (I\circ C) = \kappa(\alpha\la I \ra).$$
    14341466$C$ represents a snapshot of loop indexes in the compiled code, while
    1435 $I\circ C$ is the corresponding snapshot in the source code.
    1436 
    1437 A part from carrying over the proofs, we would like to extend the approach
     1467$I\circ C$ is the corresponding snapshot in the source code. Semantics preservation
     1468will make sure that when with snapshot $C$ we emit $\alpha\ra I\la$ (that is,
     1469we have $\alpha\la I\circ C\ra$ in the trace), this means that $\alpha$ must be
     1470emitted in the source code with indexing $I\circ C$, so the cost
     1471$\kappa(\alpha)\circ (I\circ C)$ applies.
     1472
     1473Apart from carrying over the proofs, we would like to extend the approach
    14381474to more loop transformations. Important examples are loop inversion
    14391475(where a for loop is reversed, usually to make iterations appear as truly
     
    14461482guarded loop (the $n$ in the first example).
    14471483
     1484Finally, as stated in the introduction, the approach should allow integrating
     1485some techniques for cache analysis, a possibility that for now has been put aside
     1486as the standard 8051 architecture targeted by the CerCo project has no cache.
     1487As possible developments of this line of work without straying from the 8051
     1488architecture, two possibilities present themselves.
     1489\begin{enumerate}
     1490 \item One could extend the development to some 8051 variants, of which some have
     1491  been produced with a cache.
     1492 \item One could make the compiler implement its own cache: this cannot
     1493  apply to RAM accesses of the standard 8051 architecture, as the difference in
     1494  cost of accessing the two types of RAM is of just 1 clock cycle, which makes
     1495  any implementation of cache counterproductive. So this possibility should
     1496  either artificially change the accessing cost of RAM of the model just for the
     1497  sake of possible future adaptations to other architectures, or otherwise
     1498  model access to an external memory by means of the serial port.\end{enumerate}
     1499
     1500
    14481501%
    14491502% \newpage
Note: See TracChangeset for help on using the changeset viewer.