La lecture en ligne est gratuite
Télécharger




AVERTISSEMENT

Ce document est le fruit d'un long travail approuvé par le
jury de soutenance et mis à disposition de l'ensemble de la
communauté universitaire élargie.

Il est soumis à la propriété intellectuelle de l'auteur. Ceci
implique une obligation de citation et de référencement lors
de l’utilisation de ce document.

D’autre part, toute contrefaçon, plagiat, reproduction
illicite encourt une poursuite pénale.


➢ Contact SCD Nancy 1 : theses.sciences@scd.uhp-nancy.fr




LIENS


Code de la Propriété Intellectuelle. articles L 122. 4
Code de la Propriété Intellectuelle. articles L 335.2- L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm Departement de formation doctorale en informatique Ecole doctorale IAEM Lorraine
UFR STMIA
Developpement prouve de structures
de donnees sans verrou
THESE
presentee et soutenue publiquement le 26-30 janvier 2008
pour l’obtention du
Doctorat de l’universite Henri Poincare { Nancy-Universite
(specialite informatique)
par
Lo c Fejoz
Composition du jury
Rapporteurs : Yamine Ait-Ameur
Christoph Weidenbach
Examinateurs : Jean-Paul Bodeveix
Claude Godart
Dominique Mery
Stephan Merz
Viktor Vafeiadis
Laboratoire Lorrain de Recherche en Informatique et ses Applications | UMR 7503Mis en page avec la classe thloria.i
Remerciements
Je remercie tout d’abord mon superviseur, Stephan Merz, pour son accompagnement et sa compre-
hension, ainsi que Pascal Fontaine pour ses nombreuses remarques de relecture. Je remercie egalement
toute l’equipe Mosel pour ces agreables annees passees ensemble. Je remercie les rapporteurs, et toutes
les personnes que j’ai pu rencontrer a travers cette these. Je sais gre a Microsoft Research de leur sou-
tien nancier gr^ ace leur programme de nancement Microsoft Research PhD Scholarship. En n je suis
reconnaissant envers ma femme Jacqueline.iiiii
a Erwann,
qui de toute facon aurait ete trop jeune pour comprendre.ivTable des matieres
Chapitre 1 Introduction 1
Chapitre 2 Exclusion Mutuelle 5
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.2 Section critique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.3 Semaphore . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2.4 Solution pour 2 processus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.5 Generalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
Chapitre 3 Structures de donnees partagees 11
3.1 Concurrence et correction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
3.2 De nition sequentielle des types abstraits . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
3.3 Caracterisation d’une trace . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.4 Consistance sequentielle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
3.5 Linearisabilite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.6 Modeles de memoire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
3.7 Primitives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
Chapitre 4 Modeles formels 23
4.1 Assume-guarantee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
4.1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
4.1.2 Exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
4.2 Logique de separation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4.3 Ra nement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4.4 B . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
+ +4.5 CAL et TLA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
Chapitre 5 Modelisation d’algorithmes sans verrou 35
5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5.2 Formalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
Chapitre 6 Preuve de correction 43
6.1 Ra nement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
6.2 Correction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
vvi Table des matieres
Chapitre 7 Application 53
7.1 Generateur d’obligation de preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
7.2 A ectation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
7.3 A ectation avec descripteur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
7.4 RDCSS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
Chapitre 8 Conclusion et travaux futurs 63
Annexes 67
Annexe A A ectation en Assume-guarantee 67
A.1 Assignment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
A.1.1 Atomic assignement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
A.1.2 Atomic assignement with CAS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
Annexe B Aectation en B evenementiel 71
B.1 Speci