TP -- Concurrence

Programmation, modélisation et vérification d'un GC parallèle

Le but de cette séance est de finir le TP précédent.

Modélisation en Promela et vérification avec Spin

Vous pouvez partir du modèle suivant de la première version (incorrecte) de ce GC en Promela. Puis :

Pour un nombre de cellules petit (par exemple, N=6) exhiber sur cette modélisation une trace qui rend accessible endfree à partir de root.
Ecrire à la fin du Collector du code qui permet se rendre compte si, suite au ramassage des cellules libres, la cellule endfree devient accessible à partir du root. Ce code doit etre effectué de telle facon à ne pas interférer avec le Mutator.
En utilisant le code ci-dessus, utiliser la vérification de Spin pour exhiber la trace du premier point (voir l'indication de la feuille de TP).:
Introduisez de la synchronisation de manière à éliminer ce problème. Utilisez la solution vue en cours (avec trois couleurs).
Dans cette dernière version, le Collector effectue un dernier passage (quand k==N+1) pour determiner s'il existe des noeuds gris. Que se passe-t-il si on enlève ce code ? Trouver un exemple qui illustre le problème que vous avez trouvé.

Programmation en Java

Pour la synchronisation en exclusion mutuelle des processus, vous pouvez utiliser la classe suivante, qui implemente un semaphore :

public class Lock
{
 private int valeur =1;

 public synchronized void P()
 {
 while(valeur == 0)
 {
 try{wait();}
 catch(InterruptedException e){}
 }
 valeur=0;
 }
 public synchronized void V() 
 {
 valeur=1;
 notifyAll();
 }
}