Concurrence¶

Comprendre les modèles fondamentaux de la concurrence — avant de distribuer, il faut savoir synchroniser.

Pourquoi la concurrence est centrale¶

Des qu'un système a plus d'un fil d'exécution — threads, processus, services, nœuds — les problèmes de concurrence emergent. L'ordre d'exécution n'est plus deterministe. Deux opérations qui lisent et ecrivent la même donnée peuvent produire un résultat différent selon leur entrelacement.

Raynal (Concurrent Programming: Algorithms, Principles, and Foundations) pose le cadre : la concurrence n'est pas un problème a éviter, c'est une propriété a maîtriser. Les systèmes distribués modernes sont intrinsequement concurrents. Comprendre les fondations permet de choisir les bons patterns plutôt que de subir les bugs de concurrence en production.

La concurrence se manifeste a tous les niveaux :

Mémoire partagee vs passage de messages¶

Deux grands modèles de concurrence coexistent. Le choix conditionne l'architecture du système.

Mémoire partagee (shared memory)¶

Les threads ou processus accedent a une zone mémoire commune. La synchronisation passe par des primitives de verrouillage : mutex, semaphores, variables conditionnelles. C'est le modèle dominant dans les langages imperatifs (Java, C++, C#).

sequenceDiagram
    participant A as Thread A
    participant M as Mutex
    participant B as Thread B

    A->>M: lock(mutex)
    Note over B,M: Thread B bloque
    B--xM: lock(mutex)
    A->>A: counter += 1
    A->>M: unlock(mutex)
    M->>B: lock(mutex) accorde
    B->>B: counter += 1
    B->>M: unlock(mutex)

Avantages : faible latence (pas de copie de données), modèle familier. Inconvénients : risque de deadlock, race conditions subtiles, difficulté a raisonner sur l'entrelacement.

Passage de messages (message passing)¶

Les acteurs ou processus communiquent en s'envoyant des messages. Aucune donnée n'est partagee directement. Le modèle d'acteurs (Hewitt, Agha) formalise cette approche : chaque acteur a une boite aux lettres, traite un message à la fois, et peut créer d'autres acteurs.

graph LR
    A[Acteur A] --"message: increment"--> B[Acteur B<br/>etat: counter=0]
    B --"message: result(1)"--> A
    C[Acteur C] --"message: increment"--> B
    B --"message: result(2)"--> C

Erlang/OTP, Akka (Scala/Java), et Go (channels) implementent ce modèle. L'absence de mémoire partagee élimine les deadlocks classiques mais introduit d'autres problèmes : mailbox overflow, message ordering, livelock.

Exclusion mutuelle¶

L'exclusion mutuelle garantit qu'un seul processus à la fois accede a une section critique. Sans elle, les entrelacements produisent des états incoherents.

Problème fondamental¶

Deux threads incrementent un compteur partage :

sequenceDiagram
    participant A as Thread A
    participant C as counter = 5
    participant B as Thread B

    A->>C: read(counter) = 5
    B->>C: read(counter) = 5
    A->>C: write(counter, 6)
    B->>C: write(counter, 6)
    Note over C: perdu : devrait etre 7

C'est une race condition. Le résultat dépend de l'ordre d'exécution, qui n'est pas garanti.

Algorithme de Peterson¶

Pour deux processus, l'algorithme de Peterson résout l'exclusion mutuelle sans support matériel :

flag[0] = false, flag[1] = false
turn = 0

Process i:
    flag[i] = true
    turn = 1 - i
    while flag[1-i] and turn == 1-i:
        wait
    // section critique
    flag[i] = false

En pratique, on utilise des primitives système (mutex POSIX, synchronized Java, lock C#) qui s'appuient sur des instructions atomiques du processeur (compare-and-swap, test-and-set).

Semaphores¶

Generalisation de l'exclusion mutuelle. Un semaphore autorise N accès simultanés (N=1 pour un mutex). Dijkstra a formalisé les opérations P (wait/acquire) et V (signal/release).

Cas d'usage : limiter le nombre de connexions a une base de données, contrôler l'accès concurrent a une ressource partagee avec capacité limitee.

Deadlock, livelock, starvation¶

Trois pathologies de la concurrence, distinctes mais souvent confondues.

Deadlock¶

Deux processus s'attendent mutuellement, chacun detenant une ressource dont l'autre a besoin. Les quatre conditions de Coffman doivent être reunies simultanément :

1. Exclusion mutuelle : la ressource n'est pas partageable
2. Hold and wait : un processus detient une ressource et en attend une autre
3. No preemption : on ne peut pas forcer un processus a libérer sa ressource
4. Circular wait : chaîne circulaire d'attente

graph LR
    PA[Process A<br/>detient Lock 1] --"attend Lock 2"--> PB[Process B<br/>detient Lock 2]
    PB --"attend Lock 1"--> PA

Prevention : ordonner les acquisitions de verrous (toujours acquerir Lock 1 avant Lock 2). Si tous les processus respectent le même ordre, la condition de circular wait est cassee.

Détection : construire un graphe d'attente et chercher les cycles. Les bases de données relationnelles le font nativement et tuent la transaction la moins coûteuse.

Livelock¶

Les processus changent d'état en réaction l'un à l'autre mais aucun ne progresse. Contrairement au deadlock, ils ne sont pas bloques — ils bougent, mais inutilement. Analogie : deux personnes dans un couloir qui se decalent du même côté simultanément.

Solution : introduire du jitter (délai aléatoire) dans les retries. C'est la stratégie d'Ethernet (CSMA/CD) et des algorithmes de backoff exponential.

Starvation¶

Un processus ne reçoit jamais l'accès à la ressource, non pas à cause d'un deadlock mais parce que d'autres processus sont toujours prioritaires. Un verrou non equitable peut provoquer la starvation : les processus qui arrivent en dernier sont systematiquement servis avant ceux qui attendent depuis longtemps.

Solution : utiliser des verrous equitables (FIFO) ou des mécanismes de vieillissement de priorité (aging).

Consensus distribué¶

Quand plusieurs nœuds doivent s'accorder sur une valeur — l'election d'un leader, l'ordre des transactions, la configuration du cluster — on a besoin d'un protocole de consensus.

Le problème du consensus¶

Chaque nœud propose une valeur. Le protocole doit garantir :

• Accord : tous les nœuds corrects decidem la même valeur
• Validite : la valeur décidée a été proposee par un nœud
• Terminaison : tous les nœuds corrects finissent par décider

Le résultat d'impossibilite FLP (Fischer, Lynch, Paterson) montre qu'aucun algorithme deterministe ne peut garantir le consensus dans un système asynchrone avec un seul nœud defaillant. En pratique, on contourne cette limite avec des timeouts (rendant le système partiellement synchrone).

Paxos (Lamport)¶

Paxos est le premier algorithme de consensus correct et prouve. Lamport l'a formalisé en 1989. Il fonctionne en deux phases :

1. Préparé : le proposer envoie un numéro de proposition N a une majorité de nœuds (acceptors). Chaque acceptor répond avec la dernière valeur qu'il a acceptee (si elle existe).
2. Accept : le proposer envoie la valeur a adopter avec le numéro N. Les acceptors l'acceptent si ils n'ont pas vu de numéro supérieur depuis.

Paxos est correct mais notoirement difficile à implémenter et a comprendre. Multi-Paxos optimise pour les sequences de décisions.

Raft¶

Raft (Ongaro, Ousterhout, 2014) a été conçu explicitement pour être plus comprehensible que Paxos, avec les mêmes garanties. Il decompose le consensus en trois sous-problèmes indépendants :

1. Election du leader : un seul leader à la fois, elu par majorité
2. Réplication du log : le leader reçoit les écritures et les répliqué sur les followers
3. Sécurité : un nœud ne peut être elu leader que s'il à le log le plus à jour

sequenceDiagram
    participant F1 as Follower 1
    participant L as Leader
    participant F2 as Follower 2

    L->>F1: AppendEntries(entry X)
    L->>F2: AppendEntries(entry X)
    F1-->>L: ack
    F2-->>L: ack
    Note over L: majorite atteinte → commit
    L->>F1: commit(entry X)
    L->>F2: commit(entry X)

etcd (utilisé par Kubernetes), Consul, et CockroachDB implementent Raft. C'est le standard de facto pour les nouveaux systèmes distribués.

Horloges logiques¶

Dans un système distribué, les horloges physiques ne sont jamais parfaitement synchronisées. Les horloges logiques capturent la causalite sans dépendre du temps physique.

Horloge de Lamport¶

Chaque processus maintient un compteur. Les règles :

1. Avant chaque événement local : incrementer le compteur
2. À l'envoi d'un message : inclure le compteur dans le message
3. À la reception : compteur = max(compteur_local, compteur_message) + 1

L'horloge de Lamport capture la relation "happened-before" : si a → b, alors L(a) < L(b). Mais la reciproque est fausse : L(a) < L(b) ne signifie pas que a à cause b.

Horloges vectorielles¶

Chaque processus maintient un vecteur de taille N (nombre de processus). Elles capturent la causalite complète : V(a) < V(b) si et seulement si a → b.

Processus A:  [1,0,0] → [2,0,0] → [3,2,0]
Processus B:  [0,1,0] → [2,2,0]
Processus C:  [0,0,1] → [0,0,2]

Deux événements sont concurrents si ni l'un ni l'autre ne domine l'autre dans l'ordre partiel. Les horloges vectorielles detectent cette concurrence, ce que les horloges de Lamport ne peuvent pas faire.

Usage pratique : DynamoDB utilise des horloges vectorielles pour détecter les conflits d'écriture concurrente. Riak les utilise pour la résolution de conflits.

Horloge hybride (HLC)¶

Combine une horloge physique et un compteur logique. CockroachDB et Spanner utilisent des variantes pour ordonner les transactions avec une précision suffisante sans synchronisation parfaite des horloges.

Spécification formelle et automates¶

Pour raisonner sur la correction d'un système concurrent, on utilise des modèles formels. Linz (An Introduction to Formal Languages and Automata) fournit les bases.

Automates finis et protocoles¶

Un protocole de communication peut être modélisé comme un automate a états finis. Chaque état représenté une situation du système, chaque transition un événement ou un message.

stateDiagram-v2
    [*] --> Idle
    Idle --> Requesting: send_request
    Requesting --> Locked: grant
    Locked --> Idle: release
    Requesting --> Requesting: deny / retry

Modéliser le protocole en automate permet de vérifier formellement :

• L'absence de deadlock : aucun état sans transition sortante (sauf les états finaux)
• L'accessibilite : tous les états sont atteignables depuis l'état initial
• La vivacite : une propriété finira par être satisfaite (le verrou sera obtenu)

Surete et vivacite¶

Deux catégories de propriétés a vérifier sur un système concurrent :

La surete est verifiable sur des executions finies. La vivacite nécessité de raisonner sur des executions infinies. Un système qui ne fait jamais rien satisfait toutes les propriétés de surete mais aucune propriété de vivacite.

TLA+ et model checking¶

Lamport a créé TLA+ pour specifier et vérifier les systèmes distribués. Le model checker TLC explore tous les entrelacements possibles et détecté les violations de propriétés.

Amazon utilisé TLA+ pour vérifier les algorithmes de DynamoDB, S3, et EBS. Microsoft l'utilisé pour Azure Cosmos DB. Ce n'est pas un outil academique — c'est un outil de production pour les systèmes critiques.

---- MODULE Counter ----
VARIABLES counter, pc

Init == counter = 0 /\ pc = "start"

Increment == pc = "start"
          /\ counter' = counter + 1
          /\ pc' = "done"

Spec == Init /\ [][Increment]_<<counter, pc>>

Safety == counter >= 0
====

Chapitre suivant : Applications reparties — client-serveur, RPC, serialisation et découverte de services.