UniTO/anno2/YearI/MCAD/lesson3-04102017.md

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)