Probleme – Un compteur juste, et ce qu'il coûte

1. Les quatre versions.

long compteur = 0;
pthread_mutex_t verrou = PTHREAD_MUTEX_INITIALIZER;

/* 1. aucune protection : FAUSSE */
void* v1(void* a) {
    for (int i = 0; i < TOURS; i++) { compteur = compteur + 1; }
    return NULL;
}
/* 2. un verrou à chaque incrément : juste, et cher */
void* v2(void* a) {
    for (int i = 0; i < TOURS; i++) {
        pthread_mutex_lock(&verrou);
        compteur = compteur + 1;
        pthread_mutex_unlock(&verrou);
    }
    return NULL;
}
/* 3. un verrou tous les PAQUET incréments : granularité choisie */
void* v3(void* a) {
    for (int i = 0; i < TOURS; i += PAQUET) {
        pthread_mutex_lock(&verrou);
        for (int k = 0; k < PAQUET; k++) { compteur = compteur + 1; }
        pthread_mutex_unlock(&verrou);
    }
    return NULL;
}
/* 4. somme locale, UNE seule prise de verrou par fil */
void* v4(void* a) {
    long local = 0;                          /* sur la pile : privé */
    for (int i = 0; i < TOURS; i++) { local = local + 1; }
    pthread_mutex_lock(&verrou);
    compteur = compteur + local;             /* la SEULE section critique */
    pthread_mutex_unlock(&verrou);
    return NULL;
}

2. Les mesures, trois exécutions concordantes, $4000000$ attendus :

3. Trois conclusions, et la troisième démolit une idée reçue.

(a) Le verrou fin coûte cher : la version 2 est $30$ fois plus lente que la version 1. Ce n'est pas le lock lui-même qui coûte — c'est la contention. Quatre fils se disputent un verrou quatre millions de fois : chaque prise raté endort un fil, et le réveiller passe par le noyau.

(b) La granularité est un réglage, pas une propriété : passer d'un verrou par incrément à un verrou tous les cent divise le temps par $11$, et rend exactement le même résultat. On ne choisit pas entre juste et rapide : on choisit la taille de la section critique.

(c) Et voici le point. La version 4, correcte, est plus rapide que la version 1, qui est fausse — $0,001$ s contre $0,003$ à $0,007$ s. Non pas malgré la protection, mais grâce à elle : chaque fil travaille sur sa propre variable de pile, que le processeur garde dans un registre et dont la ligne de cache n'est partagée avec personne. La version 1, elle, fait rebondir la même ligne de cache entre quatre cœurs à chaque incrément.

4. La correction de la version 4.

Spécification. Entrée : $p$ fils, un entier $T$. Sortie : compteur vaut $p\times T$ après le dernier pthread_join.

Invariant de la boucle locale. Après $i$ tours, local vaut $i$. La variable est sur la pile du fil : aucun autre fil ne peut y accéder, l'invariant ne peut donc pas être cassé de l'extérieur. C'est ce qui rend cette boucle triviale à prouver, là où celle de la version 1 est infalsifiable.

Invariant global. On note $S$ l'ensemble des fils ayant achevé leur section critique. L'invariant est : compteur $=|S|\times T$. Il est vrai au départ ($S=\varnothing$). Chaque exécution de la section critique ajoute $T$ et fait passer un fil dans $S$ : l'invariant est préservé. Le mutex garantit que ces exécutions sont sérialisées, donc qu'aucune n'observe un état intermédiaire d'une autre.

Conclusion. Après les $p$ pthread_join, tous les fils sont dans $S$, donc compteur $=p\times T$. Les join font partie de la preuve : sans eux, on lirait compteur à un instant où $S$ n'est pas complet, et l'exercice 22.3 dit ce qu'on obtiendrait.

Complexité. $\Theta (T)$ par fil en temps, $\Theta (p)$ prises de verrou au total — contre $\Theta (pT)$ pour la version 2. C'est le rapport $4$ contre $4000000$, et c'est exactement ce que le chronomètre a mesuré.