Correct and Efficient Bounded FIFO Queues

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.Les files FIFO mono-producteur mono-consommateur constituent l'une des structures de données concurrentes les plus simples, et leur exécution correct ne requièrt pas plus que la consistance séquentielle de la mémoire. Il n'en reste pas moins que la consistance séquentielle est une hypothèse irréaliste pour des processeurs à mémoire partageée, et l'usage de barrières mémoire pour l'imposer induit un coût significatif en performance et en énergie. Cet article revisite l'optimisation et la preuve de correction pour des files FIFO bornées en présence d'un modèle mémoire relaché, en s'appuyant sur la formalisation axiomatique récente du modèle mémoire C11. Trois architectures de processeurs mettant en œuvre des modèles mémoire divers sont utilisés pour valider expérimentalement la portabilité et les performances de notre implémentation prouvée. Par rapport à l'état de l'art, cette implémentation apporte des améliorations significatives pour un large spectre de tailles de buffers et de rafales de communication