Il professor Ricci apre la lezione con un aggiornamento sull'organizzazione dell'esame. La prova si compone di due parti: una prova pratica sotto forma di mini-progetti chiamati assignment, e un colloquio orale in cui si discutono proprio quegli assignment come occasione per esplorare gli argomenti del corso.
Il professor Ricci specifica che è consentito l'uso dell'AI negli assignment, a patto che venga usata in modo opportuno: l'importante è che lo studente sappia cosa ha fatto e sappia discuterne al colloquio. L'AI va usata come supporto, non come sostituto della comprensione.
Il colloquio orale non è un esame tradizionale: si parte dalla discussione degli assignment (cosa avete fatto, come, perché) e da lì si sviluppa una conversazione sugli argomenti del corso. È quindi essenziale aver svolto gli assignment in modo consapevole.
Un programma concorrente non banale si basa su processi che interagiscono tra loro. Il professor Ricci distingue tre tipi fondamentali di interazione:
Interazioni attese e volute: fanno parte della semantica del programma concorrente.
Interazioni attese e necessarie, ma non volute: nascono dalla necessità di coordinare l'accesso a risorse condivise.
Il professor Ricci usa l'analogia del lock: quando due processi competono per una risorsa, non ci interessa chi arriva prima, ma vogliamo evitare interferenze. La competizione va gestita, non è un'interazione voluta ma è inevitabile.
Interazioni né attese né volute: producono effetti dannosi solo quando il rapporto tra le velocità dei processi assume valori specifici (errori tempo-dipendenti).
L'esempio classico di race condition è quello di due processi che incrementano la stessa variabile condivisa in modo non atomico. Il professor Ricci lo introduce come segue.
Supponiamo di avere una variabile n inizializzata a 0, e due processi P e Q che eseguono ciascuno n := n + 1. Se l'incremento non è atomico, l'esecuzione si può spacchettare in due operazioni:
tmp := n /* lettura */
n := tmp + 1 /* scrittura */A seconda dell'interleaving, possono verificarsi scenari in cui entrambi i processi leggono il valore 0 prima che uno dei due lo scriva, portando entrambi a scrivere 1 — il cosiddetto lost update (aggiornamento perso).
Il problema nasce quando un'operazione che a livello di linguaggio sembra singola (n := n + 1) viene tradotta in più operazioni a livello macchina (leggi, modifica, scrivi). L'interleaving può avvenire nel mezzo, causando risultati inaspettati.
Per esplorare interattivamente il fenomeno, provate il simulatore seguente.
Notate come, anche se entrambi i processi eseguono le stesse istruzioni, l'ordine in cui vengono eseguite le letture e le scritture può portare a risultati diversi. Su 6 scenari possibili, solo 2 portano al valore finale corretto n = 2.
Questo è un errore subdolo: il programma può funzionare correttamente milioni di volte, e poi fallire per una specifica combinazione di eventi di scheduling. Ecco perché è così difficile debuggare i programmi concorrenti.
Il professor Ricci sottolinea con forza un punto spesso frainteso: sincronizzazione e mutua esclusione sono concetti diversi, anche se correlati.
| Sincronizzazione | Mutua Esclusione |
|---|---|
| Definisce una relazione temporale tra processi | Definisce una restrizione sull'accesso a dati condivisi |
| Mantenere relazioni temporali: azioni che avvengono "nello stesso momento" o "prima/dopo" | Non ha senso se non ci sono dati condivisi |
| Non richiede necessariamente dati condivisi | Richiede tipicamente forme implicite di sincronizzazione (blocco di azioni, attesa) |
In Java, la parola chiave synchronized è stata scelta per denotare la mutua esclusione, non la sincronizzazione. Questo crea confusione nella letteratura. Quando un metodo ha l'attributo synchronized, significa che la sua esecuzione richiede l'acquisizione del lock dell'oggetto — è mutua esclusione, non sincronizzazione nel senso proprio del termine.
Il professor Ricci cita l'articolo di Buhr e Harji: "Concurrent Urban Legends" (2005). Saper distinguere questi due concetti è un punto fondamentale che viene regolarmente chiesto al colloquio.
Per eseguire un programma concorrente abbiamo bisogno di una macchina concorrente: una macchina (astratta o fisica) progettata per gestire l'esecuzione di molteplici processi sequenziali, sfruttando più processori (fisici o virtuali).
La macchina concorrente fornisce tanti processori virtuali quanti sono i processi del programma concorrente. Poi, un livello sottostante (sistema operativo, virtual machine, hardware) mappa questi processori virtuali sui processori fisici disponibili.
La macchina concorrente fornisce tre categorie di meccanismi di base:
Un esempio concreto: Java Virtual Threads. Un programma può creare decine di migliaia di virtual thread come entità logiche, che vengono poi eseguiti da un insieme di thread fisici pari (tipicamente) al numero di processori disponibili. È la macchina concorrente (la JVM) che si occupa di questo mapping.
Analogamente, nel modello Attori (che useremo in laboratorio), si possono creare milioni di attori — entità logiche che comunicano tramite messaggi — e la macchina concorrente li mappa efficientemente sulle risorse hardware parallele.
Come possiamo studiare il comportamento di un programma concorrente in modo rigoroso, quasi matematico? Il professor Ricci introduce il modello base:
Lo stato del sistema è definito da una tupla composta da:
C'è una transizione tra due stati s1 e s2 se l'esecuzione di un'istruzione in s1 porta a s2. L'istruzione eseguita deve essere una di quelle puntate dai puntatori di controllo in s1.
Il diagramma di stato è il grafo che contiene tutti gli stati raggiungibili del programma. Gli scenari (o tracce di esecuzione) sono i cammini nel grafo a partire dallo stato iniziale. I cicli rappresentano la possibilità di computazione infinita in un grafo finito.
Una volta costruito il diagramma di stato, possiamo esplorarlo per verificare proprietà. Per ogni stato, possiamo controllare se una condizione indesiderata è vera o falsa. Questo rende deterministico il modo di stabilire se un programma concorrente è corretto. Il problema è il numero di stati: l'esplosione dello spazio degli stati.
Vediamo il primo esempio trattato dal professor Ricci: due processi con una sola azione ciascuno, che assegnano un valore a una variabile condivisa.
/* Processo P */
integer k1 := 1
p1: n := k1
/* Processo Q */
integer k2 := 2
q1: n := k2
/* Variabile condivisa */
integer n := 0In questo caso abbiamo 5 stati e 2 scenari. Il diagramma di stato è il seguente:
flowchart LR s0["<p1,q1,0,1,2>"] s1["<end,q1,1,1,2>"] s2["<p1,end,2,1,2>"] s3["<end,end,2,1,2>"] s4["<end,end,1,1,2>"] s0 -->|p1: n:=k1| s1 s0 -->|q1: n:=k2| s2 s1 -->|q1: n:=k2| s3 s2 -->|p1: n:=k1| s4
Consideriamo due processi che stampano due messaggi ciascuno:
/* Processo P */
p1: print("p1")
p2: print("p2")
/* Processo Q */
q1: print("q1")
q2: print("q2")Quanti scenari possibili? Se proviamo a elencarli:
In totale 6 scenari. Il professor Ricci fa notare come già con solo due azioni per processo la complessità inizi a crescere. Il diagramma di stato corrispondente:
flowchart LR s0["<p1,q1>"] s1["<p2,q1>"] s2["<p1,q2>"] s3["<p2,q2>"] s4["<-,q1>"] s5["<p1,->"] s6["<-,q2>"] s7["<p2,->"] s8["<-,->"] s0 -->|p1| s1 s0 -->|q1| s2 s1 -->|p2| s4 s1 -->|q1| s3 s2 -->|p1| s3 s2 -->|q2| s5 s3 -->|p2| s6 s3 -->|q2| s7 s4 -->|q1| s6 s5 -->|q2| s7 s6 -->|q2| s8 s7 -->|p2| s8
Esplorate i vari stati del diagramma con questo strumento interattivo:
Il professor Ricci osserva che se aggiungiamo un terzo processo (R con due azioni), gli scenari diventano 90. Con 6 azioni per processo? L'esplosione combinatoria è evidente.
Il professor Ricci mostra la crescita esponenziale del numero di scenari al variare del numero di azioni per processo.
| Azioni per processo | Numero di scenari |
|---|---|
| 1 | 2 |
| 2 | 6 |
| 3 | 20 |
| 4 | 70 |
| 5 | 252 |
| 6 | 924 |
| 7 | 3.432 |
| 8 | 12.820 |
| Azioni per processo | Numero di scenari |
|---|---|
| 1 | 6 |
| 2 | 90 |
| 3 | 1.680 |
| 4 | 34.650 |
La formula generale per k processi con n1, n2, ..., nk azioni ciascuno è:
(n1 + n2 + ... + nk)! / (n1! · n2! · ... · nk!)
Il professor Ricci osserva che questi numeri crescono così rapidamente che bastano poche azioni e pochi processi per avere miliardi di scenari. È il fenomeno dell'esplosione dello spazio degli stati.
Un tema centrale della lezione è l'importanza di scegliere il giusto livello di atomicità. Il professor Ricci mostra due versioni dello stesso programma:
/* Processo P */
p1: n := n + 1
/* Processo Q */
q1: n := n + 1
/* Variabile condivisa */
integer n := 0Se l'incremento è atomico, il risultato finale è sempre n = 2. Un solo scenario possibile.
/* Processo P */
integer tmp;
p1: tmp := n
p2: n := tmp + 1
/* Processo Q */
integer tmp;
q1: tmp := n
q2: n := tmp + 1
/* Variabile condivisa */
integer n := 0Se l'incremento è non atomico (spacchettato in lettura e scrittura), il risultato finale può essere n = 1 o n = 2, a seconda dell'interleaving. Su 12 stati, solo 2 scenari su 6 portano a n = 2.
Il diagramma di stato per il caso non atomico mostra 12 stati:
flowchart LR s0["<p1,q1,0,0,0>"] s1["<p2,q1,0,0,0>"] s2["<p1,q2,0,0,0>"] s3["<p2,q2,0,0,0>"] s4["<-,q1,1,0,0>"] s5["<p1,-,1,0,0>"] s6["<-,q2,1,0,1>"] s7["<p2,-,1,0,0>"] s8["<p2,-,1,1,0>"] s9["<-,q2,1,0,0>"] s10["<-,-,2,0,1>"] s11["<-,-,1,0,0>"] s0 -->|p1| s1 s0 -->|q1| s2 s1 -->|p2| s4 s1 -->|q1| s3 s2 -->|p1| s3 s2 -->|q2| s5 s3 -->|p2| s6 s3 -->|q2| s7 s4 -->|q1| s6 s5 -->|q2| s9 s6 -->|q2| s10 s7 -->|p2| s11 s8 -->|q2| s6 s9 -->|p1| s11 s10 -->|p2| s8
Il professor Ricci spiega che l'incremento atomico può essere ragionevole come assunzione di modellazione (se la macchina concorrente lo supporta), mentre l'incremento non atomico è più realistico rispetto a ciò che accade realmente a livello hardware. Ad esempio, l'istruzione assembly INC lavora sul registro, non direttamente sulla memoria: è inevitabile un passaggio lettura-modifica-scrittura.
Il professor Ricci mostra anche come le stesse operazioni appaiono a livello di macchina, sia su stack machine che su register machine:
/* Processo P */
p1: push n
p2: push #1
p3: add
p4: pop n
/* Processo Q */
q1: push n
q2: push #1
q3: add
q4: pop n/* Processo P */
p1: load R1, n
p2: add R1, #n
p3: store n, R1
/* Processo Q */
q1: load R1, n
q2: add R1, #n
q3: store n, R1Il professor Ricci sottolinea che la scelta del livello di atomicità ha un impatto diretto sul numero di stati e scenari. Azioni atomiche più grandi riducono la complessità del modello, ma potrebbero non essere realistiche rispetto all'implementazione sottostante. È un trade-off fondamentale nella modellazione.
Non tutti i processi terminano. Il professor Ricci introduce il caso di processi con comportamento ciclico infinito:
/* Processo P - cerca di portare n ad almeno 1 */
p1: while (n < 1)
p2: n := n + 1
/* Processo Q - cerca di portare n a 0 o meno */
q1: while (n >= 0)
q2: n := n - 1
/* Variabile condivisa */
integer n := 1Questo esempio è tratto dal libro di Ben-Ari. I due processi hanno obiettivi opposti: P vuole incrementare n fino a 1, Q vuole decrementarlo fino a 0 o meno.
Il diagramma di stato è complesso, con molteplici cicli che rappresentano computazioni potenzialmente infinite. A seconda dell'interleaving, il sistema può terminare (quando entrambi i processi escono dai loro cicli) o continuare indefinitamente.
I processi ciclici sono la norma, non l'eccezione, nei sistemi concorrenti. Un sistema operativo, un server web, un controller industriale: sono tutti progettati per non terminare. La correttezza riguarda ciò che accade durante l'esecuzione, non solo alla fine.
I cicli nel diagramma di stato rappresentano la possibilità di computazione infinita in un grafo finito. L'analisi di questi cicli è cruciale per le proprietà di liveness.
Il professor Ricci estende il concetto di atomicità dalle azioni alle strutture dati. Un oggetto dati è detto atomico se può trovarsi in un numero finito di stati pari al numero di valori che può assumere, e le operazioni cambiano atomicamente quello stato. I tipi primitivi nei linguaggi concorrenti sono tipicamente atomici (con eccezioni, come double in Java).
I tipi di dato astratti composti da oggetti dati più semplici non sono atomici (es. classi in OO, struct in C). Per questi si possono identificare due tipi di stati:
La corrispondenza è parziale: esistono stati interni senza corrispondente stato esterno (stati inconsistenti). In programmazione sequenziale questo non è un problema (grazie all'information hiding), ma in programmazione concorrente un processo potrebbe operare su un oggetto mentre un altro lo sta modificando, trovandolo in uno stato inconsistente.
La correttezza dei programmi concorrenti (anche di quelli che non terminano) si definisce in termini di proprietà delle computazioni: condizioni che devono essere verificate in ogni possibile scenario.
Proprietà di sicurezza (safety): "le cose cattive non devono mai accadere". Una proprietà safety deve essere vera in ogni stato di ogni computazione. Tipicamente espressa come invariante.
Esempi:
Le proprietà safety sono più facili da verificare: basta trovare un singolo stato che le violi per dimostrare che il programma non è corretto. Il professor Ricci le descrive spesso "in negativo": piuttosto che dire "voglio che X sia sempre vero", si dice "non voglio che X sia mai falso".
Proprietà di vitalità (liveness): "le cose buone devono prima o poi accadere". Una proprietà liveness afferma che in ogni computazione esiste qualche stato in cui la proprietà è vera.
Esempi:
Verificare liveness è più complesso: non basta controllare stato per stato, bisogna analizzare l'intera computazione. Una proprietà liveness non può essere violata in un singolo stato, ma solo lungo un'intera traccia di esecuzione.
Il professor Ricci sottolinea che la distinzione tra safety e liveness è concettualmente fondamentale. Al colloquio, saper identificare se una proprietà è di safety o liveness è un punto chiave. Esempio: "non voglio deadlock" è una proprietà di safety (il deadlock è una situazione in un certo stato del sistema). "ogni processo deve prima o poi entrare in sezione critica" è una proprietà di liveness.
La fairness è una proprietà di liveness che riguarda la certezza che "qualcosa di buono accada infinite volte". L'esempio principale: un processo attivato infinite volte durante l'esecuzione di un'applicazione, a ciascun processo viene dato un turno equo.
La fairness è un requisito sul scheduling. A seconda della politica di scheduling, i programmi possono comportarsi diversamente. Tre definizioni principali:
| Tipo | Definizione | Esempio |
|---|---|---|
| Incondizionata | Ogni azione non condizionale che è eligible viene eseguita prima o poi. | Un'istruzione print("ok") in un loop sarà eseguita prima o poi. |
| Debole (weak) | Ogni azione condizionale la cui condizione diventa e rimane vera viene eseguita prima o poi. | while(flag = false){ n := 1-n }: se flag diventa false e rimane false, il ciclo prima o poi esegue. |
| Forte (strong) | Ogni azione condizionale la cui condizione diventa vera infinitamente spesso viene eseguita prima o poi. | Un lock conteso: se un processo lo rilascia e lo riacquisisce infinite volte, l'altro prima o poi lo otterrà. |
Il professor Ricci illustra la fairness con questo esempio:
/* Processo P */
p1: while flag = false
p2: n := 1 - n
/* Processo Q */
q1: flag := true
/* Variabili condivise */
integer n := 0
boolean flag := falseL'algoritmo termina? Se assumiamo solo scenari fair, sì: prima o poi q1 verrà eseguito, impostando flag = true e facendo terminare P. Lo scenario non-terminante (in cui P continua a ciclare all'infinito senza che Q venga mai eseguito) non è fair.
La fairness non è una proprietà del programma, ma della politica di scheduling della macchina concorrente. Quando analizziamo un programma, possiamo assumere diversi livelli di fairness e vedere come cambia il comportamento.
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 {
<sezione non critica>
<protocollo di entrata>
<sezione critica>
<protocollo di uscita>
<sezione non 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.
Il professor Ricci presenta i tentativi di soluzione in ordine cronologico, mostrando come ogni tentativo risolva alcuni problemi ma ne introduca altri.
/* Variabile condivisa */
integer turn := 1
/* Processo P */
loop forever {
p0: NCS
p1: await turn = 1
p2: CS
p3: turn := 2
}
/* Processo Q */
loop forever {
q0: NCS
q1: await turn = 2
q2: CS
q3: turn := 1
}Risultato: la mutua esclusione è soddisfatta (non ci sono stati con p3 ∧ q3), e non c'è deadlock. Tuttavia, la starvation non è evitata: se il processo che ha il permesso (turn) rimane indefinitamente nella sua NCS (perché la NCS non ha obbligo di progresso), l'altro processo non potrà mai entrare in CS.
boolean wantp := false, wantq := false;
/* Processo P */
loop forever {
p1: NCS
p2: wantp := true
p3: await !wantq
p4: CS
p5: wantp := false
}
/* Processo Q */
loop forever {
q1: NCS
q2: wantq := true
q3: await !wantp
q4: CS
q5: wantq := false
}Risultato: la mutua esclusione è violata. Lo stato <p3,q3,true,true> è raggiungibile: entrambi i processi possono trovarsi contemporaneamente in CS. Il problema è la non atomicità del protocollo di entrata.
boolean wantp := false, wantq := false;
/* Processo P */
loop forever {
p1: NCS
p2: wantp := true
p3: await !wantq
p4: CS
p5: wantp := false
}
/* Processo Q */
loop forever {
q1: NCS
q2: wantq := true
q3: await !wantp
q4: CS
q5: wantq := false
}Risultato: la mutua esclusione è risolta, ma si introduce un deadlock (più precisamente un livelock): entrambi i processi impostano want a true contemporaneamente e poi restano in attesa l'uno dell'altro all'await.
boolean wantp := false, wantq := false;
/* Processo P */
loop forever {
p1: NCS
p2: wantp := true
p3: while (wantq) {
p4: wantp := false
p5: wantp := true
}
p6: CS
p7: wantp := false
}Risultato: il livelock è risolto, ma rimane la possibilità di starvation nel caso di perfetto interleaving (i due processi continuano a cedersi il passo all'infinito senza mai entrare in CS).
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.
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.
Con test-and-set, la sezione critica diventa:
integer lock := 0;
/* Processo P */
loop forever {
p1: NCS
repeat {
p2: test_and_set(lock, was_locked)
p3: until was_locked = 0
p4: CS
p5: lock := 0
}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.
Per N processi, una soluzione alternativa introduce un sistema di ticket (come al banco del pane):
int num := 1
int next := 1
turn[1:n] := [0, 0, 0, ...]
/* Processo P[i] */
loop forever {
p1: NCS
p2: < turn[i] := num; num := num + 1 >
p3: await turn[i] = next
p4: CS
p5: next := next + 1
}Ogni processo prende un ticket (turn[i]) 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.
L'algoritmo del panificio ha un potenziale problema: overflow aritmetico. I valori di turn e num crescono monotonamente senza limite. In un sistema con esecuzione infinita, prima o poi si raggiungerà il massimo intero rappresentabile.
Il professor Ricci distingue nettamente tra testing e verification:
| Testing | Verification |
|---|---|
| Attività che cerca failure (rivelando fault) | Verifica se il sistema soddisfa le sue specifiche |
| "Have we built the system right?" | "Have we built the right system?" |
| Verifica che una proprietà valga per qualche scenario selezionato | Verifica che una proprietà valga per tutti gli scenari possibili |
| Rivela la presenza di errori, non la loro assenza | Richiede tecniche formali |
Il testing tradizionale non è sufficiente per i programmi concorrenti. Lo stesso input può produrre output diversi a seconda dello scenario. Non si può "debuggare" un programma concorrente nel modo normale, perché ogni esecuzione produce probabilmente uno scenario diverso. Inoltre, i test stessi possono introdurre artefatti di temporizzazione che mascherano i bug (fenomeno degli heisenbug).
Due tecniche formali principali per la verifica:
Il model checking è la tecnica più importante per verificare automaticamente la correttezza di sistemi concorrenti. La strategia si basa sull'esplorazione esaustiva dell'intero spazio degli stati del sistema:
Il grande problema del model checking è la state-space explosion: lo spazio degli stati cresce esponenzialmente con il numero di processi e azioni. Sistemi reali possono avere miliardi o trilioni di stati. Le tecniche moderne per gestirlo includono: riduzione del numero di variabili, costruzione incrementale del grafo, e simbolic model checking (che lavora con insiemi di stati anziché stati singoli).
Un invariante è una formula che deve essere invariabilmente vera in ogni punto di ogni computazione (es. [] ¬ (p3 ∧ q3)). Gli invarianti si dimostrano per induzione sugli stati:
La dimostrazione induttiva non richiede di generare tutti gli stati, ma richiede la formulazione di un invariante induttivo sufficientemente forte — un'abilità che il professor Ricci descrive come "un'arte difficile".
Per esprimere formalmente le proprietà di correttezza, serve un linguaggio formale che tenga conto dell'evoluzione temporale del sistema. La Linear Temporal Logic (LTL), introdotta da Amir Pnueli nel 1977, è la logica temporale più diffusa.
| Operatore | Notazione | Significato | Proprietà |
|---|---|---|---|
| Always (Box) | [] p / G p | p è vera in tutti gli stati futuri | Safety |
| Eventually (Diamond) | <> p / F p | p è vera in qualche stato futuro | Liveness |
| Next | O p / X p | p è vera nello stato successivo | — |
| Until | p U q | q diventa vera prima o poi, e p è vera fino a quel momento | — |
| Weak Until | p W q | Come Until, ma q non è obbligata a diventare vera. Se non lo fa, p rimane vera indefinitamente | — |
L'operatore [] (always) si usa per specificare proprietà safety. L'esempio fondamentale: la mutua esclusione nel problema della sezione critica:
[] ¬ (p3 ∧ q3)
Questa formula dice: "in ogni stato di ogni computazione, non è vero che entrambi i processi sono contemporaneamente in sezione critica".
L'operatore <> (eventually) si usa per specificare proprietà liveness. L'esempio: l'assenza di starvation:
[](p2 → <> p3)
Questa formula dice: "per tutti gli stati, se il processo P è in procinto di entrare in CS (p2), allora prima o poi vi entrerà (p3)".
| Formula | Significato |
|---|---|
[] p → p | Riflessività dell'always |
p → <> p | Riflessività dell'eventually |
¬ [] p → <> ¬ p | Dualità: se non sempre p, allora prima o poi non p |
<> [] p | Stabilizzazione: prima o poi p diventa stabilmente vera |
[] <> p | Progresso infinito: p si verifica infinite volte |
<> p = true U p | Eventualmente in termini di Until |
[] p = ¬ <> (¬ p) | Sempre in termini di Eventually |
Il professor Ricci accenna a un esempio di deduzione in logica temporale:
(<> [] p ∧ <> [] q) → <> [] (p ∧ q) è vera.
([] <> p ∧ [] <> q) → [] <> (p ∧ q) è falsa.
Questo mostra come ragionare su formule temporali richieda attenzione: la verità dipende dall'ordine degli operatori.
Il professor Ricci introduce un concetto più sottile: l'overtaking. Consideriamo uno scenario in cui un processo P cerca di entrare in CS, ma Q continua a entrare e uscire ripetutamente (1000 volte) prima che P finalmente entri. Questo non è tecnicamente starvation (prima o poi P entra), ma è chiaramente ingiusto.
La proprietà di k-bounded overtaking garantisce che, da quando P tenta di entrare in CS, un altro processo può entrare al massimo k volte prima di P.
Esempio: 1-bounded overtaking (al massimo un sorpasso):
tryp → (¬ CSq) W (CSq W ((¬ CSq) W CSp))
Questa formula usa l'operatore Weak Until (W) per descrivere: da quando P è in tryp, segue un intervallo in cui Q non è in CS, poi eventualmente un intervallo in cui Q è in CS, poi un altro intervallo in cui Q non è in CS, che termina quando P è in CS. Al massimo un intervallo continuo di Q in CS prima che P sia ammesso.
Il professor Ricci presenta alcuni strumenti concreti per la verifica formale dei programmi concorrenti.
SPIN è un model checker ampiamente utilizzato sia nella ricerca accademica che nello sviluppo industriale. È estremamente efficiente e viene usato per modellare e analizzare sistemi concorrenti e distribuiti.
PROMELA (Process Meta Language) è il linguaggio usato in SPIN per scrivere modelli di programmi concorrenti. Ha un numero limitato di costrutti, specificamente progettati per costruire modelli di sistemi concorrenti.
Il professor Ricci mostra un esempio: l'algoritmo di Dekker in PROMELA.
/* Dekker's algorithm in PROMELA (esempio dalle slide) */
bool wantp, wantq;
byte turn;
proctype P() {
do :: /* loop forever */
wantp = true;
do :: wantq ->
if :: turn == 2 ->
wantp = false;
(turn == 1); /* await */
wantp = true;
:: else -> skip
fi
:: else -> break
od;
/* critical section */
turn = 2;
wantp = false;
/* non-critical section */
od
}
proctype Q() {
do :: /* loop forever */
wantq = true;
do :: wantp ->
if :: turn == 1 ->
wantq = false;
(turn == 2); /* await */
wantq = true;
:: else -> skip
fi
:: else -> break
od;
/* critical section */
turn = 1;
wantq = false;
/* non-critical section */
od
}JPF è un model checker specializzato per la verifica di programmi Java, sviluppato dalla NASA. Funziona come una JVM speciale che esegue i programmi teoricamente lungo tutti i possibili percorsi di esecuzione (tutti gli scenari), verificando violazioni di proprietà come:
Se trova un errore, JPF riporta l'intera sequenza di esecuzione che porta all'errore. È un progetto open-source (http://javapathfinder.sourceforge.net/).
Il professor Ricci cita un caso storico: l'uso del model checking da parte di Intel dopo il Pentium Bug del 1994, e l'adozione da parte della NASA dopo l'incidente del Mars Polar Lander (1999). Questi eventi hanno dimostrato l'importanza della verifica formale nei sistemi critici.
TLA+ (Temporal Logic of Actions) è un linguaggio formale di specifica introdotto da Leslie Lamport, basato su semplice matematica discreta (teoria degli insiemi e predicati). È usato per specificare e verificare sistemi reali complessi, come ad esempio Amazon Web Services.
PlusCal (ex +CAL) è un linguaggio algoritmico basato su TLA+, pensato per scrivere algoritmi come si farebbe in un linguaggio di programmazione. Un algoritmo PlusCal viene tradotto in una specifica TLA+, che può essere verificata con il model checker TLC.
Il professor Ricci mostra l'esempio dell'algoritmo di Peterson in PlusCal:
-- algorithm Peterson {
variables flag = [i \in {0,1} |-> false], turn = 0;
process (proc \in {0,1})
a0: while (true) {
a1: flag[self] := true;
a2: turn := Not(self);
a3a: if (flag[Not(self)]) { goto a3b } else { goto cs };
a3b: if (turn = Not(self)) { goto a3a } else { goto cs };
cs: skip; \* critical section
a4: flag[self] := false;
}
}
}Le specifiche TLA+ descrivono l'insieme di tutti i possibili comportamenti legali (tracce di esecuzione) di un sistema. Possono descrivere sia le proprietà di correttezza desiderate (il "cosa") sia il progetto del sistema (il "come"). L'obiettivo è dimostrare che il progetto implementa correttamente le proprietà desiderate.
Esempio di verifica di mutua esclusione in TLA+:
MutualExclusion == (pc[0] /= "cs") \/ (pc[1] /= "cs")
theorem Spec => []MutualExclusionIl modello TLC verifica che questo invariante sia vero in tutti gli stati raggiungibili. Per l'algoritmo di Peterson, con solo 146 stati raggiungibili, la verifica è immediata. Per algoritmi più complessi, con miliardi di stati, TLC non può più verificare esaustivamente e serve una dimostrazione deduttiva.
La sincronizzazione definisce relazioni temporali tra processi ("A deve avvenire prima di B"), mentre la mutua esclusione definisce una restrizione sull'accesso a dati condivisi ("un solo processo alla volta può accedere a questa risorsa"). La mutua esclusione è una forma implicita di sincronizzazione, ma la sincronizzazione non richiede necessariamente dati condivisi. In Java, synchronized è un esempio di naming che crea confusione: denota mutua esclusione, non sincronizzazione.
Le race condition si verificano quando due o più processi accedono concorrentemente a risorse condivise e il risultato dipende dall'ordine specifico delle operazioni. Sono difficili da debuggare perché sono tempo-dipendenti: producono errori solo per specifici interleaving. Inoltre, il debugging stesso altera i tempi di esecuzione, facendo sparire il bug (fenomeno degli heisenbug). L'esempio classico è il lost update nell'incremento non atomico di una variabile condivisa.
La formula generale è (n1 + n2)! / (n1! · n2!). Per 2 processi con 3 azioni ciascuno: (3+3)! / (3! · 3!) = 720 / (6 · 6) = 20 scenari. L'esplosione combinatoria è evidente: con 6 azioni per processo si arriva a 924 scenari, con 8 a 12.820.
Le proprietà di safety richiedono che "le cose cattive non accadano mai", e sono verificate se sono vere in ogni stato di ogni computazione (es. mutua esclusione, assenza di deadlock). Sono più facili da verificare: basta uno stato che le violi per falsificarle. Le proprietà di liveness richiedono che "le cose buone prima o poi accadano", e sono verificate se in ogni computazione esiste qualche stato in cui la proprietà è vera (es. assenza di starvation, comunicazione affidabile). Sono più difficili da verificare perché richiedono di analizzare l'intera traccia di esecuzione.
I tre tipi di fairness riguardano il scheduling:
La differenza sta in quante volte la condizione deve diventare vera perché l'azione sia garantita. La strong fairness è più difficile da garantire ma è necessaria per alcuni tipi di algoritmi.
Quattro proprietà fondamentali:
Inoltre, la CS deve avere la proprietà di progress (una volta iniziata, deve terminare), mentre la NCS no.
L'overtaking descrive la situazione in cui un processo Q può entrare in sezione critica ripetutamente mentre un processo P è in attesa. Non è starvation (P prima o poi entra), ma è ingiusto. La proprietà di k-bounded overtaking limita a k il numero di volte che Q può sorpassare P. Si esprime con l'operatore Weak Until W. Esempio di 1-bounded overtaking:
tryp → (¬ CSq) W (CSq W ((¬ CSq) W CSp))
Il testing verifica che una proprietà valga per alcuni scenari selezionati; rivela la presenza di errori ma non la loro assenza. La verification usa tecniche formali (model checking o dimostrazione induttiva) per verificare che una proprietà valga per tutti gli scenari possibili. Per i programmi concorrenti, il testing tradizionale è insufficiente perché lo stesso input può dare output diversi e gli heisenbug possono sparire durante il debugging.
I principali operatori LTL sono:
[] p (Always/Box): p è vera in tutti gli stati futuri → esprime proprietà di safety.<> p (Eventually/Diamond): p è vera in qualche stato futuro → esprime proprietà di liveness.O p (Next/X): p è vera nello stato successivo.p U q (Until): q diventa vera prima o poi e p è vera fino a quel momento.p W q (Weak Until): come Until ma q non è obbligata a diventare vera.Sono strumenti di verifica formale:
Tutti risolvono il problema di verificare la correttezza di sistemi concorrenti dove il testing tradizionale è insufficiente.