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
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Résumé : 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.
Type de document :
Rapport
[Research Report] RR-8365, INRIA. 2013
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00862450
Contributeur : Albert Cohen <>
Soumis le : lundi 16 septembre 2013 - 16:41:22
Dernière modification le : samedi 21 octobre 2017 - 20:10:13
Document(s) archivé(s) le : jeudi 6 avril 2017 - 20:59:33

Fichier

RR-8365.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

423

Téléchargements de fichiers

310