# TD 2 -- Théorie et pratique de la concurrence

###### tags `TD` `M1 S1` `Concurrence`
[Sommaire](/bAJa0viuQp68XN74HxpVJA)
> [time= 29 sept 2020]

[TOC]

## Exercice 1
### Enoncé

### Réponse
#### 1)
##### exclusion mutuelle
$$
\textbf{G}(\lnot p_5 \lor \lnot q_5) \land
\textbf{G}(\lnot q_5 \lor \lnot r_5) \land
\textbf{G}(\lnot r_5 \lor \lnot p_5)\\
ou \\
\textbf{G}\lnot( p_5 \land q_5) \land
\textbf{G}\lnot( q_5 \land r_5) \land
\textbf{G}\lnot( r_5 \land p_5)\\
ou \\
\lnot \textbf{F}(p_5 \land q_5) \land
\lnot \textbf{F}(q_5 \land r_5) \land
\lnot \textbf{F}(r_5 \land p_5) \land
$$

#### absence de famine
$$
\textbf{G}(p_2 \Rightarrow \textbf{F} p_5) \land
\textbf{G}(q_2 \Rightarrow \textbf{F} q_5) \land
\textbf{G}(r_2 \Rightarrow \textbf{F} r_5) \land
$$

#### 2)
Cette algorithme n'est pas coorect car on peut avoir:
$$
\begin{array}{|ccc||ccc|}
\hline
\text{P1} & \text{P2} & \text{P3} &
\text{D1} & \text{D2} & \text{D3} & \text{turn} \\
\hline
p_1 & q_1 & r_1 & \bot & \bot & \bot & 1\\
p_1 & q_1 & r_2 & \bot & \bot & \bot & 1\\
p_1 & q_1 & r_3 & \bot & \bot & \top & 1\\
p_1 & q_1 & r_4 & \bot & \bot & \top & 1\\
p_1 & q_1 & r_5 & \bot & \bot & \top & 1\\
p_1 & q_2 & r_5 & \bot & \bot & \top & 1\\
p_1 & q_3 & r_5 & \bot & \top & \top & 1\\
p_1 & q_4 & r_5 & \bot & \top & \top & 3\\
p_2 & q_4 & r_5 & \bot & \top & \top & 3\\
p_3 & q_4 & r_5 & \top & \top & \top & 3\\
p_4 & q_4 & r_5 & \top & \top & \top & 2\\
p_4 & q_5 & r_5 & \top & \top & \top & 2\\
\hline
\end{array}
$$
On a 2 processus en section critique $q_5$ et $r_5$. On n'as donc pas exclusion mutuelle.

## Exercice 2
### Enoncé

### Réponse
#### 1)

Cette algorithme n'est pas coorect car on peut avoir:
$$
\begin{array}{|ccc||ccc|}
\hline
\text{P1} & \text{P2} & \text{S3} &
\text{req} & \text{autorisation} & \text{fin}\\
\hline
p_{{}_1 1} & p_{{}_1 1} & s_1 & 0 & 0 & \top \\
p_{{}_2 1} & p_{{}_1 1} & s_1 & 0 & 0 & \top \\
p_{{}_3 1} & p_{{}_1 1} & s_1 & 0 & 0 & \top \\
p_{{}_2 1} & p_{{}_1 1} & s_1 & 1 & 0 & \top \\
p_{{}_2 1} & p_{{}_1 1} & s_2 & 1 & 0 & \top \\
p_{{}_2 1} & p_{{}_1 1} & s_3 & 1 & 0 & \bot \\
p_{{}_4 1} & p_{{}_1 1} & s_4 & 1 & 1 & \bot \\
p_{{}_5 1} & p_{{}_1 1} & s_4 & 1 & 1 & \bot \\
p_{{}_6 1} & p_{{}_1 1} & s_4 & 1 & 1 & \top \\
p_{{}_1 1} & p_{{}_1 1} & s_4 & 0 & 1 & \top \\
p_{{}_2 1} & p_{{}_1 1} & s_4 & 0 & 1 & \top \\
p_{{}_4 1} & p_{{}_1 1} & s_4 & 0 & 1 & \top \\
p_{{}_4 1} & p_{{}_2 1} & s_4 & 0 & 1 & \top \\
p_{{}_4 1} & p_{{}_3 1} & s_4 & 0 & 1 & \top \\
p_{{}_4 1} & p_{{}_2 1} & s_4 & 2 & 1 & \top \\
p_{{}_4 1} & p_{{}_2 1} & s_5 & 2 & 1 & \top \\
p_{{}_4 1} & p_{{}_2 1} & s_1 & 2 & 0 & \top \\
p_{{}_4 1} & p_{{}_2 1} & s_2 & 2 & 0 & \top \\
p_{{}_4 1} & p_{{}_2 1} & s_3 & 2 & 0 & \bot \\
p_{{}_4 1} & p_{{}_2 1} & s_4 & 2 & 2 & \bot \\
p_{{}_4 1} & p_{{}_4 1} & s_4 & 2 & 2 & \bot \\
\hline
\end{array}
$$

on a 2 processus $p_i$ en section critique. Il y a donc pas exlusion mutuelle.

#### 2)a)
##### exclusion mutuelle
$$
\bigwedge\limits_{1 \leq i < j \leq n} \: G \neg (p_{{}_i 4} \land p_{{}_j 4})
$$

##### absence de famine
$$
\bigwedge\limits_{i = 0}^{n} \: G (p_{{}_i 2} \Rightarrow F p_{{}_i 4})
$$

#### 2)b)

#### 2)c)
Non cette algorithme ne guaranti pas l'absence de famine. \\
ex: P2 peut prendre toujours la main.

## Exercice 3
### Enoncé

### Réponse
#### 1) exclusion mutuelle LTL
$$
\bigwedge\limits_{1 \leq i < j \leq n} \: G \neg (p_{{}_i 9} \land p_{{}_j 9})
$$

#### 2) preuve

[original a la page 19](https://www.irif.fr/~francoisl/DIVERS/poly-tpc-1112.pdf)

#### 3) absence de famine LTL
$$
\bigwedge\limits_{i = 0}^{n} \: G (p_{{}_i 2} \land p_{{}_i 9})
$$
#### 4) preuve absence de famine
[original a la page 20](https://www.irif.fr/~francoisl/DIVERS/poly-tpc-1112.pdf)
#### 5) attente bornée
Non il n'y a pas attente borné