Certifying cost annotations in compilers
Roberto M. Amadio (PPS), Nicolas Ayache (PPS, INRIA Paris -, Rocquencourt), Yann R\'egis-Gianas (PPS, INRIA Paris - Rocquencourt), Ronan, Saillard (PPS, INRIA Paris - Rocquencourt)

TL;DR
This paper introduces a labelling approach for building compilers that can reliably lift execution cost information from object code to source code, demonstrating its effectiveness through formal analysis and practical implementation.
Contribution
It proposes a novel labelling method for cost annotations in compilers, emphasizing compositionality, soundness, and scalability, validated by formal study and prototype implementation.
Findings
Labelling approach shows good compositionality.
Formal analysis supports soundness and precision.
Successful implementation on a C compiler fragment.
Abstract
We discuss the problem of building a compiler which can lift in a provably correct way pieces of information on the execution cost of the object code to cost annotations on the source code. To this end, we need a clear and flexible picture of: (i) the meaning of cost annotations, (ii) the method to prove them sound and precise, and (iii) the way such proofs can be composed. We propose a so-called labelling approach to these three questions. As a first step, we examine its application to a toy compiler. This formal study suggests that the labelling approach has good compositionality and scalability properties. In order to provide further evidence for this claim, we report our successful experience in implementing and testing the labelling approach on top of a prototype compiler written in OCAML for (a large fragment of) the C language.
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.
Taxonomy
TopicsSoftware Engineering Research · Logic, programming, and type systems · Formal Methods in Verification
