Certifying and reasoning on cost annotations in C programs

Nicolas Ayache 1 Roberto Amadio 1 Yann Régis-Gianas 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : We present a so-called labelling method to enrich a compiler in order to turn it into a ''cost annotating compiler'', that is, a compiler which can {\em lift} pieces of information on the execution cost of the object code as cost annotations on the source code. These cost annotations characterize the execution costs of code fragments of constant complexity. The first contribution of this paper is a proof methodology that extends standard simulation proofs of compiler correctness to ensure that the cost annotations on the source code are sound and precise with respect to an execution cost model of the object code. As a second contribution, we demonstrate that our label-based instrumentation is scalable because it consists in a modular extension of the compilation chain. To that end, 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 {\sc C} language. As a third and last contribution, we provide evidence for the usability of the generated cost annotations as a mean to reason on the concrete complexity of programs written in {\sc C}. For this purpose, we present a {\sc Frama-C} plugin that uses our cost annotating compiler to automatically infer trustworthy logic assertions about the concrete worst case execution cost of programs written in a fragment of the {\sc C} language. These logic assertions are synthetic in the sense that they characterize the cost of executing the entire program, not only constant-time fragments. (These bounds may depend on the size of the input data.) We report our experimentations on some {\sc C} programs, especially programs generated by a compiler for the synchronous programming language {\sc Lustre} used in critical embedded software.
Type de document :
Communication dans un congrès
FMICS 2012 - 17th International Workshop on Formal Methods for Industrial Critical Systems, Aug 2012, Paris, France. 2012
Liste complète des métadonnées

https://hal.inria.fr/hal-00702665
Contributeur : Yann Regis-Gianas <>
Soumis le : jeudi 31 mai 2012 - 11:54:07
Dernière modification le : mardi 11 octobre 2016 - 13:55:43
Document(s) archivé(s) le : jeudi 15 décembre 2016 - 09:26:55

Fichier

ccac-fmics-final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00702665, version 2

Collections

INRIA | PPS | USPC

Citation

Nicolas Ayache, Roberto Amadio, Yann Régis-Gianas. Certifying and reasoning on cost annotations in C programs. FMICS 2012 - 17th International Workshop on Formal Methods for Industrial Critical Systems, Aug 2012, Paris, France. 2012. <hal-00702665v2>

Partager

Métriques

Consultations de
la notice

478

Téléchargements du document

234