Changeset 518


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

small changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r517 r518  
    102102
    103103However, 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.
    104 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.
     104To 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.
    105105Ideally, we would like to have a compositional cost model that assigns the same cost to all occurrences of one instruction.
    106106However, 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.
    107107Therefore both the cost model and intensional specifications are affected by the compilation process.
    108108
    109 In the current EU Project CerCo (`Certified Complexity') we approach the problem of reasoning about intensional properties of programs as follows.
     109In the current EU project CerCo (`Certified Complexity') we approach the problem of reasoning about intensional properties of programs as follows.
    110110We are currently developing a compiler that induces a cost model on the high level source code.
    111111Costs are assigned to each block of high level instructions by considering the costs of the corresponding blocks of compiled object code.
    112 The cost model is therefore inherently non compositional.
     112The cost model is therefore inherently non-compositional.
    113113However, 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.
    114114A prototype compiler, where no approximation of the cost is provided, has been developed.
     
    127127With modern processors, though possible~\cite{??,??,??}, it is difficult to compute exact costs or to reasonably approximate them.
    128128This is because the execution of a program itself has an influence on the speed of processing.
    129 For instance, caching and memory effects in the processor are used in advanced features such as branch prediction.
     129For instance, caching, memory effects and other advanced features such as branch prediction all have a profound effect on execution speeds.
    130130For this reason CerCo decided to focus on 8-bit microprocessors.
    131131These 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.
Note: See TracChangeset for help on using the changeset viewer.