# 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)