Changeset 3116 for Deliverables/D6.3

Timestamp:

Apr 10, 2013, 5:07:26 PM (8 years ago)

Author:

sacerdot

Message:

...

File:

• Deliverables/D6.3/report.tex (modified) (4 diffs)

Deliverables/D6.3/report.tex

@@ -238 +238 @@
 We start presenting an idealized model of the execution of a generic
 microprocessor (with caches) that has all interrupts disabled and no I/O
-instructions.
+instructions. We then classify the models according to some properties of
+their cost model. Then we show how to extend the labelling approach of CerCo
+to cover models that are classified in a certain way. 
+
+\paragraph{The microprocessor model}
 
 Let $\sigma,\sigma_1,\ldots$ range over $\Sigma$, the set of the fragments of
@@ -246 +250 @@
 
 Let $\delta,\delta_1,\ldots$ range over $\Delta$, the set of the
-fragments of the microprocessor state that holds the internal state of the
+fragments of the microprocessor state that holds the \emph{internal state} of the
 microprocessor (e.g. the content of the pipeline and caches, the status of
 the branch prediction unit, etc.).
@@ -255 +259 @@
 
 Let $I,I_1,\ldots$ range over $\mathcal{I}$, the
-the set of instructions of the processor and let
-$\gamma,\gamma_1,\ldots$ range over $\Gamma$, the set of operands
+the set of \emph{instructions} of the processor and let
+$\gamma,\gamma_1,\ldots$ range over $\Gamma$, the set of \emph{operands}
 of instructions after the fetching and decoding passes.
-Thus a pair $(I,\gamma)$ represents a decoded instruction and already contains
+Thus a pair $(I,\gamma)$ represents a \emph{decoded instruction} and already contains
 the data required for execution. Execution needs to access the data state only
 to write the result.
@@ -273 +277 @@
 functions:
 \begin{itemize}
- \item The functional transition function $\longleftarrow : \Sigma \to \Sigma$
+ \item The \emph{functional transition} function $\longrightarrow : \Sigma \to \Sigma$
    over data states. This is the only part of the semantics that is relevant
    to functional analysis.
- \item The internal state transition function
-   $\Longleftarrow : \Sigma \times \Delta \to \Delta$ that updates the internal
+ \item The \emph{internal state transition} function
+   $\Longrightarrow : \Sigma \times \Delta \to \Delta$ that updates the internal
    state.
- \item The cost function $K: \mathcal{I} \times \Delta \to \mathbb{N}$ that
-   assigns a cost to transitions. Since decoded instructions hold the data
+ \item The \emph{cost function} $K: \mathcal{I} \times \Gamma \times \Delta \to \mathbb{N}$
+   that assigns a cost to transitions. Since decoded instructions hold the data
    they act on, the cost of an instruction may depend both on the data being
    manipulated and on the internal state.
 \end{itemize}
 
-Given a processor state $(\sigma,\delta)$, the processor evoltes in the
+Given a processor state $(\sigma,\delta)$, the processor evolves in the
 new state $(\sigma',\delta')$ in $n$ cost units if
-$\sigma \longleftarrow \sigma'$ and $(\sigma,\delta) \Longleftarrow \sigma'$
+$\sigma \longrightarrow \sigma'$ and $(\sigma,\delta) \Longrightarrow \delta'$
 and $fetch(\sigma) = (I,\gamma)$ and $K(I,\gamma,\delta) = n$.
+
+An \emph{execution history} is a stream of states and transitions
+$\sigma_0 \longrightarrow \sigma_1 \longrightarrow \sigma_2 \ldots$
+that can be either finite or infinite. Given an execution history, the
+corresponding \emph{execution path} is the stream of program counters
+obtained from the execution history by forgetting all the remaining information.
+The execution path of the history $\sigma_0 \longrightarrow \sigma_1 \longrightarrow \sigma_2 \ldots$ is $pc_0,pc_1,\ldots$ where each $pc_i$ is the program
+counter of $\sigma_i$.
 
 We claim this simple model to be generic enough to cover real world
 architectures.
 
+\paragraph{Classification of cost models}
+A cost function is \emph{exact} if it assigns to transitions the real cost
+incurred. It is \emph{approximated} if it returns an upper bound of the real
+cost.
+
+A cost function is \emph{operand insensitive} if it does not depend on the
+operands of the instructions to be executed. Formally, $K$ is operand insensitive
+if there exists a $K': \mathcal{I} \times \Delta \to \mathbb{N}$ such that
+$K(I,\gamma,\delta) = K'(I,\delta)$. In this case, with an abuse of terminology,
+we will identify $K$ with $K'$.
+
+The cost functions of simple hardware architectures, in particular RISC ones,
+are naturally operand insensitive. In the other cases an exact operand sensitive
+cost function can always be turned into an approximated operand insensitive one
+by taking $K'(I,\delta) = \max\{K(I,\gamma,\delta)~|~\gamma \in \Gamma\}$.
+The question when one performs these approximation is how severe the
+approsimation is. A measure is given by the \emph{jitter}, which is defined
+as the difference between the best and worst cases. In our case, the jitter
+of the approximation $K'$ would be $\max\{K(I,\gamma,\delta)~|~\gamma \in \Gamma\} - \min\{K(I,\gamma,\delta)~|~\gamma \in \Gamma\}$. According to experts
+of WCET analysis, the jitters relative to operand sensitivity in modern
+architectures are small enough to make WCET estimations still useful.
+Therefore, in the sequel we will focus on operand insensitive cost models only.
+
+Note that cost model that are operand insensitive may still have significant
+dependencies over the data manipulated by the instructions, because of the
+dependency over internal states. For example, an instruction that reads data
+from the memory may change the state of the cache and thus greatly affect the
+execution time of successive instructions.
+
+Nevertheless, operand insensitivity is an important property for the labelling
+approach. In~\cite{tranquilli} we introduced \emph{dependent labels} and
+\emph{dependent costs}, which are the possibility of assigning costs to basic
+blocks of instructions which are also dependent on the state of the high level
+program at the beginning of the block. The idea we will now try to pursue is
+to exploit dependent costs to capture cost models that are sensitive to
+the internal states of the microprocessor. Operand sensitivity, however, is
+a major issue in presence of dependent labels: to lift a data sensitive cost
+model from the object code to the source language, we need a function that
+maps high level states to the operands of the instructions to be executed,
+and we need these functions to be simple enough to allow reasoning over them.
+Complex optimizations performed by the compiler, however, make the mappings
+extremely cumbersomes and history dependent. Moreover, keeping
+track of status transformations during compilation would be a significant
+departure from classical compilation models which we are not willing to
+undertake. By assuming or removing operand sensitivity, we get rid of part
+of the problem: we only need to make our costs dependent on the internal
+state of the microprocessor. The latter, however, is not at all visible
+in the high level code. Our next step is to make it visible.
+
+In general, the value of the internal state at a certain point in the program
+history is affected by all the preceding history. For instance, the
+pipeline stages either hold operands of instructions in execution or bubbles
+\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
+object code data which we do not know how to relate simply to the source code
+data. We therefore introduce a new classification. 
+
+A \emph{view} over internal states is a pair $(\mathcal{V},|.|)$ where
+$\mathcal{V}$ is a non empty set and $|.|:\Delta \to \mathcal{V}$ is
+a forgetful function over internal states.
+
+The operand insensitive cost function $K$ is \emph{dependent on the view
+$\mathcal{V}$} if there exists a $K': \mathcal{I} \times \mathcal{V} \to \mathbb{N}$ such that $K(I,\delta) = K'(I,|\delta|)$. In this case, with an abuse of terminology, we will identify $K$ with $K'$.
+
+Among the possible views, the ones that we will easily be able to work
+with in the labelling approach are the \emph{execution path dependent views}.
+A view $(\mathcal{V},|.|)$ is execution path dependent when there exists
+a transition function $\hookrightarrow : PC \times \mathcal{V} \to \mathcal{V}$
+such that for all $(\sigma,\delta)$ and $pc$ such that $pc$ is the program
+counter of $\sigma$, $(\sigma,\delta) \Longrightarrow \delta'$ iff
+$(pc,|\delta|) \hookrightarrow |\delta'|$.
+
+As a final definition, we say that a cost function $K$ is
+\emph{data independent} if it is dependent on a view that is execution path
+dependent. In the next paragraph we will show how we can extend the
+labelling approach to deal with data independent cost models.