- Feb 15, 2011, 10:44:32 AM (6 years ago)
- 1 edited
r512 r513 102 102 In 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. 103 103 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. 104 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. 105 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. 106 Ideally, we would like to have a compositional cost model that assigns the same cost to all occurrences of one instruction. 107 However, 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. 108 Therefore both the cost model and intensional specifications are affected by the compilation process. 115 109 116 110 In the EU Project CerCo (Certified Complexity) we will approach the problem
Note: See TracChangeset for help on using the changeset viewer.