Dérivation d'algorithmes sans verrou à partir d'une spécification atomique

Loïc Fejoz 1 Stephan Merz 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Pour gérer les accès de plusieurs processus à des données partagées, on utilise souvent un verrou global. Ici nous nous intéressons aux algorithmes sans verrou qui permettent un accès simultané en lecture et écriture. Malgré une littérature récente abondante, il y a peu de preuves de ces algorithmes. Nous proposons une méthode modulaire qui permettra de dériver des algorithmes sans verrou à partir d'une spécification atomique qui décrit la fonctionnalité des opérations élémentaires sur une structure de données. Cette méthode peut être utilisée dans un style "~à la B~" (approche top-down), mais elle permet aussi d'ajouter des points de linéarisation aux algorithmes, en adaptant le style de la méthode "~assume-guarantee~". Dans le présent article, on donne une formalisation de la méthode, et on explique son utilisation sur des exemples simplifiés. Nous comparons cette méthode à des méthodes plus classiques telles que B et TLA+.
Keywords : lock-free algorithm correctness refinement
Type de document :
Communication dans un congrès
Marie-Laure Potet and Pierre-Yves Schobbens and Hubert Toussaint and Germain Saval. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL07, Jun 2007, Namur, Belgique. Presses universitaires de Namur, 2007, pp.213-226, 2007, Actes de la 8e conférence AFADL Approches Formelles dans l'Assistance au Développement de Logiciels
Liste complète des métadonnées
https://hal.inria.fr/inria-00162146
Contributeur : Loïc Fejoz <>
Soumis le : jeudi 12 juillet 2007 - 15:19:35
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : lundi 24 septembre 2012 - 11:01:28

Fichiers

afadl07-fejoz-merz.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00162146, version 1

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Loïc Fejoz, Stephan Merz. Dérivation d'algorithmes sans verrou à partir d'une spécification atomique. Marie-Laure Potet and Pierre-Yves Schobbens and Hubert Toussaint and Germain Saval. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL07, Jun 2007, Namur, Belgique. Presses universitaires de Namur, 2007, pp.213-226, 2007, Actes de la 8e conférence AFADL Approches Formelles dans l'Assistance au Développement de Logiciels. 〈inria-00162146〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

291

Téléchargements de fichiers

318

Contact


archive-ouverte@inria.fr