Paradigmi Concorrenti - Appunti

I CINQUE FILOSOFI: MODELLO

Per realizzare il sistema concorrente possiamo utilizzare un semaforo, oppure un flag.

FORK = (get -> put -> FORK).

PHIL = (sitdown -> right.get -> left.get -> eat ->

left.put -> right.put -> arise -> PHIL).

||DINERS(N=5) = forall[i:0..N-1]

(ph[i]:PHIL || {ph[i].left, ph[(i-1+N)%N].right}::FORK).

Una possibile traccia di esecuzione:

ph.1.sitdown

ph.2.sitdown tutti i filosofi si siedono a tavola

ph.3.sitdown

ph.4.sitdown

ph.5.sitdown

ph.1.right.get i filosofi prendono tutti la forchetta alla loro destra, così però nessuno può

ph.2.right.get prendere la forchetta alla propria sinistra. Aspettano che si liberi, ma non

ph.3.right.get si possono liberare se nessuno dei filosofi sta usando 2 forchette

ph.4.right.get

ph.5.right.get

STALLO 20

DEADLOCK

Il più semplice sistema suscettibile di cadere in uno stato di deadlock:

Due processi, due risorse.

RISORSA = (prendi -> lascia -> RISORSA).

P = (a.prendi -> b.prendi -> usa -> a.lascia -> b.lascia -> P).

Q = (b.prendi -> a.prendi -> usa -> b.lascia -> a.lascia -> Q).

||S = (p:P || q:Q || {p,q} :: a:RISORSA || {p,q} :: b:RISORSA).

Esecuzione:

p.a.prendi -> q.b.prendi -> DEADLOCK

q.b.prendi -> p.a.prendi -> DEADLOCK

Che cosa succede se: ?

Q = (a.prendi -> b.prendi -> usa -> b.lascia -> a.lascia -> Q).

Non c’è più deadlock.

Deadlock = blocco critico, stallo. Dal punto di vista grafico viene rappresentato come uno stato senza archi uscenti.

Definizione: Il deadlock è dato da un insieme di processi, ognuno dei quali è in attesa di un certo evento che può

essere provocato solo da un altro processo appartenente a tale insieme.

Le condizioni sufficienti e necessarie che rendono possibile uno stato di deadlock sono:

 risorse con vincolo di mutua esclusione;

 acquisizione incrementale delle risorse (cioè i processi interessati devono accumulare un certo numero di

risorse, e in questo accumulo mantengono le risorse acquisite);

 divieto di rapina, di strappare una risorsa ad un altro processo (no preemption);

 circolo delle attese (introdurre un ordine specifico di acquisizione delle risorse, oppure escludere alcuni

processi dall’attività).

IMPORTANTE: ogni condizione è necessaria per generare uno stato di deadlock, tutte le condizioni sono sufficienti.

Grafo di allocazione delle risorse: se un processo ha acquisito una certa

risorsa e ne aspetta un'altra, che a sua volta è stata acquisita da un altro

processo, allora si parla di circolo delle attese.

DEADLOCK – Soluzioni

Obiettivo: progettare un sistema concorrente in modo che sia impossibile raggiungere uno stato di deadlock.

Idea: impedire che si verifichino contemporaneamente le 4 condizioni.

 Mutua esclusione: generalmente impossibile da evitare (vogliamo risorse condivise!)

 Acquisizione incrementale:

o imporre ai processi che acquisiscono insieme tutte le risorse di cui hanno bisogno (inefficiente)

o timeout e rilascio volontario (livelock) 21

 Divieto di rapina: rilevazione dinamica di deadlock e terminazione “violenta”

 Circolo delle attese: protocolli ad hoc (ad esempio: classificazione delle risorse e ordine prefissato delle

acquisizioni).

I cinque filosofi – Soluzioni immuni da deadlock

Strategia: impedire strutturalmente che si possa formare un circolo vizioso di attese.

1 – Asimmetria tra filosofi (presenza di filosofi mancini)

FORK = (get -> put -> FORK).

PHIL(I=0) = ( when (I%2 == 0) sitdown -> left.get -> right.get -> … -> PHIL |

when (I%2 == 1) sitdown -> right.get -> left.get -> … -> PHIL ).

2 – Un guardiano garantisce che al massimo N-1 filosofi siano seduti contemporaneamente a tavola.

const N = 5

FORK = (get -> put -> FORK).

PHIL = (sitdown -> right.get -> left.get -> eat ->

left.put -> right.put -> arise -> PHIL).

BUTLER = BUTLER[0],

BUTLER[0] = (sitdown -> BUTLER[1]),

BUTLER[nf:1..N-1] = (when (nf < N-1) sitdown -> BUTLER[nf+1] |

arise -> BUTLER[nf-1]).

3 – Timeout

FORK = (get ‐> put ‐> FORK).

PHIL = (sitdown -> SEDUTO),

SEDUTO = (right.get -> DESTRA),

DESTRA = (left.get -> eat -> RILASCIO | timeout -> right.put -> SEDUTO),

RILASCIO = (left.put -> right.put -> arise -> PHIL).

Deadlock – Rimedi :

 Prevenzione

- statica

- dinamica

 Rilevamento e ripristino 22

Lezione 10

Es.: Il caposquadra prepara delle schede con dei lavori da fare, e poi le deposita sul tavolo (che ha una capacità

massima). Gli operai prendono le schede per controllare il lavoro da fare; prima però guardano la lavagna

per vedere quali lavori sono stati già fatti.

-> capacità max della lavagna (lavori svolti)

const S = 5 -> capacità max del tavolo

const C = 3 -> numero operai

const N = 4

LAVAGNA = L[0],

L[n:0..S] = (when n < S op[1..N].fineop -> L[n+1] |

when n == S op[1..N].fineop -> L[S] |

leggi[n] -> L[n]).

CAPOSQUADRA = (leggi[n:0..S] ->

if n < S then (deposita -> CAPOSQUADRA)

else STOP).

OPERAIO = (preleva -> fineop -> OPERAIO).

TAVOLO = T[0],

T[q:0..C] = (when q < C deposita -> T[q+1] |

when q > 0 op[1..N].preleva -> T[q-1]).

||OFFICINA = (op[1..N]:OPERAIO || TAVOLO || LAVAGNA || CAPOSQUADRA).

Es.: Un sistema è composto da un insieme di banche e un insieme di operatori finanziari che devono spostare fondi

da una banca all’altra. Ogni operatore ciclicamente seleziona due banche e trasferisce 1€ da una banca

all’altra. Il conto da cui si preleva non può avere un fondo negativo, e il conto in cui si deposita ha un limite

massimo. Ogni banca gestisce un solo conto.

- Ogni singola azione agisce su due conti

- Bisogna sempre verificare la consistenza dei conti ad ogni operazione

const NBANCHE = 3

const NOPERATORI = 3

range ID_BANCHE = 0..NBANCHE-1

range ID_OP = 0..NOPERATORI-1

const MAX = 3

const MIN = 0

range CONTO = MIN..MAX

BANCA = LIBERA[2],

LIBERA[amount:CONTO] = (acquisisci -> OCCUPATA[amount]),

OCCUPATA[amount:CONTO] = (

when (amount > MIN) preleva -> ok -> OCCUPATA[amount-1] |

when (amount == MIN) preleva -> ko -> OCCUPATA[amount] |

when (amount < MAX) deposita -> ok -> OCCUPATA[amount+1] |

when (amount == MAX) deposita -> ko -> OCCUPATA[amount] |

rilascia -> LIBERA[amount]

).

OPERATORE = (scegli[i:ID_BANCHE][j:ID_BANCHE] -> TROVAMIN[i][j]),

TROVAMIN[i:ID_BANCHE][j:ID_BANCHE] = (

when(i<=j) conferma -> TRANSAZIONE[i][j] |

when(j<=i) conferma -> TRANSAZIONE[j][i]

), 23

TRANSAZIONE[da:ID_BANCHE][a:ID_BANCHE] = (

//per semplicità si trasferisce sempre dal primo al secondo

when(da != a) b[da].acquisisci -> b[a].acquisisci -> PRELEVA[da][a] |

when(da == a) b[da].acquisisci -> PRELEVA[da][a]

),

PRELEVA[da:ID_BANCHE][a:ID_BANCHE] = (

b[da].preleva -> (b[da].ok -> DEPOSITA[da][a] | b[da].ko -> RILASCIA[da][a])

),

DEPOSITA[da:ID_BANCHE][a:ID_BANCHE] = (

b[a].deposita -> (b[a].ok -> RILASCIA[da][a] | b[a].ko ->b[da].deposita ->

b[da].ok -> RILASCIA[da][a])

),

RILASCIA[da:ID_BANCHE][a:ID_BANCHE] = (

when (da == a) b[da].rilascia -> OPERATORE |

when (da != a) b[a].rilascia -> b[da].rilascia -> OPERATORE

).

||SYS=(o[ID_OP]::b[ID_BANCHE]:BANCA || o[ID_OP]:OPERATORE). 24

Lezione 11

Es.: Gestione di un albergo: un’agenzia prenota una stanza, poi decide se annullare la prenotazione o se

confermarla. Non si possono prenotare stanze già prenotate o in attesa di conferma. L’agenzia non può

prenotare altre stanze se ci sono altre prenotazioni in sospeso.

- Per tenere conto delle prenotazioni non andate a buon fine, utilizziamo l’indice 0 per quelle non

andate bene, 1 per quelle andate bene.

- Le camere dell’albergo hanno 3 stati: prenotate, confermate, libere.

Valore iniziale delle camere: 0 0 NC

- INVARIANTE = proprietà che rimane invariante nel corso dell’esecuzione.

L’albergo è composto da stanze prenotate (np), confermate (nc), libere (nl), e la somma di questi

valori deve essere uguale al numero totale delle camere NC. Questa relazione vale sempre, e quindi è

una proprietà invariante.

const NC = 4

const NA = 1

Agenzia = (prenota[0] -> Agenzia | prenota[1] -> Scelta),

Scelta = (annulla -> Agenzia | conferma -> Agenzia).

||Agenzie = (a[1..NA]:Agenzia).

Cliente = (chiede_stanza -> … -> libera).

Albergo = A[0][0][NC],

A[np:0..NC][nc:0..NC][nl:0..NC] = (

when nl > 0 prenota[1] -> A[np+1][nc][nl-1] |

when nl == 0 prenota[0] -> A[np][nc][nl] |

when np > 0 conferma -> A[np-1][nc+1][nl] |

when np > 0 annulla -> A[np-1][nc][nl+1] |

when nc > 0 libera -> A[np][nc-1][nl+1]

).

||S = (Agenzie || a[1..NA]::Albergo)/{libera/{a[1..NA]}.libera}.

se manca questa parte, abbiamo prenota.0 per Albergo e a.1.prenota.0 per Agenzie;

siccome sono diversi vengono considerati come due azioni indipendenti! 25

Lezione 12

Es.: Dei cuccioli mangiati tutti nella stessa ciotola, prendendo una porzione alla volta. Quando la ciotola si svuota

la mamma la riempe.

const NC = 4

const Piena = 5

Cucciolo = (fame -> mangia -> Cucciolo).

||Cuccioli = (c[1..NC]:Cucciolo).

Mamma = (riempi -> Mamma).

Ciotola = C[Piena],

C[q:0..Piena] = ( when q > 0 c[1..NC].mangia -> C[q-1] |

when q == 0 riempi -> C[Piena] ).

||Pasto = (Ciotola || Cuccioli || Mamma).

Es. Cuccioli: i cuccioli mangiano dalla ciotola, oppure giocano e poi vengono lavati dalla mamma.

const NC = 4

const Piena = 5

Cucciolo = (fame -> mangia -> Cucciolo |

gioca -> lava -> Cucciolo ).

||Cuccioli = (c[1..NC]:Cucciolo).

Mamma = (riempi -> Mamma | c[1..NC].lava -> Mamma).

Ciotola = …

||Pasto = … 26

Lezione 13

Es.: Un giardino pubblico ha 2 cancelli di accesso. Il gestore vuole sapere quante persone entrano nel giardino.

const N = 4

range T = 0..N

set VarAlpha = {value.write[0..N+1], value.read[T]}

Lock = (prendi -> lascia -> Lock).

VAR = VAR[0][0],

VAR[u:T][0] = (acquisisci -> VAR[u][1]),

VAR[u:T][1] = ( read[u] -> VAR[u][1] |

write[v:T] -> VAR[v][1] |

rilascia -> VAR[u][0] |

write[N+1] -> STOP ).

||VARLOCK = (VAR || Lock).

Cancello = (parti -> Run),

Run = (arriva -> Incrementa | end -> Cancello),

Incrementa = (value.acquisisci -> value.read[x:T] -> value.write[x+1] ->

value.lascia -> Run) + VarAlpha.

||Giardino = (est:Cancello || ovest:Cancello || {est,ovest}::value:VAR)

/ {parti/{est,ovest