Dérivation d'algorithmes sans verrou à partir d'une spécification atomique - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2007

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

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+.
Fichier principal
Vignette du fichier
afadl07-fejoz-merz.pdf (214.14 Ko) Télécharger le fichier
slides.beamer.pdf (601.92 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Format : Autre

Dates et versions

inria-00162146 , version 1 (12-07-2007)

Identifiants

  • HAL Id : inria-00162146 , version 1

Citer

Loïc Fejoz, Stephan Merz. Dérivation d'algorithmes sans verrou à partir d'une spécification atomique. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL07, Marie-Laure Potet (IMAG, Grenoble) ; Pierre-Yves Schobbens (Facultés Universitaires Notre-Dame de la Paix - Namur, Belgique), Jun 2007, Namur, Belgique. pp.213-226. ⟨inria-00162146⟩
103 Consultations
96 Téléchargements

Partager

Gmail Facebook X LinkedIn More