• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Design and Verification of Distributed Phasers.
Karthik, Murthy, Sri Raj, Paul, Kuldeep S., Meel, Tiago Cogumbreiro and John Mellor-Crummey.
In Proceedings of International European Conference on Parallel and Distributed Computing (Euro-Par), January 2016.
A phaser is an expressive synchronization construct that unifies collective and point-to-point coordination with dynamic registration of parallel tasks. Each task can participate in a phaser as a signaler, a waiter, or both. The participants in a phaser may change over time as tasks are added and deleted. In this paper, we present a highly concurrent and scalable design of phasers for a distributed memory environment. Our design for a distributed phaser employs a pair of skip lists augmented with the ability to collect and propagate synchronization signals. To enable a high degree of concurrency, addition and deletion of participant tasks are performed in two phases: a "fast single-link-modify" step followed by multiple hand-over-hand "lazy multi-link-modify" steps. Verifying highly-concurrent protocols is difficult. We analyze our design for a distributed phaser using the SPIN model checker. A straight-forward approach to model checking a distributed phaser operation requires an infeasibly large state space. To address this issue, we employ a novel "message-based" model checking scheme to enable a non- approximate complete model checking of our phaser design. We guarantee the semantic properties of phaser operations by ensuring that a set of linear temporal logic formulae are valid during model checking. We also present complexity analysis of the cost of synchronization and structural operations.
@inproceedings{PMMCM16,
title={Design and Verification of Distributed Phasers},
author={
Murthy, Karthik, and Paul, Sri Raj, and Meel, Kuldeep S., and Cogumbreiro,
Tiago and Mellor-Crummey, John
},
year={2016},
month=jan,
bib2html_dl_pdf={../Papers/europar16.pdf},
code={http://srp7.web.rice.edu/phaser/},
booktitle=EUROPAR,
bib2html_rescat={Software Engineering},
bib2html_pubtype={Refereed Conference},
abstract={
A phaser is an expressive synchronization construct that unifies
collective and point-to-point coordination with dynamic registration of
parallel
tasks. Each task can participate in a phaser as a signaler, a waiter, or
both.
The participants in a phaser may change over time as tasks are added and
deleted.
In this paper, we present a highly concurrent and scalable design of phasers
for a
distributed memory environment.
Our design for a distributed phaser employs a pair of skip lists augmented
with the
ability to collect and propagate synchronization signals. To enable a high
degree of
concurrency, addition and deletion of participant tasks are performed in two
phases:
a "fast single-link-modify" step followed by multiple hand-over-hand "lazy
multi-link-modify"
steps.
Verifying highly-concurrent protocols is difficult. We analyze our design
for a
distributed phaser using the SPIN model checker. A straight-forward approach
to
model checking a distributed phaser operation requires an infeasibly large
state space.
To address this issue, we employ a novel "message-based" model checking
scheme to enable
a non- approximate complete model checking of our phaser design. We
guarantee the
semantic properties of phaser operations by ensuring that a set of linear
temporal logic
formulae are valid during model checking.
We also present complexity analysis of the cost of synchronization and
structural
operations.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Thu Sep 10, 2026 16:32:38