Nested atomic sections with thread escape: Compilation to threads and locks

International audienceFor the sake of modularity, programming languages with atomic sections should offer nesting and inner parallelism in such sections. The possible escape of a thread created inside a section makes these languages also more expressive. In this paper we address the compilation of such a language towards a language with threads and locks. The design decisions of this compilation pass and of the target language were made with respect to the ultimate goal of a mechanised proof of semantic preservation