The refinement based approach is a successful technique for the development of verified software. It typically ends with imperative programs (organized in components) together with axiomatic descriptions of data structures and functions in predicate logic. Many projects have used this methodology successfully. One very extensive project is our Flashix project, in which we developed and verified a file system for flash memory.

Specifications and programs use the referentially transparent copy semantics of predicate logic, the weakest precondition calculus for sequential programs, and a rely-guarantee calculus for concurrent programs. To get executable code from such programs, theorem provers typically generate functional programs with immutable data structures.

The resulting code is usually inefficient since destructive updates, that are necessary for the efficient use of e.g. arrays, are not correct in general. In addition, the necessary garbage collection is not possible for applications in operating system kernels, or in real-time applications. These require code that manages memory explicitly, e.g. C-code.

Moving from abstract, referentially transparent data structures to efficient, destructive code is difficult, since explicit information where memory should be allocated or which updates can overwrite is not present.

In previous work we have developed an approach, that translates in a way that keeps all data structures disjoint (unshared) between components, and modifies unshared data structures destructively. Although this leads to a considerable improvement, compared to manually written code, it is still inefficient. An assignment x := y still has to copy the data structure stored in y to preserve disjointness. These copy operations can often be avoided using a careful analysis.

The goal of this project is to develop a systematic data flow analysis that allows the generation of optimal C-Code with a minimum of copy operations, such that the resulting code is as efficient as manually written code. For this, we want to define a specification language with algebraic specifications for abstract data types, as well as concurrent imperative programs. We want to formally specify the core of the data flow analysis and verify that the transformation from the specification language yields correct code without memory leaks.

Partners

Funded by