124 lines
3.5 KiB
Markdown
124 lines
3.5 KiB
Markdown
# Primitive di Sincronizzazione
|
|
|
|
## Semafori
|
|
|
|
Dijkstra: I semafori un tipo di dato astratto (puo' essere considerato un oggetto), che assume solo valori interi >= 0, su cui si eseguono solo **DUE** operazioni atomiche (P = wait, V = signal).
|
|
|
|
### Semantica di P e V:
|
|
|
|
--- P
|
|
void P (semaphore S) {
|
|
<< when (val(S) > 0) val(S)--; >>
|
|
}
|
|
|
|
--- V
|
|
void V (semaphore S) {
|
|
<< val(S)++; >>
|
|
}
|
|
|
|
<<...>> vuol dire "eseguito in sezione critica"
|
|
|
|
Nota: ci sono implementazioni semaforiche che permettono al semaforo di assumere valori negativi, in questo modo il numer o di processi in attesa e' dato dal valore <0
|
|
|
|
### Atomicita' di P e V
|
|
|
|
L'atomicita' in ambiente monoprocessore si ottiene disabilitando l'interrupt ed effettuando la chiamata. Questo pero' non basta in architetture multiprocessore a memoria condivisa: la granularita' dell'atomicita' e' infatti diversa.
|
|
|
|
Per questo motivo, in architetture multiprocessore si usano procedure di *test and set* per creare operazioni di *lock e unlock*.
|
|
|
|
### Invariante semaforico
|
|
|
|
Un invariante semaforico e' un'uguaglianza sempre vera associata a un semaforo, che rimane per tutta la durata di vita del semaforo.
|
|
|
|
### Terminologia
|
|
|
|
* val(sem,t) : valore del semaforo all'istante t
|
|
* I(sem) : valore iniziale del semaforo
|
|
* nP(sem, t) : volte in cui e' stata eseguita **con successo** l'operazione P su sem all'istante t
|
|
* nV(sem, t) : volte in cui e' stata eseguita **con successo** l'operazione V su sem all'istante t
|
|
|
|
Vale quindi:
|
|
```
|
|
val (sem, t) = I + nV(sem,t) - nP(sem,t) <- V incrementa, P decrementa
|
|
|
|
nP(sem, t) <= I + nV (sem, t) <- Invariante semaforico
|
|
```
|
|
|
|
### Problema della mutua esclusione - Soluzioni
|
|
|
|
Uno e un solo processo puo' avere accesso alla sezione critica.
|
|
|
|
Una buona soluzione deve soddisfare le proprieta' classiche:
|
|
1. Garanzia della mutua esclusione
|
|
2. Non correlazione : un processo che non deve accedere alla SC (sezione critica) e che ne e' al di fuori **non deve influenzare** processi che tentano di accedere alla sezione critica.
|
|
3. Assenza di Deadlock : se la sezione critica e' libera, e vari processi vogliono entrare, in un tempo finito uno deve entrare
|
|
4. Assenza di Starvation : se un processo vuole entrare nella sezione critica, l'attesa dev'essere **finita**.
|
|
|
|
#### Soluzione Semaforica - MUTEX
|
|
|
|
Se OP e' una operazione su una variabile condivisa:
|
|
```
|
|
semaphore mutex = 1
|
|
P1
|
|
.
|
|
.
|
|
P(mutex)
|
|
OP
|
|
V(mutex)
|
|
```
|
|
Ogni operazione critica deve essere preceduta da un P(mutex) e un V(mutex).
|
|
|
|
##### Dimostrazione della soluzione mutex
|
|
|
|
Si vuole mostrare che la soluzione mutex e' ottimale al problema della mutua esclusione.
|
|
Dimostreremo ogni proprieta' analizzata:
|
|
|
|
1. Garanzia di ME
|
|
|
|
ncs(t) : numero di processi che al tempo t operano in sezione critica
|
|
|
|
* Essendo che ogni processo esegue obbligatoriamente una P e una V (**Invariante topologico**):
|
|
|
|
```
|
|
ncs(t) = nP(mutex,t) - nV (mutex, t)
|
|
|
|
```
|
|
* Inoltre, su mutex vale l'invariante semaforico
|
|
|
|
```
|
|
nP(mutex, t) <= 1+nV(mutex,t) --> ncs(t) <= 1
|
|
```
|
|
|
|
* Utilizzando l'invariante topologico:
|
|
```
|
|
nV(mutex, t) <= nP(mutex, t) --> ncs(t) >= 0
|
|
```
|
|
* quindi:
|
|
```
|
|
0 <= ncs <= 1
|
|
```
|
|
* dimostrato
|
|
|
|
|
|
2. No deadlock
|
|
|
|
* Dimostrazione per assurdo: esiste un istante t in cui c'e' deadlock
|
|
```
|
|
val(mutex, t) = 0 && ncs(t) = 0
|
|
```
|
|
* dato che il val di mutex e' 0
|
|
|
|
```
|
|
1+nV(mutex, t) - nP(mutex,t) = 0
|
|
```
|
|
* ma questo entra in collisione con la definizione di ncs:
|
|
|
|
```
|
|
nP(mutex, t) - nV(mutex,t) = ncs(t) = 0
|
|
```
|
|
* per assurdo, dimostrato (1 != 0)
|
|
|
|
3. No starvation
|
|
|
|
Non dimostrabile, non conoscendo l'implementazione del semaforo (FIFO queue e' fair, ma non e' l'unica implementazione)
|
|
|