Formalization of Phase Ordering

Tiago Cogumbreiro
(Rice University)
Jun Shirako
(Rice University)
Vivek Sarkar
(Rice University)

Phasers pose an interesting synchronization mechanism that generalizes many collective synchronization patterns seen in parallel programming languages, including barriers, clocks, and point-to-point synchronization using latches or semaphores. This work characterizes scheduling constraints on phaser operations, by relating the execution state of two tasks that operate on the same phaser. We propose a formalization of Habanero phasers, May-Happen-In-Parallel, and Happens-Before relations for phaser operations, and show that these relations conform with the semantics. Our formalization and proofs are fully mechanized using the Coq proof assistant, and are available online.

In Dominic Orchard and Nobuko Yoshida: Proceedings of the Ninth workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2016), Eindhoven, The Netherlands, 8th April 2016, Electronic Proceedings in Theoretical Computer Science 211, pp. 13–24.
Published: 17th June 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: