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.
Type de document :
Communication dans un congrès
ACM Symposium on Applied Computing (SAC), Apr 2015, Salamanca, Spain. ACM, 2015, 〈http://www.acm.org/conferences/sac/sac2015〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01105093
Contributeur : Frédéric Loulergue <>
Soumis le : lundi 19 janvier 2015 - 17:01:19
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Identifiants

  • HAL Id : hal-01105093, version 1

Collections

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. ACM, 2015, 〈http://www.acm.org/conferences/sac/sac2015〉. 〈hal-01105093〉

Partager

Métriques

Consultations de la notice

201