2019-01398 - Post-Doctoral Research Visit F/M - "Abstract Machine for Linux I/O scheduling"

Contract type : Public service fixed-term contract

Level of qualifications required : PhD or equivalent

Fonction : Post-Doctoral Research Visit

Context

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.

Assignment

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.

Main activities

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.

 

 

Skills


*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.

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

Remuneration

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