X ENS Informatique C MPI 2026Sujet

Vérification de systèmes concurrents

Rappels

Langage C

Langage OCaml

• -Si lst1 et lst2 sont deux listes, lst1 @ lst2 est leur concaténation. Elle se calcule en temps linéaire en la longueur de lst1. L'ajout e::lst d'un élément e en tête de la liste lst se fait en temps constant.
• -List.mem x lst renvoie true s'il existe un élément e de la liste lst tel que x = e, et false sinon. Elle s'exécute en temps linéaire en la longueur de lst.
• -List.assoc k [(k_1, v_1); …; (k_n, v_n)] renvoie le premier v_i tel que k = k_i s'il existe, et lève l'exception Not_found sinon. Elle s'exécute en temps linéaire en la longueur de la liste.
• -List.iter f [e_1; …; e_n] exécute f e_i pour i = 1, 2, …, n, et renvoie (). Son temps d'exécution est la somme des temps d'exécution des f e_i.
• -List.map f [e_1; …; e_n] renvoie [f e_1; …; fe_n ]. Son temps d'exécution est la somme des temps d'exécution des f e_i.
• -List.filter f lst renvoie la liste des éléments e de lst tels que f e = true, dans l'ordre. Son temps d'exécution est la somme des temps d'exécution des f e.
• -List.fold_left f a_0[e_1; …; e_n] renvoie a_n où a_(k + 1) = fa_k e_(k + 1) pour tout 0 ≤ k < n. Son temps d'exécution est la somme des temps d'exécution des f a_k e_(k + 1).

• -Array.init n f renvoie le tableau [|f 0;…;f (n-1)|] pour n positif. Son temps d'exécution est la somme des temps des f i pour i = 0, 1, . . , , n-1.
• -Array.make n v renvoie le tableau [|v;...;v|] de taille n dont chaque case contient la même valeur v, pour n positif. Son temps d'exécution est linéaire en n.

Partie I : Systèmes de transitions

• -un ensemble fini d'états S;
• -un ensemble fini d'actions A;
• -une application D : S → 2^A indiquant pour chaque état s l'ensemble D(s) des actions disponibles en s;
• -une fonction partielle δ : S × A → S de domaine {(s, α) ∈ S × A|α ∈ D(s)} indiquant pour chaque état s et α ∈ D(s) le résultat δ(s, α) de la transition α depuis s.

Figure 1 - Représentation graphique d'un système de transitions simple.

• (a)L'ensemble I est un invariant.
• (b)Pour tout s ∈ I, on a s⊨P.

• 1. P_1 = {w ∈ S^ω||w|_s = 0 pour au moins un s ∈ S}
• 2. P_2 = {w ∈ S^ω||w|_s = + ∞ pour tout s ∈ S}
• 3. P_3 = {w ∈ S^ω||w|_s < + ∞ pour au moins un s ∈ S}

• 1. P_1 = {w ∈ S^ω||u|_a = 0 pour tout u ∈ Σ^∗ préfixe de w}
• 2. P_2 = {w ∈ S^ω|‖u|_a − |u|_b|≤1 pour tout u ∈ Σ^∗ préfixe de w}
• 3. P_3 = {w ∈ S^ω||u|_a ≤ |u|_b pour tout u ∈ Σ^∗ préfixe de w}
• 4. P_4 = {w ∈ S^ω||u|_a ≤ |u|_b ≤ |u|_a + 1 pour tout u ∈ Σ^∗ préfixe de w}

type trans_sys = {
    size : int; (* états = { 0,1,...,size-1 } *)
    next : state -> (action * state) list; (* transitions *)
}

• • -les états sont les entiers positifs (ou nuls) strictement inférieurs à t.size;
  • -les transitions à partir d'un état s sont données par t.next s, qui est une liste d'associations sans répétition d'une même action : on a s a s' pour tout (a, s') dans t.next s.

val reachable : trans_sys -> state -> (state -> bool) -> bool

Partie II : Ultime invariance

Figure 2 - Exemple de système sur A = {α, β}.

(** Parcours externe: [outer_iter t sO f] appelle la fonction [f] sur
    tous les états [s] accessibles à partir de [s0]. *)
let outer_iter (t:trans_sys) (s0:state) (f:state->unit) : unit =
    ... (* Implémentation à réaliser en question 10. *)
(** Exception utilisée pour interrompre la recherche. *)
exception Found
(** [verify t phi sO] vérifie que [sO] satisfait [EA phi].
        Ici [phi] n'est pas un ensemble mais une fonction,
        représentant l'ensemble des états [s] tels que [phi s = true]. *)
let verify (t:trans_sys) (phi:state->bool) (s0:state) : bool =
    (* Parcours internes: détection de cycle *)
    let marked = Array.make t.size false in
    let cycle_check start =
        let rec inner_visit s =
            if not marked.(s) then begin
                marked.(s) <- true;
                List.iter
                    (fun (_,s') ->
                        if s' = start then raise Found;
                        inner_visit s')
                    (t.next s)
            end
        in
        inner_visit start
    in
    (* Parcours externe: états accessibles *)
    try
        outer_iter t s0
            (fun s' -> if not (phi s') then cycle_check s');
        true
    with Found -> false

• (a)L'énumération suit un ordre postfixe.
• (b)Si deux nœuds s et s^′ ont le même parent dans l'arbre, et que s a été visité avant s^′ dans le parcours en profondeur, alors s (et tous ses descendants dans l'arbre) apparaît avant s^′ (et tous ses descendants) dans l'énumération.

Partie III : Programmation multi-threads en C

• -La fonction pthread_create lance un nouveau thread (en français, fil d'exécution). Elle prend en premier argument un pointeur pthread vers un descripteur de thread dans lequel les informations concernant le nouveau thread seront remplies, pour permettre de s'y référer ensuite. En second argument, elle prend un pointeur attr vers des attributs de threads; il n'est pas utile d'en connaître la teneur exacte, car on se contentera de donner ici une valeur par défaut décrite plus loin. En troisième argument, elle prend une fonction start_routine qui attend un argument de type void* et renvoie une valeur du même type - on ignorera cette valeur de retour dans le sujet. En dernier argument est donnée la valeur arg qui sera passée à la fonction start_routine pour démarrer le calcul dans le nouveau thread.
• -La fonction pthread_join permet d'attendre la fin de l'exécution du thread dont le descripteur est donné en premier argument. Dans ce sujet, on lui passera toujours NULL en second argument, et on ignorera l'entier renvoyé.
• -La fonction pthread_attr_init prend en argument un pointeur vers des attributs de thread, et initialise ces attributs avec des valeurs par défaut. On ignorera l'entier renvoyé.

• a.Quels sont les affichages possibles à la fin de l'exécution du programme de la figure 5 ? Expliquer brièvement comment chaque valeur peut être obtenue.
• b.L'objectif de ce programme est manifestement d'obtenir dans m le maximum des quatre entiers contenus dans array. Quelle est la façon canonique de corriger notre programme pour éviter les exécutions menant à un résultat incorrect? Proposer une correction du programme par l'insertion de quelques lignes ^1. On ne demande pas de produire du code C valide : une description haut niveau des instructions à insérer suffit.

/* Les types pthread_t (descripteur de thread)
    et pthread_attr_t (attributs de thread)
    sont déclarés dans <pthread.h>.
    Il est inutile de préciser leurs définitions. */
int pthread_attr_init(pthread_attr_t *attr);
int pthread_create(pthread_t *pthread,
        pthread_attr_t *attr,
        void *(*start_routine)(void *),
        void *arg);
int pthread_join(pthread_t pthread, void **retval);

int m = -1;
void* max2(void* pair) {
    int m1 = ((int*)pair)[0];
    int m2 = max(m1, ((int*)pair)[1]);
    int m3 = max(m2, m);
    m = m3;
    return NULL;
}
int main() {
    int array[4] = {10, 20, 30, 40};
    /* Attributs par défaut des threads */
    pthread_attr_t attr;
    pthread_attr_init(&attr);
    /* Création des threads */
    pthread_t thread1, thread2;
    pthread_create(&thread1, &attr, max2, array);
    pthread_create(&thread2, &attr, max2, &(array[2]));
    /* Attente de fin et affichage du résultat */
    pthread_join(thread1, NULL);
    pthread_join(thread2, NULL);
    printf("m == %d\n", m);
}

• -const int nb_threads indiquant le nombre de threads à utiliser ;
• -const int items_per_thread indiquant combien de valeurs chaque thread devra traiter;
• -int m, initialisée à -1, destinée à contenir le résultat final du calcul comme dans l'exemple de la figure 5.

• -La fonction doit être appelée (précondition) avec en argument a l'adresse d'un tableau contenant (au moins) items_per_thread éléments de type int, tous positifs.
• -À titre indicatif, la fonction calcule alors le maximum v de ces items_per_thread éléments, puis effectue l'affectation m = v si la variable globale m est inférieure à v. Le fonctionnement précis de la fonction n'a cependant pas d'importance dans la suite du sujet.

• a.Alloue sur le tas un tableau array de nb_threads*items_per_thread valeurs de type int.
• b.Initialise chaque case du tableau avec un entier positif pseudo-aléatoire. Celui-ci sera simplement obtenu via l'expression rand()%max_item qui renvoie un entier entre 0 (inclus) et max_item (exclu), cette dernière variable étant supposée déclarée globalement.
• c.Lance nb_threads exécutant tous la fonction local_max, appelée dans chaque thread sur l'adresse d'un sous-tableau de array commençant à un index de la forme k*items_per_thread, de sorte que chaque valeur du tableau sera prise en compte par exactement un thread.
• d.Affiche la valeur de m une fois que tous les threads ont terminé leur exécution.

Partie IV : Systèmes de transitions concurrents

• -Exécuter α ne change pas la disponibilité de β : pour tout s ∈ S tel que α ∈ D(s), on a β ∈ D(s) ⇔ β ∈ D(δ(s, α)).
• -Exécuter β ne change pas la disponibilité de α : pour tout s ∈ S tel que β ∈ D(s), on a α ∈ D(s) ⇔ α ∈ D(δ(s, β)).
• -L'ordre d'exécution de α et β n'a pas d'importance : pour tout s ∈ S tel que α ∈ D(s) et β ∈ D(s), on a δ(δ(s, α), β) = δ(δ(s, β), α). L'indépendance de α et β est notée α ↔ β. Elle peut être résumée de façon moins précise mais visuelle comme suit, pour tout état s, avec s^′ = δ(δ(s, α), β) = δ(δ(s, β), α) :
  

  

• (A1) X ≠ ∅ si D(s_0) ≠ ∅.
• (A2)Pour toute exécution s_0→−^(α_0)…→−^(α_n)s_(n + 1) à partir de s_0 et telle que α_i ∉ X pour tout i ≤ n, on a α_i ↔ X pour tout i ≤ n.