Algorithme de Peterson

Voici le pseudo-code de l'algorithme écrit en Java[1]. Les deux threads possèdent comme identifiant 0 et 1, ils peuvent obtenir leur identifiant en appelant ThreadID.get().

class Peterson implements Lock {
    // index du thread local, vaut 0 ou 1
    private boolean[] drapeau = new boolean[2];
    private int victime;
    public void lock() {
        int i = ThreadID.get();
        int j = 1 - i;
        drapeau[i] = true;                      // je suis intéressé
        victime = i;                            // il va en premier
        while (drapeau[j] && victime == i) {}   // j'attends
    }
    public void unlock() {
        int i = ThreadID.get();
        drapeau[i] = false;                     // je ne suis plus intéressé
    }
}

L'algorithme de Peterson satisfait la propriété de l'exclusion mutuelle.

Preuve. Supposons qu'il ne satisfasse pas l'exclusion mutuelle. Considérons les dernières exécutions des threads A et B avant qu'elles ne s'entrecroisent au niveau de leur section critique, respectivement CS_A et CS_B. En inspectant le code, on remarque que :

write_A(drapeau[A] = vrai) ⇒ write_A(victime = A) ⇒ read_A(drapeau[B]) ⇒ read_A(victime) ⇒ CS_A, (1) write_B(drapeau[B] = vrai) ⇒ write_B(victime = B) ⇒ read_B(drapeau[A]) ⇒ read_B(victime) ⇒ CS_B (2)

Supposons que A est le dernier thread a écrire dans le champ victime, cette supposition ayant peu d'impact sur la parte de généralité de l'algorithme. Ainsi, on peut écrire :

write_B(victime = B) ⇒ write_A(victime = A) (3)

L'équation (3) suppose que A a observé la variable victime dans (1). Comme A est entré dans sa zone critique, par conséquent A a forcément observé que drapeau[B] était faux. Nous avons donc :

write_A(victime = A) ⇒ read_A(drapeau[B] == faux) (4)

En combinant les équations (2) et (4) ensemble, on obtient :

write_B(drapeau[B] = vrai) ⇒ write_B(victime= B) ⇒ write_A(victime= A) ⇒ read_A(drapeau[B] == faux). (5)

Via les règles de transitivité de l'implication (⇒), on peut réécrire (5) en :

write_B(drapeau[B] = vrai) ⇒ read_A(drapeau[B] == faux).

Ce qui constitue une contradiction. En effet, aucune autre écriture de drapeau[B] n'a pu être effectuée avant les exécutions de la section critique. Par conséquent l'hypothèse de base est erronée et l'algorithme de Peterson satisfait bien la propriété de l'exclusion mutuelle. □

L'algorithme de Peterson satisfait la propriété de l'absence de famine.

Preuve. Supposons que cela ne soit pas le cas. Il y a donc au moins un des deux threads qui s'exécute pour toujours sans jamais entrer dans la section critique. Supposons que cela soit A (la preuve est similaire si on supposait que cela soit B). A exécute donc la ligne while (drapeau[j] && victime == i) {} en boucle, et attendant donc que soit drapeau[j] devienne faux, soit que victime soit égale à B.

Que fait B tandis que A exécute cette ligne de code ? Il doit être en train d'entrer et sortir de la zone critique de manière répétée. Cela veut donc dire que B met la variable victime à B à chaque fois qu'il veut entrer dans la section critique. Par conséquent, la variable victime est toujours égale à B et ne change jamais de valeur. Si c'est le cas, A peut alors sortir de la boucle puisqu'une des deux conditions est remplie. C'est donc une contradiction.

Si ce n'est pas ça, c'est alors parce que B est également coincée dans la boucle en attendant de pouvoir entrer dans la zone critique, attendant que soit flag[A] devienne faux soit victime soit mise à A. Mais victime ne peut pas valoir à la fois A et B. C'est donc également une contradiction. Par conséquent, l'hypothèse de base est fausse et l'algorithme satisfait bien la propriété de l'absence de famine. □

L'algorithme de Peterson satisfait la propriété de l'absence d'interblocage.

Preuve. Comme il a déjà démontré que l'algorithme satisfait la propriété de l'absence de famine, et que la propriété de l'absence de famine est une propriété plus forte que l'absence d'interblocage, alors l'algorithme est garanti de ne pas avoir d'interblocage. □