Correct and efficient work-stealing for weak memory models

Nhat Minh Lê, Antoniu Pop, Albert Cohen, Francesco Zappa Nardelli

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Chase and Lev's concurrent deque is a key data structure in shared-memory parallel programming and plays an essential role in work-stealing schedulers. We provide the first correctness proof of an optimized implementation of Chase and Lev's deque on top of the POWER and ARM architectures: these provide very relaxed memory models, which we exploit to improve performance but considerably complicate the reasoning. We also study an optimized x86 and a portable C11 implementation, conducting systematic experiments to evaluate the impact of memory barrier optimizations. Our results demonstrate the benefits of hand tuning the deque code when running on top of relaxed memory models. © 2013 ACM.
Original languageEnglish
Title of host publicationProceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP|Proc ACM SIGPLAN Symp Prins Pract Parall Program PPOPP
Place of PublicationNew York, USA
PublisherAssociation for Computing Machinery
Pages69-79
Number of pages10
ISBN (Print)9781450319225
DOIs
Publication statusPublished - 2013
Event18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2013 - Shenzhen
Duration: 1 Jul 2013 → …

Conference

Conference18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2013
CityShenzhen
Period1/07/13 → …

Keywords

  • lock-free algorithm
  • proof
  • relaxed memory model
  • work-stealing

Fingerprint

Dive into the research topics of 'Correct and efficient work-stealing for weak memory models'. Together they form a unique fingerprint.

Cite this