Introdotto da Dijkstra nel 1965, il problema della sezione critica (Critical Section problem) è uno dei più importanti e studiati nella programmazione concorrente, nel contesto della competizione tra processi.
Abbiamo N processi, ciascuno esegue un ciclo infinito che si divide in due parti:
P[1..n]:
loop forever
<non-critical section>
<entry (o pre-) protocol>
<critical section>
<exit (o post-) protocol>
<non-critical section>Il compito è progettare i protocolli di entrata e uscita che soddisfino le seguenti proprietà:
| Proprieta | Descrizione |
|---|---|
| Mutua esclusione | Le sezioni critiche di due o piu processi non devono essere interleave |
| Assenza di deadlock | Se qualche processo cerca di entrare in CS, uno di loro deve prima o poi riuscirci |
| Assenza di starvation | Se un processo cerca di entrare in CS, deve prima o poi riuscirci |
| Bounded waiting | Esiste un limite superiore al numero di volte che altri processi possono entrare in CS prima che un processo in attesa ci riesca |
La sezione critica non e una zona di memoria: e una sezione di codice. Quando un processo e nella propria sezione critica, gli altri processi possono fare qualunque cosa — l'importante e che non siano anch'essi nella loro sezione critica.
C'è anche la proprietà di progress per la CS: una volta che un processo inizia la sezione critica, deve terminarla prima o poi. La NCS, invece, non ha obbligo di progresso (un processo può rimanere infinitamente nella NCS o terminare).
Il professor Ricci osserva che il problema della sezione critica modella situazioni reali: ad esempio, un check-in kiosk in aeroporto che accede a un database centrale dei passeggeri. Ogni chiosco è un processo concorrente che deve accedere in mutua esclusione al database condiviso.
Ricordate la differenza: la violazione della mutua esclusione si cerca nel diagramma di stato cercando stati <p3,q3,_> (entrambi in CS). La starvation riguarda la possibilita che un processo aspetti per sempre in p2 (pre-protocol) mentre l'altro e in NCS.
I due protocolli sono detti anche protocollo di ingresso (entry/pre-protocol) e di uscita (exit/post-protocol).
turnIl primo tentativo usa una variabile condivisa turn che indica a chi spetta entrare in sezione critica:
integer turn := 1
p q
loop forever loop forever
p1: NCS q1: NCS
p2: await turn = 1 q2: await turn = 2
p3: CS q3: CS
p4: turn := 2 q4: turn := 1Verifica di mutua esclusione: il diagramma di stato ha 16 stati (con NCS e CS espansi) o 4 stati (versione ridotta rimuovendo NCS e CS). Non esistono stati <p2,q2,_> nella versione ridotta (o <p3,q3,_> in quella completa) — la mutua esclusione e soddisfatta.
Assenza di deadlock: se entrambi vogliono entrare, uno dei due otterra il turno giusto. Anche questa e soddisfatta.
Assenza di starvation: NON soddisfatta. Se il processo P esegue la CS e poi si ferma nella NCS (o termina), Q rimane bloccato in q2: await turn = 2 per sempre, perche turn e rimasto a 2. turn funziona come un permesso di accesso: se chi detiene il permesso non lo rilascia (perche e bloccato in NCS), l'altro processo non potra mai entrare.
La variabile turn crea una dipendenza rigida: il testimone passa avanti e indietro. Se un processo si ferma dopo aver usato la CS, l'intero sistema si blocca per l'altro processo.
In sintesi: la mutua esclusione è soddisfatta (non esiste stato <p3,q3,_>), l'assenza di deadlock è soddisfatta, ma la starvation è possibile: se un processo rimane indefinitamente nella sua NCS, il turn non cambia e l'altro processo non può mai entrare in CS. La soluzione non è corretta.
want separateIntroduciamo variabili booleane separate per indicare l'intenzione di entrare in CS:
boolean wantp := false, wantq := false
p: q:
p1: NCS q1: NCS
p2: while wantq skip q2: while wantp skip
p3: wantp := true q3: wantq := true
p4: CS q4: CS
p5: wantp := false q5: wantq := falseIl problema e che il pre-protocol (test + set) non e atomico: esiste uno scenario in cui entrambi i processi passano il test (while) prima che uno dei due setti la propria variabile, portando allo stato <p3,q3,true,true> dove entrambi entrano in CS. Mutua esclusione violata.
Spostiamo l'assegnamento prima dell'await, rendendo l'intenzione immediata:
boolean wantp := false, wantq := false
p: q:
p1: wantp := true q1: wantq := true
p2: await wantq = false q2: await wantp = false
p3: CS q3: CS
p4: wantp := false q4: wantq := falseLa mutua esclusione ora e soddisfatta. Tuttavia, se entrambi settano la propria variabile a true prima di eseguire l'await, si trovano in deadlock: P aspetta che wantq sia false, ma wantq e true e Q non puo cambiarlo perche e bloccato ad aspettare wantp false. Piu precisamente, e un livelock (entrambi sono attivi ma nessuno progredisce).
Se un processo scopre che l'altro e in competizione, rinuncia temporaneamente alla sua intenzione:
p: q:
p1: wantp := true q1: wantq := true
p2: while wantq do q2: while wantp do
p3: wantp := false q3: wantq := false
p4: wantp := true q4: wantq := true
p5: CS q5: CS
p6: wantp := false q6: wantq := falseIl livelock e risolto: i processi ora rilasciano l'intenzione quando c'e contesa. Tuttavia, in caso di interleaving perfetto (scenario simmetrico), puo verificarsi starvation: entrambi continuano a settare e resettare la propria variabile all'infinito senza mai entrare in CS.
| Tentativo | Idea | Problema |
|---|---|---|
| 1 (turn) | Variabile turn che alterna il permesso | Starvation se l'altro si ferma in NCS |
| 2 (want) | Flag booleani di intenzione | Violazione mutua esclusione (non atomicita del pre-protocol) |
| 3 (want + await) | Set prima dell'await | Deadlock / livelock se entrambi settano contemporaneamente |
| 4 (while loop) | Rinuncia in caso di contesa | Starvation per interleaving perfetto |
Dekker combina il primo e il quarto tentativo: introduce il turn per risolvere la contesa, ma lo usa solo quando c'e effettiva competizione. Quando l'altro processo non vuole entrare, si procede senza attendere il turno.
L'algoritmo e corretto: soddisfa mutua esclusione, assenza di deadlock e assenza di starvation su architetture che forniscono solo load e store come istruzioni atomiche.
Peterson propone una soluzione piu concisa, unendo due await in una singola condizione composta:
boolean wantp := false
boolean wantq := false
integer turn := 1
p: q:
loop forever loop forever
NCS NCS
wantp := true wantq := true
turn := 2 turn := 1
await (!wantq or turn = 1) await (!wantp or turn = 2)
CS CS
wantp := false wantq := falseLa condizione await (!wantq or turn = 1) dice: "se Q non vuole entrare, passa; se Q vuole entrare, aspetta il tuo turno". La variabile turn e l'arbitro che decide in caso di contesa simultanea.
Trovato dal matematico olandese T.J. Dekker nel 1965, è la prima soluzione corretta al problema della sezione critica per due processi. Combina il primo (turn) e il quarto tentativo: il diritto di insistere per entrare (non il diritto di entrare) viene passato esplicitamente tra i processi usando la variabile turn.
boolean wantp := false
boolean wantq := false
integer turn := 1
p: q:
loop forever loop forever
NCS NCS
wantp := true wantq := true
while wantq = true while wantp = true
if turn = 2 then if turn = 1 then
wantp := false wantq := false
await turn = 1 await turn = 2
wantp := true wantq := true
CS CS
turn := 2 turn := 1
wantp := false wantq := falseDekker soddisfa mutua esclusione, assenza di deadlock e assenza di starvation. Funziona su qualsiasi architettura che fornisca solo load e store come istruzioni atomiche.
Peterson è corretto e più semplice di Dekker. È spesso usato come esempio didattico di soluzione al problema della sezione critica. La versione seguente, commentata riga per riga, usa la forma con busy-wait esplicito:
Il professor Ricci presenta i tentativi di soluzione in ordine cronologico, mostrando come ogni tentativo risolva alcuni problemi ma ne introduca altri. Dekker combina il primo e il quarto tentativo, introducendo il concetto di passaggio esplicito del diritto di insistere (non del diritto di entrare) tramite la variabile turn:
boolean wantp := false, wantq := false;
integer turn := 1;
/* Processo P */
loop forever {
p1: NCS
p2: wantp := true
p3: while (wantq) {
p4: if (turn = 2) {
p5: wantp := false
p6: await turn = 1
p7: wantp := true
}
}
p8: CS
p9: turn := 2
p10: wantp := false
}L'algoritmo di Dekker è corretto: soddisfa mutua esclusione, assenza di deadlock e assenza di starvation.
Peterson ha proposto una soluzione più concisa, che condensa due istruzioni await in una con una condizione composta:
L'algoritmo di Peterson è considerato la soluzione più elegante per due processi. Il professor Ricci lo presenterà anche in una lezione successiva nel contesto di Java.
Il professor Ricci sottolinea che non è richiesto di ricordare a memoria i dettagli di tutti gli algoritmi, ma è importante capire come si analizza la correttezza: costruire il diagramma di stato, verificare che gli stati critici non siano raggiungibili, e controllare le proprietà di safety e liveness.
Ricapitolando: dopo vari tentativi (secondo tentativo con variabili wantp/wantq che viola la mutua esclusione; terzo tentativo che soffre di deadlock; quarto tentativo che soffre di starvation per interleaving perfetto), si arriva alla soluzione finale. Peterson funziona su qualsiasi architettura che fornisca load e store come istruzioni atomiche. La dimostrazione di correttezza puo essere fatta costruendo il diagramma di stato ridotto (solo le etichette rilevanti per la sincronizzazione) e verificando le tre proprieta.
Il widget seguente anticipa il capitolo sui semafori: mostra come un semaforo binario protegga la sezione critica, lo stesso obiettivo raggiunto qui "a mano" da Dekker e Peterson.
L'algoritmo del fornaio (bakery algorithm) e una soluzione per N processi che introduce il concetto di biglietto numerato, come in una panetteria: ogni cliente (processo) prende un numero e viene servito in ordine crescente.
int num := 1
int next := 1
turn[1:n] := [0, 0, 0, ...]
p[i]:
loop forever
NCS
<turn[i] := num; num := num + 1> { atomico }
await turn[i] = next
CS
next := next + 1Ogni processo prende un ticket (turn[i]) in modo atomico, poi attende che il suo numero sia il prossimo a essere servito (next). Quando esce dalla CS, incrementa next per far passare il processo successivo.
Problema: overflow aritmetico. I contatori num e next crescono monotonamente e con interi a dimensione finita possono arrivare a overflow, causando il reset a 0 e la violazione della proprieta di ordinamento.
Il bakeri algorithm e un esempio importante perche mostra come risolvere la sezione critica per un numero arbitrario di processi, ma evidenzia anche i limiti pratici degli interi finiti.
Gli algoritmi di Dekker e Peterson funzionano su qualsiasi architettura che fornisca solo load e store come istruzioni atomiche. Tuttavia, il problema della sezione critica si semplifica enormemente se possiamo sfruttare istruzioni atomiche composte fornite dalla macchina concorrente.
L'istruzione test-and-set è un'operazione atomica che combina lettura e scrittura:
test-and-set(x, r):
< r := x, x := 1 >L'uso delle parentesi angolari < ... > indica che il gruppo di istruzioni è atomico: nessun interleaving possibile all'interno.
Il test-and-set permette di realizzare un lock in modo semplice: la variabile lock vale 0 (libero) o 1 (occupato). L'istruzione atomica test-and-set legge il valore corrente e lo imposta a 1 in un'unica operazione indivisibile. Se il valore letto era 0, il lock era libero e ora è stato acquisito. Se era 1, il lock era occupato e bisogna ritentare.
Le principali istruzioni atomiche composte sono:
| Istruzione | Descrizione |
|---|---|
| test-and-set (x, r) | <r := x; x := 1> — atomico |
| exchange (x, r) | Scambia il valore di x con r in modo atomico |
| fetch-and-add (x, v) | <tmp := x; x := x + v; return tmp> — atomico |
| compare-and-swap (x, e, v) | <if x == e then x := v; return true else return false> |
Con test-and-set possiamo realizzare un lock semplice:
integer lock := 0
integer was_locked
loop forever
NCS
repeat
test_and_set(lock, was_locked)
until was_locked = 0
CS
lock := 0La test_and_set e atomica e fa due cose contemporaneamente: copia il vecchio valore di lock in was_locked e setta lock a 1. Se was_locked risultava 0, significa che il lock era libero e il processo puo entrare. Se era 1, qualcun altro ha gia preso il lock e bisogna riprovare (busy-wait).
Questa soluzione funziona con N processi, non solo 2.
La caratteristica fondamentale di test_and_set e che modifica una variabile condivisa e ne restituisce il valore precedente in un unico passo atomico. Non e possibile interleaving tra la lettura e la scrittura.
synchronizedIl costrutto synchronized in Java implementa sezioni atomiche usando un lock condiviso:
// processo (thread) A
synchronized (lock) {
<statement a>
<statement b>
}
// processo (thread) B
synchronized (lock) {
<statement c>
<statement d>
}Non possono esistere scenari con sequenze come a.c.b.d o c.a.d.b — i blocchi synchronized sullo stesso oggetto lock sono eseguiti in mutua esclusione.
Sfruttando istruzioni atomiche composte si può realizzare un meccanismo di lock elementare: due operazioni atomiche (acquire e release) proteggono la sezione critica.
lock sharedlock
p: q:
loop forever loop forever
NCS NCS
acquire(sharedlock) acquire(sharedlock)
CS CS
release(sharedlock) release(sharedlock)test-and-set e compare-and-swap sono la base su cui vengono costruiti tutti i meccanismi di sincronizzazione di piu alto livello: semafori, lock, monitor. Il professore sottolinea che la scelta del giusto livello di atomicita e cruciale.
Il test cerca la presenza di bug eseguendo il programma su scenari selezionati, rivela la presenza di errori ma non la loro assenza. La verifica (verification) vuole stabilire se una proprieta di correttezza vale in tutti i possibili scenari di esecuzione, usando tecniche formali come il model checking o la dimostrazione induttiva di invarianti.
Un processo soffre di starvation quando, pur cercando di entrare nella sua sezione critica (esegue il pre-protocol), non riesce mai ad accedervi perche altri processi continuano a entrare prima di lui. Nel primo tentativo (con turn), la starvation si verifica quando il processo che detiene il permesso (turn) si ferma nella NCS, impedendo all'altro di entrare per sempre.
1. Mutua esclusione (una risorsa non puo essere usata da piu processi contemporaneamente); 2. Hold and wait (un processo che gia detiene risorse puo richiederne altre); 3. No preemption (le risorse non possono essere rimosse forzatamente); 4. Circular wait (due o piu processi formano una catena circolare di attesa). Tutte e quattro devono valere simultaneamente perche si verifichi deadlock.
Con la formula []!(p3 ∧ q3) (o equivalentemente G!(p3 ∧ q3)): "sempre non (p3 e q3 contemporaneamente)". Dove p3 e q3 sono proposizioni atomiche che indicano che il control pointer del processo P o Q si trova nella sezione critica.
Tre differenze fondamentali: (1) wait su semaforo puo non bloccare (se S.V > 0), waitC blocca sempre; (2) signal su semaforo ha sempre effetto (incrementa o sblocca), signalC non fa nulla se la coda e vuota; (3) signal sblocca un processo arbitrario, signalC sblocca dalla testa della coda FIFO; (4) un processo sbloccato da signal riprende immediatamente, mentre con signalC deve attendere che il segnalante esca dal monitor (dipende dalla disciplina).
Esprime che, dal momento in cui un processo P tenta di entrare nella sezione critica, un altro processo Q puo entrare in CS al massimo k volte prima che P entri a sua volta. E una proprieta piu forte della semplice assenza di starvation, che garantisce non solo che P prima o poi entri, ma che lo faccia entro un numero limitato di "sorpassi".
Il problema principale e la state-space explosion: il numero di stati cresce esponenzialmente con il numero di processi e di variabili. Viene affrontato con tecniche come: (a) riduzione del modello eliminando dettagli irrilevanti; (b) costruzione incrementale del grafo fermandosi al primo stato falsificante; (c) model checking simbolico, che lavora con insiemi di stati descritti intensivamente (BDD) invece che singoli stati.
Peterson combina l'uso di variabili di intenzione (wantp, wantq) con una variabile turn che funge da arbitro in caso di contesa simultanea. La condizione composta await (!wantq or turn = 1) garantisce: (1) se Q non vuole entrare, P passa direttamente; (2) se entrambi vogliono entrare, turn decide chi passa. L'ultimo che setta turn "perde" e deve aspettare, prevenendo sia la violazione di mutua esclusione che la starvation.