Monotonous multi-thread programming (with potential PhD continuation)

This internship takes place in the context of a collaboration with Airbus on the topic of safe and efficient parallelization of critical embedded control software onto multi-cores. 

Scientific context:

Mastering concurrency is difficult, and yet hardware design resolutely moves towards increasingly massive parallelism based on the use of chip-multiprocessors. Threads are one of the major programming paradigms for such multi-/many-core systems. They arguably provide the best portability and the finest control over resource allocation. This explains why threads are the only concurrency model integrated in the C language (as part of the C11 standard revision), which in turn established C11 as the preferred programming model for defining the semantics of low-level shared-memory parallelism, and then for providing mechanized proof apparatus.

But the expressiveness of C11 threads comes at a price. As a model of computation, threads are wildly non-deterministic and non-compositional, making both programming and formal analysis difficult. The intrinsic complexity of shared memory parallelism is compounded in C11 by the behavior of weakly-consistent memory models, which is represented at language level to allow the writing of efficient code without resorting to external annotations. As a consequence, C11 allows for counter-intuitive behaviors like the production of out-of-thin-air values. All these reasons explain why multi-threaded software is often bug-ridden even in the context of critical systems.

Large, ambitious research projects such as VST (Verified Software Toolchain) or DeepSpec have been enacted to build the methods and the (formal and software) tools supporting the design of correct multi-threaded software. However, while formally-verified software is mostly needed in domain-specific applications, projects such as VST focused on general-purpose concurrency constructs, like semaphores and critical sections. Programming such domain-specific systems with semaphores and critical sections is often inefficient and cumbersome.

Our proposal targets a large class of domain-specific applications where concurrency is constrained, providing strong monotony and determinism properties. Such is the case in embedded control, in machine learning, or in automatically-parallelized software... A typical example is that of parallelized avionics software. In this case, the use of low-level, fine-grain synchronization allows achieving both the strict safety guarantees required by the industry and a highly efficient use of various multi-cores (based on Kalray, Power, or ARM architecture).

Contact:

More information on the internship offer can be obtained by contacting dumitru.potop@inria.fr, jean-marie.madiot@inria.fr, or pierre.courtieu@cnam.fr.

Assignments:

The objective of this intership is to formally define a restriction of the general C11 concurrency model that exhibits strong monotony and determinism properties. Previous work on our state-of-the-art parallelization toolflow has already identified synchronization primitives and a software organization that support efficient and safe code generation for large-scale avionics applications. This internship will focus on:

• Formalizing sufficient properties ensuring that the execution of a multi-thread program is monotonous and deterministic (and data race-free, serializable...). These properties must be amenable to low-cost verification by means of static analysis. They will define our monotonous and deterministic sub-set of concurrent C11.
• Exploring the mechanization of the semantics of our concurrent C11 sub-set in the framework of concurrent separation logic (CSL) while maintaining compatibility with the sequential semantics of CompCert.

The developments will be evaluated on parallelized avionics software produced by our state-of-the-art parallellization toolflow.

Main activities :

• State of the art analysis
• Formalization of the sufficient properties identifying our concurrent C11 sub-set.
• Exploring the mechanization of the semantics in the framework of CSL.
• Contributing to writing a paper on the topic

Languages : proficiency in either French or English

• 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 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