Formalization of Phase Ordering

Formalization of Phase Ordering

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...

Full description

Bibliographic Details
Main Authors: Tiago Cogumbreiro, Jun Shirako, Vivek Sarkar
Format: Article
Language:English
Published: Open Publishing Association 2016-06-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1606.05937v1
id doaj-a6956f2a9fa5410a8d5b871d27927e7e
record_format Article
spelling doaj-a6956f2a9fa5410a8d5b871d27927e7e2020-11-25T02:27:44ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-06-01211Proc. PLACES 2016132410.4204/EPTCS.211.2:16Formalization of Phase OrderingTiago Cogumbreiro0Jun Shirako1Vivek Sarkar2 Rice University Rice University 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.http://arxiv.org/pdf/1606.05937v1
collection DOAJ
language English
format Article
sources DOAJ
author Tiago Cogumbreiro
Jun Shirako
Vivek Sarkar
spellingShingle Tiago Cogumbreiro
Jun Shirako
Vivek Sarkar
Formalization of Phase Ordering
Electronic Proceedings in Theoretical Computer Science
author_facet Tiago Cogumbreiro
Jun Shirako
Vivek Sarkar
author_sort Tiago Cogumbreiro
title Formalization of Phase Ordering
title_short Formalization of Phase Ordering
title_full Formalization of Phase Ordering
title_fullStr Formalization of Phase Ordering
title_full_unstemmed Formalization of Phase Ordering
title_sort formalization of phase ordering
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2016-06-01
description 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.
url http://arxiv.org/pdf/1606.05937v1
work_keys_str_mv AT tiagocogumbreiro formalizationofphaseordering
AT junshirako formalizationofphaseordering
AT viveksarkar formalizationofphaseordering
_version_ 1724841058479636480

Similar Items