Skip to Main content Skip to Navigation
Conference papers

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

Frédéric Dabrowski 1 Frédéric Loulergue 2, 3, 1 Thomas Pinsard 1 
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : For 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.
Complete list of metadata
Contributor : Frédéric Loulergue Connect in order to contact the contributor
Submitted on : Monday, January 19, 2015 - 5:01:19 PM
Last modification on : Saturday, June 25, 2022 - 10:12:43 AM


  • HAL Id : hal-01105093, version 1


Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard. Nested atomic sections with thread escape: Compilation to threads and locks. ACM Symposium on Applied Computing (SAC), Apr 2015, Salamanca, Spain. ⟨hal-01105093⟩



Record views