Nested Atomic Sections with Thread Escape: A Formal Definition

Abstract : We consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our 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 also available.
Type de document :
Communication dans un congrès
ACM. ACM Symposium on Applied Computing (SAC), 2014, Gyeongju, South Korea. 2014
Liste complète des métadonnées

https://hal.inria.fr/hal-00905949
Contributeur : Frédéric Loulergue <>
Soumis le : mardi 19 novembre 2013 - 08:38:02
Dernière modification le : mardi 20 janvier 2015 - 01:04:29

Identifiants

  • HAL Id : hal-00905949, version 1

Collections

Citation

Frederic Dabrowski, Frédéric Loulergue, Thomas Pinsard. Nested Atomic Sections with Thread Escape: A Formal Definition. ACM. ACM Symposium on Applied Computing (SAC), 2014, Gyeongju, South Korea. 2014. 〈hal-00905949〉

Partager

Métriques

Consultations de la notice

124