3.5 KiB
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:
- Garanzia della mutua esclusione
- 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.
- Assenza di Deadlock : se la sezione critica e' libera, e vari processi vogliono entrare, in un tempo finito uno deve entrare
- 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:
- 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
- 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)
- No starvation
Non dimostrabile, non conoscendo l'implementazione del semaforo (FIFO queue e' fair, ma non e' l'unica implementazione)