Analyse du sujet d'Informatique C MPI X/ENS 2026 : vérification de systèmes concurrents

Partie I : systèmes de transitions et propriétés de trace

La première partie posait le cadre formel du sujet. Un système de transitions T = (S, A, D, δ) est composé d'un ensemble fini d'états S, d'un ensemble fini d'actions A, d'une application D indiquant les actions disponibles en chaque état, et d'une fonction de transition partielle δ. Une exécution infinie est une suite infinie d'états et d'actions vérifiant les transitions, et sa trace est la suite des états visités. Une propriété de trace P est un ensemble de mots infinis sur S ; un état s satisfait P si toutes ses exécutions infinies ont une trace dans P.

La question 1 demandait de montrer l'équivalence entre invariance et satisfaction universelle d'une propriété de trace de la forme I^ω dans un système sans état terminal. La démonstration reposait sur la définition même d'un invariant : I est un invariant si et seulement si δ(s, α) ∈ I pour tout s ∈ I et α ∈ D(s), ce qui traduit exactement le fait que toute exécution infinie à partir d'un état de I reste dans I. C'était une question de mise en route, accessible à tous, qui servait à s'approprier le formalisme.

La question 2 portait sur les propriétés de sûreté, définie comme la propriété P telle que pour tout mot w ∉ P, il existe un préfixe fini interdit au-delà duquel aucun prolongement n'est dans P. Les candidats devaient identifier lesquelles parmi trois propriétés données étaient des propriétés de sûreté. La question 3 travaillait sur les propriétés régulières dans un système à deux états, en demandant de construire les automates reconnaissant les ensembles de préfixes interdits minimaux pour quatre propriétés de sûreté concrètes. C'était la question la plus technique de la partie I, mêlant raisonnement combinatoire sur les mots et construction d'automates.

La question 4 demandait de montrer que l'ensemble des préfixes interdits minimaux est régulier si et seulement si l'ensemble de tous les préfixes interdits est régulier, résultat non trivial dont la preuve reposait sur la clôture des langages réguliers par quotient. La question 5 portait sur l'implémentation en OCaml d'une fonction reachable vérifiant l'accessibilité d'un ensemble d'états cibles dans un système de transitions, en temps linéaire en le nombre d'états et de transitions. La question 6 proposait de ramener la vérification d'une propriété de sûreté à un problème d'inaccessibilité dans un système de transitions augmenté, construit à partir du produit du système T et de l'automate A reconnaissant les préfixes interdits minimaux.

Partie II : ultime invariance et parcours en profondeur imbriqués

La partie II introduisait la notion d'ultime invariance, notée EAΦ (eventually always Φ), définie comme la propriété des mots infinis w tels qu'à partir d'un certain rang, tous les états sont dans Φ. Autrement dit, w satisfait EAΦ si et seulement si la trace finit par rester indéfiniment dans Φ. La question 7 demandait d'identifier, sur un système concret donné en figure 2, les états satisfaisant EAΦ et EAΦ^ω pour un ensemble Φ = {s₂, s₄, s₅, s₆} donné. Ce travail d'analyse graphique, bien que manuel, était essentiel pour comprendre la suite.

La question 8 était le résultat pivot de la partie : montrer que s ⊭ EAΦ si et seulement s'il existe un état accessible depuis s qui est hors de Φ et qui fait un cycle. Cette caractérisation transforme la vérification d'une propriété de liveness infinie en un problème de détection de cycle dans un graphe fini, ce qui est algorithmiquement traitable. La preuve directe reposait sur la construction d'une exécution infinie qui revient indéfiniment sur un état hors de Φ ; la réciproque découlait de la définition même d'EAΦ.

L'algorithme des parcours en profondeur imbriqués (figure 3) était ensuite présenté, avec deux niveaux de parcours : un parcours externe (outer_iter) qui explore tous les états accessibles depuis s₀, et pour chaque état hors de Φ, un parcours interne (cycle_check) qui vérifie si cet état est dans un cycle. L'astuce de l'algorithme est que tous les parcours internes partagent un tableau marked commun : ainsi, chaque état n'est traité par inner_visit qu'au plus une fois au cours de tous les appels à cycle_check, ce qui garantit une complexité linéaire globale.

La question 9 demandait de montrer une propriété cruciale de l'énumération postfixe des états : si s₁ apparaît avant s₂ dans cette énumération et qu'il existe une exécution de s₁ à s₂, alors s₁ fait un cycle sur lui-même. La preuve reposait sur les propriétés de l'ordre postfixe dans un parcours en profondeur : si s₁ est énuméré avant s₂, c'est que s₁ a été entièrement traité (avec tous ses descendants) avant que s₂ ne soit énuméré, ce qui implique que le chemin de s₁ à s₂ repasse nécessairement par s₁. C'est une question de démonstration formelle que peu de candidats ont probablement traitée complètement.

La question 10 demandait d'implémenter outer_iter en OCaml en garantissant l'ordre postfixe requis. La question 11 portait sur la spécification de cycle_check et la preuve de correction de verify. La question 12 interrogeait sur la robustesse de l'algorithme : la fonction verify reste-t-elle correcte si outer_iter parcourt les états en ordre préfixe plutôt que postfixe ? La réponse était non, et un contre-exemple à moins de quatre états suffisait à l'illustrer : un cycle de longueur 2 entre deux états hors de Φ aurait pu ne pas être détecté si le premier état était traité dans le parcours interne avant que le second ne soit visité dans le parcours externe.

Partie III : programmation multi-threads en C avec pthread

La partie III rappelait les éléments de programmation concurrente en C via la bibliothèque pthread. Les trois fonctions présentées étaient pthread_create (lancement d'un nouveau thread), pthread_join (attente de la terminaison d'un thread) et pthread_attr_init (initialisation des attributs d'un thread avec les valeurs par défaut).

La question 13 portait sur un programme C concret (figure 5) calculant le maximum de quatre entiers contenus dans un tableau de taille 4, réparti sur deux threads. La sous-question a demandait quels affichages sont possibles à la fin de l'exécution. La réponse dépendait de l'ordre d'entrelacement des threads : les deux threads lisent et écrivent la variable globale msans synchronisation, ce qui crée une course aux données (data race). Les affichages possibles comprenaient des résultats incorrects comme 30 ou 40, en plus du résultat correct 40. La sous-question b demandait comment corriger le programme pour garantir l'exclusion mutuelle, typiquement par l'ajout d'un mutex protégeant les accès à m.

La question 14 generalisait à nb_threads threads calculant le maximum de nb_threads * items_per_thread valeurs, et demandait d'écrire une fonction main complète en C : allocation dynamique du tableau sur le tas, initialisation pseudo-aléatoire, lancement de nb_threadsthreads appelant chacun local_max sur un sous-tableau distinct, attente de tous les threads, affichage du résultat et libération de la mémoire. Il était précisé que cette question ne demandait pas de gérer les accès concurrents à m.

Partie IV : systèmes de transitions concurrents et réduction de l'explosion combinatoire

La partie IV était la plus ambitieuse et la plus originale du sujet. Elle s'intéressait à la modélisation des programmes multi-threads par des systèmes de transitions, en mettant en évidence le phénomène d'explosion combinatoire due aux entrelacements d'instructions concurrentes, et en introduisant des techniques théoriques pour le réduire.

La question 15 demandait de compter le nombre d'exécutions différentes de longueur 8 dans le système modélisant le programme de la figure 5. Avec deux threads effectuant chacun 4 instructions, le nombre d'entrelacements possibles est C(8,4) = 70, ce qui illustre concrètement l'explosion combinatoire dès l'échelle d'un programme simple.

La notion centrale de la partie IV était celle d'actions indépendantes. Deux actions α et β sont indépendantes (noté α ↔ β) si leur exécution simultanée est commutative : D(s) contient β si et seulement si D(δ(s, α)) le contient, D(s) contient α si et seulement si D(δ(s, β)) le contient, et δ(δ(s, α), β) = δ(δ(s, β), α). La question 16 demandait d'analyser les indépendances dans le système de la figure 5 pour les états s₀, s', s₁ et s''.

La question 17 étudiait les ensembles persistants pour un état s₀ : un sous-ensemble X de D(s₀) non vide tel que, dans toute exécution commençant par des actions hors de X, les actions de X restent disponibles et indépendantes de toutes les actions hors de X. La propriété fondamentale des ensembles persistants est qu'ils permettent de ne pas explorer toutes les transitions disponibles depuis un état, mais seulement celles d'un ensemble persistant minimal, sans perdre d'information sur les propriétés à vérifier. Les questions 17 à 19 construisaient progressivement les fondements théoriques justifiant cette réduction.

La question 20 introduisait la notion d'ordre induit par un mot sans répétition u sur son alphabet, défini comme la plus petite relation transitive telle que u_i <_u u_j si i < j et u_i ↔ u_j. Les questions 20 et 21 travaillaient sur des exemples concrets et montraient que deux mots sans répétition contenant les mêmes lettres sont équivalents pour la relation de permutation si et seulement si leurs ordres induits coïncident.

La partie se concluait sur la notion de mise en veille (sleep sets). Pour un système T et un ordre total sur les actions, le système T^< = (S^<, A, D^<, δ^<) est défini avec des états qui sont des paires (s, Z) où s est un état de T et Z est un ensemble d'actions en veille. L'idée est qu'une action α en veille ne sera pas exécutée depuis (s, Z) si elle est indépendante de toutes les actions exécutées depuis s₀. Les questions 22 à 24 étudient concrètement ce mécanisme sur le programme de la figure 6, en construisant le système T et son système avec mise en veille T^<, et en prouvant que la mise en veille sélectionne précisément les représentants lexicographiques minimaux des classes d'équivalence par permutation.