@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@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.},
}