@inproceedings{f7f3baa3c09d4122a3e213fdd0aef76a,
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.",
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",
month = feb,
day = "23",
doi = "10.1145/2442516.2442524",
language = "English",
isbn = "9781450319225",
series = "Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP",
publisher = "Association for Computing Machinery",
pages = "69--79",
booktitle = "PPoPP 2013 - Proceedings of the 2013 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming",
note = "18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2013 ; Conference date: 23-02-2013 Through 27-02-2013",
}