2019-01398 - Post-Doctoral Research Visit F/M - "Abstract Machine for Linux I/O scheduling"
Le descriptif de l’offre ci-dessous est en Anglais

Type de contrat : CDD de la fonction publique

Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Post-Doctorant

Contexte et atouts du poste

The ANR VeriAMOS project will attack the problem of verifying a class of Operating Systems services thanks to both Domain Specific Languages (DSL) and static analyzers. We will investigate whether the restricted expressiveness and the higher level of abstraction provided by the use of a DSL will make it possible to design static analyzers that can statically and fully automatically verify important classes of semantic properties on OS code, while retaining adequate performance of the OS service.

The VeriAMOS project is involving researchers from INRIA - Antique team, Whisper team, and UGA-LIG - Erods team.

Mission confiée

The goal of the project to design a high-level, expressive DSL targeting the needs of I/O scheduling policies and it's implementation on top of a verified abstract machine. The approach will be first applied to the scheduling of I/Os for Solid-State Drives.  The DSL compiler will generate C programs that use the primitives of the abstract machine. C generated code from the DSL and the abstract machine code will have to be verifiable by a static analyzer designed by the Antique team.

Principales activités

The postdoc fellow will be in charge of the design of the abstract machine, and it's implementation within the Linux kernel. This work will be carry on in coordination with the others project partners to support the execution of the C-code generated from the DSL programs and the verification of the C implementation.

 

 

Compétences


*Required expertise and interests*

An experience in programming at the Linux kernel level is required. Interest or experience in program verification or static analysis is welcome.

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

Rémunération

  • Gross Salary per month: 2 653€ brut/mensuel