Changeset 1676


Ignore:
Timestamp:
Feb 6, 2012, 6:50:57 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

    r1674 r1676  
    637637of the compiled code which have constant cost.
    638638
    639 There are two properties one asks of the cost estimate. The first, paramount to
     639There are two properties one asks of the cost estimate. The first one, paramount to
    640640the correctness of the method, is \emph{soundness}: the actual execution cost
    641641is bounded by the estimate. In the labelling approach, this is guaranteed if every
    642642loop in the control flow of the compiled code passes through at least one cost
    643 label. The second, optional but desirable, is \emph{preciseness}: the estimate
    644 is not in fact an estimate but the actual cost. In the labelling approach, this will
     643label. The second one, optional but desirable, is \emph{preciseness}: the estimate
     644\emph{is} the actual cost. In the labelling approach, this will
    645645be true if for every label every possible execution of the compiled code starting
    646 from such a label yields the same cost. In simple architectures such as the 8051
     646from such a label yields the same cost before hitting another one. In simple
     647architectures such as the 8051
    647648micro-controller this can be guaranteed by having labels at the immediate start of any
    648649branch of the control flow, and by ensuring no duplicate labels are present.
    649650
    650651It should be underlined that the above mentioned requirements must hold when
    651 executing the code at the
    652 end of the compilation chain. If one is careful to inject the labels at good
    653 key places in the source code, one can still think of two main obstacles:
     652executing the code obtained at the
     653end of the compilation chain. So even If one is careful injecting the labels at good
     654key places in the source code, the requirements might still fail because of two main obstacles:
    654655\begin{itemize}
    655656 \item compilation introduces important changes in the control flow, inserting
    656657loops or branches: an example in addressing this is the insertion of functions
    657658in the source code replacing instructions unavailable in the target architecture
    658 that require loops (e.g.\ multi-word division and generic shift in the 8051
    659 architecture) so that the annotation process be sound, or the effort put in
     659and that require loops to be carried out (e.g.\ multi-word division and generic
     660shift in the 8051 architecture), or the effort put in
    660661providing unbranching translations of higher level instructions~
    661662\cite{D2.2};
     
    671672comes to some common code transformations done along a compilation chain. In
    672673particular most of \emph{loop optimizations} disrupt such conditions directly.
    673 For example in what we will call \emph{loop peeling} a first iteration of the
     674In what we will call \emph{loop peeling}, for example, a first iteration of the
    674675loop is hoisted ahead of it, possibly to have a different cost than later iterations
    675676because of further transformation such as dead code elimination or invariant
    676677code motion.
    677678
    678 The second point strikes a difference in favour to existing tools for the
    679 estimate of execution costs to the detriment of CerCo's approach advocated in~
    680 \cite{D2.1}. We will take as example the well known tool \s{aiT}~\cite{absint},
     679The second point strikes a difference in favour of existing tools for the
     680estimate of execution costs and to the detriment of CerCo's approach advocated in~
     681\cite{D2.1}. We will take as an example the well known tool \s{aiT}~\cite{absint},
    681682based on abstract interpretation: such a tool allows to estimate the
    682683worst-case execution time (WCET) taking into account advanced aspects of the
     
    693694presented in~\cite{D2.1} is common to both points: the inability to state
    694695different costs for different occurrences of labels, where the difference
    695 might be originated by labels being duplicated along compilation
    696 or the costs being sensitive to the state of execution.
     696might be originated by labels being duplicated along the compilation
     697or the costs being sensitive to the current state of execution.
    697698
    698699The preliminary work
    699 we present here addresses this node, introducing cost labels that are dependent
     700we present here addresses this weakness by introducing cost labels that are dependent
    700701on which iteration of its containing loops it occurs in. This is achieved by
    701702means of \emph{indexed labels}: all cost labels are decorated with formal
     
    718719code. Integrating this transformation to the labelling approach would also allow
    719720to integrate the common case of cache analysis explained above: the analysis
    720 of cache hits and misses in the case of usually benefits from a form of
     721of cache hits and misses usually benefits from a form of
    721722\emph{virtual} loop peeling~\cite{cacheprediction}.
    722723
     
    755756to present the development and the problems it is called to solve.
    756757
    757 The version of the minimal imperative language \imp that we will present has,
     758The version of the minimal imperative language \imp{} that we will present has,
    758759with respect to the bare-bone usual version, \s{goto}s and labelled statements.
    759760Break and continue statements can be added at no particular expense. Its syntax
     
    822823\end{array}
    823824\end{gathered}$$
    824 
    825 
    826825\caption{The syntax and operational semantics of \imp.}
    827826\label{fig:minimp}
     
    829828The actual
    830829grammar 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
     830precise one. For the sake of conciseness we also treat boolean and
    832831arithmetic expressions together (with the usual convention of an expression
    833 being true iff non-zero).
     832being true iff non-zero). We may omit the \s{else} clause of a conditional
     833if it leads to a \s{skip} statement.
    834834
    835835We will suppose programs are
    836836\emph{well-labelled}, i.e.\ every label labels at most one occurrence of statement
    837837in 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
     838The \s{find} helper function has the task of not only finding the labelled
    839839statement in the program, but also building the correct continuation. The continuation
    840840built by \s{find} replaces the current continuation in the case of a jump.
     
    852852unreachable \s{goto} jumping to them.}. Many loop optimizations do not preserve
    853853the semantics of multi-entry loops in general, or are otherwise rendered
    854 ineffective. Usually compilers implement a multi-entry loop detection which
    855 avoids those loops from being targeted by optimizations~\cite{muchnick,morgan}.
     854ineffective. Usually compilers implement a single-entry loop detection which
     855avoids the multi-entry ones from being targeted by optimizations~\cite{muchnick,morgan}.
     856The loop transformations we present are local, i.e.\ they target a single loop
     857and transform it. Which loops are targeted may be decided by an \emph{ad hoc}
     858heuristic, however this is not important here.
    856859
    857860
     
    896899\end{array}$$
    897900where 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
     901for the empty trace. Cost labels are emitted by cost-labelled statements only%
     902\footnote{In the general case the evaluation of expressions can emit cost labels
     903too (see \autoref{sec:conc}).}. We then write $\to[\lambda]\!\!^*$ for the transitive
    899904closure of the small step semantics which produces by concatenation the trace
    900905$\lambda$.
     
    10371042containing $\ell$, or the empty path if none exists; and $\s{gotosof}_P$ from
    10381043a label $\ell$ to the occurrences of \s{goto}s pointing to it. Then the set
    1039 $\s{multyentry}_P$ of multy-entry loops of $P$ can be computed by adding to it
    1040 all occurrences $p$ such that there exists a label $\ell$ and an occurrence
    1041 $q$ with $\s{loopof}_P(\ell)=p$, $q\in \s{gotosof}_P(\ell)$ and $p\not\le q$
    1042 (where $\le$ is the prefix relation)\footnote{Possible simplification to this
     1044$\s{multientry}_P$ of multi-entry loops of $P$ can be computed by
     1045$$\s{multientry}_P\ass\{\, p \mid \exists \ell,q.p =\s{loopof}_P(\ell),q\in\s{gotosof}_P(\ell), q \not\le p\,\}$$
     1046where $\le$ is the prefix relation\footnote{Possible simplification to this
    10431047procedure include keeping track just of while loops containing labels and
    10441048\s{goto}s (rather than paths in the syntactic tree of the program), and making
     
    10541058\begin{array}{lh{-100pt}l}
    10551059 (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}
    1056 \\& \text{if $S=\sop{while}b\sbin{do}T$ and $S\notin \s{multyentry}_P$,}\\[3pt]
     1060\\& \text{if $S=\sop{while}b\sbin{do}T$ and $S\notin \s{multientry}_P$,}\\[3pt]
    10571061(\sop{while}b\sbin{do}\alpha\la Id_k \ra : \Ell^\iota_P(T,k));\beta\la Id_k \ra : \s{skip}
    10581062\\& \text{otherwise, if $S=\sop{while}b\sbin{do}T$,}\\[3pt]
     
    14661470$C$ represents a snapshot of loop indexes in the compiled code, while
    14671471$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,
     1472will make sure that when with snapshot $C$ we emit $\alpha\la I\ra$ (that is,
    14691473we have $\alpha\la I\circ C\ra$ in the trace), this means that $\alpha$ must be
    14701474emitted in the source code with indexing $I\circ C$, so the cost
Note: See TracChangeset for help on using the changeset viewer.