source: Deliverables/Dissemination/README @ 3287

Last change on this file since 3287 was 2577, checked in by tranquil, 7 years ago

abstract of indexed labels talk

File size: 3.3 KB
2This directory contains documents for the presentation of the project
3in the dissemination workshops and in the final review.
5Each module is supposed to last between 15' and 30', so it should be
6supported by a set of 15-30 slides and possibly by a short demo.
8Not all modules need to be presented each time.
12Abstract (*To come (Bologna?)*)
15The labelling approach to certified cost annotations.
17We present a so-called labelling method to enrich a compiler in order
18to turn it into a ``cost annotating compiler'', that is, a compiler
19which can ``lift'' pieces of information on the execution cost of the
20object code as cost annotations on the source code. These cost
21annotations characterize the execution costs of code fragments of
22constant complexity.  First, we provide a proof methodology that
23extends standard simulation proofs of compiler correctness to ensure
24that the cost annotations on the source code are sound and precise
25with respect to an execution cost model of the object code.  Second,
26we demonstrate that our label-based instrumentation is scalable
27because it consists in a modular extension of the compilation
28chain. To that end, we report our successful experience in
29implementing and testing the labelling approach on top of a prototype
30compiler written in OCAML for (a large fragment of) the C language.
33Reasoning on cost annotations of C programms.
35We provide evidence for the usability of the generated cost
36annotations as a mean to reason on the concrete complexity of programs
37written in C. For this purpose, we present a Frama-C plugin that uses
38our cost annotating compiler to automatically infer trustworthy logic
39assertions about the concrete worst case execution cost of programs
40written in a fragment of the C language. These logic assertions are
41synthetic in the sense that they characterize the cost of executing
42the entire program, not only constant-time fragments. (These bounds
43may depend on the size of the input data.) We report our
44experimentations on some C programs, including programs generated by a
45compiler for the synchronous programming language Lustre used in
46critical embedded software.
50Targeting more advanced optimisations: indexed labelling.
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
63Certifying and reasoning on cost annotations of functional programs.
65We design a labelling method to insert cost annotations in a
66higher-order functional program, to certify their correctness with
67respect to a standard, typable compilation chain to assembly code
68including safe memory management, and to reason about them in a
69higher-order Hoare logic.
70Slides: funcca-slide.pdf
73Compiler certification in Matita (tentative title, add more modules if needed...)
74Abstract (*To come (Edinburgh/Bologna?)*)
Note: See TracBrowser for help on using the repository browser.