Nested Atomic Sections with Thread Escape: An Operational Semantics
Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard · 2013
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 a formal operational semantics of this language that satisfies a specification on execution traces designed in a companion paper.