Correct and efficient bounded FIFO queues

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

doi:10.1109/SBAC-PAD.2013.8

Correct and efficient bounded FIFO queues

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

Advanced Processor Technology

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-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 language	English
Title of host publication	Proceedings - Symposium on Computer Architecture and High Performance Computing\|Proc. Symp. Comput. Archit. High Perform. Comput.
Publisher	IEEE Computer Society
Pages	144-151
Number of pages	7
ISBN (Print)	9781479929276
DOIs	https://doi.org/10.1109/SBAC-PAD.2013.8
Publication status	Published - 2013
Event	2013 25th International Symposium on Computer Architecture and High Performance Computing, SBAC-PAD 2013 - Porto de Galinhas, PE Duration: 1 Jul 2013 → …

Conference

Conference	2013 25th International Symposium on Computer Architecture and High Performance Computing, SBAC-PAD 2013
City	Porto de Galinhas, PE
Period	1/07/13 → …

Keywords

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

Access to Document

10.1109/SBAC-PAD.2013.8

Cite this

@inproceedings{b806ddb403574a609916f270ee4aa0ce,

title = "Correct and efficient bounded FIFO queues",

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

keywords = "Data-flow programming, FIFO queue, Kahn process network, Lock-free algorithm, Weak memory model",

author = "L{\^e}, {Nhat Minh} and Adrien Guatto and Albert Cohen and Antoniu Pop",

year = "2013",

doi = "10.1109/SBAC-PAD.2013.8",

language = "English",

isbn = "9781479929276",

pages = "144--151",

booktitle = "Proceedings - Symposium on Computer Architecture and High Performance Computing|Proc. Symp. Comput. Archit. High Perform. Comput.",

publisher = "IEEE Computer Society ",

address = "United States",

note = "2013 25th International Symposium on Computer Architecture and High Performance Computing, SBAC-PAD 2013 ; Conference date: 01-07-2013",

}

Lê, NM, Guatto, A, Cohen, A & Pop, A 2013, Correct and efficient bounded FIFO queues. in Proceedings - Symposium on Computer Architecture and High Performance Computing|Proc. Symp. Comput. Archit. High Perform. Comput.. IEEE Computer Society , pp. 144-151, 2013 25th International Symposium on Computer Architecture and High Performance Computing, SBAC-PAD 2013, Porto de Galinhas, PE, 1/07/13. https://doi.org/10.1109/SBAC-PAD.2013.8

Correct and efficient bounded FIFO queues. / Lê, Nhat Minh; Guatto, Adrien; Cohen, Albert et al.
Proceedings - Symposium on Computer Architecture and High Performance Computing|Proc. Symp. Comput. Archit. High Perform. Comput.. IEEE Computer Society , 2013. p. 144-151.

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

TY - GEN

T1 - Correct and efficient bounded FIFO queues

AU - Lê, Nhat Minh

AU - Guatto, Adrien

AU - Cohen, Albert

AU - Pop, Antoniu

PY - 2013

Y1 - 2013

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

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

KW - Data-flow programming

KW - FIFO queue

KW - Kahn process network

KW - Lock-free algorithm

KW - Weak memory model

U2 - 10.1109/SBAC-PAD.2013.8

DO - 10.1109/SBAC-PAD.2013.8

M3 - Conference contribution

SN - 9781479929276

SP - 144

EP - 151

BT - Proceedings - Symposium on Computer Architecture and High Performance Computing|Proc. Symp. Comput. Archit. High Perform. Comput.

PB - IEEE Computer Society

T2 - 2013 25th International Symposium on Computer Architecture and High Performance Computing, SBAC-PAD 2013

Y2 - 1 July 2013

ER -

Correct and efficient bounded FIFO queues

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this