Concept and project objective(s)
The project aims at the construction of a formally verified complexity preserving compiler from a large subset of C to some typical micro-controller assembly, of the kind traditionally used in embedded systems.
The work comprises the definition of cost models for the input and target languages, and the machine-checked proof of preservation of complexity (concrete, not asymptotic) along compilation. In particular, the compiler will also return tight and certified cost annotations for the source program (expressed in terms of clock-cycles) for program slices with O(1) complexity. It is then up to the user, possibly assisted by automatic tools, to 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 ongoing research on techniques for invariants generation and cost inference for imperative programs, with two additional benefits: the guarantee that the inferred intensional properties will carry over to assembly code; and the adoption of a cost model that is absolutely precise, being induced from the generated assembly language.
The main focus of the current project is on the certified, cost annotating compiler. As for the way cost annotations are used, we shall develop a proof-of-concept prototype, by interfacing to already existing tools, to show how this information can be exploited in a useful manner. We will develop abstract interpretation techniques to infer automatically complexity bounds and, in particular, we will test these techniques on the C code generated by the compilers of synchronous languages, such as Lustre or Esterel.
The major breakthrough of the project is the possibility to give a tight performance estimate for the executable code (for computing platforms such as microcontrollers, not relying on operating systems), a task that is currently regarded as highly visionary in the compiler community. The essential paradigm shift consists in creating the (certified) infrastructure allowing to draw conclusions on the target code, while comfortably reasoning on the source. The compiler will be open source, and all proofs will be public domain.