# Changeset 518

Ignore:
Timestamp:
Feb 15, 2011, 3:05:02 PM (6 years ago)
Message:

small changes

File:
1 edited

### Legend:

Unmodified
 r517 However, if we consider intensional properties of programs---such as space, time or energy spent into computation and transmission of data---the situation is more complex. To express even be able to express these properties, and to be able to reason about them, we are forced to adopt a cost model that assigns a cost to single, or blocks, of instructions. To even be able to express these properties, and to be able to reason about them, we are forced to adopt a cost model that assigns a cost to single, or blocks, of instructions. Ideally, we would like to have a compositional cost model that assigns the same cost to all occurrences of one instruction. However, compiler optimisations are inherently non-compositional: each occurrence of a high level instruction is usually compiled in a different way according to the context it finds itself in. Therefore both the cost model and intensional specifications are affected by the compilation process. In the current EU Project CerCo (Certified Complexity') we approach the problem of reasoning about intensional properties of programs as follows. In the current EU project CerCo (Certified Complexity') we approach the problem of reasoning about intensional properties of programs as follows. We are currently developing a compiler that induces a cost model on the high level source code. Costs are assigned to each block of high level instructions by considering the costs of the corresponding blocks of compiled object code. The cost model is therefore inherently non compositional. The cost model is therefore inherently non-compositional. However, the model has the potential to be extremely \emph{precise}, capturing a program's \emph{realistic} cost, by taking into account, not ignoring, the compilation process. A prototype compiler, where no approximation of the cost is provided, has been developed. With modern processors, though possible~\cite{??,??,??}, it is difficult to compute exact costs or to reasonably approximate them. This is because the execution of a program itself has an influence on the speed of processing. For instance, caching and memory effects in the processor are used in advanced features such as branch prediction. For instance, caching, memory effects and other advanced features such as branch prediction all have a profound effect on execution speeds. For this reason CerCo decided to focus on 8-bit microprocessors. These are still widely used in embedded systems, and have the advantage of an easily predictable cost model due to the relative sparcity of features that they possess.