Semafori, Monitor, Modellazione e Verifica di Programmi Concorrenti

1. Semafori: definizione e operazioni base

I semafori sono il piu classico dei meccanismi di coordinazione tra processi. Introdotti da Edsger Dijkstra nel 1968, rappresentano un costrutto di programmazione generale che permette di risolvere virtualmente ogni problema di mutua esclusione e sincronizzazione. Il nome deriva dall'analogia con i semafori stradali: bloccano e sbloccano l'esecuzione dei processi (il "traffico") a seconda delle necessita.

Un semaforo S e un tipo di dato composito con due campi:

• S.V — un intero >= 0 che rappresenta il "valore" del semaforo
• S.L — un insieme di identificatori di processi bloccati sul semaforo

Può essere inizializzato con un valore k >= 0 per S.V e l'insieme vuoto per S.L. Fornisce due operazioni atomiche fondamentali: wait(S) (detta anche P(S)) e signal(S) (detta anche V(S)).

Operazione wait(S)

Se il valore S.V e maggiore di 0 (semaforo "verde"), viene semplicemente decrementato. Altrimenti, se S.V = 0 (semaforo "rosso"), il processo chiamante viene bloccato e aggiunto a S.L.

wait(S) =
  if (S.V > 0)
    S.V = S.V - 1
  else
    S.L = S.L + {p}
    p.state = blocked

Operazione signal(S)

Se nessun processo e in attesa, il valore del semaforo viene incrementato. Altrimenti, viene selezionato un processo arbitrario dalla coda S.L e sbloccato.

signal(S) =
  if (S.L = {})
    S.V = S.V + 1
  else
    q = arbitrary_element(S.L)
    S.L = S.L - {q}
    q.state = ready

2. Tipologie di semafori e invarianti

Invariante del semaforo

Sia k il valore iniziale, #signal(S) il numero di signal eseguiti, e #wait(S) il numero di wait completati (un processo bloccato in wait non conta come eseguito). L'invariante fondamentale che ogni semaforo soddisfa e:

S.V = k + #signal(S) - #wait(S)

Da cui deriva immediatamente S.V >= 0. Questo teorema e alla base della verifica di correttezza dei programmi che usano semafori.

Semafori forti vs deboli

Nei semafori forti, S.L non e un insieme ma una coda FIFO: i processi vengono sbloccati nell'ordine in cui si sono bloccati, garantendo l'assenza di starvation. Nei semafori deboli, S.L e un insieme: la starvation e possibile. Esistono anche busy-wait semaphores, senza S.L, in cui il processo attende in un ciclo di busy waiting fino a quando il valore non diventa positivo; appropriati solo in sistemi multiprocessore con bassa contesa.

3. Sezione critica con semafori

Usando un semaforo come lucchetto, la soluzione del problema della sezione critica per due processi diventa banale. Un semaforo binario S inizializzato a 1 protegge l'accesso: ogni processo esegue wait(S) prima di entrare nella sezione critica e signal(S) dopo averla lasciata.

P:                          Q:
loop forever                loop forever
  NCS                         NCS
  wait(S)                     wait(S)
  CS                          CS
  signal(S)                   signal(S)

Il diagramma di stato ridotto (che elimina le sezioni non critiche e critiche, mantenendo solo i protocolli di ingresso/uscita) evidenzia le proprieta di correttezza. Con un semaforo binario, la mutua esclusione e garantita: non esiste uno stato in cui entrambi i processi siano contemporaneamente in CS.

Simulatore: sezione critica con semaforo

Usate i pulsanti per avanzare i processi P e Q. Il semaforo S protegge l'ingresso nella sezione critica. Verificate che non sia mai possibile avere entrambi i processi in CS contemporaneamente.

La soluzione vale anche per N processi, ma attenzione: con semafori deboli la proprieta di assenza di starvation non e garantita. Un processo potrebbe essere continuamente scavalcato nella competizione per il lock.

4. Producer-Consumer con semafori

Il problema produttore-consumatore e un classico esempio di problema di ordinamento dell'esecuzione. Due tipi di processi cooperano: i produttori creano dati, i consumatori li elaborano. E uno dei pattern piu ubiquitari in informatica (browser-server, sistema operativo-stampante, input-output).

Buffer infinito

Con un buffer infinito, l'unica sincronizzazione necessaria e che il consumatore non provi a prelevare da un buffer vuoto. Si usa un semaforo availItems inizializzato a 0, che funge da resource semaphore contando gli elementi disponibili.

Produttore:                 Consumatore:
loop forever                loop forever
  Item el = produce           wait(availItems)
  append(buffer, el)          Item el = take(buffer)
  signal(availItems)          consume(el)

Buffer limitato (bounded buffer)

Con un buffer di dimensione N, serve anche impedire al produttore di inserire in un buffer pieno. Si introducono due semafori "split": availItems (elementi disponibili) e availPlaces (posti disponibili), inizializzato a N. L'invariante e: availItems + availPlaces = N.

Produttore:                 Consumatore:
loop forever                loop forever
  Item el = produce           wait(availItems)
  wait(availPlaces)           Item el = take(buffer)
  append(buffer, el)          signal(availPlaces)
  signal(availItems)          consume(el)

Con mutua esclusione sul buffer

Se le operazioni sul buffer (append/take) non sono atomiche, serve un semaforo mutex aggiuntivo per proteggere l'accesso alla struttura dati condivisa. L'ordine e importante: prima si attende il semaforo di sincronizzazione (availPlaces/availItems), poi quello di mutua esclusione (mutex).

Produttore:                     Consumatore:
loop forever                      loop forever
  Item el = produce                 wait(availItems)
  wait(availPlaces)                 wait(mutex)
  wait(mutex)                       Item el = take(buffer)
  append(buffer, el)                signal(mutex)
  signal(mutex)                     signal(availPlaces)
  signal(availItems)                consume(el)

5. Il problema dei Filosofi a cena

Problema classico della programmazione concorrente, introdotto da Dijkstra nel 1971 (originariamente come problema di sincronizzazione per 5 computer in competizione per 5 unita a nastro) e reso celebre da Tony Hoare nella versione dei filosofi a cena.

Descrizione: Cinque filosofi trascorrono la vita alternando due attivita: pensare e mangiare. I pasti sono consumati a un tavolo con 5 piatti e 5 forchette. Al centro c'e una scodiglia di spaghetti sempre piena. Ogni filosofo ha bisogno di due forchette per mangiare — quella a sinistra e quella a destra — ma può raccoglierle solo una alla volta.

L'obiettivo e progettare protocolli pre- e post- che garantiscano: mutua esclusione sulle forchette, assenza di deadlock, assenza di starvation, ed efficienza in assenza di contesa.

// PRIMO TENTATIVO (deadlock!)
semaphore fork[0..4] = [1,1,1,1,1]

Philosopher(i):
  loop forever
    think
    wait(fork[i])                // sinistra
    wait(fork[(i+1) % N])        // destra
    eat
    signal(fork[i])
    signal(fork[(i+1) % N])

6. Deadlock: condizioni di Coffman

Un deadlock e una situazione in cui due o piu processi sono in attesa che gli altri terminino, e nessuno può proseguire. Le condizioni necessarie di Coffman (1971) per il verificarsi di un deadlock sono quattro, e devono valere tutte simultaneamente:

1. Mutua esclusione — una risorsa non può essere usata da piu processi contemporaneamente
2. Hold and wait — i processi che già detengono risorse possono richiederne di nuove
3. No preemption — le risorse non possono essere sottratte forzatamente a un processo che le detiene
4. Circular wait — esiste una catena circolare di processi dove ognuno attende una risorsa detenuta dal successivo

In Java non esiste un meccanismo automatico di rilevamento e recupero deadlock: se i thread si bloccano, l'unica opzione e terminare l'applicazione. I database, invece, adottano tecniche di deadlock detection and recovery: analizzano il grafo delle dipendenze in attesa e, se trovano un ciclo, selezionano una "vittima" e abortiscono la transazione.

7. Soluzioni per i Filosofi: ticket e ordinamento

Soluzione con ticket (sala da pranzo)

Per garantire liveness, si limita il numero di filosofi che possono mangiare contemporaneamente: si introduce un semaforo ticket inizializzato a N-1. Solo N-1 filosofi su N possono competere per le forchette, rompendo la circolarita. Questa soluzione soddisfa tutte le proprieta.

semaphore fork[0..4] = [1,1,1,1,1]
semaphore ticket = (4, {})

Philosopher(i):
  loop forever
    think
    wait(ticket)              // entra nella sala
    wait(fork[i])
    wait(fork[(i+1) % N])
    eat
    signal(fork[i])
    signal(fork[(i+1) % N])
    signal(ticket)            // esce dalla sala

Soluzione con ordinamento delle forchette

Si osserva che il deadlock non si verifica se l'ultimo filosofo prende prima la forchetta destra e poi la sinistra. In generale, la regola e: acquisire sempre i lock in un ordine totale prestabilito. Questo rende impossibile la condizione di circular wait.

semaphore fork[0..4] = [1,1,1,1,1]
int first = min(i, (i+1) % N)
int second = max(i, (i+1) % N)

Philosopher(i):
  loop forever
    think
    wait(fork[first])
    wait(fork[second])
    eat
    signal(fork[first])
    signal(fork[second])

8. Il problema Lettori-Scrittori

Problema formulato da Courtois, Heymans e Parnas nel 1971. I processi si dividono in due classi: lettori (possono leggere contemporaneamente senza escludersi) e scrittori (devono escludere sia altri scrittori che i lettori). E l'astrazione dell'accesso concorrente a database o risorse condivise.

Gli invarianti da rispettare:

nR >= 0
nW = 0  oppure  nW = 1
(nR > 0 => nW = 0) AND (nW = 1 => nR = 0)

Soluzione con semafori

I lettori usano un lock mutex per aggiornare il contatore nR. Il primo lettore acquisisce il lock rw (escludendo scrittori); gli altri lettori incrementano solo il contatore. L'ultimo lettore rilascia rw.

Lettore:                        Scrittore:
  wait(mutexR)                    wait(rw)
  if (nR == 0)                    write(dbase)
    wait(rw)                      signal(rw)
  nR++
  signal(mutexR)
  read(dbase)
  wait(mutexR)
  nR--
  if (nR == 0)
    signal(rw)
  signal(mutexR)

9. Oltre i semafori: i monitor

I semafori sono potenti ma di basso livello: programmi soggetti a errori, difficili da usare in programmi concorrenti complessi. I monitor sono l'evoluzione naturale: un'astrazione di dati che incapsula stato, operazioni e politiche di sincronizzazione/mutua esclusione. Introdotti da Brinch Hansen (1973) e generalizzati da Hoare (1974).

Definizione: Un monitor e un modulo che incapsula l'accesso concorrente a uno stato condiviso, fornendo:

• Mutua esclusione intrinseca — le procedure vengono eseguite in mutua esclusione (al massimo un processo attivo per volta)
• Sincronizzazione esplicita — tramite variabili di condizione che permettono di sospendere e risvegliare i processi

Un monitor e una generalizzazione del concetto di kernel in un sistema operativo (dove il kernel centralizza le sezioni critiche) e una generalizzazione del concetto di oggetto in OOP (classi che incapsulano dati + operazioni + politica di sincronizzazione).

monitor Counter {
    int count;
    procedure inc() { count = count + 1; }
    procedure getValue() : int { return count; }
}

L'esempio del contatore mostra la potenza dell'astrazione: non c'e alcun wait/signal esplicito per la mutua esclusione. Il monitor garantisce automaticamente che due processi non eseguano mai inc() contemporaneamente.

10. Variabili di condizione e signaling discipline

Le variabili di condizione sono tipi primitivi che permettono di sospendere (waitC) e risvegliare (signalC) processi all'interno di un monitor. Ogni variabile di condizione e associata a una coda FIFO di processi bloccati.

waitC(cond) =              signalC(cond) =
  append p to cond.queue     if cond.queue != empty
    p.state = blocked          q = remove head of cond.queue
    monitor.lock = release     q.state = ready

waitC rilascia il lock del monitor quando sospende il processo (essenziale per non bloccare l'intero monitor). signalC non ha effetto se la coda e vuota — a differenza di signal su semaforo, che invece incrementa sempre il contatore.

Semantica di segnalazione

11. Monitor in Java: synchronized, wait, notify

Java offre due approcci per implementare monitor. Il primo, di piu basso livello, sfrutta i meccanismi nativi della JVM: synchronized, wait, notify, notifyAll.

Quando un metodo e dichiarato synchronized, la JVM genera automaticamente le istruzioni bytecode monitorenter e monitorexit. Ogni oggetto Java ha un intrinsic lock (o monitor lock) associato.

Pattern del monitor in Java

Regole per implementare il monitor pattern:

1. Tutti i metodi pubblici devono essere synchronized
2. Nessun campo pubblico
3. Il codice del monitor deve accedere solo a oggetti completamente confinati al suo interno
4. E disponibile un'unica variabile di condizione implicita (l'oggetto stesso)

Esempio: SynchCell

Semantica di wait

• Se il thread e stato interrotto, wait lancia InterruptedException
• Altrimenti, il thread viene bloccato e posto nel wait set dell'oggetto
• Il lock di sincronizzazione viene rilasciato (anche se rientrante)
• Al risveglio, il lock viene riacquisito prima di proseguire

Semantica di notify e notifyAll

• notify rimuove un thread arbitrario dal wait set (nessuna garanzia su quale)
• Il thread risvegliato deve riacquisire il lock e si blocca finche il notificante non rilascia il lock
• notifyAll opera su tutti i thread nel wait set (ma riacquisiranno il lock uno alla volta)

Spurious wakeup e il pattern while

La documentazione Java avverte: "A thread can also wake up without being notified, interrupted, or timing out, a so-called spurious wakeup." Per questo il pattern corretto e sempre wrappare wait in un ciclo while che riverifica la condizione:

synchronized void get() {
    while (!available) {    // SEMPRE while, mai if!
        try { wait(); } catch (InterruptedException ex) {}
    }
    return value;
}

Un'altra limitazione del meccanismo di base: piu predicati di condizione diversi devono essere associati alla stessa unica variabile di condizione (l'oggetto). Questo forza l'uso di notifyAll invece di notify, e il ciclo while permette a ogni thread di riverificare la propria condizione specifica al risveglio.

12. Bounded buffer come monitor

Implementiamo il bounded buffer produttori-consumatori usando il monitor pattern in Java, con synchronized/wait/notifyAll.

public class BoundedBuffer<Item> {
    private int first, last, count;
    private Item[] buffer;

    public BoundedBuffer(int size) {
        first = last = count = 0;
        buffer = (Item[]) new Object[size];
    }

    public synchronized void put(Item item) throws InterruptedException {
        while (isFull()) { wait(); }
        last = (last + 1) % buffer.length;
        count++;
        buffer[last] = item;
        notifyAll();
    }

    public synchronized Item get() throws InterruptedException {
        while (isEmpty()) { wait(); }
        first = (first + 1) % buffer.length;
        count--;
        notifyAll();
        return buffer[first];
    }

    public synchronized boolean isEmpty() { return count == 0; }
    public synchronized boolean isFull() { return count == buffer.length; }
}

13. ReentrantLock e Condition: monitor di alto livello

La libreria java.util.concurrent fornisce classi per implementare monitor con variabili di condizione multiple, superando le limitazioni del meccanismo synchronized.

La classe ReentrantLock e un'implementazione rientrante di lock mutex. Da un lock si possono creare multiple Condition, che rappresentano variabili di condizione distinte.

SynchCell con ReentrantLock

public class SynchCell2 {
    private int value;
    private boolean available;
    private Lock mutex;
    private Condition isAvail;

    public SynchCell2() {
        available = false;
        mutex = new ReentrantLock();
        isAvail = mutex.newCondition();
    }

    public void set(int v) {
        try {
            mutex.lock();
            value = v;
            available = true;
            isAvail.signalAll();
        } finally {
            mutex.unlock();
        }
    }

    public int get() {
        try {
            mutex.lock();
            if (!available) {
                try { isAvail.await(); } catch (InterruptedException ex) {}
            }
            return value;
        } finally {
            mutex.unlock();
        }
    }
}

Note importanti: i metodi non sono synchronized; il lock e gestito esplicitamente con lock()/unlock(); e essenziale il blocco finally per garantire il rilascio anche in caso di eccezioni; Condition offre await(), signal(), signalAll() al posto di wait/notify/notifyAll.

BoundedBuffer con condition variabili multiple

Con ReentrantLock possiamo finalmente avere notFull e notEmpty come variabili di condizione separate, permettendo segnalazioni selettive:

Notate: nel put si fa notEmpty.signal() (sveglia solo consumatori), nel get si fa notFull.signal() (sveglia solo produttori). Nessun overhead di risvegli inutili!

14. Semantica di segnalazione: effetti indesiderati

Il professore ha dedicato una parte significativa della lezione a mostrare un comportamento curioso della semantica di segnalazione in Java. La semantica adottata (Signal-and-Continue con E = W < S) può portare a ordini di esecuzione controintuitivi.

Scenario dimostrativo: Tre thread competono per un monitor. T1 entra, esegue await() e si sospende. T2 entra, esegue signal() e rilascia. T3 sta aspettando di entrare. Chi ottiene il lock dopo T2?

Con E = W < S, il thread risvegliato (T1) compete ad armi pari con i thread in attesa sul lock (T3). Dipende dall'implementazione della JVM e dallo scheduler del sistema operativo chi entra per primo. Nell'esempio mostrato, T3 e entrato prima di T1.

OUTPUT OSSERVATO:
First thread started.
First thread inside, going to wait
Second thread started.
Second thread inside
Third thread started.
Second thread inside, going to signal
Second thread inside signaled.
Third thread inside.            // <- T3 entra prima di T1!
First thread unblocked.         // <- T1 solo dopo T3

Errore comune: Confondere wait/notify (meccanismi di base su Object) con await/signal (da Condition). Il professore ha mostrato il caso in cui, usando ReentrantLock, si chiama erroneamente wait() invece di await() o notify invece di signal, cosa che causa IllegalMonitorStateException o comportamenti errati.

15. Laboratorio: barriera e latch

Il professore ha dedicato la parte finale della lezione a mostrare due componenti di coordinazione riutilizzabili implementati come monitor: la barriera e il latch (countdown).

Barriera (Barrier)

Una barriera e un punto di sincronizzazione in cui N thread si incontrano. Ogni thread chiama await() e rimane bloccato finche tutti gli N partecipanti non sono arrivati. L'ultimo thread che arriva sblocca tutti gli altri.

Implementazione con synchronized:

public class CyclicBarrierMonitor {
    private int nParticipants;
    private int nArrived;

    public CyclicBarrierMonitor(int n) {
        nParticipants = n;
        nArrived = 0;
    }

    public synchronized void await() throws InterruptedException {
        nArrived++;
        while (nArrived < nParticipants) {
            wait();        // aspetta che arrivino tutti
        }
        notifyAll();       // sblocca tutti
    }
}

Versione con ReentrantLock + Condition: nella seconda implementazione, si usa una condition variable allArrived con await() e signalAll(). Attenzione: notifyAll chiamato sulla condition variable non equivale a signalAll — un errore subdolo che il professore ha mostrato in aula.

Latch (CountDown)

Un latch permette a thread di attendere (await()) finche non viene raggiunto un conteggio zero tramite chiamate countDown(). A differenza della barriera, non e ciclico e il conteggio e monotono decrescente.

public class CountDownLatchMonitor {
    private int count;

    public CountDownLatchMonitor(int count) { this.count = count; }

    public synchronized void await() throws InterruptedException {
        while (count > 0) { wait(); }
    }

    public synchronized void countDown() {
        if (count > 0) {
            count--;
            if (count == 0) { notifyAll(); }
        }
    }
}

16. Modellazione di programmi concorrenti

Il secondo modulo della lezione introduce la modellazione dell'esecuzione concorrente. Modellare significa creare una descrizione rigorosa del comportamento del programma al giusto livello di astrazione, includendo le informazioni rilevanti e astraendo da quelle non rilevanti.

Modello per l'esecuzione concorrente:

• Ogni processo e una sequenza di azioni atomiche (esecuzione di un'istruzione senza possibilita di interleaving)
• Indipendenza dalla velocita (speed independence): l'esecuzione e modellata come un interleaving arbitrario delle azioni dei processi
• Un singolo processore astratto globale esegue tutte le azioni
• Il control pointer indica la prossima istruzione eseguibile per ogni processo

Questo modello e una astrazione: nella realta, i sistemi non hanno uno stato globale (questione di fisica). Ma l'astrazione e giustificata perche permette l'analisi formale, indipendente da tempi e velocita dei processori.

17. Diagrammi di stato ed esplosione degli scenari

L'esecuzione di un programma concorrente può essere rappresentata formalmente con stati e transizioni. Lo stato e definito da una tupla che include il control pointer di ogni processo e i valori di tutte le variabili.

Esempio base: due processi che assegnano a una variabile condivisa n:

P: int k1 = 1;      Q: int k2 = 2;
   n = k1;              n = k2;
int n = 0;  // globale

Il diagramma di stato ha 5 stati e 2 scenari: (p1, q1) e (q1, p1). Solo 2 esecuzioni possibili. Ma quando i processi hanno piu azioni, il numero di scenari cresce drammaticamente.

Esplosione combinatoria: con 2 processi di m azioni ciascuno, gli scenari sono (2m)!/(m! m!). Con 3 processi di m azioni: (3m)!/(m! m! m!). Per m=3 e 3 processi: 1680 scenari. Per m=8 e 2 processi: 12820.

Esploratore del diagramma di stato

Interagite con il diagramma di stato del problema dell'incremento non atomico. Cliccate sugli stati per vedere le transizioni possibili.

18. Proprieta di correttezza: safety e liveness

La correttezza dei programmi concorrenti (potenzialmente non terminanti) e definita in termini di proprieta delle computazioni — condizioni che devono essere verificate in ogni scenario possibile.

Verifica vs Testing:

• Testing — verifica su scenari selezionati. Rivela la presenza di errori, non la loro assenza. Problema: heisenbugs (il test stesso può mascherare i bug alterando i tempi)
• Verifica formale — dimostra che una proprieta vale per tutti gli scenari possibili. Tecniche: model checking, dimostrazioni induttive di invarianti

19. Fairness e scheduling

La fairness (equita) e una proprieta di liveness per cui qualcosa di buono accade infinitamente spesso. Dipende dalla politica di scheduling del sistema.

Esempio: due processi, uno con ciclo while flag = false e uno che setta flag = true. Se la schedulazione non e fair, il primo processo potrebbe ciclare all'infinito senza mai vedere flag = true — uno scenario non fair (non terminante) che e possibile in assenza di garanzie di fairness.

20. Logica temporale lineare (LTL)

Introdotta da Amir Pnueli (1977), la logica temporale lineare e un formalismo per esprimere proprieta di programmi concorrenti che evolvono nel tempo. Aggiunge operatori temporali alla logica proposizionale.

Operatori base

Mutua esclusione in LTL: (p3 q3) — in ogni stato, non entrambi i processi in CS.

Assenza di starvation: (p2 p3) — sempre, se un processo vuole entrare in CS, prima o poi ci riuscira.

Overtaking limitato (k-bounded): specifica che un processo può essere superato al massimo k volte prima di entrare in CS. Per 1-bounded: tryp ( CSq) W (CSq W (( CSq) W CSp))

21. Model checking: SPIN, Promela e Java Path Finder

Il model checking e la tecnica piu importante per la verifica automatica di proprieta di correttezza di sistemi concorrenti. Strategia: esplorare esaustivamente l'intero spazio degli stati del sistema e verificare se certe proprieta sono soddisfatte.

Se il sistema soddisfa la proprieta, il model checker genera una conferma. Altrimenti, produce un contresempio (trace) — utilissimo per identificare bug, non solo per provare correttezza.

SPIN e Promela

SPIN e un model checker ampiamente usato in ambito accademico e industriale. Promela e il linguaggio di modellazione per SPIN, con costrutti limitati pensati per costruire modelli di sistemi concorrenti. SPIN e stato usato dalla NASA (dopo l'incidente del Mars Polar Lander del 1999) e da Intel (dopo il bug Pentium del 1994).

// 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 e un model checker specializzato per la verifica di programmi Java, sviluppato dalla NASA e open-source. E una JVM speciale che esegue il programma lungo tutti i possibili scenari (execution paths), verificando proprieta come assenza di deadlock, eccezioni non catturate, violazioni di invarianti.

TLA+ e PlusCal

Leslie Lamport ha sviluppato TLA+ (Temporal Logic of Actions), un linguaggio di specifica formale usato per verificare sistemi reali complessi (es. Amazon Web Services). PlusCal (ex +CAL) e un linguaggio algoritmico basato su TLA+ che permette di scrivere algoritmi in uno stile simile a un linguaggio di programmazione, tradotti poi in TLA+ per la verifica con il model checker TLC.

22. L'importanza della verifica formale

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