Changeset 3666


Ignore:
Timestamp:
Mar 16, 2017, 5:21:42 PM (9 days ago)
Author:
boender
Message:

Updated the proof part

Location:
Papers/jar-cerco-2017
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/cerco.bib

    r3661 r3666  
    18231823  doi = {10.1007/3-540-45937-5_16}
    18241824}
     1825
     1826@Inbook{Ayache2012,
     1827author="Ayache, Nicolas
     1828and Amadio, Roberto M.
     1829and R{\'e}gis-Gianas, Yann",
     1830editor="Stoelinga, Mari{\"e}lle
     1831and Pinger, Ralf",
     1832title="Certifying and Reasoning on Cost Annotations in C Programs",
     1833bookTitle="Formal Methods for Industrial Critical Systems: 17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings",
     1834year="2012",
     1835publisher="Springer Berlin Heidelberg",
     1836address="Berlin, Heidelberg",
     1837pages="32--46",
     1838isbn="978-3-642-32469-7",
     1839doi="10.1007/978-3-642-32469-7_3",
     1840url="http://dx.doi.org/10.1007/978-3-642-32469-7_3"
     1841}
  • Papers/jar-cerco-2017/cerco.tex

    r3659 r3666  
    4444\usepackage{stmaryrd}
    4545\usepackage{url}
     46\usepackage[all]{xy}
    4647
    4748\usepackage{tikz}
  • Papers/jar-cerco-2017/development.tex

    r3662 r3666  
    77\label{sect.formal.development}
    88
    9 \subsection*{Statistics}
     9\subsection{Statistics}
    1010
    1111\begin{tabular}{|c|c|}
  • Papers/jar-cerco-2017/proof.tex

    r3659 r3666  
    66%   Main theorem statement
    77
    8 \section{Introduction}
    9 In~\cite{D2.1}, Armadio \emph{et al} propose an approach for building a compiler for a large fragment of the \textsc{c} programming language.
    10 The novelty of their proposal lies in the fact that their proposed design is capable of lifting execution cost information from the compiled code and presenting it to the user.
    11 This idea is foundational for the CerCo project, which strives to produce a mechanically certified version of such a compiler.
    12 
    13 To summarise, Armadio's proposal consisted of `decorations' on the source code, along with the insertion of labels at key points.
    14 These labels are preserved as compilation progresses, from one intermediate language to another.
    15 Once the final object code is produced, such labels should correspond to the parts of the compiled code that have a constant cost.
    16 
    17 Two properties must hold of any cost estimate.
    18 The first property, paramount to the correctness of the method, is \emph{soundness}, that is, that the actual execution cost is bounded by the estimate.
    19 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.
    20 The second property, optional but desirable, is \emph{preciseness}: the estimate \emph{is} the actual cost.
    21 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 before hitting another one.
    22 In simple architectures such as the 8051 micro-controller this can be guaranteed by placing labels at the start of any branch in the control flow, and by ensuring that no labels are duplicated.
    23 
    24 The reader should note that the above mentioned requirements must hold when executing the code obtained at the end of the compilation chain.
    25 So even if one is careful about injecting the labels at suitable places in the source code, the requirements might still fail because of two main obstacles:
    26 \begin{itemize}
    27 \item
    28 The compilation process introduces important changes in the control flow, inserting loops or branches.
    29 For example, the insertion of functions in the source code replacing instructions that are unavailable in the target architecture.
    30 This require loops to be inserted (for example, for multi-word division and generic shift in the 8051 architecture), or effort spent in providing unbranching translations of higher level instructions~\cite{D2.2}.
    31 \item
    32 Even when the compiled code \emph{does}---as far as the the syntactic control flow graph is concerned---respect the conditions for soundness and preciseness, the cost of blocks of instructions might not be independent of context, so that different passes through a label might have different costs.
    33 This becomes a concern if one wishes to apply the approach to more complex architectures, for example one with caching or pipelining.
    34 \end{itemize}
    35 The first point unveils a weakness of the current labelling approach when it comes to some common code transformations performed along a compilation chain.
    36 In particular, most \emph{loop optimisations} are disruptive, in the sense outlined in the first bulletpoint above.
    37 An example optimisation of this kind is \emph{loop peeling}.
    38 This optimisation is employed by compilers in order to trigger other optimisations, for example, dead code elimination or invariant code motion.
    39 Here, a first iteration of the loop is hoisted out of the body of the loop, possibly being assigned a different cost than later iterations.
    40 
    41 The second bulletpoint above highlights another weakness. Different tools allow to predict up to a certain extent the behaviour of cache.
    42 For example, the well known tool \s{aiT}~\cite{absint}---based on abstract interpretation---allows the user to estimate the worst-case execution time (\textsc{wcet}) of a piece of source code, taking into account advanced features of the target architecture. While
    43 such a tool is not fit for a compositional approach which is central to CerCo's project\footnote{\s{aiT} assumes the cache is empty at the start of computation, and treats each procedure call separately, unrolling a great part of the control flow.},
    44 \s{aiT}'s ability to produce tight estimates of execution costs would sthill enhance the effectiveness of the CerCo compiler, \eg{} by integrating such techniques in its development.
    45 A typical case where cache analysis yields a difference in the execution cost of a block is in loops: the first iteration will usually stumble upon more cache misses than subsequent iterations.
    46 
    47 If one looks closely, the source of the weakness of the labelling approach as 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 the compilation, or the costs being sensitive to the current state of execution.
    48 The preliminary work we present here addresses this weakness by introducing cost labels that are dependent on which iteration of its containing loops it occurs in.
     8\section{Compiler proof}
     9\label{sect.compiler.proof}
     10
     11\subsection{Labelling approach}
     12
     13In this section, we will explore the labelling approach mentioned in the introduction in more detail.
     14
     15The `labelling' approach to the problem of building
     16cost annotations is summarized in the following diagram.
     17
     18\newcolumntype{M}[1]{>{\raggedright}m{#1}}
     19
     20\-
     21
     22\begin{tabular}{M{10cm}||M{4cm}}
     23$$
     24\xymatrix{
     25% Row 1
     26  L_1 \\
     27%
     28% Row 2
     29  L_{1,\ell}
     30  \ar[u]^{\cl{I}}
     31  \ar@/^/[d]^{\w{er}_1}
     32  \ar[r]^{\cl{C}_1}
     33%
     34& L_{2,\ell}
     35  \ar[d]^{\w{er}_2} 
     36%
     37& \ldots \hspace{0.3cm}\ar[r]^{\cl{C}_k}
     38%
     39& L_{k+1, \ell}
     40  \ar[d]^{\w{er}_{k+1}}  \\
     41%
     42% Row 3
     43  L_1                                 
     44  \ar@/^/[u]^{\cl{L}}
     45  \ar[r]^{\cl{C}_1}
     46& L_2   
     47& \ldots\hspace{0.3cm}
     48  \ar[r]^{\cl{C}_{k}}
     49& L_{k+1}
     50}
     51$$
     52&
     53$$
     54\begin{array}{ccc}
     55\w{er}_{i+1} \comp \cl{C}_{i} &= &\cl{C}_{i} \comp \w{er}_{i} \\
     56
     57\w{er}_{1} \comp \cl{L} &= &\w{id}_{L_{1}} \\
     58
     59\w{An}_{1} &= &\cl{I} \comp \cl{L} 
     60\end{array}
     61$$
     62\end{tabular}
     63
     64\-
     65
     66For each language $L_i$ considered in the compilation process,
     67we define an extended {\em labelled} language $L_{i,\ell}$ and an
     68extended operational semantics. The labels are used to mark
     69certain points of the control. The semantics makes sure
     70that whenever we cross a labelled control point a labelled and observable
     71transition is produced.
     72
     73For each labelled language there is an obvious function $\w{er}_i$
     74erasing all labels and producing a program in the corresponding
     75unlabelled language.
     76The compilation functions $\cl{C}_i$ are extended from the unlabelled
     77to the labelled language so that they enjoy commutation
     78with the erasure functions. Moreover, we lift the soundness properties of
     79the compilation functions from the unlabelled to the labelled languages
     80and transition systems.
     81
     82A {\em labelling} $\cl{L}$  of the source language $L_1$ is just a function
     83such that $\w{er}_{L_{1}} \comp \cl{L}$ is the identity function.
     84An {\em instrumentation} $\cl{I}$ of the source labelled language  $L_{1,\ell}$
     85is a function replacing the labels with suitable increments of, say,
     86a fresh \w{cost} variable. Then an {\em annotation} $\w{An}_{1}$ of the
     87source program can be derived simply as the composition of the labelling
     88and the instrumentation functions: $\w{An}_{1} = \cl{I}\comp \cl{L}$.
     89
     90As for the direct approach, suppose $s$ is some adequate representation
     91of the state of a program. Let $S$ be a source program and suppose
     92that its annotation satisfies the following property:
     93\begin{equation}\label{STEP1}
     94(\w{An}_{1}(S),s[c/\w{cost}])  \eval s'[c+\delta/\w{cost}]
     95\end{equation}
     96where $\delta$ is some non-negative number.
     97Then the definition of the instrumentation and the fact that
     98the soundness proofs of the compilation functions have been lifted
     99to the labelled languages allows to conclude that
     100\begin{equation}\label{step2}
     101(\cl{C}(L(S)),s[c/\w{cost}])  \eval (s'[c/\w{cost}],\lambda)
     102\end{equation}
     103where $\cl{C} = \cl{C}_{k} \comp \cdots \comp \cl{C}_{1}$ and
     104$\lambda$ is a sequence (or a multi-set) of labels whose `cost'
     105corresponds to the number $\delta$ produced by the
     106annotated program.
     107Then the commutation properties of erasure and compilation functions
     108allows to conclude that the {\em erasure} of the compiled
     109labelled code $\w{er}_{k+1}(\cl{C}(L(S)))$ is actually  equal to
     110the compiled code $\cl{C}(S)$ we are interested in.
     111Given this, the following question arises:
     112
     113\begin{quote}
     114Under which conditions
     115the sequence $\lambda$, {\em i.e.}, the increment $\delta$,
     116is a sound and possibly precise description of the
     117execution cost of the object code?
     118\end{quote}
     119
     120To answer this question, we observe that the object code we are interested in is some kind of assembly code
     121and its control flow can be easily represented as a control flow
     122graph. The fact that we have to prove the soundness of the compilation
     123functions means that we have plenty of pieces of information
     124on the way the control flows in the compiled code, in particular as
     125far as procedure calls and returns are concerned.
     126These pieces of information allow to build a rather accurate representation
     127of the control flow of the compiled code at run time.
     128
     129The idea is then to perform two simple checks on the control flow
     130graph. The first check is to verify that all loops go through a labelled node.
     131If this is the case then we can associate a finite cost with
     132every label and prove that the cost annotations are sound.
     133The second check amounts to verify that all paths starting from
     134a label have the same cost. If this check is successful then we can
     135conclude that the cost annotations are precise.
     136
     137This approach, as published in~\cite{Ayache2012} is the one used in the CerCo project. However, it has some weaknesses, which we will describe in the next subsection. We also propose a method to resolve these weaknesses.
     138
     139\subsection{Indexed labelling}
     140
     141THe labelling approach as described above does not deal well with some optimisations the compiler might introduce, such as changes in the control flow. For example, the 8051 architecture does not have an instruction for
     142multi-word division, which means that a function containing loops has to be inserted into the code. In fact, this is symptomatic of a more general weakness: the inability to state different costs for different occurrences of labels,
     143where the difference might be originated by labels being duplicated along the compilation, or the costs being sensitive to the current state of execution.
     144
     145We present a solution that addresses this weakness by introducing cost labels that are dependent on the iteration of their containing loop.
    49146This is achieved by means of \emph{indexed labels}; all cost labels are decorated with formal indices coming from the loops containing such labels.
    50 These indices allow us to rebuild, even after multiple loop transformations, which iterations of the original loops in the source code a particular label occurrence belongs to.
     147These indices allow us to keep track, even after multiple loop transformations, of which iteration of the original loop in the source code a particular label occurrence belongs to.
    51148During the annotation stage of the source code, this information is presented to the user by means of \emph{dependent costs}.
    52149
    53 We concentrate on integrating the labelling approach with two loop transformations.
    54 For general information on general compiler optimisations (and loop optimisations in particular) we refer the reader to the vast literature on the subject (\eg\cite{muchnick,morgan}).
     150Over the course of this section, we will use two specific types of optimisations to introduce the indexed labelling approach. We argue that these two types pose a good foundation for extending the labelling approach,
     151in order to cover more and more common optimisations, as well as gaining insight into how to integrate advanced cost estimation techniques, such as cache analysis, into the CerCo compiler.
     152Moreover loop peeling itself has the fortuitous property of enhancing and enabling other optimisations.
     153Experimentation with CerCo's untrusted prototype compiler, which implements constant propagation and partial redundancy elimination~\cite{PRE,muchnick}, show how loop peeling enhances those other optimisations.
    55154
    56155\paragraph{Loop peeling}
    57 As already mentioned, loop peeling consists in preceding the loop with a copy of its body, appropriately guarded.
     156Loop peeling consists in preceding the loop with a copy of its body, appropriately guarded.
    58157This is used, in general, to trigger further optimisations, such as those that rely on execution information which can be computed at compile time, but which is erased by further iterations of the loop, or those that use the hoisted code to be more effective at eliminating redundant code.
    59158Integrating this transformation in to the labelling approach would also allow the integration of the common case of cache analysis explained above; the analysis of cache hits and misses usually benefits from a form of \emph{virtual} loop peeling~\cite{cacheprediction}.
     
    62161This optimisation consists of the repetition of several copies of the body of the loop inside the loop itself (inserting appropriate guards, or avoiding them altogether if enough information about the loop's guard is available at compile time).
    63162This can limit the number of (conditional or unconditional) jumps executed by the code and trigger further optimisations dealing with pipelining, if appropriate for the architecture.
    64 \\\\
    65 Whilst we cover only two loop optimisations in this report, we argue that the work presented herein poses a good foundation for extending the labelling approach, in order to cover more and more common optimisations, as well as gaining insight into how to integrate advanced cost estimation techniques, such as cache analysis, into the CerCo compiler.
    66 Moreover loop peeling itself has the fortuitous property of enhancing and enabling other optimisations.
    67 Experimentation with CerCo's untrusted prototype compiler, which implements constant propagation and partial redundancy elimination~\cite{PRE,muchnick}, show how loop peeling enhances those other optimisations.
    68 
    69 \paragraph{Outline}
    70 We will present our approach on a minimal `toy' imperative language, \imp{} with \s{goto}s, which we present in Section~\ref{sec:defimp} along with formal definitions of the loop transformations.
    71 This language already presents most of the difficulties encountered when dealing with \textsc{c}, so we stick to it for the sake of this presentation.
    72 In Section~\ref{sec:labelling} we summarize the labelling approach as presented in~\cite{D2.1}.
    73 Section~\ref{sec:indexedlabels} presents \emph{indexed labels}, our proposal for dependent labels which are able to describe precise costs even in the presence of the various loop transformations we consider.
    74 Finally Section~\ref{sec:conc} goes into more detail regarding the implementation of indexed labels in CerCo's untrusted compiler and speculates on further work on the subject.
    75 
    76 \section{\imp{} with goto}\label{sec:defimp}
    77 We briefly outline the toy language, \imp{} with \s{goto}s.
    78 The language was designed in order to pose problems for the existing labelling approach, and as a testing ground for our new notion of indexed labels.
    79 
    80 The syntax and operational semantics of our toy language are presented in~\ref{fig:minimp}.
    81 Note, we may augment the language further, with \s{break} and \s{continue}, at no further expense.
     163
     164\subsubsection{\imp{} with goto}\label{sec:defimp}
     165We briefly outline a toy language, \imp{} with \s{goto}s.
     166This language was designed in order to pose problems for the existing labelling approach, and as a testing ground for our new notion of indexed labels.
     167
     168The syntax and operational semantics of \imp{} are presented in figure~\ref{fig:minimp}.
     169Note that we can augment the language with \s{break} and \s{continue} statements at no further expense.
     170
    82171\begin{figureplr}
    83172$$\begin{gathered}
     
    146235\label{fig:minimp}
    147236\end{figureplr}
     237
    148238The precise grammar for expressions is not particularly relevant so we do not give one in full.
    149239For the sake of conciseness we also treat boolean and arithmetic expressions together (with the usual \textsc{c} convention of an expression being true iff non-zero).
     
    158248We posit the existence of a suitable notion of `sequential instructions', wherein each instruction has a single natural successor to which we can add our own, for every language $L$ further down the compilation chain.
    159249
    160 \subsection{Loop transformations}
     250\subsubsection{Loop transformations}
    161251We call a loop $L$ \emph{single-entry} in $P$ if there is no \s{goto} to $P$ outside of $L$ which jumps into $L$.\footnote{This is a reasonable aproximation: it defines a loop as multi-entry if it has an external but unreachable \s{goto} jumping into it.}
    162252Many loop optimisations do not preserve the semantics of multi-entry loops in general, or are otherwise rendered ineffective.
     
    264354\end{example}
    265355
    266 \section{Labelling: a quick sketch of the previous approach}
    267 \label{sec:labelling}
    268 Plainly labelled \imp{} is obtained by adding to the code \emph{cost labels} (with metavariables $\alpha,\beta,\ldots$), and cost-labelled statements:
    269 $$
    270 S,T\gramm \cdots \mid \alpha: S
    271 $$
    272 Cost labels allow us to track some program points along the compilation chain.
    273 For further details we refer to~\cite{D2.1}.
    274 
    275 With labels the small step semantics turns into a labelled transition system along with a natural notion of trace (\ie lists of labels) arises.
    276 The evaluation of statements is enriched with traces, so that rules follow a pattern similar to the following:
    277 $$
    278 \begin{array}{lblL}
    279 (\alpha: S, K,s) &\to[\alpha]_P (S,K,s)\\
    280 (\s{skip}, S \cdot K,s) &\to[\varepsilon]_P (S, K, s)\\
    281 & \text{etc.}
    282 \end{array}$$
    283 Here, we identify cost labels $\alpha$ with singleton traces and we use $\varepsilon$ for the empty trace.
    284 Cost labels are emitted by cost-labelled statements only\footnote{In the general case the evaluation of expressions can emit cost labels too (see~\ref{sec:conc}).}.
    285 We then write $\to[\lambda]\!\!^*$ for the transitive closure of the small step semantics which produces by concatenation the trace $\lambda$.
    286 
    287 \paragraph{Labelling}
    288 Given an \imp{} program $P$ its \emph{labelling} $\alpha:\Ell(P)$ in $\ell-\imp$ is defined by putting cost labels after every branching statement, at the start of both branches, and a cost label at the beginning of the program. Also, every labelled statement gets a cost label,
    289 which is a conservative approach to ensuring that all loops have labels inside them, as a loop might be done with \s{goto}s.
    290 The relevant cases are
    291 $$\begin{aligned}
    292   \Ell(\sop{if}e\sbin{then}S\sbin{else}T) &=
    293     \sop{if}e\sbin{then}\alpha:\Ell(S)\sbin{else}\beta:\Ell(T)\\
    294   \Ell(\sop{while}e\sbin{do}S) &=
    295     (\sop{while}e\sbin{do}\alpha:\Ell(S));\beta:\s{skip}\\
    296   \Ell(\ell : S) &=
    297     (\ell : \alpha : \Ell(S))
    298   \end{aligned}$$
    299 where $\alpha,\beta$ are fresh cost labels.
    300 In all other cases the definition just passes to substatements.
    301 
    302 \paragraph{Labels in the rest of the compilation chain}
    303 All languages further down the chain get a new sequential statement $\sop{emit}\alpha$ whose effect is to be consumed in a labelled transition while keeping the same state.
    304 All other instructions guard their operational semantics and do not emit cost labels.
    305 
    306 Preservation of semantics throughout the compilation process is restated, in rough terms, as:
    307 $$
    308 \text{starting state of $P$}\to[\lambda]\!\!^*\;\text{halting state} \iff
    309 \text{starting state of $\mathcal C(P)$} \to[\lambda]\!\!^*\;\text{halting state}
    310 $$
    311 Here $P$ is a program of a language along the compilation chain, starting and halting states depend on the language, and $\mathcal C$ is the compilation function\footnote{The case of divergent computations needs to be addressed too.
    312 Also, the requirement can be weakened by demanding some sort weaker form of equivalence of the traces than equality.
    313 Both of these issues are beyond the scope of this presentation.}.
    314 
    315 \paragraph{Instrumentations}
    316 Let $\mathcal C$ be the whole compilation from $\ell\imp$ to the labelled version of some low-level language $L$.
    317 Supposing such compilation has not introduced any new loop or branching, we have that:
    318 \begin{itemize}
    319 \item
    320 Every loop contains at least a cost label (\emph{soundness condition})
    321 \item
    322 Every branching has different labels for the two branches (\emph{preciseness condition}).
    323 \end{itemize}
    324 With these two conditions, we have that each and every cost label in $\mathcal C(P)$ for any $P$ corresponds to a block of sequential instructions, to which we can assign a constant \emph{cost}\footnote{This in fact requires the machine architecture to be `simple enough', or for some form of execution analysis to take place.}
    325 We therefore may assume the existence of a \emph{cost mapping} $\kappa_P$ from cost labels to natural numbers, assigning to each cost label $\alpha$ the cost of the block containing the single occurrance of $\alpha$.
    326 
    327 Given any cost mapping $\kappa$, we can enrich a labelled program so that a particular fresh variable (the \emph{cost variable} $c$) keeps track of the summation of costs during the execution.
    328 We call this procedure \emph{instrumentation} of the program, and it is defined recursively by:
    329 $$
    330 \mathcal I(\alpha:S) = c \ass c + \kappa(\alpha) ; \mathcal I(S)
    331 $$
    332 In all other cases the definition passes to substatements.
    333 
    334 \paragraph{The problem with loop optimisations}
    335 Let us take loop peeling, and apply it to the labelling of a program without any prior adjustment:
    336 $$
    337 (\sop{while}e\sbin{do}\alpha:S);\beta:\s{skip}
    338 \mapsto
    339 (\sop{if}b\sbin{then} \alpha : S; \sop{while} b \sbin{do} \alpha :
    340 S[\ell'_i/\ell_i]);
    341 \beta:\s{skip}
    342 $$
    343 What happens is that the cost label $\alpha$ is duplicated with two distinct occurrences.
    344 If these two occurrences correspond to different costs in the compiled code, the best the cost mapping can do is to take the maximum of the two, preserving soundness (\ie the cost estimate still bounds the actual one) but losing preciseness (\ie the actual cost could be strictly less than its estimate).
    345 
    346 \section{Indexed labels}
     356\subsubsection{Indexed labels}
    347357\label{sec:indexedlabels}
    348358This section presents the core of the new approach.
     
    364374\end{enumerate}
    365375
    366 \subsection{Indexing the cost labels}
     376\subsubsection{Indexing the cost labels}
    367377\label{ssec:indlabs}
    368378
     
    423433In plainer words: each single-entry loop is indexed by $i_k$ where $k$ is the number of other single-entry loops containing this one, and all cost labels under the scope of a single-entry loop indexed by $i_k$ are indexed by all indices $i_0,\ldots,i_k$, without any transformation.
    424434
    425 \subsection{Indexed labels and loop transformations}\label{ssec:looptrans}
     435\subsubsection{Indexed labels and loop transformations}\label{ssec:looptrans}
    426436We define the \emph{reindexing} $I \circ (i_k\mapsto a*i_k+b)$ as an operator on indexings by setting:
    427437\begin{multline*}
     
    465475Again, the reindexing is as expected: each copy of the unrolled body has its indices remapped so that when they are executed, the original iteration of the loop to which they correspond can be recovered.
    466476
    467 \subsection{Semantics and compilation of indexed labels}
     477\subsubsection{Semantics and compilation of indexed labels}
    468478In order to make sense of loop indices, one must keep track of their values in the state.
    469479A \emph{constant indexing} (metavariables $C,\ldots$) is an indexing which employs only constant simple expressions.
     
    537547In fact, the statement of preservation of semantics does not change at all, if not for considering traces of evaluated indexed cost labels rather than traces of plain ones.
    538548
    539 \subsection{Dependent costs in the source code}
     549\subsubsection{Dependent costs in the source code}
    540550\label{ssec:depcosts}
    541551The task of producing dependent costs from constant costs induced by indexed labels is quite technical.
     
    641651$$
    642652
    643 \subsection{A detailed example}\label{ssec:detailedex}
     653\subsubsection{A detailed example}\label{ssec:detailedex}
    644654Take the program in \autoref{fig:example1}. Its initial labelling will be:
    645655$$\begin{array}{l}
     
    759769\end{equation}
    760770We will see later on \autopageref{pag:continued} how such an expression can be simplified.
    761 \section{Notes on the implementation and further work}
     771
     772\subsection{Notes on the implementation and further work}
    762773\label{sec:conc}
    763774Implementing the indexed label approach in CerCo's untrusted Ocaml prototype does not introduce many new challenges beyond what has already been presented for the toy language, \imp{} with \s{goto}s.
     
    852863This corresponds to a reasonable limitation on the number of times loop unrolling may be applied to the same loop: at most once.
    853864
    854 \paragraph{Further work}
    855 For the time being, indexed labels are only implemented in the untrusted Ocaml compiler, while they are not present yet in the Matita code.
    856 Porting them should pose no significant problem.
    857 Once ported, the task of proving properties about them in Matita can begin.
    858 
    859 Because most of the executable operational semantics of the languages across the frontend and the backend are oblivious to cost labels, it should be expected that the bulk of the semantic preservation proofs that still needs to be done will not get any harder because of indexed labels.
    860 The only trickier point that we foresee would be in the translation of \s{Clight} to \s{Cminor}, where we pass from structured indexed loops to atomic instructions on loop indices.
    861 
    862 An invariant which should probably be proved and provably preserved along the compilation chain is the non-overlap of indexings for the same atom.
    863 Then, supposing cost correctness for the unindexed approach, the indexed one will just need to amend the proof that
    864 $$\forall C\text{ constant indexing}.\forall \alpha\la I\ra\text{ appearing in the compiled code}.
    865   \kappa(\alpha)\circ (I\circ C) = \kappa(\alpha\la I \ra).
    866 $$
    867 Here, $C$ represents a snapshot of loop indices in the compiled code, while $I\circ C$ is the corresponding snapshot in the source code.
    868 Semantics preservation will ensure that when, with snapshot $C$, we emit $\alpha\la I\ra$ (that is, we have $\alpha\la I\circ C\ra$ in the trace), $\alpha$ must also be emitted in the source code with indexing $I\circ C$, so the cost $\kappa(\alpha)\circ (I\circ C)$ applies.
    869 
    870 Aside from carrying over the proofs, we would like to extend the approach to more loop transformations.
    871 Important examples are loop inversion (where a for loop is reversed, usually to make iterations appear to be truly independent) or loop interchange (where two nested loops are swapped, usually to have more loop invariants or to enhance strength reduction).
    872 This introduces interesting changes to the approach, where we would have indexings such as:
    873 $$i_0\mapsto n - i_0\quad\text{or}\quad i_0\mapsto i_1, i_1\mapsto i_0.$$
    874 In particular dependency over actual variables of the code would enter the frame, as indexings would depend on the number of iterations of a well-behaving guarded loop (the $n$ in the first example).
    875 
    876 Finally, as stated in the introduction, the approach should allow some integration of techniques for cache analysis, a possibility that for now has been put aside as the standard 8051 target architecture for the CerCo project lacks a cache.
    877 Two possible developments for this line of work present themselves:
    878 \begin{enumerate}
    879 \item
    880 One could extend the development to some 8051 variants, of which some have been produced with a cache.
    881 \item
    882 One could make the compiler implement its own cache: this cannot apply to \textsc{ram} accesses of the standard 8051 architecture, as the difference in cost of accessing the two types of \textsc{ram} is only one clock cycle, which makes any implementation of cache counterproductive.
    883 So for this proposal, we could either artificially change the accessing cost of \textsc{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.
    884 \end{enumerate}
    885 
    886 \section{Compiler proof}
    887 \label{sect.compiler.proof}
     865%%% HERE BEGINS A NEW BIT
    888866
    889867\section{Introduction}
Note: See TracChangeset for help on using the changeset viewer.