# Cour 4 -- Théorie de la concurrence

###### tags `cour` `M1 S1` `Concurrence`

[Somaire](IAsAMpizSpawifCj1gZ__g#)\
[precedent](/hH2Gad18QOOHxIbJMKa81A)

> [time= 7 oct 2020]

[TOC]

## Algorithme de Lamport 1978 (suite)
Les horloge local sont croissante.

Dans son préprotocole, le processus Pi envoie le même message **(request,c,i)** à tous les autres processus et le stocke dans Fi[i].

1. envoie une reuquest
2. envoie un ack
3. envoie une realease

### Exemple

### Exclusion mutuelle
hypothèse:
L’algorithme de Lamport 1978 assure l’exclusion
(en supposant que les blocs indiqués sont bien éxécuté de maière atomique localement).

#### preuve
Supposons que $P_{i1}$ et $P_{i2}$ soient au même instant en SC.\
On a:
$$
F^{i1}[i_1] = (\text{request}, t_1, i_1) \text{ et }
F^{i2}[i_2] = (\text{request}, t_2, i_2)
$$

Supoosons que $(t_1, i_1) << (t_2, i_2)$



## Absence d'interblocage
L’algorithme de Lamport 1978 vérifie l’absence d’interblocage
(en supposant que les blocs indiqués sont bien éxécuté de maière atomique localement).

Supposons que des proc. se bloquent end et que les autres sont en SNC\
Soit Pi le proc. bloqué le plus prioritaire, c-à-d. minimisant sa date d’envoi de son request.
Pi bloque dans un await (pour un Pj). Pj n’est pas bloqué. Donc il est en
SNC et si Pi bloque c’est que l’ack venant de Pj tarde... mais il viendra!.


### absence de famine
L’algorithme de Lamport 1978 vérifie l’absence de famien
(en supposant que les blocs indiqués sont bien éxécuté de maire atomique localement et l’équité entre procéssus et la finitude des SC!.

#### preuve
Preuve: Supposons que des processus soient en situations de famine.
Soit P~i~ le proc.affamé le plus prioritaire, cad minisant sa date t~1~d'envoie de son request.\
P~i~ bloque dans un await(pour un P~j~).\
Mais p~i~ a recu (ou recevra) le *request* de P~i~ et lui a répondu (ou répondra) un **ack**...


### Attente bornée
**n - 1** processus peuvent doubler un autre proc

### Nombre de message envoyer pour accédé à la SC
**3(n - 1)**

## algorithme de Ricart-Agrawala (1981)
Cette algo est proche de celui de **lamport** il veux limiter le nombre de message
- Lorsque Pj reçoit une request de Pi, il ne répond (un mesg ok) que si il ne veut pas aller en SC ou si sa demande est moins prioritaire que celle de Pi.
- Si Pj n’envoie pas ok à Pi tout de suite, il le fera après avoir quitter la SC.
- La priorité pr est calculée par chaque processus en prenant le max des priorités reçues dans les request des autres. Plus pr est petit, plus le processus est prioritaire.

### algo

### Exclusion mutuelle
L'algorithme de Ricart-Agrawala assure l'exclusion mutuelle (en supposant que les blocks indiqués sont bien exécutés de manière atomique localement).

#### preuve
Suppposons t~0i1~ < t~0i2~:
- Cas 1: t~i2~ < t~0i2~
- pr~i2~ > pr~i1~ \
pas de Send(ok, i1)!
- Cas 2: t~i2~ < t~0i2~
- ( pr~i1~ << pr~i2~ )
- ( pr~i2~ << pr~i1~ )

### Absence de famine
L'algorithme de Ricart-Agrawala vérifie l'absence de famine (en supposant que les blocks indiqués sont bien exécutés de manière atomique localement et l’équité entre procéssus et la finitude des SC!).

#### preuve
Supposons que des processus soient en situation de famine.
Soit P~i~ le processus affamé le plus prioritaire (ie. pr~i~ min).\
Soit P~k~ un autre processus bloqué n'ayant pas envoyé ok à P~i~.\
A la reception de (req, pr~i~, i) on avait (pr~k~, k << pr~i~, i)

Depuis pr~k~, a donc changé et *ok* a été envyé à P~i~

### Nombre de message envoyer
2(n - 1)