Indexed Labels for Loop Iteration Dependent Costs
Paolo Tranquilli (DISI -- Universit\`a di Bologna Alma Mater)

TL;DR
This paper introduces indexed labels for loop iteration-dependent costs, enhancing the precision of resource consumption analysis in source code by accounting for loop iterations and transformations.
Contribution
It extends the labeling approach with formal loop iteration indexing, enabling more accurate cost analysis during compilation and source code lifting.
Findings
Implemented in CerCo's compiler for C to 8051 assembly.
Improves precision of resource analysis in the presence of code transformations.
Addresses weaknesses of previous labeling methods with formal indexing.
Abstract
We present an extension to the labelling approach, a technique for lifting resource consumption information from compiled to source code. This approach, which is at the core of the annotating compiler from a large fragment of C to 8051 assembly of the CerCo project, looses preciseness when differences arise as to the cost of the same portion of code, whether due to code transformation such as loop optimisations or advanced architecture features (e.g. cache). We propose to address this weakness by formally indexing cost labels with the iterations of the containing loops they occur in. These indexes can be transformed during the compilation, and when lifted back to source code they produce dependent costs. The proposed changes have been implemented in CerCo's untrusted prototype compiler from a large fragment of C to 8051 assembly.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
