Changeset 1674
 Timestamp:
 Feb 6, 2012, 12:32:06 PM (6 years ago)
 Location:
 Deliverables/addenda/indexed_labels
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/addenda/indexed_labels/report.tex
r1673 r1674 168 168 \newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}} 169 169 %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}} 171 171 %environment for figures 172 172 % ************Macros for mathematical symbols************* … … 572 572 \newcommand{\gramm}{\mathrel{::=}} 573 573 \newcommand{\ass}{\mathrel{:=}} 574 575 \renewcommand{\to}[1][]{\stackrel{#1}{\rightarrow}} 574 576 %<<<<<<<<<<<< 575 577 \begin{document} … … 641 643 label. The second, optional but desirable, is \emph{preciseness}: the estimate 642 644 is 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 starting645 be true if for every label every possible execution of the compiled code starting 644 646 from such a label yields the same cost. In simple architectures such as the 8051 645 647 microcontroller this can be guaranteed by having labels at the immediate start of any … … 754 756 755 757 The version of the minimal imperative language \imp that we will present has, 756 with respect to the bare bone usual version, \s{goto}s and labelled statements.758 with respect to the barebone usual version, \s{goto}s and labelled statements. 757 759 Break 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 nonzero). We will consistently suppose programs are 763 \emph{welllabelled}, 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} 760 and operational semantics is presented in \autoref{fig:minimp}. 761 \begin{figureplr} 766 762 $$\begin{gathered} 767 763 \begin{array}{nlBl>(R<)n} … … 830 826 \caption{The syntax and operational semantics of \imp.} 831 827 \label{fig:minimp} 832 \end{figure} 833 834 835 828 \end{figureplr} 829 The actual 830 grammar for expressions is not particularly relevant so we do not give a 831 precise one. For the sake of this presentation we also treat boolean and 832 arithmetic expressions together (with the usual convention of an expression 833 being true iff nonzero). 834 835 We will suppose programs are 836 \emph{welllabelled}, i.e.\ every label labels at most one occurrence of statement 837 in the program, and every \s{goto} points to a label actually present in the program. 838 The \s{find} helper functions has the task of not only finding the labelled 839 statement in the program, but also building the correct continuation. The continuation 840 built by \s{find} replaces the current continuation in the case of a jump. 836 841 837 842 \paragraph{Further down the compilation chain.} … … 890 895 & \text{etc.} 891 896 \end{array}$$ 897 where we identify cost labels $\alpha$ with singleton traces and we use $\varepsilon$ 898 for the empty trace. We then write $\to[\lambda]\!\!^*$ for the transitive 899 closure of the small step semantics which produces by concatenation the trace 900 $\lambda$. 892 901 893 902 \paragraph{Labelling.} … … 1140 1149 We are ready to update the definition of the operational semantics of 1141 1150 indexed 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$$ 1151 constant indexings. We add a special indexed loop construct for continuations 1152 that keeps track of active indexed loop indexes: 1153 $$K,\ldots \gramm \cdots  i_k:\sop{while} b \sbin {do} S \sbin{then} K$$ 1154 The 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 1156 indicates the loop is the active one in which we already are, while the former 1157 is a loop that still needs to be started% 1158 \footnote{In the presence of \s{continue} and \s{break} statements active 1159 loops need to be kept track of in any case.}. 1160 The \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).$$ 1146 1163 The state will now be a 4uple 1147 1164 $(S,K,s,C)$ which adds a constant indexing to the 3uple of regular … … 1154 1171 (i_k:\sop{while}b\sbin{do}S,K,C) &\to[\varepsilon]_P 1155 1172 \begin{cases} 1156 (S,i_k {\uparrow} \cdot \sop{while}b\sbin{do}S\cdotK,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} 1159 1176 \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} 1161 1183 \end{aligned}$$ 1162 The starting state with store $s$ for a program $P$ becomes then 1184 Some 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 1163 1194 $(P,\s{halt},s,(i_0\mapsto 0,\dots,i_{n1}\mapsto 0)$ where $i_0,\ldots,i_{n1}$ cover 1164 1195 all loop indexes of $P$\footnote{For a program which is the indexed labelling of an … … 1166 1197 avoid computing this value in advance if we define $C[i{\downarrow}0]$ to extend 1167 1198 $C$'s domain as needed, so that the starting constant indexing can be the empty one.}. 1199 \end{itemize} 1168 1200 1169 1201 \paragraph{Compilation.} … … 1433 1465 \kappa(\alpha)\circ (I\circ C) = \kappa(\alpha\la I \ra).$$ 1434 1466 $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 1468 will make sure that when with snapshot $C$ we emit $\alpha\ra I\la$ (that is, 1469 we have $\alpha\la I\circ C\ra$ in the trace), this means that $\alpha$ must be 1470 emitted in the source code with indexing $I\circ C$, so the cost 1471 $\kappa(\alpha)\circ (I\circ C)$ applies. 1472 1473 Apart from carrying over the proofs, we would like to extend the approach 1438 1474 to more loop transformations. Important examples are loop inversion 1439 1475 (where a for loop is reversed, usually to make iterations appear as truly … … 1446 1482 guarded loop (the $n$ in the first example). 1447 1483 1484 Finally, as stated in the introduction, the approach should allow integrating 1485 some techniques for cache analysis, a possibility that for now has been put aside 1486 as the standard 8051 architecture targeted by the CerCo project has no cache. 1487 As possible developments of this line of work without straying from the 8051 1488 architecture, 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 1448 1501 % 1449 1502 % \newpage
Note: See TracChangeset
for help on using the changeset viewer.