La correttezza dei programmi concorrenti — anche di quelli potenzialmente non terminanti — si definisce in termini di proprietà delle computazioni: condizioni che devono essere verificate in ogni possibile scenario di esecuzione, non solo in alcuni. La correttezza non può essere verificata con il testing tradizionale: lo stesso input può dare output diversi a seconda dello scenario.
Verifica vs Testing:
| Attività | Descrizione |
|---|---|
| Testing | Ricerca di failure rivelando fault. Verifica una proprietà per alcuni scenari selezionati. Rivela la presenza di errori, non la loro assenza. |
| Verification | Verifica che una proprietà valga per tutti gli scenari possibili. Richiede tecniche formali. |
| Validation | Verifica che il sistema soddisfi le aspettative del cliente («abbiamo costruito il sistema giusto?»). |
Il testing tradizionale è insufficiente per programmi concorrenti: ogni esecuzione segue uno scenario diverso, e i bug concorrenti sono spesso heisenbug (scompaiono in debug). Servono metodi formali basati su modelli astratti.
Il professore distingue due categorie fondamentali di proprietà.
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, anche detta progress): "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.
La fairness è una proprietà di liveness che richiede che qualcosa di buono accada infinite volte. Esistono tre livelli, in ordine crescente di forza: unconditional, weak e strong fairness — approfonditi nella sezione 3.
In sintesi: la verifica delle proprietà di safety è più semplice perché basta trovare un singolo stato che violi la proprietà per concludere la non-correttezza; la verifica delle proprietà di liveness richiede invece di analizzare tutti i possibili scenari per intero, non solo gli stati singoli.
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.
[] !bad); liveness = "qualcosa di buono accade prima o poi" (<> good). La fairness è un tipo specifico di liveness che richiede che []<> eligible.
La fairness (equità) è 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. In pratica, riguarda la politica di scheduling: un'azione che può essere eseguita, prima o poi verrà effettivamente eseguita.
La fairness è un requisito sullo scheduling: a seconda della politica di scheduling, i programmi possono comportarsi diversamente. Si distinguono tre livelli, cumulativi (weak e strong includono la unconditional fairness):
| Tipo | Definizione | Esempi |
|---|---|---|
| Incondizionata (unconditional) | Ogni azione atomica non condizionale che è eligible (idonea) viene eseguita prima o poi. | Un'istruzione print("ok") in un loop sarà eseguita prima o poi; n := n + 1 (nessuna guardia). |
| 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; await turn = 1 con turn che diventa e resta 1. |
| 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à; await turn = 1 con turn che diventa 1 periodicamente. |
Uno scenario è unconditionally fair se, in ogni stato, un'istruzione che è continuamente abilitata appare prima o poi nello scenario. 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 permettiamo scenari non-fair, il processo P può loopare all'infinito senza che Q esegua mai q1, e l'algoritmo non termina: P continua a ciclare senza mai vedere flag = true. Se assumiamo solo scenari fair, invece, prima o poi q1 verrà eseguito, impostando flag = true e facendo terminare P. Lo scenario non-terminante non è fair: un algoritmo può quindi terminare o meno a seconda che si assumano scenari fair o unfair.
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.
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 (Premio Turing), è la logica temporale più diffusa: aggiunge operatori temporali alla logica proposizionale per esprimere proprietà che devono valere in tutti gli scenari possibili.
Le proposizioni atomiche sono di due tipi: (1) valori di variabili booleane (es. wantp è vera se wantp == true) e (2) label dei control pointer (es. p3 è vera se il control pointer del processo P è su p3).
| Operatore | Notazione | Significato | Proprietà |
|---|---|---|---|
| Always (Box) | [] p / □ p / G p | p è vera in tutti gli stati futuri | Safety |
| Eventually (Diamond) | <> p / ◇ p / F p | p è vera in qualche stato futuro | Liveness |
| Next | O p / ○ 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 | — |
| 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 → [] ¬ p | Dualità (inversa): se p non diventa mai vera, allora sempre non-p |
<> [] p | Stabilizzazione: prima o poi p diventa stabilmente vera (da un certo punto in poi p è sempre vera) |
[] <> p | Progresso infinito: p si verifica infinite volte (sempre eventualmente vero) |
<> 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: p e q possono essere veri in infiniti stati, ma mai contemporaneamente. È un errore comune assumere il contrario.
Questo mostra come ragionare su formule temporali richieda attenzione: la verità dipende dall'ordine degli operatori.
L'operatore [] (always) si usa per specificare proprietà safety: specifica che una proprietà deve valere in tutti gli stati di tutte le computazioni. L'esempio fondamentale è la mutua esclusione nel problema della sezione critica: lo stato "cattivo" è quando entrambi i processi sono in CS. Usiamo [] per dire che non deve mai accadere:
[] ¬ (p3 ∧ q3)
Questa formula dice: "in ogni stato di ogni computazione, non è vero che entrambi i processi sono contemporaneamente in sezione critica" (p3 e q3 sono le etichette dell'inizio della CS). La formula è vera se non esiste alcuno stato accessibile in cui entrambi i processi si trovano contemporaneamente all'inizio della loro sezione critica: è una invariante, deve valere in ogni stato.
In generale: []p dove p = !q e q descrive lo stato "cattivo".
L'operatore <> (eventually) si usa per specificare proprietà liveness: una proprietà deve diventare vera in qualche stato futuro. L'esempio è la progress property (assenza di starvation): se un processo è in attesa (stato p2), deve prima o poi entrare in CS (p3):
[](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)". L'operatore [] esterno serve per dire che questo vale per ogni occorrenza della richiesta.
Attenzione all'implicazione: P → Q equivale a !P ∨ Q. Se la premessa è falsa (P non è in p2), l'implicazione è vera a prescindere da Q. E la formula cattura correttamente che non ci interessa la starvation se P non ha mai richiesto di entrare.
La proprietà di mutua esclusione per il problema della sezione critica si scrive in LTL come [] ¬(p3 ∧ q3). La proprietà di progress (assenza di starvation) si scrive [](p2 → <> p3) — se un processo è in attesa, prima o poi entrerà nella sezione critica.
Il professor Ricci introduce un concetto più sottile: l'overtaking (sorpasso). La libertà da starvation può essere una proprietà debole: 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. È vero che <> CSp — questo non è tecnicamente starvation, prima o poi P entra e la proprietà è soddisfatta — ma il comportamento è chiaramente ingiusto e insoddisfacente.
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), espresso con l'operatore Weak Until:
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: Q può entrare al massimo una volta.
tryp), Q può occupare la sezione critica per al massimo un intervallo continuo prima che P entri (CSp).Il bounded overtaking è un classico esempio di come LTL possa esprimere proprietà più raffinate della semplice liveness. Studiare la formula con W annidati e saperla spiegare. Notare che l'operatore W (weak until) è fondamentale perché non richiede che la condizione di "uscita" si verifichi necessariamente.