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 metadatas

https://hal.inria.fr/hal-01105093
Contributor : Frédéric Loulergue <>
Submitted on : Monday, January 19, 2015 - 5:01:19 PM
Last modification on : Thursday, January 17, 2019 - 3:06:06 PM

Identifiers

  • HAL Id : hal-01105093, version 1

Citation

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⟩

Share

Metrics

Record views

247