# Cour 2 -- Théorie de la concurrence

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

[Somaire](IAsAMpizSpawifCj1gZ__g#)\
[precedent](/hkQL_-GXTG6nXzaiRtdNtg)

> [time= 23 sept 2020]

[TOC]

{%hackmd B0rpdjqcRfel-RZiyDj0PA %}

### attente borné
On sais qu'il n'y a pas famine. Mais on ne sais pas le nombre de fois que l'algorithme va attendre pour etre obligé de prendre la main.

## Logique temporelle
### LTL (linear-time temporal logic)
:::success
**Logique de temps linéaire.**\
le comportement d'un programme est vu comme l'ensemble
:::

## syntaxe
:::success
$$
\phi, \psi ::= P \:|\:
\neg \phi \:|\:
\textbf{X} \phi \:|\:
\phi \: \textbf{U} \: \psi
$$
:::
- $X \phi$: **next** (demain $\phi$)
- $\phi \: \textbf{U} \: \psi$: **until** (un jour $\psi$ et avant $\phi$: "toujours $\phi$ jusqu'à $\psi$")

:::success
abréviation
- $\textbf{F} \: \varphi= \top \: \textbf{U} \: \phi$: "un jour dans le futur"
- $\textbf{G} \: \varphi= \neg \: \textbf{F} \: \neg \varphi$: globaly ("toujours dans le futur)"
:::

## sémantique
on interprète les formules de LTL sur une ++exécution étiquetée++
$$
\rho = s_0 \rightarrow s_1 \rightarrow s_2 \rightarrow s_3 \cdots \rightarrow s_i \rightarrow s_{i+1} \cdots
$$

- $s_0$ est le présent
- $s_1 \rightarrow s_2 \rightarrow s_3 \cdots$ est le futur

un étiquetage de chaque état $s_j$ par les propositions atomues vraies en $s_j$ est $\ell(s_j)$

$\rho^i \text{est le i-ème suffix:} s_i \rightarrow s_{i+1} \cdots$

On interprète les formules de LTL sur une ++éxécution++ d'un diagramme d'état.\
Chaque ***s~j~** est de la forme: **(p, q, v1, v2)**.
Avec:
- *p* et *q* les point d'instruction de chanque processus
- *v1* et *v2* les valeur de chaque variable

$S_0 \in Q, \rho = s_0 \: s_1 \: s_2 \: s_3 \: s_4 \: \cdots$ une éxécution et $\ell$ un étiquetage de chaque état par des proposition atomique.

- $\rho \vDash P \text{ ssi } P \in \ell(s_0)$
- $\rho \vDash \varphi \lor \psi \text{ ssi } (\rho \vDash \varphi \text{ ou } \psi \vDash \rho )$
- $\rho \vDash \lnot \varphi \text{ ssi } (\rho \nvDash \varphi)$
- $\rho \vDash \: \textbf{X} \: \varphi \text{ ssi } (\rho^1 \vDash \varphi) \qquad \text{ avec } \rho^1 = s_1 \: s_2 \: s_3 \: \cdots$
- $\rho \vDash \varphi \: \textbf{U} \: \psi \text{ ssi } \exists \, i \geq 0 \,(\rho^i \vDash \psi \text{ et } (\forall \, 0 \leq j \lt i : \rho^j \vDash \varphi))$

$\vDash$ = statisfait
### Exemple

$$
\textbf{G}(\text{probleme}) \Rightarrow \textbf{F} \text{ alarme}\\
\textbf{G}(\text{request}) \Rightarrow \textbf{F} \text{ service}\\
\textbf{G}(\neg \text{ bug})
$$

- $\textbf{G F} \text{ acceuil}$ : infiniment souvent
- $\textbf{F G} \text{ ok}$: un jour toujours ok
- $\textbf{G F} \text{ request} \Rightarrow \textbf{G F} \text{ service}$
- $\textbf{G F}(a \land b) \Rightarrow \textbf{G F}\text{ a } \land \textbf{G F} \text{ b}$
- $\textbf{G F}\text{ a } \land \textbf{G F} \text{ b} \nRightarrow \textbf{G F}(a \land b)$

### Exclusion mutuelle
*Jamais* les 2 process
us ne se trouve en meme temps en SC.
$$
\neg \textbf{F} (SC_1 \land SC_2)\\
\textbf{G} (\neg SC_1 \lor \neg SC_2)
$$

### Absence de famine
Si un processus demande l'acces à la SC, il y arrivera *un jour*.
$$
\textbf{G} ( D_1 \Rightarrow \textbf{F} SC_1) \land
\textbf{G} ( D_1 \Rightarrow \textbf{F} SC_2)
$$

### Propriété
- **propriété de sureté**\
"une mauvaise chose n'arrive jamais"\
ex: l'exlusion mutuelle
- **propriété de vivacité**\
"une bonne chose fini par arriver"\
ex: absence de famine
- **propriété d'équité**\
exprime une forme d'équité sur une exécution\
ex: une éxécution où les 2 processus "avancent" infiniment souvent.

## Algorithme de Peterson (1981)

- Exlusion mutuelle\
$G(\neg p5 \lor \neg q5)$
- Absence de famine\
$G(p2 \Rightarrow \textbf{F }p5)$

### Exlusion mutuelle
Supposons que P~2~ rejoin P~1~ en SC\
on sais que on a D1 = D2 = True\
P~2~ à franchie q4 comme D2 == True alors on a turn == 2\
donc on est passé par p3\
Comment P1 a passé p4:
1. D2 == False?\
Donc depuis, P~2~ a fait D2 := True et turn := 1\
Et P2 ne peut franchir le await...
3. turn == 1 ?\
Mais alors si turn vaut toujours 1 tant que P~1~ est en SC alors P2 ne peut pas le rejoindre

### Absense d'interblocage
interblocage si:\
$$
\neg (turn == 1 \lor \neg D2) \land \neg(turn == 2 \lor \neg D1)\\
(turn \neq 1 \land D2) \land (turn \neq 2 \land D1)\\
(turn = 2 \land D2 \land turn == 1 \land D1) \qquad \textbf{faux}
$$

### Absence de famine
:::success
L’algo. de Peterson garantit l'absence de famine sous hypothèse:
- d'équité entre processus
- en supposant que:
- toute section critique termine
- conduit à l'exécution du post-protocole.
:::
Supposons P~1~ en famine.\
Alors on a toujours $D1=\top$\
Et $D2 =\top$ et $turn == 1$ ++inifiniment souvent++. (pour ne pas pouvoir passer le await)\
$D2 =\top \Rightarrow$ P~1~ est en *q3, q4, q5, q6*
- de *q3* il irait à *q4* et on a $turn == 1$ **(donc P1 peut passer)** :x:
- de *q4* il irait *q5* si
- $turn == 2$ *(impossible car on a exécuté *q3*)*
- $D1=\bot$ *(impossible $D1=\top$) toujours*
- de *q5* il irait en q6
- de *q6* il irait donc $D2=\bot$,
puis irais en *q1*, puis *q2* et *q3*

### Attente borné
oui il y a attente borné.

### privilege
On a pas besoin d'initialiser turn donc l'algo ne **donne aucun privilège**.

## Extention de l'algorithme de Peterson
## Filter Lock

### Peterson revu

### Algorithme

Définition:
- un processus a passé le niveau k
lorsqu’il a dépassé le « await » (p5) pour l’itération j=k. \
(et si k=0: lorsqu’il a commencé son préprotocole).
- $nb_{\geq k}$ est le nombre de processus ayant passé le niveau k.

#### Propriété
$$
\forall \: 0 \leq j \leq n - 1, nb_{\geq j} \leq n - j
$$

- $j = 0$: oui $nb_{\geq 0} \leq n$
- $j \gt 0$: par hypothèse d’induction, on sait qu’il y a au plus $n - j + 1$ processus qui ont passé le niv. $j - 1$.

Supposons que tous (donc $n - j + 1$) processus aient passé le niveau j.\
Soit *P* le dernier à avoir fait $victim[j]:=id_P$\
Tout autre *P'* (au delà du niveau j) a donc fait **avant**:
- $level[id_{P'}]:= j$

et ensuite:
- $victim[j] := id_{P'}$


#### Corrolaire
$$
nb_{\geq n - 1} \leq 1.
$$

### Exclusion mutuelle
On a donc bien l'exclusion mutuelle. (grace au corraolaire)

### Absence de famine
L’algo. Filter Lock garantit l'absence de famine sous hypothèse d'équité entre processus et en supp. que toute SC termine (et conduit à l’exéc. du post-protocole).

#### proriété
Tout proc. ayant atteint le niveau $j \geq 1$, arrivera au niveau $j + 1$ (ou en SC si $j = n - 1$).

$j = n - 1$ oui, il y a bien absence de famine

$j < n - 1$: Soit *P* ayant atteint le niveau *j* et supposons qu’il soit bloqué dans le **await** à ce niveau pour toujours...
1. Par h.i., les proc. des niveaux supérieurs accéderont à la CS...
2. Aucun proc du niveau j-1 ne pourra accéder au niveau j (sinon victim serait mis à jour et P serait débloqué !). Donc **victim est figée**.
3. Si P n’est pas le seul au niv. j, c’est le seul à être bloqué. Et après le succès des autres, il finira par passer (∀ ...) !

[suivant](hH2Gad18QOOHxIbJMKa81A)