Changeset 2577 for Deliverables
- Timestamp:
- Jan 11, 2013, 5:00:57 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/Dissemination/README
r2567 r2577 48 48 49 49 Module: 50 Targeting more advanced optimisations: indexed labelling (tentative title). 51 Abstract (* To come (Bologna?)*) 50 Targeting more advanced optimisations: indexed labelling. 51 Abstract 52 We present an extension to the labelling approach. The original approach looses 53 preciseness when differences arise as to the cost of the same portion of code, 54 whether due to code transformation such as loop optimisations or advanced 55 architecture features (e.g. cache). We propose to address this weakness by 56 formally indexing cost labels with the iterations of the containing loops they 57 occur in. These indexes can be transformed during the compilation, and when 58 lifted back to source code they produce dependent costs. 59 The proposed changes have been implemented in CerCo's untrusted prototype 60 compiler. 52 61 53 Module: 62 Module: 54 63 Certifying and reasoning on cost annotations of functional programs. 55 64 Abstract
Note: See TracChangeset
for help on using the changeset viewer.