Post-Doctoral Research Visit F/M Source-to-Source Optimization of OCaml Programs
Type de contrat : CDD
Niveau de diplôme exigé : Thèse ou équivalent
Fonction : Post-Doctorant
Contexte et atouts du poste
The work is conducted as part of the ANR OptiTrust project.
Mission confiée
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.
Principales activités
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.
Compétences
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.
Avantages
- 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
Rémunération
2788 € gross/month
Informations générales
- Thème/Domaine :
Architecture, langages et compilation
Ingénierie logicielle (BAP E) - Ville : Strasbourg
- Centre Inria : Centre Inria de l'Université de Lorraine
- Date de prise de fonction souhaitée : 2024-10-01
- Durée de contrat : 1 an
- Date limite pour postuler : 2024-08-10
Attention: Les candidatures doivent être déposées en ligne sur le site Inria. Le traitement des candidatures adressées par d'autres canaux n'est pas garanti.
Consignes pour postuler
Sécurité défense :
Ce poste est susceptible d’être affecté dans une zone à régime restrictif (ZRR), telle que définie dans le décret n°2011-1425 relatif à la protection du potentiel scientifique et technique de la nation (PPST). L’autorisation d’accès à une zone est délivrée par le chef d’établissement, après avis ministériel favorable, tel que défini dans l’arrêté du 03 juillet 2012, relatif à la PPST. Un avis ministériel défavorable pour un poste affecté dans une ZRR aurait pour conséquence l’annulation du recrutement.
Politique de recrutement :
Dans le cadre de sa politique diversité, tous les postes Inria sont accessibles aux personnes en situation de handicap.
Contacts
- Équipe Inria : CAMUS
-
Recruteur :
Charguéraud Arthur / Arthur.Chargueraud@inria.fr
L'essentiel pour réussir
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.
A propos d'Inria
Inria est l’institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l’interface d’autres disciplines. L’institut fait appel à de nombreux talents dans plus d’une quarantaine de métiers différents. 900 personnels d’appui à la recherche et à l’innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start-up. L'institut s'efforce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.