Correct and efficient work-stealing for weak memory models

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

doi:10.1145/2442516.2442524

Correct and efficient work-stealing for weak memory models

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

Advanced Processor Technology

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-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 language	English
Title of host publication	Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP\|Proc ACM SIGPLAN Symp Prins Pract Parall Program PPOPP
Place of Publication	New York, USA
Publisher	Association for Computing Machinery
Pages	69-79
Number of pages	10
ISBN (Print)	9781450319225
DOIs	https://doi.org/10.1145/2442516.2442524
Publication status	Published - 2013
Event	18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2013 - Shenzhen Duration: 1 Jul 2013 → …

Conference

Conference	18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2013
City	Shenzhen
Period	1/07/13 → …

Keywords

lock-free algorithm
proof
relaxed memory model
work-stealing

Access to Document

10.1145/2442516.2442524

Cite this

@inproceedings{335cf90f97d348c697f0ae5c8d53f5d1,

title = "Correct and efficient work-stealing for weak memory models",

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. {\textcopyright} 2013 ACM.",

keywords = "lock-free algorithm, proof, relaxed memory model, work-stealing",

author = "L{\^e}, {Nhat Minh} and Antoniu Pop and Albert Cohen and {Zappa Nardelli}, Francesco",

year = "2013",

doi = "10.1145/2442516.2442524",

language = "English",

isbn = "9781450319225",

pages = "69--79",

booktitle = "Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP|Proc ACM SIGPLAN Symp Prins Pract Parall Program PPOPP",

publisher = "Association for Computing Machinery",

address = "United States",

note = "18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2013 ; Conference date: 01-07-2013",

}

Lê, NM, Pop, A, Cohen, A & Zappa Nardelli, F 2013, Correct and efficient work-stealing for weak memory models. in Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP|Proc ACM SIGPLAN Symp Prins Pract Parall Program PPOPP. Association for Computing Machinery, New York, USA, pp. 69-79, 18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2013, Shenzhen, 1/07/13. https://doi.org/10.1145/2442516.2442524

Correct and efficient work-stealing for weak memory models. / Lê, Nhat Minh; Pop, Antoniu; Cohen, Albert et al.
Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP|Proc ACM SIGPLAN Symp Prins Pract Parall Program PPOPP. New York, USA: Association for Computing Machinery, 2013. p. 69-79.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Correct and efficient work-stealing for weak memory models

AU - Lê, Nhat Minh

AU - Pop, Antoniu

AU - Cohen, Albert

AU - Zappa Nardelli, Francesco

PY - 2013

Y1 - 2013

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

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

KW - lock-free algorithm

KW - proof

KW - relaxed memory model

KW - work-stealing

U2 - 10.1145/2442516.2442524

DO - 10.1145/2442516.2442524

M3 - Conference contribution

SN - 9781450319225

SP - 69

EP - 79

BT - Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP|Proc ACM SIGPLAN Symp Prins Pract Parall Program PPOPP

PB - Association for Computing Machinery

CY - New York, USA

T2 - 18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2013

Y2 - 1 July 2013

ER -

Correct and efficient work-stealing for weak memory models

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this