Changeset 3208


Ignore:
Timestamp:
Apr 29, 2013, 3:36:37 PM (4 years ago)
Author:
sacerdot
Message:

Final version.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D6.3/pipelines.tex

    r3207 r3208  
    4848also depends on the internal state of stateful hardware components that are
    4949designed to optimize the average case. Pipelines, caches, branch predictors are
    50 tipical examples of components that have no impact on the functional behavior
     50typical examples of components that have no impact on the functional behavior
    5151of the code, but that greatly augment the code performance.
    5252
     
    6868and in traditional WCET. Only the latter can deal with modern hardware.
    6969Section~\ref{static2} contains the new material. We revise our static analysis
    70 and the labelling approach in general to accomodate modern hardware.
     70and the labelling approach in general to accommodate modern hardware.
    7171Temporary conclusions are found in Section~\ref{conclusions}.
    7272
     
    7777\begin{itemize}
    7878 \item There is a lot of recent and renewed activity in the formal method
    79    community to accomodate resource analysis using techniques derived from
     79   community to accommodate resource analysis using techniques derived from
    8080   functional analysis (type systems, logics, abstract interpretation,
    8181   amortized analysis applied to data structures, etc.)
     
    140140functional and non functional invariants. This is what we attempted with
    141141the CerCo Cost Annotating Frama-C Plug-In. The Frama-C architecture allows
    142 several plug-ins to perform all kind of static analisys on the source code,
     142several plug-ins to perform all kind of static analysis on the source code,
    143143reusing results from other plug-ins and augmenting the source code with their
    144144results. The techniques are absolutely not limited to linear algebra and
     
    280280by taking $K'(I,\delta) = \max\{K(I,\gamma,\delta)~|~\gamma \in \Gamma\}$.
    281281The question when one performs these approximation is how severe the
    282 approsimation is. A measure is given by the \emph{jitter}, which is defined
     282approximation is. A measure is given by the \emph{jitter}, which is defined
    283283as the difference between the best and worst cases. In our case, the jitter
    284284of the approximation $K'$ would be $\max\{K(I,\gamma,\delta)~|~\gamma \in \Gamma\} - \min\{K(I,\gamma,\delta)~|~\gamma \in \Gamma\}$. According to experts
     
    305305and we need these functions to be simple enough to allow reasoning over them.
    306306Complex optimizations performed by the compiler, however, make the mappings
    307 extremely cumbersomes and history dependent. Moreover, keeping
     307extremely cumbersome and history dependent. Moreover, keeping
    308308track of status transformations during compilation would be a significant
    309309departure from classical compilation models which we are not willing to
     
    316316history is affected by all the preceding history. For instance, the
    317317pipeline stages either hold operands of instructions in execution or bubbles
    318 \footnote{A bubble is formed in the pipeline stage $n$ when an instruction is stucked in the pipeline stage $n-1$, waiting for some data which is not available yet.}. The execution history contains data states that in turn contain the
     318\footnote{A bubble is formed in the pipeline stage $n$ when an instruction is stuck in the pipeline stage $n-1$, waiting for some data which is not available yet.}. The execution history contains data states that in turn contain the
    319319object code data which we do not know how to relate simply to the source code
    320320data. We therefore introduce a new classification.
     
    351351be executed.
    352352
    353 The reference to execution historys in the names is due to the following
     353The reference to execution histories in the names is due to the following
    354354fact: every execution history dependent transition function $\hookrightarrow$
    355355can be lifted to the type $EP \times \mathcal{V} \to \mathcal{V}$ by folding
     
    406406$\hookrightarrow : PC^n \times \{0,1\}^n \to \{0,1\}^n$.
    407407
    408 While the model is a bit simplicistic, it can nevertheless be used to describe
     408While the model is a bit simplicist, it can nevertheless be used to describe
    409409existing pipelines. It is also simple to be convinced that the same model
    410410also captures static branch prediction: speculative execution of conditional
    411411jumps is performed by always taking the same branch which does not depend on
    412 the execution history. In order to take in account jumpt predictions based on
     412the execution history. In order to take in account jump predictions based on
    413413the execution history, we just need to incorporate in the status and the view
    414414statistical informations on the last executions of the branch.
     
    457457pipeline stages.
    458458
    459 The first imporant theorem in the labelling approach is the correctness of the
     459The first important theorem in the labelling approach is the correctness of the
    460460static analysis: if the (dependent) cost associated to a label $L$ is $k$,
    461461then executing a program from the beginning of the basic block to the end
     
    537537  $(L_1,L_2,v) \hookrightarrow v'$ unless $L_1$ is \texttt{NULL}.
    538538  In that case \texttt{(\_\_next(NULL,}$L$\texttt{)} = $v_0$ where
    539   $v_0 = |\delta_0|$ and $\delta_0$ is the initial value of the internal stat
     539  $v_0 = |\delta_0|$ and $\delta_0$ is the initial value of the internal state
    540540  at the beginning of program execution.
    541541 
     
    548548
    549549\paragraph{An example of instrumentation in presence of a pipeline}
    550 In Figure~\ref{factprogi} we show how the instrumentationof a program
     550In Figure~\ref{factprogi} we show how the instrumentation of a program
    551551that computes the factorial of 10 would look like in presence of a pipeline.
    552552The instrumentation has been manually produced. The \texttt{\_\_next}
     
    667667   A more refined possibility consists in approximating the output only on
    668668   those labels whose jitter is small or for those that mark basic blocks
    669    that are executed only a small number of times. By simplyfing the
     669   that are executed only a small number of times. By simplifying the
    670670   \texttt{\_\_next} function accordingly, it is possible to considerably
    671671   reduce the search space for automated provers.
     
    675675   approximations. For example, if it is known that a loop can be executed at
    676676   most 10 times, computing the cost of 10 iterations yields a
    677    better bound than multiplying by 10 the worst case of a single interation.
     677   better bound than multiplying by 10 the worst case of a single interaction.
    678678
    679679   We clearly can do the same on the source level.
     
    710710execution timing is \emph{execution path dependent} (our terminology).
    711711
    712 We have already seen that we are able to accomodate in the labelling approach
     712We have already seen that we are able to accommodate in the labelling approach
    713713cost functions that are dependent on views that are execution path dependent.
    714714Before fully embracing the PROARTIS vision,
     
    731731negligible probability. Therefore, it becomes no longer interesting to estimate
    732732the actual worst case bound. What becomes interesting is to plot the probability
    733 that the execution time will exceed a certain treshold. For all practical
     733that the execution time will exceed a certain threshold. For all practical
    734734purposes, a program that misses its deadline with a negligible probability
    735735(e.g. $10^-9$ per hour of operation) will be perfectly acceptable when deployed
     
    744744based on measurements and it is justified by the following assumption: if
    745745the probabilities associated to every hardware operation are all independent
    746 and identically distributed, then measuring the fime spent on full runs of
     746and identically distributed, then measuring the time spent on full runs of
    747747sub-systems components yields a probabilistic estimate that remains valid
    748748when the sub-system is plugged in a larger one. Moreover, the probabilistic
     
    782782that of natural numbers to any group. Moreover, by imposing labels after
    783783every function call, commutativity can be dropped and the approach works on
    784 every monoid (usually called \emph{cost monoids} in the litterature).
     784every monoid (usually called \emph{cost monoids} in the literature).
    785785Because random variables and convolutions form a monoid, we immediately have
    786786that the labelling approach extends itself to SPTA. The instrumented code
     
    835835$2^n$: a view can usually just be represented by a word. This is not the
    836836case for the views on caches, which are in principle very large. Therefore,
    837 the dependent labelling approach for data indepedent cost functions that we
     837the dependent labelling approach for data independent cost functions that we
    838838have presented here could still be unpractical for caches. If that turns out
    839839to be the case, a possible strategy is the use of abstract interpretations
     
    858858We achieve this in CerCo by designing a certified Cost Annotating Compiler that
    859859keeps tracks of transformations of basic blocks, in order to create a
    860 correspondence (not necessaritly bijection) between the basic blocks of the
     860correspondence (not necessarily bijection) between the basic blocks of the
    861861source and target language. We then prove that the sequence of basic blocks
    862862that are met in the source and target executions is correlated. Then,
Note: See TracChangeset for help on using the changeset viewer.