Post-Doctoral Research Visit F/M Source-to-Source Optimization of OCaml Programs
Contract type : Fixed-term contract
Level of qualifications required : PhD or equivalent
Fonction : Post-Doctoral Research Visit
Context
The work is conducted as part of the ANR OptiTrust project.
Assignment
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.
Main activities
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.
Skills
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.
Benefits package
- 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
Remuneration
2788 € gross/month
General Information
- Theme/Domain :
Architecture, Languages and Compilation
Software engineering (BAP E) - Town/city : Strasbourg
- Inria Center : Centre Inria de l'Université de Lorraine
- Starting date : 2024-10-01
- Duration of contract : 1 year
- Deadline to apply : 2024-08-10
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.
Instruction to apply
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Contacts
- Inria Team : CAMUS
-
Recruiter :
Charguéraud Arthur / Arthur.Chargueraud@inria.fr
The keys to success
There you can provide a "broad outline" of the collaborator you are looking for what you consider to be necessary and sufficient, and which may combine :
- tastes and appetencies,
- area of excellence,
- personality or character traits,
- cross-disciplinary knowledge and expertise...
This section enables the more formal list of skills to be completed and 'lightened' (reduced) :
- "Essential qualities in order to fulfil this assignment are feeling at ease in an environment of scientific dynamics and wanting to learn and listen."
- " Passionate about innovation, with expertise in Ruby on Rails development and strong influencing skills. A thesis in the field of **** is a real asset."
Concretely, the candidate will contribute to the OptiTrust code base, which is implemented in OCaml. The work should lead to the writing and presentation of research papers on the work produced.
About Inria
Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.