synchronizedsynchronized a livello di metodo e di bloccoReentrantLock, tryLock, lockInterruptiblyIl professor Ricci apre la lezione riprendendo i concetti fondamentali che costituiscono il ponte fra la lezione precedente e il laboratorio odierno. Un programma concorrente non ha un unico comportamento deterministico: lo stesso input puo generare output diversi a seconda dell'interleaving delle istruzioni atomiche dei thread. Per questo il testing tradizionale non basta: eseguire un programma concorrente cento volte con gli stessi dati puo sempre far emergere un nuovo scenario problematico. Il model checking affronta il problema in modo radicale: esplora tutti gli scenari possibili in modo automatico.
Un programma concorrente va modellato come un insieme di possibili scenari di esecuzione (computazioni). La correttezza non si dimostra provando qualche input, ma verificando proprieta che devono valere in tutti gli scenari.
Le proprieta di correttezza si dividono in due grandi famiglie:
Proprieta di sicurezza: "le cose cattive non devono mai accadere". Una proprieta P deve essere vera in ogni stato di ogni computazione. Sono tipicamente espresse come invarianti. Esempi fondamentali:
Proprieta di vitalita: "le cose buone devono prima o poi accadere". Per ogni computazione, deve esistere qualche stato in cui P e vera. Esempi:
Fairness: una proprieta di liveness che richiede che "qualcosa di buono accada infinitamente spesso". Dipende dalla politica di scheduling. Tre livelli:
Distinguere safety da liveness e saper riconoscere esempi concreti: la mutua esclusione e una proprieta di safety; l'assenza di starvation e una proprieta di liveness. La fairness e un'ipotesi sullo scheduler che puo trasformare alcune proprieta da false a vere.
Una parte significativa del laboratorio e dedicata all'installazione di Java PathFinder (JPF), un model checker sviluppato dalla NASA per la verifica di programmi Java. JPF e una JVM speciale che esegue il programma esplorando tutti i possibili scenari di esecuzione, verificando proprieta come assenza di deadlock, eccezioni non catturate, violazioni di assert.
Il professore mostra il metodo piu agile per installare JPF: tramite Docker. I passaggi descritti nel repo del corso (lab activity 3) prevedono:
labactivity03.eclipse-temurin:11 (JDK 11 gia installato).docker compose build (cioe docker-compose build) per costruire l'immagine.docker compose up per avviare il container.Il comando docker compose build puo richiedere molto tempo (il professore parla di "un quarto d'ora"). Inoltre, durante il laboratorio emergono problemi con gradlew a causa di caratteri di controllo nascosti: se il container da errore, provare a sostituire il file gradlew usando sed per rimuovere caratteri anomali e poi renderlo eseguibile con chmod +x gradlew.
# Struttura dei comandi per JPF via Docker (dal repo del corso)
docker compose build # costruisce l'immagine
docker compose up # avvia il container
# Dentro il container:
./gradlew clean build # compila i sorgenti
# Per eseguire JPF:
./runjpf config-file.jpfIl Dockerfile di JPF parte da un'immagine base con JDK 11, copia i sorgenti di JPF, li compila e prepara l'ambiente. Il docker-compose.yml monta una directory locale (pcd-jpf) come volume, in modo che i file compilati delle esercitazioni siano accessibili al model checker.
Una volta avviato il container, per eseguire Java PathFinder su un programma serve un file di configurazione con estensione .jpf. Questi file specificano:
target: la classe Java che contiene il main da analizzare.classpath: dove trovare i bytecode compilati (tipicamente target/classes per progetti Maven).sourcepath: la directory dei sorgenti.Il professore mostra un file d'esempio test-sequential.jpf che punta alla classe pcd.lab03.jpf.TestSequential. La struttura tipica e:
# test-sequential.jpf
target = pcd.lab03.jpf.TestSequential
classpath = ${jpf}/build:/path/to/target/classes
sourcepath = /path/to/srcIl comando per lanciare JPF e: runjpf test-sequential.jpf. JPF esegue il programma esplorando sistematicamente tutti gli interleaving, partendo dallo stato iniziale e costruendo incrementalmente il grafo degli stati raggiungibili.
JPF non e un interprete Java normale: e una JVM specializzata per il model checking. Invece di eseguire un singolo percorso, esplora tutti i percorsi possibili, gestendo il nondeterminismo delle schedule dei thread. Se trova una violazione (es. un deadlock), produce l'intera traccia di esecuzione che porta all'errore.
Il professore usa l'esempio concreto dal repo labactivity03 per mostrare come si realizza una sezione critica in Java con il costrutto synchronized. Due thread, WorkerA e WorkerB, eseguono azioni cicliche. WorkerA esegue A1, A2, A3; WorkerB esegue B1, B2, B3. L'obiettivo e fare in modo che A2 e A3 (oppure A2 da sola) siano eseguite in mutua esclusione rispetto a B2 e B3.
L'idea base e: un blocco synchronized(lock) crea una regione critica: prima di entrare, il thread cerca di acquisire il lock intrinseco dell'oggetto specificato. Se un altro thread lo possiede gia, il thread si blocca (viene messo nell'entry set dell'oggetto). Quando il lock viene rilasciato (usciendo dal blocco), un thread in attesa viene risvegliato e puo acquisirlo.
Il costrutto synchronized implementa automaticamente: (1) mutua esclusione sul blocco, (2) rilascio automatico del lock anche in caso di eccezione, (3) relazione happens-before di memoria. Non e possibile dimenticare di rilasciare il lock, a differenza dei lock espliciti.
Nel codice mostrato dal professore, i worker estendono una classe base Worker che fornisce metodi di utilita come waitSome() (attesa casuale). La struttura e:
// Idea: sezione critica con blocco synchronized su un oggetto condiviso
Object lock = new Object();
// Thread A
synchronized (lock) {
// A2: azione in sezione critica
// A3: azione in sezione critica
}
// Thread B
synchronized (lock) {
// B2: azione in sezione critica
// B3: azione in sezione critica
}Il professore sottolinea che questo e il modo "piu raw, piu semplice, piu basso livello" per realizzare una sezione critica. Nella pratica si usano astrazioni di piu alto livello, ma comprendere synchronized e fondamentale.
Il cuore del laboratorio e l'esempio del contatore condiviso. Il professore presenta una classe Counter con un campo int count e un metodo inc(). Due thread incrementano lo stesso contatore. Senza sincronizzazione, l'operazione count++ non e atomica: e una sequenza read-modify-write (leggi, incrementa, scrivi).
Nel codice del professore, questo si manifesta come lost update: due thread possono leggere lo stesso valore, incrementarlo ciascuno nella propria variabile locale, e riscriverlo, perdendo uno degli incrementi. Con 100.000 incrementi per thread (totale atteso 200.000), il risultato effettivo sara minore, e diverso a ogni esecuzione.
count++ non e atomico. A livello macchina corrisponde a: (1) carica count in un registro, (2) incrementa il registro, (3) scrivi il registro in count. Un interleaving fra (1) e (3) di due thread produce risultati errati. synchronized rende l'intera sequenza atomica rispetto agli altri thread sincronizzati sullo stesso lock.
Il professore simula mentalmente lo scenario: se entrambi i thread leggono count=5 prima che uno dei due lo abbia scritto, entrambi scriveranno 6 invece di 7. Ecco un simulatore interattivo per visualizzare il fenomeno:
Il professore introduce la definizione di thread safety tratta dal testo "Java Concurrency in Practice": una classe e thread-safe se puo essere usata correttamente in qualsiasi contesto, sequenziale o concorrente, senza che chi la usa debba preoccuparsi di sincronizzazione aggiuntiva. Le classi di java.util (es. ArrayList) non sono thread-safe perche la sincronizzazione ha un costo e sarebbe sprecata in contesti sequenziali.
La scelta di non rendere thread-safe le classi della libreria standard per default e una decisione progettuale: il programmatore sceglie quando serve e paga solo quel costo. In contesti concorrenti si usano wrapper sincronizzati (Collections.synchronizedList(...)) o strutture specializzate (ConcurrentHashMap).
Il professore mostra un'evoluzione: invece di un blocco synchronized esplicito, si puo dichiarare l'intero metodo come synchronized. In Java, scrivere:
public synchronized void inc() {
count++;
}equivale a:
public void inc() {
synchronized (this) {
count++;
}
}Il lock viene acquisito sull'oggetto stesso (this) prima di eseguire il corpo del metodo e rilasciato automaticamente all'uscita. Questo pattern si avvicina all'idioma del monitor: una classe i cui metodi pubblici sono eseguiti in mutua esclusione per costruzione.
public class Counter {
private int count = 0;
public void inc() { count++; }
public int get() { return count; }
}
// Uso concorrente: PERICOLOSO!
// count++ non atomico -> lost updatepublic class SafeCounter {
private int count = 0;
public synchronized void inc() { count++; }
public synchronized int get() { return count; }
}
// Uso concorrente: SICURO
// synchronized rende inc() e get() atomiciIl professore nota che get() deve essere synchronized anch'esso: altrimenti un thread potrebbe leggere un valore incoerente mentre un altro sta eseguendo inc() (anche se count++ e su una variabile int, la visibilita di memoria non e garantita senza sincronizzazione).
Oltre a synchronized, Java offre lock espliciti nel pacchetto java.util.concurrent.locks. Il professore presenta ReentrantLock e le sue varianti, sottolineando un aspetto critico: il lock va rilasciato esplicitamente, e per questo il pattern canonico prevede try/finally.
import java.util.concurrent.locks.ReentrantLock;
ReentrantLock lock = new ReentrantLock();
public void m() {
lock.lock(); // acquisisce il lock (si blocca se necessario)
try {
// sezione critica
} finally {
lock.unlock(); // rilasciato SEMPRE, anche in caso di eccezione
}
}Il professore elenca le varianti offerte da ReentrantLock:
| Metodo | Comportamento |
|---|---|
lock() | Acquisisce il lock, bloccandosi se necessario. Ignora gli interrupt. |
lockInterruptibly() | Come lock() ma risponde all'interrupt: se il thread viene interrotto mentre aspetta, lancia InterruptedException e si sblocca. |
tryLock() | Tenta di acquisire il lock senza bloccarsi: restituisce subito true (lock preso) o false (lock occupato). |
tryLock(time, unit) | Tenta di acquisire il lock aspettando al piu il tempo specificato; restituisce false se scaduto. |
A differenza di synchronized, con ReentrantLock e possibile dimenticare di rilasciare il lock (se si omette il finally). Un'eccezione nel corpo del blocco lascerebbe il lock perpetuamente acquisito, bloccando tutti gli altri thread. Il pattern try/finally e obbligatorio.
Il professore nota che Java offre anche una sintassi piu moderna con try(var lock = ...) (ARM per lock, introdotta in versioni recenti), ma il pattern classico rimane il piu diffuso.
Il professore introduce un esempio piu complesso che illustra il pattern check-and-act e le sue insidie. Un BoundedCounter e un contatore con soglie minime e massime: se si tenta di incrementare oltre il massimo, lancia OverflowException; se si tenta di decrementare sotto il minimo, lancia UnderflowException.
Il problema emerge quando due worker operano sullo stesso contatore:
Il pattern check-and-act consiste nel controllare una condizione e poi agire di conseguenza. In un contesto concorrente, questo pattern e intrinsecamente non atomico: tra la lettura della condizione e l'azione, un altro thread puo modificare lo stato, invalidando la condizione appena letta.
Il pattern check-and-act e una delle cause piu comuni di race condition. La soluzione e rendere atomico l'intero blocco check+act usando synchronized o un lock. Il BoundedCounter mostra anche che bisogna sincronizzare tutti i metodi pubblici, non solo quelli che modificano lo stato.
Il professore dedica una parte della lezione alle proprieta di liveness dei thread, riprendendo materiale da "Java Concurrency in Practice". Anche se la sezione critica garantisce mutua esclusione, non e sufficiente: il programma deve anche progressare. Due problemi classici:
Deadlock (stallo): due o piu thread aspettano ciascuno un lock che l'altro possiede, e nessuno puo proseguire. Le condizioni necessarie (Coffman, 1971) sono quattro e devono valere tutte contemporaneamente:
Starvation (inedia): un thread e pronto per eseguire ma non ottiene mai la CPU o il lock che richiede, perche altri thread vengono sempre preferiti dallo scheduler. A differenza del deadlock, il thread non e bloccato permanentemente, ma non fa progressi per un periodo indefinito.
Livelock: i thread non sono bloccati ma continuano a eseguire azioni che non portano a progresso. Un esempio tipico: due thread che rilevano un conflitto e "cedono" il passo all'altro, finendo per oscillare senza mai procedere. Il professore lo menziona a proposito del terzo tentativo di soluzione della sezione critica.
Il professore sottolinea che la JVM non ha un meccanismo automatico di rilevamento o recupero dai deadlock: "if threads deadlock, that's all, folks!" — l'unica opzione e arrestare l'applicazione. Il supporto si limita a strumenti di diagnostica post-mortem (stack trace, thread dump).
Il professore mostra il deadlock nella sua forma piu semplice: deadly embrace (abbraccio mortale). Due thread, A e B, e due lock, L1 e L2:
La soluzione strutturale al deadlock segue una regola semplice ma potente: acquisire i lock sempre nello stesso ordine globale. Se tutti i thread acquisiscono L1 prima di L2, il ciclo di attesa non puo formarsi, perche non ci puo essere un thread che tiene L2 e richiede L1 mentre un altro tiene L1 e richiede L2.
Le condizioni di Coffman sono necessarie ma non sufficienti: se anche tutte valgono, un deadlock potrebbe non verificarsi (serve il giusto interleaving). Per evitarli: (1) acquisire lock in ordine globale, (2) usare tryLock() con timeout, (3) ridurre il numero di lock, (4) usare astrazioni di piu alto livello.
Il professore torna al framework teorico del modulo 1.2, mostrando come si costruiscono modelli dell'esecuzione concorrente. L'idea fondamentale: ogni processo viene modellato come una sequenza di azioni atomiche. L'esecuzione concorrente e una sequenza ottenuta interleaveando arbitrariamente le azioni dei processi, sotto l'ipotesi di speed independence (indipendenza dalla velocita).
Un esempio semplice: due processi P e Q, ciascuno con una singola assegnazione:
P: Q:
integer k1 := 1 integer k2 := 2
p1: n := k1 q1: n := k2
integer n := 0I due scenari possibili sono: p1,q1 (n finale = 2) oppure q1,p1 (n finale = 1). Il valore finale di n dipende dall'ordine di esecuzione.
Il diagramma di stato rappresenta formalmente l'esecuzione: ogni stato e una tupla che contiene il control pointer di ogni processo e i valori di tutte le variabili (globali e locali). Una transizione fra stati corrisponde all'esecuzione di un'istruzione atomica. Lo stato e definito come:
<p_i, q_j, n, k1, k2>dove p_i e il control pointer di P, q_j quello di Q, e gli altri sono i valori delle variabili. Dal punto di partenza, si costruiscono incrementalmente tutti gli stati raggiungibili. Il grafo risultante ha 5 stati e 2 scenari per l'esempio sopra.
Il modello a interleaving arbitrario e una potente astrazione: ignora il tempo e si concentra sull'ordine parziale delle azioni e sulla loro atomicita. Questo rende i programmi concorrenti trattabili con l'analisi formale, indipendentemente dalla velocita dei processori o dal carico di sistema.
Il numero di scenari possibili cresce in modo esplosivo all'aumentare del numero di processi e di azioni atomiche. Il professore mostra una tabella che lo dimostra in modo concreto:
| Azioni per processo | 2 processi | 3 processi |
|---|---|---|
| 1 | 2 | 6 |
| 2 | 6 | 90 |
| 3 | 20 | 1.680 |
| 4 | 70 | 34.650 |
| 5 | 252 | — |
| 6 | 924 | — |
| 7 | 3.432 | — |
| 8 | 12.820 | — |
La formula generale per m processi ciascuno con n azioni atomiche e data dal coefficiente multinomiale: (m * n)! / (n!)^m. Questo spiega il fenomeno noto come state-space explosion: anche con pochi processi e poche azioni, il numero di scenari da esplorare cresce vertiginosamente, rendendo necessario l'uso di tecniche di riduzione (come l'esplorazione incrementale o la riduzione dell'ordine parziale).
Il professore fa notare che questa crescita e rilevante quando le azioni non hanno dipendenze fra loro. Se ci sono dipendenze (es. un processo deve attendere il risultato di un altro), il numero di scenari diminuisce perche alcuni interleaving sono invalidati dalle condizioni di sincronizzazione.
Il professore approfondisce il concetto di atomicita, che non riguarda solo le singole operazioni ma anche le strutture dati. Un oggetto dati si dice atomico se puo trovarsi in un numero finito di stati uguale al numero di valori che puo assumere, e le operazioni cambiano atomicamente quello stato. I tipi primitivi di Java sono generalmente atomici (con eccezioni, come double).
Ma i tipi astratti di dati (classi, struct) composti da piu oggetti semplici sono tipicamente non atomici. Per questi si possono identificare due tipi di stato:
La corrispondenza fra stati interni ed esterni e parziale: esistono stati interni che non hanno un corrispondente esterno. Gli stati interni che hanno un corrispondente esterno sono detti consistenti.
Il problema: quando si esegue un'operazione su un ADT non atomico, si possono attraversare stati interni non consistenti. In un contesto sequenziale questo non e un problema (grazie all'information hiding). In un contesto concorrente, invece, un thread potrebbe osservare l'oggetto in uno stato inconsistente mentre un altro thread vi sta operando.
Il non atomiche delle strutture dati e la ragione profonda per cui serve la sincronizzazione. Non basta rendere atomiche le singole operazioni: bisogna garantire che nessun thread veda mai l'oggetto in uno stato intermedio inconsistente. synchronized, i lock e i monitor servono proprio a questo.
Il professore mostra l'esempio del contatore a livello macchina per illustrare come anche un semplice count++ sia in realta una sequenza di 3-4 istruzioni macchina (su stack machine: push n, push #1, add, pop n), e come l'interleaving fra queste istruzioni produca risultati errati.
flowchart LR
subgraph P["Processo P"]
direction TB
p1["p1: push n"] --> p2["p2: push #1"]
p2 --> p3["p3: add"]
p3 --> p4["p4: pop n"]
end
subgraph Q["Processo Q"]
direction TB
q1["q1: push n"] --> q2["q2: push #1"]
q2 --> q3["q3: add"]
q3 --> q4["q4: pop n"]
end
Se l'interleaving e p1, q1, p2, p3, p4, q2, q3, q4, entrambi i processi leggono n=0 e scrivono n=1, producendo il lost update.
Il professore introduce la Logica Temporale Lineare (LTL), formalizzata da Amir Pnueli nel 1977, come linguaggio per esprimere proprieta di correttezza dei programmi concorrenti. LTL estende la logica proposizionale con operatori temporali che permettono di ragionare sull'evoluzione degli stati nel tempo.
| Operatore | Notazione | Significato |
|---|---|---|
| Always (box) | [] P o G P | P e vera in tutti gli stati futuri (safety) |
| Eventually (diamond) | <> P o F P | P diventa vera prima o poi in qualche stato futuro (liveness) |
| Next | O P o X P | P e vera nel prossimo stato |
| Until | P U Q | P e vera fino a quando Q diventa vera (inclusivo) |
| Weak Until | P W Q | Come Until, ma Q puo anche non diventare mai vera |
Il professore mostra come si esprimono le proprieta di correttezza in LTL:
[] !(p3 && q3) — mai entrambi in CS.[](p2 -> <> p3) — ogni volta che P vuole entrare in CS, prima o poi ci riesce.Saper scrivere in LTL: mutua esclusione []!(p3&&q3), progress/starvation [](p2-><>p3), e capire la differenza fra []<>P (infinitamente spesso) e <>[]P (stabilizzazione). Duality: ![]P = <>!P.
Il professore menziona altri strumenti di verifica formale, inquadrandoli nel panorama piu ampio del model checking:
SPIN e uno dei model checker piu utilizzati, sia in ambito accademico che industriale. PROMELA (Process Meta-Language) e il linguaggio di modellazione per SPIN. Permette di descrivere sistemi concorrenti con un insieme limitato di costrutti, appositamente progettati per costruire modelli astratti. SPIN puo verificare proprieta LTL sullo spazio degli stati del modello PROMELA.
Il professore mostra un esempio di Dekker in PROMELA, dimostrando come si modella un algoritmo di mutua esclusione e lo si verifica con SPIN.
Java PathFinder (JPF) e specializzato per Java: verifica il codice Java reale, non un modello astratto. Funziona come una JVM speciale che esegue il programma lungo tutti i possibili percorsi di esecuzione. Piu lento di una JVM normale, ma in compenso puo trovare bug che sfuggirebbero a qualsiasi test. NASA lo usa per software mission-critical. Il professore passa al laboratorio proprio per far provare JPF agli studenti.
TLA+ (Temporal Logic of Actions), introdotto da Leslie Lamport, e un linguaggio di specifica formale basato su logica temporale e insiemistica. Usato da Amazon Web Services per verificare i propri sistemi distribuiti (es. meccanismi di consenso, protocolli di replicazione). PlusCal e un linguaggio algoritmico basato su TLA+ che viene tradotto automaticamente in specifiche TLA+ verificabili con il model checker TLC.
Il professore mostra un esempio di Peterson in PlusCal.
La scelta fra SPIN/PROMELA, JPF e TLA+ dipende dal contesto: SPIN richiede di modellare il sistema in PROMELA (astrazione), JPF lavora direttamente sul codice Java (nessuna astrazione, ma limitato a Java), TLA+ e per specifiche di piu alto livello (protocolli, architetture).
Il professore approfondisce come LTL esprima formalmente le proprieta di correttezza, mostrando esempi concreti tratti dal problema della sezione critica. Le proposizioni atomich sono di due tipi: (1) valori di variabili booleane (es. wantp e vera se wantp == true) e (2) label dei control pointer (es. p3 e vera se il control pointer di P e su p3).
L'operatore [] (box/always) specifica che una proprieta deve valere in tutti gli stati di tutte le computazioni. Questo e lo strumento per esprimere proprieta di safety. L'esempio centrale: la mutua esclusione per la sezione critica si esprime come:
[] !(p3 && q3) // p3 e q3 = etichette dell'inizio della CSQuesta formula e vera se non esiste alcuno stato accessibile in cui entrambi i processi si trovano contemporaneamente all'inizio della loro sezione critica. E una invariante: deve valere in ogni stato.
L'operatore <> (diamond/eventually) specifica che una proprieta deve diventare vera in qualche stato futuro. Per la liveness (assenza di starvation):
[](p2 -> <> p3) // ogni volta che P e in p2, prima o poi arriva a p3cioe: ogni volta che un processo vuole entrare nella sezione critica (p2), prima o poi ci riesce (p3). L'operatore [] esterno serve per dire che questo vale per ogni occorrenza della richiesta.
Il professore spiega che la semplice proprieta di liveness puo essere debole: un processo potrebbe essere superato infinite volte eppure "prima o poi" entrare (magari dopo 1000 superamenti). Per questo serve il concetto di k-bounded overtaking: dal momento in cui P tenta di entrare, Q puo entrare al massimo k volte prima di P. Con l'operatore Weak Until (W):
tryp -> (!CSq) W (CSq W ((!CSq) W CSp)) // per 1-bounded overtakingQuesta formula dice: dopo tryp, segue un intervallo in cui Q non e in CS, poi eventualmente uno in cui Q e in CS, poi Q non e piu in CS, e solo allora P puo entrare. Q puo entrare al massimo una volta.
Il bounded overtaking e un classico esempio di come LTL possa esprimere proprieta piu raffinate della semplice liveness. Studiare la formula con W annidati e saperla spiegare. Notare che l'operatore W (weak until) e fondamentale perche non richiede che la condizione di "uscita" si verifichi necessariamente.
Il professore conclude la parte teorica mostrando come JPF analizza un programma Java. L'esempio e un programma sequenziale semplice (test-sequential) che serve per verificare il setup. Ma l'obiettivo a regime e usare JPF per verificare programmi concorrenti, come quelli della sezione critica.
JPF esplora il grafo degli stati del programma in esecuzione. Per ogni punto di scelta (scheduling point), prova tutte le possibili selezioni del thread da eseguire successivamente. Se durante l'esplorazione trova una violazione (deadlock, eccezione non catturata, asserzione fallita, o violazione di una proprieta LTL specificata), si ferma e produce un controesempio: la sequenza di stati che porta dall'inizio alla violazione.
Il model checking e complementare al testing. Il testing verifica scenari specifici e puo trovare bug, ma non puo dimostrare l'assenza di errori. Il model checking, se puo esplorare l'intero spazio degli stati, fornisce una garanzia formale di correttezza. In pratica, lo spazio degli stati e spesso troppo grande, ma JPF usa tecniche di riduzione (partial order reduction, state matching) per renderlo fattibile.
Il professore anticipa che nei prossimi laboratori si usera JPF per verificare i programmi scritti durante il corso, compresi quelli con synchronized, lock espliciti, e i vari algoritmi di sincronizzazione discussi nella parte di teoria.
I programmi da verificare con JPF devono essere compilati con JDK 11 (o versione supportata). Il professore mostra che nel pom.xml del progetto Maven si specifica javac 11 come target, per generare bytecode compatibile. I file .class finiscono in target/classes (non in build), e questo va specificato nel classpath del file .jpf.
Il pattern check-and-act consiste nel controllare una condizione (es. "if (counter > 0)") e poi eseguire un'azione che dipende da quella condizione (es. "counter--"). In ambito concorrente, il check e l'act sono due operazioni distinte: tra la lettura della condizione e l'esecuzione dell'azione, un altro thread puo modificare lo stato, invalidando la condizione. La soluzione e rendere atomico l'intero blocco con synchronized o un lock.
(1) Mutua esclusione: le risorse non sono condivisibili. (2) Hold and wait: un processo tiene una risorsa mentre ne richiede un'altra. (3) No preemption: le risorse non possono essere sequestrate. (4) Attesa circolare: esiste un ciclo di processi che attendono risorse l'uno dall'altro. Tutte e quattro devono valere simultaneamente perche si verifichi un deadlock.
synchronized e ReentrantLock?synchronized e un costrutto intrinseco del linguaggio: il lock viene acquisito e rilasciato automaticamente (anche in caso di eccezioni), e non e possibile dimenticarsi di rilasciarlo. ReentrantLock e un lock esplicito che richiede uno sbLocco esplicito (pattern try/finally obbligatorio). Offre funzionalita aggiuntive: lockInterruptibly() (risponde agli interrupt), tryLock() (non bloccante), tryLock(timeout) (con time-out), e la possibilita di creare lock equi (fair).
Mutua esclusione: [] !(p3 && q3) (mai entrambi in CS). Assenza di starvation (progress): [](p2 -> <> p3) (ogni volta che P vuole entrare in CS, prima o poi ci riesce). La prima e una proprieta di safety (e vera in ogni stato), la seconda di liveness (richiede uno stato futuro in cui la proprieta diventa vera).
JPF e una JVM specializzata per il model checking: invece di eseguire il programma lungo un singolo percorso (come una JVM normale), esplora tutti i possibili percorsi di esecuzione generati dai diversi interleaving dei thread. Per ogni percorso, verifica le proprieta specificate (assenza di deadlock, eccezioni non catturate, invarianti). Se trova una violazione, produce la traccia completa che vi conduce. JPF e piu lento di una JVM normale perche esplora esponenzialmente piu percorsi.
Per m processi ciascuno con n azioni atomiche, il numero di scenari e dato dalla formula (m*n)! / (n!)^m (coefficiente multinomiale). Ad esempio, 2 processi con 4 azioni generano 70 scenari; 3 processi con 4 azioni generano 34.650 scenari. Questa crescita esplosiva e nota come state-space explosion ed e la ragione per cui servono tecniche avanzate (riduzione dell'ordine parziale, hashing degli stati, model checking simbolico) per rendere la verifica fattibile.
Una classe e thread-safe se puo essere usata correttamente in qualsiasi contesto, sequenziale o concorrente, senza che chi la usa debba aggiungere sincronizzazione. La correttezza e garantita internamente dall'implementazione. Le classi della libreria standard Java (es. ArrayList) non sono thread-safe per scelta progettuale: la sincronizzazione ha un costo, e in contesti puramente sequenziali sarebbe sprecata. Classi con stato immutabile (nessun metodo modifica lo stato) sono thread-safe per definizione.
Weak fairness: un'azione condizionale la cui condizione diventa e rimane vera viene prima o poi eseguita. Strong fairness: un'azione condizionale la cui condizione diventa vera infinitamente spesso (anche se non rimane vera) viene prima o poi eseguita. La strong fairness e piu difficile da garantire per lo scheduler. Entrambe presuppongono la fairness incondizionata (ogni azione non condizionale viene prima o poi eseguita).