Changeset 2577


Ignore:
Timestamp:
Jan 11, 2013, 5:00:57 PM (7 years ago)
Author:
tranquil
Message:

abstract of indexed labels talk

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/Dissemination/README

    r2567 r2577  
    4848
    4949Module:
    50 Targeting more advanced optimisations: indexed labelling (tentative title).
    51 Abstract (* To come (Bologna?)*)
     50Targeting more advanced optimisations: indexed labelling.
     51Abstract
     52We present an extension to the labelling approach. The original approach looses
     53preciseness when differences arise as to the cost of the same portion of code,
     54whether due to code transformation such as loop optimisations or advanced
     55architecture features (e.g. cache). We propose to address this weakness by
     56formally indexing cost labels with the iterations of the containing loops they
     57occur in. These indexes can be transformed during the compilation, and when
     58lifted back to source code they produce dependent costs.
     59The proposed changes have been implemented in CerCo's untrusted prototype
     60compiler.
    5261
    53 Module: 
     62Module:
    5463Certifying and reasoning on cost annotations of functional programs.
    5564Abstract
Note: See TracChangeset for help on using the changeset viewer.