Cours "théorie et pratique de la concurrence" -- M1 (2011--2012)

Equipe enseignante

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


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:

Sujets des TD

La page des TD est ici.

Références bibliographiques

Email: francois.laroussinie[at]liafa.jussieu.fr