2016/06/20 by Tiago Cogumbreiro, Jun Shirako, Vivek Sarkar
Computer Science · #cs.DC #cs.LO
paper · pdf · doi:10.4204/eptcs.211.2
published as EPTCS 211, 2016, pp. 13-24 · In Proceedings PLACES 2016, arXiv:1606.05403
arxiv created 2016/06/20 · arxiv updated 2016/06/21
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.