A formal semantics of nested atomic sections with thread escape

Frédéric Dabrowski 1 Frédéric Loulergue 2, 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 : The multi-core trend is widening the gap between programming languages and hardware. Taking parallelism into account in the programs is necessary to improve performance. Unfortunately, current mainstream programming languages fail to provide suitable abstractions to do so. The most common pattern relies on the use of mutexes to ensure mutual exclusion between concurrent accesses to a shared memory. However, this model is error-prone and scales poorly by lack of modularity. Recent research proposes atomic sections as an alternative. The user simply delimits portions of code that should be free from interference. The responsibility for ensuring interference freedom is left either to the compiler or to the run-time system. In order to provide enough modularity, it is necessary that both atomic sections could be nested and threads could be forked inside an atomic section. In this paper we focus on the semantics of programming languages providing these features. More precisely, without being tied to a specific programming language, we consider program traces satisfying some basic well-formedness conditions. Our main contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. A formalisation of our results in the Coq proof assistant is described.
Type de document :
Article dans une revue
Computer Languages, Systems and Structures, Elsevier, 2015, pp.24
Liste complète des métadonnées

Contributeur : Frédéric Loulergue <>
Soumis le : jeudi 16 avril 2015 - 22:30:46
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37


  • HAL Id : hal-01143199, version 1



Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard. A formal semantics of nested atomic sections with thread escape. Computer Languages, Systems and Structures, Elsevier, 2015, pp.24. 〈hal-01143199〉



Consultations de la notice