Equipe enseignante
- Cours: François Laroussinie (lundi 12h30--14h30,
amphi 10E)
- TD: Arnaud Sangnier
(jeudi 8h30--10h30; 071E (ou 548C)
Actualités
Des notes de cours sur la première partie du
cours sont disponibles
ici.
Une correction (partielle) de
l'examen de session 1 est disponible
ici.
Vous trouverez ci-dessous les sujets des deux sessions de l'an -->
dernier.
Programme
- Introduction
- Logique temporelle pour énoncer la correction des
programmes concurrents
- Programmes concurrents
- Problèmes d'exclusion mutuelle: Algorithmes (Dekker, Peterson, Bakery, ...) + preuves de correction
- Langage Promela et outil SPIN.
- Sémaphores, moniteurs
- Systèmes avec canaux de communication
- Autres problèmes: Le problème des philosophes, lecteurs/écrivains.
- Algèbres de processus (CCS)
- Définition, exemples
- Notions d'équivalence entre processus
- Logique modale pour la spécification des processus CCS
Algorithmes d'exclusion mutuelle et vérification avec SPIN
Voici quelques algorithmes décrits en Promela (le langage de
l'outil Spin). Une remarque importante s'impose: le but recherché ici
est de rester le plus proche possible de l'algorithme présenté en
cours (quitte à perdre en efficacité pour la vérification automatique
via l'outil SPIN), il s'agit donc plutôt de code "jouet"... En particulier, nous avons codé la section non
critique de manière à ce qu'elle puisse bloquer, ajouté des "skip"
pour marquer les sections critiques,...
L'outil SPIN est un model-checker (outil de vérification automatique)
accessible ici:
SPIN
Pour l'utiliser je recommande d'utiliser l'outil jSpin de Moti
Ben-Ari:
jSPIN .
Les fichiers Promela pour utiliser Spin:
-
Algorithme "A1"
-
Algorithme de Dekker
-
Algorithme de Peterson
- Algorithme de la boulangerie
Attention: ici le codage des "tickets"
(Nb) avec des entiers sur 8 bits (Byte) fait que l'algorithme
est... faux : les propriétés classiques d'exclusion mutuelle ou
d'absence de famine ne sont pas vérifiées. Par contre on peut vérifier
des propriétés plus faibles qui intègrent la valeur des tickets: une
sorte d'exclusion mutuelle bornée ((!cs1 || !cs2) W nbg) où nbg
caractérise les états avec un ticket ayant une grande valeur (ici
100). On peut faire pareil pour l'absence de famine (propriété afb
dans le code) à condition de placer le label PRE après le calcul du
ticket (donc au milieu du pre-protocole).
Exercice: expliquer ces deux points...
Sujets des TD
La page des TD est
ici.
Références bibliographiques
- "Principles of Concurrent and Distributed Programming" (Second edition):
M. Ben-Ari.
Addison-Wesley, 2006.
- "Reactive Systems: Modelling, Specification and Verification":
Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen, Jiri Srba.
Cambridge University Press, July 2007.
Email: francois.laroussinie[at]liafa.jussieu.fr