Résumé

  • La relation happened-before est le plus petit ordre partiel engendré par l’ordre local d’un processus, l’arête entre l’envoi et la réception d’un même message, puis la transitivité.
  • La Clock Condition ne va que dans un sens : a → b impose C(a) < C(b). Une valeur scalaire plus petite ne prouve pas qu’a a causé, informé ou physiquement précédé b.
  • Deux événements concurrents n’ont aucun chemin happened-before dans un sens ou l’autre. Ils sont non ordonnés dans le modèle observé, et non nécessairement simultanés sur une horloge physique.

Deux services inscrivent deux lignes qui semblent raconter toute l’histoire. L’événement A porte le temps logique 41, B le temps 42. Le tableau de bord trie, dessine une flèche et suggère qu’A a provoqué B. Les nombres rendent ce récit lisible ; ils ne le rendent pas démontré.

L’article de Leslie Lamport publié en 1978, Time, Clocks, and the Ordering of Events in a Distributed System, ne cherchait pas une horloge universelle cachée. Il fixait la limite exacte de l’ordre qu’un système distribué peut justifier sans en avoir une.

Le plus petit ordre compatible avec les traces

Lamport décrit des processus composés chacun d’une suite d’événements et reliés par des messages. La relation happened-before est la plus petite relation satisfaisant trois règles : l’ordre interne d’un processus ; l’envoi d’un message avant la réception de ce même message ; la transitivité de ces deux types d’arêtes.

« Plus petite » signifie que les trous restent des trous. Lorsque ni a → b ni b → a ne tient, les événements sont concurrents. Le modèle ne choisit pas arbitrairement lequel placer en premier.

Lamport explique qu’a → b signifie qu’a peut affecter causalement b. Il existe un chemin par lequel de l’information pourrait se propager. Ce n’est pas encore la preuve que le contenu d’a a produit le résultat de b, qu’un humain l’a voulu ou qu’une responsabilité peut être attribuée. L’accessibilité causale et la cause sémantique ne sont pas le même dossier de preuve.

Même la définition de l’événement compte. Une note du papier observe que la réception peut être modélisée par la pose d’un bit d’interruption ou par l’exécution du gestionnaire ; le choix modifie l’ordre des événements. Une chronologie sans définition de ses unités est déjà ambiguë.

Une implication qui n’a pas de réciproque

Une horloge logique attribue un nombre aux événements. La Clock Condition exige que a → b entraîne C(a) < C(b). Pour l’obtenir, chaque processus augmente son compteur entre deux événements, joint sa valeur aux messages et, à la réception, avance son horloge au-delà de sa valeur actuelle et de l’horodatage reçu.

Ces règles empêchent une arête known happened-before de remonter numériquement le temps. Elles ne permettent pas de conclure, à partir de C(a) < C(b), qu’a → b.

Lamport montre pourquoi la réciproque est impossible avec un simple scalaire. Elle contraindrait tous les événements concurrents à porter la même valeur. Or un événement peut être concurrent avec deux événements qui sont, eux, ordonnés dans un autre processus. Leur donner le même temps violerait alors l’ordre interne.

L’horodatage scalaire certifie donc la conservation des flèches connues. Il ne certifie pas que toute paire croissante contient une flèche.

L’ordre total est une règle de décision

Une application doit parfois choisir alors que l’ordre partiel laisse plusieurs réponses valides. Lamport propose de trier selon l’horloge logique puis d’utiliser un ordre fixe des processus pour départager les égalités. On obtient un ordre total cohérent avec happened-before.

Cet ordre n’est pourtant pas unique. Une autre horloge respectant la Clock Condition ou un autre départage produit une autre linéarisation. Seul l’ordre partiel provient nécessairement du système d’événements.

Une file, une réplication ou une interface d’audit peut donc retenir un ordre déterministe. Elle doit l’étiqueter comme politique. Si le départage est présenté comme une découverte du passé, un mécanisme de contrôle devient une fausse preuve historique.

Le coup de téléphone absent

L’exemple du « comportement anormal » reste saisissant. Une personne émet A sur un ordinateur, téléphone à un ami dans une autre ville, puis l’ami émet B. Le téléphone étant extérieur au système, B peut recevoir un horodatage inférieur et être classé avant A.

Aucun algorithme limité aux événements internes ne peut reconstruire une arête qu’il n’a jamais observée. Lamport propose d’introduire explicitement l’information d’ordre manquante ou de recourir à des horloges physiques suffisamment synchronisées, avec des hypothèses plus fortes.

Aujourd’hui, l’arête manquante peut être un appel de support, une approbation humaine, un webhook ou une file gérée ailleurs. « Aucun chemin trouvé » veut seulement dire « aucun chemin dans cette capture ». Ce n’est pas une preuve d’absence d’influence dans le monde.

Temps scalaire, vectoriel et physique

L’horloge scalaire de Lamport suffit pour préserver l’implication de la Clock Condition et construire un ordre total cohérent. Dix ans plus tard, Colin Fidge et Friedemann Mattern élaborent des structures de temps vectoriel qui conservent davantage l’ordre partiel. Mattern souligne qu’une projection vers des entiers linéaires perd de l’information : des événements possiblement concurrents reçoivent des nombres différents comme s’ils étaient nécessairement ordonnés.

Deux vecteurs peuvent rester incomparables si aucun événement n’appartient au passé causal de l’autre. C’est précieux pour le débogage, les instantanés et les conflits. Mais le résultat dépend toujours des événements et messages enregistrés ; il ne retrouve pas un appel absent et n’explique pas la motivation humaine.

Le temps physique répond à une autre question. Le même article de Lamport traite ensuite de dérive, de vitesse d’horloge, de délai minimal des messages et de bornes de synchronisation. Ces hypothèses rapprochent les étiquettes du temps réel ; elles ne transforment pas un compteur logique en montre et exigent leur propre marge d’incertitude.

L’attribution historique doit rester aussi précise. Lamport formalise happened-before et les horloges logiques scalaires, tout en créditant Paul Johnson et Bob Thomas pour l’idée antérieure d’horodater les messages. Les horloges vectorielles relèvent des travaux ultérieurs de Fidge et Mattern.

Un reçu d’ordre honnête

Une analyse solide indique la définition et la version de l’événement, le processus, la séquence locale, l’identifiant du message, la correspondance envoi-réception, l’algorithme d’horloge et la frontière de la télémétrie. Une affirmation de temps réel doit encore préciser la source physique et son erreur ; une affirmation de cause doit montrer le mécanisme qui a modifié l’issue.

La conclusion peut alors être exacte : happened-before dans le modèle capturé ; concurrence dans ce modèle ; position imposée par un départage ; antériorité physique dans une incertitude donnée ; ou cause sémantique non démontrée.

La leçon de Lamport n’est pas de tout trier et d’appeler le résultat vérité. Elle consiste à séparer l’ordre connu, l’ordre choisi et l’ordre encore impossible à prouver.

Sources