# Changeset 3116

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

...

File:
1 edited

### Legend:

Unmodified
 r3114 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 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.). 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. 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.