Temps logique dans SR
Ordre Causal
Relation de précédence directe
Relation de précédence causal
Un événement e précède directement un événement e'. ⭐ e-->e'
✅ Les événements e et e' ont lieu dans le même processus, e se produit exactement avant e' sur ce processus.
✅L'événement e correspond à l'envoi d'un message par un processus, l'événement e' correspond à la réception du même message par un autre processus.
{
La relation est transitive.
Si e-->e' , e'-->e'' ==> e-->e"
Définie comme la fermeture réflexive et transitive
:✅[e = e’ (réflexivité)
✅ ∃ e1, e2, …, em tels que e1 = e et em = e’ et
∀i, ei • > ei+1 (transitivité)
{
e • > e’
Définit un ordre partiel des
événements.
Si deux événements x et y se produisent dans des processus différents, il se peut qu’aucune des deux relations x • > y et x • > y ne soit vraie.
Deux événements x et y non comparables par la relation de
précédence causale, sont dits concurrents : on note x||y
A un événement e on peut associer trois ensembles d’événements
Passé(e) : ensemble des événements antérieurs à e dans l’ordre
causal
Futur(e) : ensemble des événements postérieurs à e dans l’ordre
causal
Concurrent(e) : ensemble des événements concurrents avec e
dans l’ordre causal.
Délivrance Causale
Définition
del(m), est l’opération consistant à le rendre accessible aux applications utilisatrices
Pourra être retardée lors de sa réception pour garantir un ordre de délivrance souhaité
Ordre de délivrance FIFO
Ordre de délivrance causale
sndi(m 1,j) • > sndi(m 2,j) ⇒ del j(m 1) • > del j(m 2 )
sndi(m 1,k) • > sndj(m 2,k) ⇒ del k(m 1) • > del k(m 2 )
Horloges et estampilles scalaires
Définition
e • > e’ ⇒ HL e ⊆ HLe’
Principe
Chaque site gère un compteur dont la valeur est un entier.
Sur chaque site ce compteur est initialisé à 0 au lancement du système.
La valeur de l’horloge logique d’un site est incrémentée chaque fois qu’un événement local s’y produit. Un tel événement est : ⇒ soit une opération purement locale, ⇒ soit l’envoi d’un message. Dans ce cas la valeur courante (après incrémentation) de l’horloge de l’émetteur est embarquée avec le message (« piggybacking ») et sert à l’estampiller.
La réception d’un message permet de synchroniser l’horloge du récepteur avec celle de l’émetteur du message (qui est transportée par le message).
Le principe consiste à attribuer à l’horloge du récepteur une valeur supérieure à la fois à la valeur courante de l’horloge du site et à celle de l’estampille du message reçu.
Algorithme de Lamport
si un événement local se produit sur le site i, HLi est incrémentée : HLi ++
si un événement correspondant à l’envoi d’un message se produit sur le site i, HLi est incrémentée, et le message m est envoyé avec la nouvelle valeur de HLi comme estampille : EL m = HL
si un événement correspondant à la réception d’un message m d’estampille EL m se produit sur le site i : HLi = max (HLi , EL m) + 1
Propriétés des estampilles scalaires
Ordre des événements n’est pas un ordre strict
plusieurs événements peuvent porter la même valeur.
Pour rendre cet ordre strict on adjoint à la valeur de l’horloge logique
d’un site l’identification du site
L’estampille logique d’un événement HL(e) d’un événement e du site i
est un couple (HLi , i).
Si HLi < HLj
HLi = HLj et i < j
(HLi , i) ⊂ (HLj , j)
Ordre ainsi défini est total :
Induit une chaîne de tous les événements.
Horloges et estampilles vectorielles
Définition
HVi désigne l’horloge vectorielle du site i
EV m désigne l’estampille vectorielle attribuée au message m lors de son envoi
✅ si un événement local se produit sur le site i, HVi [i] est
incrémentée : HVi [i] ++
✅ si un événement correspondant à l’envoi d’un message se produit sur le site i, HVi [i] est incrémentée, et le message m est envoyé avec la nouvelle valeur de HVi comme estampille : EV m = HV
✅si un message m d’estampille EV m est reçu sur le site i : – HVi [i] est incrémentée, – ∀ j ≠ i , HVi [j] = max (HVi [j] , EV m [j])
Horloges et estampilles matricielles
Propriétés
Propriété fondamentale
Relation d’ordre sur les estampilles vectorielles
• EV e est l’estampille vectorielle de e :
⇒ ∀ i , EV e [i] = Card ( {e’ / e’ ∈ Si et e’ • > e } )
⇒ i.e. la valeur de la i-ème composante de EV e correspond au nombre d’événements du site Si qui appartiennent au passé de e.
EV e est l’estampille vectorielle de e
⇒ EV e ⊆ Eve’ ⇔ ∀ i, EV e [i] ≤ Eve’ [i]
Cette relation d’ordre reflète exactement la relation de précédence causale entre événements :
✅ Si EV e est l’estampille vectorielle de e : – e • > e’ ⇔ EV e ⊆ Eve’ – e || e’ ⇔ EV e || Eve’
Inconvénient
Ne permettent pas de corriger la défaillance vis-àvis de la délivrance causale des messages
Définition
Sur le site Si, la matrice HMi va
✅Mémoriser le nombre de messages que le site Si a envoyé aux différents autres sites : cette information est fournie par la i-ème ligne de la matrice. L'élément diagonal compte les événements sur le site Si.
✅Mémoriser, pour chacun des autres sites j, le nombre de messages émis par ce site dont le site i a connaissance.
✅Ainsi, sur le site i, la valeur EMi[j,k] donne le nombre de messages en provenance du site Sj délivrables sur le site Sk dont le site Si a connaissance.
Principe
Dans un système de n sites, les horloges d'un site i et les estampilles des événements (et des messages) sont des matrices carrées d'ordre n.
HMi désigne l'horloge matricielle du site Si.
EMm désigne l'estampille matricielle du message m.
Modification et synchronisation des horloges
Lorsqu'un événement local se produit sur le site Si : HMi[i,i] est incrémenté.
Lorsqu'un message est expédié du site Si vers le site Sj : HMi[i,i] et HMi[i,j] sont incrémentés.
Lorsqu'un message m en provenance du site Sj est reçu sur le site Si :
Il faut s'assurer que tous les messages envoyés antérieurement au site Si y sont effectivement arrivés, correspondant aux conditions suivantes : HMm[j,i] = HMi[j,i] + 1 (ordre FIFO sur le canal (j,i)). Pour tout k ≠ i et j, HMm[k,i] ≤ HMi[k,i] (tous les messages en provenance des sites différents de Sj ont été reçus).
Si toutes ces conditions sont vérifiées, le message est délivrable, et l'horloge du site Si est mise à jour.
Si les conditions ne sont pas toutes vérifiées, la délivrance du message est différée jusqu'à ce qu'elles le deviennent. La délivrance d'un message pourra ainsi provoquer celle des messages arrivés prématurément.
click to edit