Correct and efficient bounded FIFO queues

Nhat Minh Lê, Adrien Guatto, Albert Cohen, Antoniu Pop

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

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. © 2013 IEEE.
Original languageEnglish
Title of host publicationProceedings - Symposium on Computer Architecture and High Performance Computing|Proc. Symp. Comput. Archit. High Perform. Comput.
PublisherIEEE Computer Society
Pages144-151
Number of pages7
ISBN (Print)9781479929276
DOIs
Publication statusPublished - 2013
Event2013 25th International Symposium on Computer Architecture and High Performance Computing, SBAC-PAD 2013 - Porto de Galinhas, PE
Duration: 1 Jul 2013 → …

Conference

Conference2013 25th International Symposium on Computer Architecture and High Performance Computing, SBAC-PAD 2013
CityPorto de Galinhas, PE
Period1/07/13 → …

Keywords

  • Data-flow programming
  • FIFO queue
  • Kahn process network
  • Lock-free algorithm
  • Weak memory model

Fingerprint

Dive into the research topics of 'Correct and efficient bounded FIFO queues'. Together they form a unique fingerprint.

Cite this