Verifica formale e model checking

1. Testing, verifica e validazione

Il professor Ricci distingue nettamente tra testing e verification:

Fault, error, failure: un fault e la manifestazione di un errore (un'azione umana che produce un risultato incorretto). Un failure si verifica quando un fault viene incontrato durante l'esecuzione. Un failure puo essere causato da molti fault, e un fault puo causare molti failure.

Da qui la necessità di due tecniche formali principali per la verifica, che occupano il resto del capitolo: il model checking (esplorazione esaustiva dello spazio degli stati) e la dimostrazione induttiva di invarianti.

2. Proprietà di correttezza: safety, liveness, fairness

Il professor Ricci apre la lezione di laboratorio riprendendo i concetti fondamentali che costituiscono il ponte fra la teoria e la pratica della verifica. 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.

Il testing rivela la presenza di errori, non la loro assenza. Nei programmi concorrenti, lo stesso input puo dare output diversi in scenari diversi.

— Prof. Ricci

Safety e Liveness

Le proprieta di correttezza si dividono in due grandi famiglie:

La lezione del 20 marzo riassume le stesse tre famiglie in forma tabellare:

3. La logica temporale lineare (LTL)

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: proprieta che devono valere in tutti gli stati di tutte le computazioni.

Operatori temporali di base

La lezione del 13 marzo riprende gli stessi operatori in forma discorsiva, utile per fissarne la semantica:

• [] p (box, always, G p): p e vera in tutti gli stati futuri. Specifica proprieta di safety.
• <> p (diamond, eventually, F p): p diventa vera in qualche stato futuro. Specifica proprieta di liveness.
• O p (next, X p): p vale nel prossimo stato.
• p U q (until): prima o poi q diventa vera, e fino a quel momento p e sempre vera.
• p W q (weak until): come U, ma q non e obbligato a diventare vero. Se non lo diventa, p deve rimanere vero indefinitamente.

Specifica di proprieta

Il professore mostra come si esprimono le proprieta di correttezza in LTL:

• 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.
• Bounded overtaking (k-scavalchi): specifica che un processo puo essere superato al massimo k volte prima di entrare in CS. Si esprime con operatori W annidati.

4. Model checking

Il model checking e la tecnica piu importante per la verifica automatica di proprieta di correttezza nei sistemi concorrenti. La strategia: esplorare esaustivamente l'intero spazio degli stati del sistema e verificare se certe proprieta (espresse come formule LTL) sono soddisfatte.

• Se il sistema soddisfa la proprieta, il model checker produce una conferma.
• Altrimenti, produce una traccia (controesempio) che mostra la sequenza di stati che viola la proprieta — utilissimo per identificare bug, non solo per dimostrare correttezza.

Applicazioni

Il model checking non si applica solo al software, ma anche all'hardware (Intel lo adotto dopo il Pentium Bug del 1994) e ai sistemi mission-critical (NASA dopo il Mars Polar Lander incident del 1999). Altre applicazioni citate: Amazon Web Services per i propri sistemi cloud.

/* Dekker in PROMELA — struttura */
byte turn;
bool wantp, wantq;

active proctype P() {
  do :: skip -> /* NCS */
    wantp = true;
    do :: wantq ->
       turn = 1;
       wantp = false;
       (turn == 1);
       wantp = true;
    :: else -> break od;
    /* CS */
    wantp = false
  od
}

State-space explosion

Il grande problema del model checking e la dimensione dello spazio degli stati, che cresce esponenzialmente con il numero di processi e azioni: sistemi reali possono avere miliardi o trilioni di stati. Tecniche allo stato dell'arte includono:

• Riduzione manuale: semplificare il modello eliminando variabili o istruzioni irrilevanti per la proprieta da verificare (variabili modellabili con un numero limitato di valori)
• Costruzione incrementale: esplorare solo gli stati raggiungibili, fermandosi se si trova uno stato falsificante
• Model checking simbolico: lavorare con insiemi di stati descritti in modo intensivo (BDD) anziché estensivo

5. Dimostrazione induttiva di invarianti

Un approccio alternativo al model checking, puramente matematico: invece di esplorare tutti gli stati, si dimostra che una proprieta (invariante) — una formula che deve essere invariabilmente vera in ogni punto di ogni computazione, come [] ¬(p3 ∧ q3) — vale per induzione sugli stati di tutte le computazioni:

1. Base case: l'invariante e vero nello stato iniziale
2. Passo induttivo: assumendo che l'invariante valga in uno stato S (ipotesi induttiva), si dimostra che vale in tutti i possibili stati successivi a S

La dimostrazione induttiva non richiede di generare tutti gli stati, ma richiede la formulazione di un invariante induttivo sufficientemente forte — un'abilita che il professor Ricci descrive come "un'arte difficile".

Questo approccio e supportato da sistemi deduttivi automatici (theorem provers) e da linguaggi di specifica formale come TLA+ di Leslie Lamport, usato ad esempio da Amazon Web Services per verificare sistemi reali. TLA+ permette di specificare sia le proprieta di correttezza (il "cosa") sia il progetto del sistema (il "come"), e supporta model checking tramite TLC. Include PlusCal, un linguaggio algoritmico che viene tradotto automaticamente in TLA+.

Il professore conclude che capire il senso di queste cose — perche un algoritmo funziona, perche e stato progettato in un certo modo — e essenziale per un ingegnere, ancora di piu in un'epoca in cui l'AI genera codice. Saper riconoscere se la soluzione proposta da uno strumento automatico e corretta o meno e una competenza fondamentale.

6. Gli strumenti: SPIN/PROMELA, JPF e TLA+/PlusCal

Il professor Ricci presenta alcuni strumenti concreti per la verifica formale dei programmi concorrenti, inquadrandoli nel panorama piu ampio del model checking.

SPIN e PROMELA

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. SPIN e stato usato dalla NASA (dopo l'incidente del Mars Polar Lander del 1999) e da Intel (dopo il bug Pentium del 1994).

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
}

Nella lezione del 16 marzo il professore mostra una variante con active proctype ed etichette esplicite:

// Esempio: algoritmo di Dekker in Promela
bool wantp = false, wantq = false;
byte turn = 1;

active proctype P() {
    do :: true ->
        wantp = true;
        do :: !wantq -> break;
           :: else ->
              if :: turn == 1 -> skip;
                 :: else -> wantp = false;
                            (turn == 1);
                            wantp = true;
              fi;
        od;
        CS: skip;   // sezione critica
        turn = 2;
        wantp = false;
    od
}

Java Path Finder (JPF)

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:

• Deadlock
• Eccezioni non catturate
• Violazioni di proprietà definite dall'utente

Se trova un errore, JPF riporta l'intera sequenza di esecuzione che porta all'errore. È un progetto open-source (http://javapathfinder.sourceforge.net/).

TLA+ e PlusCal

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 => []MutualExclusion

Il 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.

Lo stato dell'arte nella verifica, riassunto dal professore: per sistemi piccoli, SPIN o JPF possono esplorare esaustivamente tutti gli stati. Per sistemi grandi si usa il model checking simbolico o la dimostrazione induttiva di invarianti. TLA+ combina entrambi gli approcci.

7. Java PathFinder: installazione con Docker

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:

1. Installare Docker sui propri computer (gia disponibile nei laboratori).
2. Clonare/aggiornare il repository del corso con il progetto Maven labactivity03.
3. Scaricare il Dockerfile fornito dal team di JPF, che si basa su eclipse-temurin:11 (JDK 11 gia installato).
4. Configurare il docker-compose.yml per costruire l'immagine.
5. Eseguire docker compose build (cioe docker-compose build) per costruire l'immagine.
6. Eseguire docker compose up per avviare il container.

# 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.jpf

8. JPF: configurazione e primo test

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.
• Opzioni di verifica aggiuntive (quali proprieta controllare).

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/src

Il 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.

9. JPF in azione: model checking di un programma Java

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 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.

10. Perché la verifica conta

Il professore conclude con una riflessione fondamentale: i programmi concorrenti non si possono debuggare nel modo tradizionale. Ogni esecuzione produce probabilmente uno scenario diverso. Un test che passa oggi potrebbe fallire domani sulla stessa macchina, o su una macchina diversa.

La verifica formale (model checking, dimostrazioni induttive) non e un lusso accademico, ma una necessita ingegneristica. Progetti critici (NASA, Amazon, Intel) usano queste tecniche non solo per trovare bug, ma per certificare l'assenza di determinate classi di errori.

Metodi formali principali:

• Model checking — generazione esaustiva degli stati e verifica automatica delle proprieta (strumenti: SPIN, JPF, TLC)
• Dimostrazioni induttive di invarianti — si dimostra che A e vero nello stato iniziale (base) e che se A e vero in uno stato S, allora e vero in tutti gli stati successivi a S (passo induttivo)

Verifica le tue conoscenze