Changes between Initial Version and Version 1 of Proposal1.1

May 11, 2010, 11:08:58 PM (9 years ago)



  • Proposal1.1

    v1 v1  
     1= Concept and project objective(s) =
     4The project aims at the construction of a formally verified complexity
     5preserving compiler from a large subset of C to some typical micro-controller
     6assembly, of the kind traditionally used in embedded systems.
     8The work comprises the definition of cost models for the input and target
     9languages, and the machine-checked proof of preservation of complexity
     10(concrete, not asymptotic) along compilation. In particular, the compiler
     11will also return tight and certified cost annotations for the source program
     12(expressed in terms of clock-cycles) for program slices with
     13O(1) complexity. It is then up to the user, possibly assisted by automatic tools,
     14to use this (trusted) information to state and to prove precise complexity assertions on the program. To this aim, he can exploit the tools provided by the
     15ongoing research on techniques for invariants generation and cost inference
     16for imperative programs, with two additional benefits: the guarantee that the
     17inferred intensional properties will carry over to assembly code; and the
     18adoption of a cost model that is absolutely precise, being induced from the
     19generated assembly language.
     23The main focus of the current project is on the certified, cost
     24annotating compiler.  As for the way cost annotations are used, we
     25shall develop a proof-of-concept prototype, by interfacing to already
     26existing tools, to show how this information can be exploited in a
     27useful manner. We will develop abstract interpretation techniques to
     28infer automatically complexity bounds and, in particular, we will test
     29these techniques on the C code generated by the compilers of synchronous
     30languages, such as Lustre or Esterel.
     33The major breakthrough of the project is the possibility to give a
     34tight performance estimate for the executable code (for computing
     35platforms such as microcontrollers, not relying on operating systems),
     36a task that is currently regarded as highly visionary in the compiler
     37community. The essential paradigm shift consists in creating the
     38(certified) infrastructure allowing to draw conclusions on the target
     39code, while comfortably reasoning on the source.  The compiler will be
     40open source, and all proofs will be public domain.