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