# Changeset 1676

Ignore:
Timestamp:
Feb 6, 2012, 6:50:57 PM (6 years ago)
Message:

corrected some faults
still TODO: running example, language corrections

Location:
 r1674 of the compiled code which have constant cost. There are two properties one asks of the cost estimate. The first, paramount to There are two properties one asks of the cost estimate. The first one, paramount to the correctness of the method, is \emph{soundness}: the actual execution cost is bounded by the estimate. In the labelling approach, this is guaranteed if every loop in the control flow of the compiled code passes through at least one cost 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 label. The second one, optional but desirable, is \emph{preciseness}: the estimate \emph{is} the actual cost. In the labelling approach, this will 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 from such a label yields the same cost before hitting another one. In simple architectures such as the 8051 micro-controller this can be guaranteed by having labels at the immediate start of any branch of the control flow, and by ensuring no duplicate labels are present. It should be underlined that the above mentioned requirements must hold when executing the code at the end of the compilation chain. If one is careful to inject the labels at good key places in the source code, one can still think of two main obstacles: executing the code obtained at the end of the compilation chain. So even If one is careful injecting the labels at good key places in the source code, the requirements might still fail because of two main obstacles: \begin{itemize} \item compilation introduces important changes in the control flow, inserting loops or branches: an example in addressing this is the insertion of functions in the source code replacing instructions unavailable in the target architecture that require loops (e.g.\ multi-word division and generic shift in the 8051 architecture) so that the annotation process be sound, or the effort put in and that require loops to be carried out (e.g.\ multi-word division and generic shift in the 8051 architecture), or the effort put in providing unbranching translations of higher level instructions~ \cite{D2.2}; comes to some common code transformations done along a compilation chain. In particular most of \emph{loop optimizations} disrupt such conditions directly. For example in what we will call \emph{loop peeling} a first iteration of the In what we will call \emph{loop peeling}, for example, a first iteration of the loop is hoisted ahead of it, possibly to have a different cost than later iterations because of further transformation such as dead code elimination or invariant code motion. The second point strikes a difference in favour to existing tools for the estimate of execution costs to the detriment of CerCo's approach advocated in~ \cite{D2.1}. We will take as example the well known tool \s{aiT}~\cite{absint}, The second point strikes a difference in favour of existing tools for the estimate of execution costs and to the detriment of CerCo's approach advocated in~ \cite{D2.1}. We will take as an example the well known tool \s{aiT}~\cite{absint}, based on abstract interpretation: such a tool allows to estimate the worst-case execution time (WCET) taking into account advanced aspects of the presented in~\cite{D2.1} is common to both points: the inability to state different costs for different occurrences of labels, where the difference might be originated by labels being duplicated along compilation or the costs being sensitive to the state of execution. might be originated by labels being duplicated along the compilation or the costs being sensitive to the current state of execution. The preliminary work we present here addresses this node, introducing cost labels that are dependent we present here addresses this weakness by introducing cost labels that are dependent on which iteration of its containing loops it occurs in. This is achieved by means of \emph{indexed labels}: all cost labels are decorated with formal code. Integrating this transformation to the labelling approach would also allow to integrate the common case of cache analysis explained above: the analysis of cache hits and misses in the case of usually benefits from a form of of cache hits and misses usually benefits from a form of \emph{virtual} loop peeling~\cite{cacheprediction}. to present the development and the problems it is called to solve. The version of the minimal imperative language \imp that we will present has, The version of the minimal imperative language \imp{} that we will present has, with respect to the bare-bone usual version, \s{goto}s and labelled statements. Break and continue statements can be added at no particular expense. Its syntax \end{array} \end{gathered}$$\caption{The syntax and operational semantics of \imp.} \label{fig:minimp} 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 precise one. For the sake of conciseness we also treat boolean and arithmetic expressions together (with the usual convention of an expression being true iff non-zero). being true iff non-zero). We may omit the \s{else} clause of a conditional if it leads to a \s{skip} statement. We will suppose programs are \emph{well-labelled}, 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 The \s{find} helper function 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. unreachable \s{goto} jumping to them.}. Many loop optimizations do not preserve the semantics of multi-entry loops in general, or are otherwise rendered ineffective. Usually compilers implement a multi-entry loop detection which avoids those loops from being targeted by optimizations~\cite{muchnick,morgan}. ineffective. Usually compilers implement a single-entry loop detection which avoids the multi-entry ones from being targeted by optimizations~\cite{muchnick,morgan}. The loop transformations we present are local, i.e.\ they target a single loop and transform it. Which loops are targeted may be decided by an \emph{ad hoc} heuristic, however this is not important here. \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 for the empty trace. Cost labels are emitted by cost-labelled statements only% \footnote{In the general case the evaluation of expressions can emit cost labels too (see \autoref{sec:conc}).}. We then write $\to[\lambda]\!\!^*$ for the transitive closure of the small step semantics which produces by concatenation the trace $\lambda$. containing $\ell$, or the empty path if none exists; and $\s{gotosof}_P$ from a label $\ell$ to the occurrences of \s{goto}s pointing to it. Then the set $\s{multyentry}_P$ of multy-entry loops of $P$ can be computed by adding to it all occurrences $p$ such that there exists a label $\ell$ and an occurrence $q$ with $\s{loopof}_P(\ell)=p$, $q\in \s{gotosof}_P(\ell)$ and $p\not\le q$ (where $\le$ is the prefix relation)\footnote{Possible simplification to this $\s{multientry}_P$ of multi-entry loops of $P$ can be computed by $$\s{multientry}_P\ass\{\, p \mid \exists \ell,q.p =\s{loopof}_P(\ell),q\in\s{gotosof}_P(\ell), q \not\le p\,\}$$ where $\le$ is the prefix relation\footnote{Possible simplification to this procedure include keeping track just of while loops containing labels and \s{goto}s (rather than paths in the syntactic tree of the program), and making \begin{array}{lh{-100pt}l} (i_k:\sop{while}b\sbin{do}\alpha\la Id_{k+1}\ra : \Ell^\iota_P(T,k+1));\beta\la Id_k \ra : \s{skip} \\& \text{if $S=\sop{while}b\sbin{do}T$ and $S\notin \s{multyentry}_P$,}\\[3pt] \\& \text{if $S=\sop{while}b\sbin{do}T$ and $S\notin \s{multientry}_P$,}\\[3pt] (\sop{while}b\sbin{do}\alpha\la Id_k \ra : \Ell^\iota_P(T,k));\beta\la Id_k \ra : \s{skip} \\& \text{otherwise, if $S=\sop{while}b\sbin{do}T$,}\\[3pt] $C$ represents a snapshot of loop indexes in the compiled code, while $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, will make sure that when with snapshot $C$ we emit $\alpha\la I\ra$ (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