Post-Doctoral Research Visit F/M Source-to-Source Optimization of OCaml Programs

The work is conducted as part of the ANR OptiTrust project.

The OCaml programming language encourages development with a high degree of
modularity and abstraction. It therefore leads to higher productivity, higher
code reuse, and fewer bugs. Moreover, thanks to its simple semantics, OCaml
code lends itself better to formal verification.

The downside of programming at a high level of modularity and abstraction is
that these aspects generally hinder code optimization. The OCaml compiler
extension called "F-lambda" performs a number of inlining steps in order to
facilitate further optimizations. Yet, it is guided by heuristics, and falls
short of performing advanced optimizations. Besides, the C++ approach of
using templates for static code specialization is associated with numerous
limitations, such as complexity in the source code, blow-up in the size of
the generated code and its compilation time, and issues with understandability
of error messages.

We would like to devise an approach that allows programmer to explicitly guide
the application of series of advanced optimizations. This approach would allow
refining high-level code down to high-performance code. Concretely, each
optimization would take the form of a source-to-source transformation.
At each step, the programmer would get feedback in the form of human-readable
code.

This approach of user-guided source-to-source transformations is already
implemented as part of the OptiTrust framework, which currently applies only
to C code, but internally relies on an imperative lambda-calculus very close
to OCaml.  For certain optimizations, their correctness is verified by means
of lightweight Separation Logic assertions, which accompany the code.

The aim of this project is to generalize the OptiTrust framework to operate on
OCaml code, and to extend the framework with transformations relevant for
ML-style programs. A possible extension to the project consists of developing
refinements from OCaml functions down to optimized C implementations of these
functions.

The concrete plan for the postdoc is as follows.

1. Extend OptiTrust to input and output OCaml syntax.

2. Implement source-to-source transformations relevant for optimizing OCaml
   programs, such as inlining, specialization, simplification of pattern
   matching, elimination of avoidable allocations, removing of indirections
   on records, refinement of data constructors e.g. to generalize from unary
   to n-ary list cells.

3. Apply the approach to case studies, such as optimization of the buckets
   of a hashtable, compilation of higher-order iterators into tight loop
   nests, specialization of the 'Sek' sequence data structure.

4. Demonstrate the possibility to refine allocation-free OCaml functions
   down to C code, with generation of C-bindings. Demonstrate the possibility
   of producing high-performance vectorized C code, e.g. for loops processing
   numeric data. An interesting case study would be the compilation of code
   from the Catala DSL, via OCaml, down to optimized C code.

The candidate must:
- be fluent in OCaml programming;
- be familiar with the notions of AST, and of semantics;
- be familiar with programs logics, in particular logical invariants;
- have knowledge of C programming.

• Subsidized meals
• Partial reimbursement of public transport costs
• Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
• Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
• Professional equipment available (videoconferencing, loan of computer equipment, etc.)
• Social, cultural and sports events and activities
• Access to vocational training
• Social security coverage

2788 € gross/month