Changeset 513


Ignore:
Timestamp:
Feb 15, 2011, 10:44:32 AM (6 years ago)
Author:
mulligan
Message:

more changes to intro

File:
1 edited

Legend:

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

    r512 r513  
    102102In particular, much attention has been placed on verifying compiler correctness with respect to extensional properties of programs, which are easily preserved during compilation; it is sufficient to completely preserve the denotational semantics of the input program.
    103103
    104 The situation is definitely more complex when we also take in account
    105 intesional properties of programs, like space, time or energy spent into
    106 computation and transmission of data. To express this properties and to
    107 reason on them we are forced to adopt a cost model that assigns a cost to
    108 single instructions or to blocks of instructions. Morally, we would like to
    109 have a compositional cost model that assigns the same cost to all occurrences
    110 of one instruction. However, compiler optimizations are inherently non
    111 compositional: each occurrence of an high level instruction is usually compiled
    112 in a different way according to the surrounding instructions. Hence the cost
    113 model is affected by compilation and thus all intensional specifications are as
    114 well.
     104However, 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.
     105To 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.
     106Ideally, we would like to have a compositional cost model that assigns the same cost to all occurrences of one instruction.
     107However, compiler optimizations 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.
     108Therefore both the cost model and intensional specifications are affected by the compilation process.
    115109
    116110In the EU Project CerCo (Certified Complexity) we will approach the problem
Note: See TracChangeset for help on using the changeset viewer.