PRCV24 · Programmation concurrente et vérification

La seule option HPC du semestre 4, et l'une des deux seules UE du cursus FISA où l'on ouvre le capot du parallélisme plutôt que d'en utiliser l'API.

Fiche signalétique

Code	PRCV24 (modules COMC24 et MPPT24)
Crédits	4 ECTS
Semestre	4, option — lundi, début de semestre
Responsable	BUREL Guillaume
Prérequis	Programmation impérative ; introduction au système d'exploitation ; langages et systèmes formels
Effectif max	32
Concurrentes sur le créneau	MOST24, GADE24
Choix	Facultatif, avec l'accord de l'entreprise

Ce que dit la brochure

Objectifs cités :

« Cette option introduit les concepts de la programmation concurrente et sa mise en œuvre à travers l'utilisation de threads. Par ailleurs, il est notoirement difficile de se faire une intuition sur la correction des programmes concurrents, en particulier concernant l'absence de blocage et l'accès aux ressources. Pour assurer cette correction, il est donc nécessaire d'avoir recours à des techniques de vérification formelles comme le model-checking. »

Module 1 · COMC24, concepts et model checking — 6 séances de cours, 3 de TD, 2 de TP, 1 d'examen :

— Organisation des traitements en activités concurrentes (processus ou threads), difficultés liées aux variables partagées, sections critiques, blocages dus aux accès concurrents — Apprentissage d'un environnement de vérification exhaustive.

Objectif cité : « maîtriser les outils standards de synchronisation de processus (sémaphores) et les techniques de vérification (model-checking) ».

Module 2 · MPPT24, modèle de programmation Pthread — 4 séances de cours, 8 de TP, évaluation en contrôle continu :

— API Posix — Conception de bibliothèques de threads utilisateur — Outils debug/profiling — Techniques de débogage en contexte multithread — Mini projet « autour d'une bibliothèque de threads utilisateur »

Bibliographie citée : les tutoriels Pthreads du Lawrence Livermore National Laboratory.

Sur la bibliographie citée

La brochure renvoie à computing.llnl.gov/tutorials/pthreads/. Ces tutoriels sont les références historiques du domaine et ils sont excellents. À noter : le LLNL a réorganisé son site et ces contenus sont désormais sur hpc-tutorials.llnl.gov. Si l'URL du document ne répond pas, chercher « LLNL HPC tutorials POSIX threads ».

Ce que ça vaut pour le HPC

Élevé, et pour une raison précise : le mot « conception ».

Écrire une bibliothèque de threads

« Conception de bibliothèques de threads utilisateur », avec un mini-projet dédié. C'est la ligne qui justifie l'UE à elle seule.

Des threads légers ordonnancés en espace utilisateur, cela veut dire implémenter soi-même le changement de contexte, la gestion des piles, l'ordonnancement coopératif, et mesurer le coût réel d'une synchronisation.

Le résultat à obtenir, et il est frappant : un changement de contexte en espace utilisateur coûte de l'ordre de quelques dizaines à quelques centaines de nanosecondes, contre plusieurs microsecondes pour créer un thread noyau. Ce facteur de cinquante à mille explique à lui seul l'existence de tout l'écosystème des runtimes de tâches : OpenMP tasks, StarPU, Cilk, TBB, Argobots, Qthreads.

C'est aussi un sujet de recherche actif, et le domaine des équipes françaises d'Inria Bordeaux et du CEA.

La vérification, qui ne se trouve nulle part ailleurs

Le model checking explore tous les entrelacements possibles d'un programme concurrent, là où un test n'en explore qu'un.

C'est le seul endroit du cursus FISA où l'on aborde la question, et elle compte : un programme concurrent qui passe mille tests peut être incorrect, parce que la course de données ne se manifeste qu'une exécution sur dix mille — c'est-à-dire en production, un vendredi soir.

Le pont à faire soi-même entre les deux modules

Les deux modules de PRCV24 se parlent peu dans l'énoncé : l'un est formel, l'autre est pratique. Le pont existe pourtant, et il est directement utile.

COMC24 vous apprend à raisonner sur la correction — sections critiques, interblocages, exploration exhaustive.

Les outils d'exécution font le même travail approximativement mais sans modélisation : ThreadSanitizer (-fsanitize=thread) trouve les courses de données réelles en une exécution, Helgrind et Archer complètent.

Faire le lien — « ce que le model-checking prouve, TSan le détecte empiriquement sur les chemins exécutés » — vous donnera une compréhension que ni l'un ni l'autre des deux modules ne donne seul. C'est développé dans OpenMP et threads.

Le piège des prérequis

Fait. PRCV24 demande « Langages et systèmes formels ». Il s'agit de LASF24, module de l'UE MATH24… du même semestre 4.

Vous suivrez donc les deux en parallèle. Ce n'est pas bloquant : la partie model checking de COMC24 arrive après les séances d'introduction. Mais si la logique n'est pas votre terrain, prenez de l'avance pendant les vacances de fin d'année.

Arriver prêt

⏱ 8 h.

1. Threads POSIX, révision. Écrire un programme qui crée des threads, les joint, protège une variable partagée par mutex. ⏱ 3 h.
2. Constater le problème avant le cours. Écrire une somme parallèle de tableau avec une variable partagée sans protection. Observer que le résultat est faux et varie. Protéger par mutex. Observer que c'est maintenant correct mais plus lent que la version séquentielle. ⏱ 2 h. Vous arriverez avec la bonne question.
3. Le modèle mémoire, au moins l'intuition. Les premiers articles du blog de Jeff Preshing sur l'ordonnancement mémoire, ou les premiers chapitres de McKenney. ⏱ 3 h.

Ressources

Priorité 1 :

• Les tutoriels Pthreads du LLNL (hpc-tutorials.llnl.gov), cités par la brochure.
• Maurice Herlihy, Nir Shavit, The Art of Multiprocessor Programming, 2ᵉ éd. La référence théorique sur la synchronisation : verrous, structures non bloquantes, modèles de mémoire, linéarisabilité.
• Paul McKenney, Is Parallel Programming Hard, And, If So, What Can You Do About It?, gratuit sur kernel.org. Écrit par l'auteur du RCU du noyau Linux. Le meilleur texte sur les barrières mémoire.

Priorité 2 :

• Le blog de Jeff Preshing (preshing.com), sur les modèles mémoire et l'atomique. Court et pédagogique.
• Le TLA+ Video Course de Leslie Lamport, pour le model checking, si l'environnement utilisé en cours vous laisse sur votre faim.
• La documentation de ThreadSanitizer et d'Archer, l'extension de TSan pour OpenMP.

Priorité 3 — les runtimes de tâches, qui sont la suite naturelle du mini-projet :

• StarPU (Inria Bordeaux) : ordonnancement de tâches sur machines hétérogènes, avec vol de travail.
• Blumofe & Leiserson, « Scheduling Multithreaded Computations by Work Stealing », JACM, 1999 — l'article fondateur, qui démontre la borne du vol de travail. Bon candidat pour l'article à lire de PDSP35.

Exercices

E1 · ★★ ⏱ 3 h — Le coût des primitives. Mesurer en nanosecondes : incrémentation ordinaire, incrémentation atomique, section critique, mutex, barrière, création de thread. Faire varier le nombre de threads. Le coût des atomiques et des verrous croît avec le nombre de threads à cause de la contention ; celui de l'incrémentation ordinaire ne bouge pas.

E2 · ★★ ⏱ 2 h — ThreadSanitizer sur du code cassé. Écrire cinq programmes avec chacun une course subtile : compteur non protégé, initialisation paresseuse, double verrouillage naïf, volatile utilisé comme synchronisation, lecture pendant écriture de structure. Vérifier que TSan les trouve et que les tests fonctionnels, eux, passent.

E3 · ★★★★ ⏱ 12 h — La bibliothèque de threads utilisateur. Le mini-projet de MPPT24, en version préparée :

• création avec pile allouée séparément ;
• changement de contexte, par swapcontext/makecontext d'abord, puis en assembleur si vous voulez aller au bout ;
• un ordonnanceur round-robin ;
• les primitives yield, join, et un mutex ;
• la mesure du coût d'un changement de contexte, comparé à pthread_create et à un changement de contexte noyau.

C'est le projet P10 de ce document, ici encadré et noté.

E4 · ★★★★ ⏱ 6 h — Une barrière à la main. Implémenter trois barrières : centralisée avec compteur atomique, à arbre, et par diffusion. Mesurer les trois de 2 à N threads. La centralisée s'écroule par contention, l'arbre est en \(O(\log p)\). C'est l'exercice qui enseigne la contention mieux que n'importe quelle explication.

E5 · ★★★ ⏱ 4 h — Du model-checking au code. Modéliser un protocole de synchronisation simple — l'exclusion mutuelle de Peterson, ou un producteur- consommateur borné — dans l'environnement de vérification vu en cours. Puis l'implémenter en C avec des atomiques, et vérifier sous TSan. Comparer ce que chaque approche détecte.

Projet

Projet PRCV24 · l'ordonnanceur avec vol de travail

⏱ 25 h · ★★★★ · Extension naturelle du mini-projet

Reprendre la bibliothèque de threads utilisateur de E3 et lui ajouter le vol de travail : chaque ordonnanceur a sa file locale de tâches prêtes et vole dans les files des autres quand il est inactif.

Les quatre étapes :

1. Une file de tâches par cœur, et un thread noyau par cœur qui la consomme.
2. Le vol : quand une file est vide, en choisir une autre au hasard et prendre une tâche à l'autre bout de la file — ce détail compte, il réduit la contention.
3. La mesure du déséquilibre : sur un ensemble de tâches de durées très variables, comparer le temps total avec un ordonnancement statique et avec le vol de travail.
4. La comparaison avec #pragma omp task, qui fait exactement cela.

Le résultat à obtenir : sur une charge déséquilibrée, le vol de travail récupère l'essentiel de l'écart entre l'ordonnancement statique et l'optimum. C'est la garantie théorique de Blumofe et Leiserson, constatée sur votre propre code.

Pourquoi ce projet. Parce qu'il vous fait écrire, en vingt-cinq heures, le cœur de ce que font OpenMP, TBB, Cilk et StarPU — et qu'après cela, ces bibliothèques cessent d'être des boîtes noires.

Erreurs fréquentes

Six pièges du multithread

1. Croire qu'une boucle parallélisée va plus vite. Si elle est limitée par la bande passante mémoire, quatre threads saturent déjà le contrôleur.
2. Le faux partage. Deux threads qui écrivent dans la même ligne de cache : facteur 5 à 20, invisible sans perf c2c.
3. Croire que volatile synchronise. Il empêche certaines optimisations du compilateur et ne génère aucune barrière mémoire. C'est l'erreur la plus répandue.
4. Déboguer un code concurrent au printf. L'entrelacement rend le diagnostic impossible et le printf modifie le comportement temporel.
5. Écrire du code sans verrou (lock-free) sans avoir lu la littérature. Utilisez les primitives existantes, qui sont correctes.
6. Oublier que la réduction flottante n'est pas reproductible. Le résultat dépend du nombre de threads, parce que l'addition flottante n'est pas associative. Ce n'est pas un bug, mais il faut le savoir avant d'écrire un test d'égalité.

Comment l'UE s'articule avec le reste

UE ou chapitre	Lien
SYEX11 (S1, tronc commun)	Les threads y sont introduits
LASF24 (S4, tronc commun)	Prérequis, suivi en parallèle
ICPA24 (S4, tronc commun)	Introduit les threads et OpenMP ; PRCV24 les approfondit
PRPA23 (S3, option)	MPI + threads = programmation hybride
PGPU35 (S5)	Le modèle de threads du GPU, à comparer
OpenMP et threads	Le complément : les cinq causes d'échec, les runtimes de tâches
ICPA24	L'UE équivalente en formation sous statut étudiant, plus large sur OpenMP

---

À retenir

PRCV24 en trois phrases

C'est la seule option HPC du semestre 4, et son module MPPT24 contient le mini-projet le plus formateur du cursus : écrire une bibliothèque de threads utilisateur, et mesurer qu'un changement de contexte y coûte cent fois moins qu'un thread noyau.

Le module COMC24 comble un manque unique : la vérification formelle de programmes concurrents n'apparaît nulle part ailleurs, et c'est le domaine où l'intuition est le plus souvent fausse.

Le prérequis LASF24 se suit au même semestre : ce n'est pas bloquant, mais prenez de l'avance si la logique n'est pas votre terrain.

Fiche suivante : Semestre 5 · vue d'ensemble.