# Changeset 3114

Ignore:
Timestamp:
Apr 10, 2013, 9:48:31 AM (4 years ago)
Message:

Some progress on pipelines/caches.

File:
1 edited

### Legend:

Unmodified
 r3113 comparisons on the kind of code used by industry in production systems. The first middle term improvement of CerCo would then consist in this kind of analysis, to support or disprove our expectations. In the case where our of analysis, to support or disprove our expectations. It seems that the newborn TACLe Cost Action (Timing Analysis on Code Level) would be the best framework to achieve this improvement. In the case where our technique remains promising, the next long term improvement would consist in integrating in the Frama-C plug-in ad-hoc analysis and combinations of analysis techniques. \subsection{Static analysis of basic blocks} \subsection{Static analysis of costs of basic blocks} At the beginning of the project we have deliberately decided to focus our attention on the control flow preservation, the cost model propagation and the exploitation of the cost model induced on the high level code. For this reason we have devoted almost no attention to the static analysis of basic blocks. This was achieved by picking a very simple hardware architecture (the 8051 microprocessor family) whose cost model is fully predictable and compositional: the cost of every instruction --- except those that deal with I/O --- is constant, i.e. it does not depend on the machine status. We do not regret this choice because, with the limited amount of man power available in the project, it would have been difficult to also consider this aspect. However, without showing if the approach can scale to most complex architectures, our methodology remains of limited interest for the industry. Therefore, the next important middle term improvement will be the extension of our methodology to cover pipelines and simple caches. We will now present our ideas on how we intend to address the problem. The obvious long term improvement would be to take in consideration multicores system and complex memory architectures like the ones currently in use in networks on chips. The problem of execution time analysis for these systems is currently considered extremely hard or even unfeasible and at the moments it seems unlikely that our methodology could contribute to the solution of the problem. \subsubsection{Static analysis of costs of basic blocks revisited} We will now describe what currently seems to be the most interesting technique for the static analysis of the cost of basic blocks in presence of complex hardware architectures that do not have non compositional cost models. 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. Let $\sigma,\sigma_1,\ldots$ range over $\Sigma$, the set of the fragments of the microprocessor states that hold the program counter, the program status word and all the data manipulated by the object code program, i.e. registers and memory cells. We call these fragments the \emph{data states}. Let $\delta,\delta_1,\ldots$ range over $\Delta$, the set of the fragments of the microprocessor state that holds the internal state of the microprocessor (e.g. the content of the pipeline and caches, the status of the branch prediction unit, etc.). The internal state of the microprocessor influences the execution cost of the next instruction, but it has no effect on the functional behaviour of the processor. The whole state of the processor is represented by a pair $(\sigma,\delta)$. 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 of instructions after the fetching and decoding passes. Thus a pair $(I,\gamma)$ represents a decoded instruction and already contains the data required for execution. Execution needs to access the data state only to write the result. Let $fetch: \Sigma \to \mathcal{I} \times \Gamma$ be the function that performs the fetching and execution phases, returning the decoded instruction ready for execution. This is not meant to be the real fetch-decode function, that exploits the internal state too to speed up execution (e.g. by retrieving the instruction arguments from caches) and that, in case of pipelines, works in several stages. However, such a function exists and it is observationally equivalent to the real fetch-decode. We capture the semantics of the microprocessor with the following set of functions: \begin{itemize} \item The functional transition function $\longleftarrow : \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 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 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 new state $(\sigma',\delta')$ in $n$ cost units if $\sigma \longleftarrow \sigma'$ and $(\sigma,\delta) \Longleftarrow \sigma'$ and $fetch(\sigma) = (I,\gamma)$ and $K(I,\gamma,\delta) = n$. We claim this simple model to be generic enough to cover real world architectures. \end{document}