# Cour 3 -- Théorie de la concurrence

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

[Somaire](IAsAMpizSpawifCj1gZ__g#)\
[precedent](/_24sdF4rT7uqUo-gfwI6QA)

> [time= 30 sept 2020]

[TOC]

## Algorithme de la boulangerie pour n processus (lamport, 1974)

Valable pour $n \geq 2$ processus.

L'agorithme est basé sur des variables propres:\
**MRSW**(Multiple reader / single writer)

:::success
Des **variables propres** sont des variables pour **un processus** utilise ses variables (lecture/ecrit) mais les autres processus ne peuvent que les lires.
:::

Cette algo est le meme algo utiliser dans les administration:
1. On prend un numéro superieur a celui des autres processus
2. le processus prioritaire est celui qui a le plus petit numéro

### Exlusion mutuelle
En logique temporel:
$$
\bigwedge\limits_{1 \leq i < j \leq n} \: G \neg (p_8i \land p_8j)
$$


### Absence d'interblocage
Si plusieurs processus se bloquent, ils resteront en p7 pour toujours.
Mais celui qui minimise l’ordre **<<** avec sa paire (Nb[i],i) passera.

Il y a donc absence d'interbloquage.

### Absence de famine
:::success
L’algo. de la Boulangerie garantit **l'absence de famine** sous hypothèse:
- d'équité entre processus
- en supposant que toute section critique termine (et conduit à l'exécution du post-protocole).
:::
logique temporelle:
$$
\bigwedge\limits_{0 < i < n } \: G (p_2i \Rightarrow F p_8i)
$$


### Attente borné
Le processus peut se faire doublé **n - 1**

### Remarque
La valeur des ticket n'est pas borné.

## Vérification automatique des algorithmes d'exclusion mutuelle

Mais cette idée n'est pas réalisable.

**On a un probleme ici indécidable.

On a un probleme ici indécidable.
On va donc réduire le probleme et faire du modele checking.

### Modele checking

mutex = mutuelle exclusion

#### outils
- [SPIN](http://spinroot.com/spin/)
- [NuSMV](http://nusmv.fbk.eu)
- [PRISM](http://www.prismmodelchecker.org)
- ...

### SPIN
SPIN est un outils pour l'annalyse de système **concurent** et **distribué**.\
Il est assez ancien (date de 1991)\
Il est basé sur le language de modélisation **PROMELA**.\
Il plusieurs techniques pour vérifier des propriétés décrites sous la forme:
- d’invariant
- propriétés LTL.

Et permet de simuler un modèle.

Conseil : Utiliser *J spin*.

#### PROMELA
extention standard: ".pml"

Des processus qui communiquent par des:
- variables globales
- canaux de communication

Des variables de type:
- bool
- byte
- short
- int (+ messages)

Les séparateur d'instruction sont:
- ;
- ->

Et des built-in:
- printf
- skip
- goto

les symbole de la LTL:
- $G$ : \[\]
- $F$ : <>
- $\Rightarrow$ :->

##### if

#### do

### garde
Si une contition "(x == 10)" est considéré comme non exécutable si elle est fause.
Dans un programme un **condition non exécutable bloque le processus**

### atomicité

Chaque instruction simple est atomique.\
Les **instructions composées ne sont pas atomiques** (par ex. if) ne sont pas atomiques.\
On peut rendre atomique un bloc d’instructions avec **atomic {...}**

### Peterson en SPIN
En promela le processus P1 de l'algo de Peterson donne:

Pour une simulation on aurra:

## PRISM
PRISM est un outil pour l’analyse de systèmes probabilistes. \
Et permet de simuler un modèle.
Qui vérifie des formules de LTL (et d’autres logiques).


- **\'** signifie la réafectation a une variable

### algorithme de Dekker


## Algo basé sur l'envoie de message

Hypothése:
- La SC termine toujours
- La SNC peut ne pas terminer
- les 2 processus restent toujours actifs
- les proc sont sur des machines différentes
- envoie de messages (un envoie est suivis **plus tard** d'une reception)
- tout message est reçu ("un jour"). Canaux fiables.
- si *Pi* envoie à *Pj* un message *M1* puis un message *M2*, *Pj* les **recevra dans l’ordre**.

### envoi / réception de messages
Un message a une forme fixé.\
Par exemple: *(type, val, numéro_expéditeur)*
- type
- request
- release
- ack
- val
- int
- numéro_expéditeur
- {1 ... n}

Envoie:
Send(msg) -> j\
Envoie d'un message à P~j~

La gestion des réceptions est confinée à un module séparé(s'exécutant en parallèle au module principal)


Hypothèse supplémentaire:
- la partie réception des mesg est toujours opérationnelle *(pas de blocage: nécessaire pour garantir la réception de tout message !)*
- ce parallélisme local peut être affaibli par des blocs atomiques locaux (entre { }).

## Algorithme de Lamport 1978
Chaque processus utilise une variable entière comme horloge locale (elle augmente de 1 avec les évènements: envoi et réception de mesg).

#### Préprotocole
1. P~i~ envoie un message « request » avec sa date locale à chaque processus, et conserve une copie de ce message. (le meme message envoyer a tout le monde, même date)
2. Puis attend d’être le plus prioritaire parmi les candidats à la SC.

Plus prioritaire = dont la date d’envoi de son mesg "request"

#### Postprotocole
P~i~ envoie un message "release" avec sa date locale à chaque processus, et converse une copie de ce message.

### algo

[suivant](/WyOYasmPQPKvNqlL6rrtHw)