Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata
Contributor : Frédéric Loulergue Connect in order to contact the contributor
Submitted on : Tuesday, November 19, 2013 - 8:38:02 AM
Last modification on : Saturday, June 25, 2022 - 10:12:26 AM


  • HAL Id : hal-00905949, version 1



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



Record views