Correct and Efficient Bounded FIFO Queues

Nhat Minh Lê 1 Adrien Guatto 1 Albert Cohen 1 Antoniu Pop 1
1 Parkas - Parallélisme de Kahn Synchrone
CNRS - Centre National de la Recherche Scientifique : UMR 8548, Inria Paris-Rocquencourt, DI-ENS - Département d'informatique de l'École normale supérieure
Abstract : Bounded single-producer single-consumer FIFO queues are one of the simplest concurrent data-structure, and they do not require more than sequential consistency for correct operation. Still, sequential consistency is an unrealistic hypothesis on shared-memory multiprocessors, and enforcing it through memory barriers induces significant performance and energy overhead. This paper revisits the optimization and correctness proof of bounded FIFO queues in the context of weak memory consistency, building upon the recent axiomatic formalization of the C11 memory model. We validate the portability and performance of our proven implementation over 3 processor architectures with diverse hardware memory models, including ARM and PowerPC. Comparison with state-of-the-art implementations demonstrate consistent improvements for a wide range of buffer and batch sizes.
Document type :
Reports
Liste complète des métadonnées

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-00862450
Contributor : Albert Cohen <>
Submitted on : Monday, September 16, 2013 - 4:41:22 PM
Last modification on : Thursday, February 7, 2019 - 3:49:35 PM
Document(s) archivé(s) le : Thursday, April 6, 2017 - 8:59:33 PM

File

RR-8365.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00862450, version 1

Collections

Citation

Nhat Minh Lê, Adrien Guatto, Albert Cohen, Antoniu Pop. Correct and Efficient Bounded FIFO Queues. [Research Report] RR-8365, INRIA. 2013. 〈hal-00862450〉

Share

Metrics

Record views

492

Files downloads

571