Semafori, Deadlock e Monitor

1. Modellare l'esecuzione concorrente

Prima di introdurre i meccanismi di coordinamento, e importante avere un modello formale di cosa significa eseguire un programma concorrente. Il professore sottolinea che questo modulo — Modeling Concurrent Program Execution — e il piu teorico del corso, ma costituisce il nucleo concettuale per comprendere davvero la programmazione concorrente, non solo dal punto di vista dello sviluppo ma anche della modellazione.

Modello a interleaving arbitrario

Ogni processo viene modellato come una sequenza di azioni atomiche. L'esecuzione concorrente e rappresentata come un interleaving arbitrario delle azioni dei vari processi, eseguite da un singolo processore astratto globale. Questa astrazione — detta speed independence assumption — ignora il tempo reale e si concentra sugli ordini parziali tra le azioni. E robusta rispetto a cambiamenti hardware e software perche indipendente da variazioni di velocita e tempistiche.

flowchart LR
  subgraph P["Processo P"]
    direction LR
    p1("p1: n := k1") --> p2("p2: ...")
  end
  subgraph Q["Processo Q"]
    direction LR
    q1("q1: n := k2") --> q2("q2: ...")
  end
  p1 --> q1
  p1 --> p2
  q1 --> q2
  q1 --> p2

Numero di scenari

Con due processi che hanno m azioni ciascuno, il numero di scenari possibili e dato dal coefficiente binomiale C(2m, m). Con 3 processi la crescita e ancora piu rapida: bastano 3 azioni per processo per avere 1680 scenari diversi. Questo rende il testing esaustivo sostanzialmente impossibile per programmi reali.

Importanza dell'atomicita

Il professore mostra un esempio cruciale: un incremento n := n + 1 sembra un'operazione singola, ma a livello macchina si scompone in load R1, n; add R1, #1; store n, R1. Se due processi eseguono questa sequenza in parallelo, il risultato finale puo essere 1 invece di 2 — una race condition. L'atomicita delle operazioni e fondamentale: se un'operazione non e atomica, processi concorrenti possono osservare stati intermedi inconsistenti.

2. Proprieta di correttezza: safety e liveness

Per un programma concorrente, la correttezza si definisce in termini di proprieta delle computazioni — condizioni che devono valere in tutti gli scenari possibili, non solo in alcuni. Il professore distingue due categorie fondamentali.

Logica Temporale Lineare (LTL)

Per specificare formalmente queste proprieta si usa la LTL (introdotta da Amir Pnueli nel 1977, Premio Turing), che aggiunge operatori temporali alla logica proposizionale:

• [] p (sempre/globally): p e vero in tutti gli stati futuri — usato per safety
• <> p (eventualmente/finally): p e vero in qualche stato futuro — usato per liveness
• p U q (until): p e vero finche q non diventa vera
• p W q (weak until): come until, ma q puo anche non avverarsi mai; se non accade, p deve rimanere vero indefinitamente

Proprieta utili: [] p → p (riflessivita), <> [] p (alla fine stabilizza), [] <> p (infinitamente spesso). Inoltre, <> p = true U p e [] p = ¬ <> ¬ p.

K-bounded overtaking

A volte la semplice assenza di starvation e una proprieta debole: un processo potrebbe essere superato 1000 volte prima di entrare in CS. La proprieta di k-bounded overtaking garantisce che un processo puo essere superato al massimo k volte. Si esprime in LTL con l'operatore weak until: tryp → (¬ CSq) W (CSq W ((¬ CSq) W CSp)) per 1-bounded overtaking.

3. Semafori: introduzione e tipo di dato

Introdotti da Edsger Dijkstra nel 1968, i semafori sono un costrutto semplice ma estremamente potente per risolvere quasi ogni problema di mutua esclusione e sincronizzazione. Il professore li introduce con un'analogia: "e qualcosa che a un certo punto vedo che se e rosso mi fermo, se e verde passo. Se mi fermo perche e rosso, probabilmente qualcun altro deve passare." Come un semaforo stradale, blocca e sblocca i processi.

Rispetto ai lock visti nel modulo precedente (che facevano solo mutua esclusione), i semafori sono piu generali: permettono anche la sincronizzazione. Il professore sottolinea che e la stessa identica struttura dati che serve a scopi diversi, semplicemente cambiando il valore di inizializzazione.

Struttura del semaforo

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

Viene inizializzato specificando un valore k ≥ 0 per S.V e l'insieme vuoto per S.L. Notazione: semaphore S = (k, {}). Fornisce due operazioni atomiche fondamentali:

• wait(S) — detta anche P(S) (dal termine olandese Proberen, "provare" o "testare")
• signal(S) — detta anche V(S) (da Verhogen, "incrementare")

4. Operazioni atomiche: wait e signal

Operazione wait(S)

wait(S) =
  < if (S.V > 0)
      S.V := S.V - 1     { semaforo verde: passa e decrementa }
    else
      S.L := S.L + {p}   { semaforo rosso: processo p bloccato }
      p.state := blocked >

Se il valore del semaforo e maggiore di zero ("verde"), viene semplicemente decrementato e il processo prosegue senza bloccarsi. Se invece e zero ("rosso"), il processo viene bloccato e il suo identificatore viene aggiunto all'insieme S.L. L'intera operazione e atomica: non puo essere interrotta tra il controllo della condizione e l'eventuale modifica di S.V o S.L.

Operazione signal(S)

signal(S) =
  < if (S.L = {})
      S.V := S.V + 1       { nessuno in attesa: incrementa il valore }
    else
      let q := elemento arbitrario di S.L  { sceglie un processo }
      S.L := S.L - {q}     { lo rimuove dalla coda }
      q.state := ready >   { e lo rende pronto per l'esecuzione }

Se non ci sono processi in attesa, il valore del semaforo viene incrementato — il semaforo "ricorda" la signal. Altrimenti, viene selezionato un processo dalla coda S.L (l'arbitrarieta della scelta e importante: in un semaforo debole e un elemento qualunque, in uno forte e il primo in coda FIFO) e portato nello stato ready.

5. Invariante e tipologie di semafori

L'invariante fondamentale

Dato un valore iniziale k per S.V, vale il seguente invariante che costituisce la base per tutte le dimostrazioni di correttezza:

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

Dove #signal(S) e il numero di operazioni signal completate con successo e #wait(S) il numero di operazioni wait completate (un processo che si blocca durante la wait NON ha completato l'operazione, quindi non viene contato).

Tipologie principali

Il professore distingue tre usi principali, che corrispondono a tre valori di inizializzazione diversi:

Il professore sottolinea: "Fin qui e competizione [mutex]. L'ultimo [event] e quello che fa fare invece sincronizzazione. Non stiamo competendo, ma stiamo cooperando, dobbiamo sincronizzare le azioni. La cosa incredibile per me e lo stesso semaforo. Semplicemente deve essere inizializzato a zero."

6. Semafori forti, deboli e busy-wait

Esistono diverse definizioni del tipo semaforo, che differiscono per le proprieta di liveness (non per quelle di safety, che seguono dall'invariante). La scelta influenza se il sistema garantisce o meno assenza di starvation.

wait(S) =
  < if (S.V > 0) S.V := S.V - 1
    else append(S.L,p); p.state := blocked >
signal(S) =
  < if (S.L = empty_queue) S.V := S.V + 1
    else q := take(S.L); q.state := ready >

wait(S) = < await (S.V > 0); S.V := S.V - 1 >
signal(S) = < S.V := S.V + 1 >

7. Sezione critica con semafori

Usare un semaforo come lock per la sezione critica e immediato: si inizializza un semaforo binario (mutex) a 1 e si segue il protocollo wait/signal prima e dopo la sezione critica. Il professore commenta che questa soluzione vale per un numero arbitrario N di processi, non solo 2.

semaphore S ← (1,{})     { permesso unico: inizializzato a 1 }

loop forever              { per ogni processo }
  p1: NCS                 { sezione non critica }
  p2: wait(S)             { pre-protocollo: acquisisce il lock }
  p3: CS                  { sezione critica }
  p4: signal(S)           { post-protocollo: rilascia il lock }

Verifica di correttezza con diagramma di stato

Costruendo il diagramma di stato ridotto, che include lo stato del semaforo {S.V, S.L} e gli stati bloccati (p1B, q1B), si verifica che la soluzione e corretta per 2 processi:

• Mutua esclusione: nessuno scenario porta entrambi i processi in CS contemporaneamente — non esistono stati <p2,q2,_>
• No deadlock: se un processo e in attesa, prima o poi entrera
• No starvation: con semaforo forte, la starvation e impossibile per la coda FIFO

flowchart TD
  subgraph "Diagramma di stato ridotto"
    s0["p1, q1, {1,{}}"] --> s1["p2, q1, {0,{}}"]
    s0 --> s2["p1, q2, {0,{}}"]
    s1 --> s3["p2, q1B, {0,{Q}}"]
    s1 --> s4["p1B, q2, {0,{P}}"]
    s2 --> s3
    s2 --> s4
  end

8. Sincronizzazione con semafori evento

I semafori non servono solo per la mutua esclusione. Inizializzando il semaforo a 0 (event semaphore), si trasformano in un meccanismo di segnalazione: un processo segnala un evento, un altro lo attende. Il professore sottolinea che cambiano anche le parole: non si parla piu di "permesso" o "lock", ma di "evento" e "segnale".

Esempio: Merge Sort concorrente

Vogliamo ordinare un array dividendolo in due meta, ordinarle concorrentemente con due processi separati, e poi fare il merge. Abbiamo bisogno di sapere quando entrambe le meta sono state ordinate. Servono due semafori evento:

semaphore S1 ← (0,{})   { evento: prima meta ordinata }
semaphore S2 ← (0,{})   { evento: seconda meta ordinata }
integer array A          { array da ordinare }

sort1:                   sort2:                   merge:
  ordina 1a meta di A      ordina 2a meta di A      wait(S1)
  signal(S1)               signal(S2)               wait(S2)
                                                     merge delle due meta

Il processo merge si blocca su S1 e S2 fino a quando entrambi i processi di sorting non hanno segnalato il completamento. Il professore nota che i nomi S1, S2 sono criptici ("piacciono tanto agli informatici") e suggerisce di usare nomi significativi come firstHalfSorted e secondHalfSorted — un consiglio di buona pratica di programmazione.

9. Producer-Consumer con buffer infinito

Il problema Producer-Consumer e un esempio classico di sincronizzazione, onnipresente in informatica. Due tipi di processi cooperano: i produttori creano dati, i consumatori li elaborano. Esempi concreti:

Buffer infinito

La comunicazione puo essere sincrona (mittente e destinatario devono essere pronti contemporaneamente) o asincrona (un buffer intermedio disaccoppia temporalmente i partecipanti). Con un buffer infinito, l'unica sincronizzazione necessaria e che il consumatore non tenti di prelevare da un buffer vuoto.

semaphore availItems ← (0,{})
UnboundedQueue<Item> buffer ← empty queue

producer:                     consumer:
  loop forever                  loop forever
    Item el ← produce             wait(availItems)
    append(buffer,el)             Item el ← take(buffer)
    signal(availItems)            consume(el)

L'invariante e: availItems.V = #buffer — il valore del semaforo corrisponde al numero di elementi presenti nel buffer. Il semaforo availItems e detto resource semaphore perche conta una risorsa disponibile (gli item).

Il professore nota che questo schema realizza un disaccoppiamento temporale: produttori e consumatori non devono conoscersi ne coordinarsi direttamente, operano a velocita diverse, e il set di processi puo essere dinamico.

10. Bounded buffer e split semaphore

Nella realta i buffer sono finiti. Con un buffer limitato, anche il produttore deve poter essere bloccato: quando il buffer e pieno, non puo produrre ulteriori elementi. Il professore usa l'analogia dello scolapiatti: "chi lava i piatti [produttore] si ferma quando lo scola piatti e pieno, indipendentemente da chi asciuga [consumatore]."

La risorsa che serve al produttore e un posto libero nel buffer. Introduciamo un secondo semaforo availPlaces, il duale di availItems.

semaphore availItems ← (0,{})
semaphore availPlaces ← (N,{})
BoundedQueue<Item> buffer ← empty queue

producer:                       consumer:
  loop forever                    loop forever
    Item el ← produce               wait(availItems)
    wait(availPlaces)               Item el ← take(buffer)
    append(buffer,el)               signal(availPlaces)
    signal(availItems)              consume(el)

availItems e availPlaces sono detti split semaphore. L'invariante e: availItems + availPlaces = N (la somma dei due valori del semaforo e sempre uguale alla dimensione del buffer).

11. Semafori combinati: mutex + sincronizzazione

Se le operazioni sul buffer non sono atomiche (ad esempio, se ci sono piu produttori e piu consumatori), serve anche un semaforo per la mutua esclusione sull'accesso al buffer condiviso. Il professore mostra la soluzione completa che combina split semaphore e mutex:

semaphore availItems ← (0,{})
semaphore availPlaces ← (N,{})
binary semaphore mutex ← (1,{})

producer:                               consumer:
  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)

12. Dining Philosophers e Deadlock

Il problema dei Filosofi a Cena fu introdotto da Dijkstra nel 1971 per illustrare il problema del deadlock (che chiamava deadly embrace). Originariamente erano cinque computer che competevano per cinque drive a nastro; Tony Hoare lo rese popolare come la storia dei filosofi. Oggi e considerato un classico veicolo didattico per confrontare formalismi di programmazione concorrente.

Cinque filosofi siedono a un tavolo con 5 piatti e 5 forchette. Alternano due attivita: pensare (la loro sezione non critica) e mangiare. Per mangiare, servono due forchette — quella a sinistra e quella a destra. La sfida e che le forchette sono condivise tra filosofi adiacenti: la forchetta i e usata dai filosofi i e (i+1)%N.

Primo tentativo (incorretto: deadlock!)

semaphore array[0..4] fork ← [1,1,1,1,1]

philosopher[i]:   { per i = 0..4 }
  loop forever
    think
    wait(fork[i])             { prendi forchetta sinistra }
    wait(fork[(i+1)%N])       { prendi forchetta destra }
    eat
    signal(fork[i])
    signal(fork[(i+1)%N])

Questo tentativo e corretto per la mutua esclusione (nessuna forchetta e mai tenuta da due filosofi contemporaneamente, perche ogni forchetta e un semaforo binario), ma soffre di deadlock: se tutti i filosofi prendono contemporaneamente la forchetta sinistra prima che qualcuno provi a prendere la destra, nessuno puo mangiare e tutti restano bloccati per sempre in attesa della forchetta destra.

13. Condizioni di Coffman

Un deadlock e una situazione in cui due o piu azioni in competizione aspettano che l'altra finisca, e quindi nessuna finisce mai. Il professore lo chiama anche deadly embrace, il termine originale di Dijkstra. Nel 1971, Coffman identifico le quattro condizioni necessarie affinche un deadlock possa verificarsi in un sistema:

1. 1. Mutua esclusione — la risorsa coinvolta non puo essere usata da piu di un processo alla volta
2. 2. Hold and wait — i processi che gia detengono risorse possono richiederne di nuove, senza rilasciare le prime
3. 3. No preemption — una risorsa non puo essere rimossa forzatamente dal processo che la detiene; solo il processo stesso puo rilasciarla esplicitamente
4. 4. Circular wait — esiste una catena circolare di processi, dove ciascuno attende una risorsa detenuta dal successivo nella catena

Il deadlock puo verificarsi solo in sistemi dove tutte e quattro le condizioni sono vere contemporaneamente. Rimuovendone anche una sola, il deadlock e prevenuto.

Deadlock con i lock (deadly embrace)

Il caso piu semplice: thread A tiene il lock L e cerca di acquisire M, mentre thread B tiene M e cerca di acquisire L. Entrambi aspettano per sempre. Nei database, questo scenario viene gestito automaticamente: il DBMS analizza il grafo delle dipendenze, identifica il ciclo, sceglie una vittima e abortisce la transazione, rilasciando i lock. Nella JVM, invece, non esiste alcun meccanismo automatico di rilevamento e recovery: "if threads deadlock, that's all, folks!" — l'unica opzione pratica e spegnere l'applicazione e fare una diagnosi post-mortem.

14. Soluzioni per i Filosofi: ticket e ordinamento

Il professore presenta due soluzioni classiche al problema dei Filosofi, entrambe valide e che soddisfano tutte le proprieta (mutua esclusione, no deadlock, no starvation, comportamento efficiente in assenza di contesa).

Soluzione con ticket (N-1)

Limitiamo il numero di filosofi che possono mangiare contemporaneamente a N-1 (quindi 4 su 5). L'idea e che se solo 4 filosofi possono tentare di prendere le forchette, almeno uno riuscira sempre a prendere entrambe. Si introduce un semaforo counting ticket inizializzato a 4:

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

philosopher[i]:
  loop forever
    think
    wait(ticket)              { entra nella sala da pranzo }
    wait(fork[i])
    wait(fork[(i+1)%N])
    eat
    signal(fork[i])
    signal(fork[(i+1)%N])
    signal(ticket)            { esce dalla sala da pranzo }

Il professore commenta: "Se hai cinque filosofi che vogliono mangiare tutti insieme, metti quattro permessi, fai mangiare solo quattro alla volta. Se metti quattro permessi, come se dovessero prendere un ticket prima di iniziare a mangiare, si risolve il problema."

Soluzione con ordinamento (breaking the wait-for chain)

Si osserva che non c'e deadlock se si impone un ordine totale nell'acquisizione delle forchette. L'idea e che ogni filosofo prende prima la forchetta con indice minore e poi quella con indice maggiore:

integer first = min(i, (i+1)%N)
integer second = max(i, (i+1)%N)

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

Il professore spiega l'intuizione: "Se lui cerca di prendere prima la forchetta con indice minore, e questa e gia stata presa da un altro, si blocca subito senza avere l'altra forchetta. Quindi l'altra forchetta puo essere presa dal filosofo vicino. Non si crea mai un ciclo di attesa."

15. Regola generale per evitare il deadlock

Dall'esperienza dei Filosofi si generalizza una regola semplice ma potentissima per evitare deadlock in sistemi con lock multipli. Il professore la presenta come forse la cosa piu importante da ricordare quando si scrive codice concorrente:

Perche funziona?

Rende impossibile la condizione di circular wait, che e una delle quattro condizioni necessarie di Coffman. Se ogni processo acquisisce i lock in ordine crescente, non si puo formare un ciclo: se P aspetta una risorsa tenuta da Q, significa che P ha lock con indici piu piccoli e Q con indici piu grandi, quindi Q non puo a sua volta aspettare una risorsa di P (perche la richiederebbe in ordine crescente, ma ha gia lock con indice maggiore).

Piuttosto che dimostrarlo formalmente, il professore ne da l'intuizione: "Notate che cosa succede se lui cerca di prendere prima la forchetta con indice minore. L'ha gia presa? Se e gia stata presa si blocca in attesa senza avere il possesso dell'altra. Quindi sostanzialmente il fatto di imporre l'ordine permette di fare in modo che, quando si crea una situazione che va verso l'essere ciclico, un processo non riesce a prendere neanche la prima."

16. Readers-and-Writers

Il problema Readers and Writers (Courtois, Heymans, Parnas, 1971) e una variante del problema della mutua esclusione, con due classi di processi che competono per l'accesso a una risorsa condivisa (tipicamente un database):

• Readers: possono leggere il dato concorrentemente — non c'e pericolo nella lettura simultanea
• Writers: devono avere accesso esclusivo — sia rispetto ad altri writer, sia rispetto ai reader, per garantire la consistenza del dato durante la scrittura

Gli invarianti da rispettare sono: nR ≥ 0, nW = 0 || nW = 1, e (nR > 0 → nW = 0) ∧ (nW = 1 → nR = 0).

Primo tentativo (troppo vincolante)

Usare un singolo semaforo rw come lock esclusivo per reader e writer e una soluzione over-constrained: serializza anche l'accesso dei reader, impedendo la lettura concorrente e quindi vanificando il vantaggio.

Soluzione ottimizzata

binary semaphore mutexR ← (1,{})
int nr ← 0
binary semaphore rw ← (1,{})

reader:                               writer:
  loop forever                          loop forever
    wait(mutexR)                          wait(rw)
    if (nr == 0)                          Item el ← create_record
      wait(rw)                            write(dbase,el)
    nr ← nr + 1                           signal(rw)
    signal(mutexR)
    Item el ← read(dbase)
    wait(mutexR)
    nr ← nr - 1
    if (nr == 0)
      signal(rw)
    signal(mutexR)

mutexR protegge la variabile condivisa nr (numero di reader attivi). rw e il lock per i writer: il primo reader lo acquisisce, l'ultimo reader lo rilascia. I writer competono sempre su rw.

Il professore spiega il flusso: "Se ci sono solo reader, arrivano, prendono il mutex per un attimo, incrementano nr, escono, leggono. Tutti concorrenti. Quando arriva un writer, si blocca su rw finche l'ultimo reader non lo rilascia." Poi nel dettaglio: il primo reader vede nr == 0, prende rw, incrementa nr. Il secondo reader arriva, prende mutexR, vede nr > 0 (il primo ha gia preso rw), salta il wait(rw), incrementa nr. Entrambi leggono concorrentemente. L'ultimo reader, quando esce, decrementa nr, vede nr == 0 e fa signal(rw) per sbloccare eventuali writer in attesa.

17. Oltre i semafori: i Monitor

I semafori sono potenti ma di basso livello: il professore sottolinea che sono espressivi e permettono di risolvere qualsiasi problema di interazione, ma il loro uso non e banale perche sono un meccanismo comunque di basso livello, facile da sbagliare. Da qui nasce l'esigenza di costrutti di piu alto livello: i Monitor.

Introdotti da Brinch Hansen (1973) e generalizzati da Tony Hoare (1974), un Monitor e un'astrazione di dati per la programmazione concorrente che incapsula in un'unica entita:

• Lo stato (variabili permanenti, private all'interno del monitor)
• Le operazioni (procedure pubbliche che costituiscono l'interfaccia)
• La politica di concorrenza (mutua esclusione implicita + sincronizzazione esplicita)

monitor MonitorName {
  { dichiarazione di variabili permanenti }
  { inizializzazione }
  procedure opName(params) { ... }
  ...
}

Proprieta fondamentali

• Mutua esclusione implicita: le procedure del monitor si eseguono automaticamente in mutua esclusione — al piu un processo alla volta puo eseguire una procedura del monitor. Non serve alcun meccanismo esplicito come wait/signal per la mutua esclusione.
• Incapsulamento: solo le procedure sono visibili all'esterno; le variabili permanenti sono accessibili solo dall'interno.
• Sincronizzazione esplicita: tramite variabili condizione, che permettono di sospendere (waitC) e risvegliare (signalC) i processi in base allo stato del monitor.

Il professore nota che il monitor e una generalizzazione del concetto di kernel dei sistemi operativi: invece di avere un unico kernel centralizzato che gestisce tutte le sezioni critiche, ogni monitor e un "mini-kernel" decentralizzato specializzato per un dato condiviso. E anche una generalizzazione del concetto di oggetto nella OOP: una classe che incapsula dati + operazioni + politica di sincronizzazione/mutua esclusione.

18. Variabili condizione e signaling discipline

Le variabili condizione sono un tipo di dato primitivo che i monitor mettono a disposizione per la sincronizzazione esplicita. Ogni variabile condizione e associata a una coda FIFO di processi bloccati su quella condizione.

Operazioni principali:

Esempio: SynchCell

monitor SynchCell {
  int value;
  boolean available := false;
  cond isAvail;

  procedure set(int v) {
    value := v;
    available := true;
    signalC(isAvail);
  }

  procedure get(): int {
    if (!available)
      waitC(isAvail);
    return value;
  }
}

Un processo chiama get() ma se il valore non e ancora disponibile (available = false), si sospende su isAvail. Quando un altro processo chiama set(), imposta il valore e segnala isAvail, risvegliando il processo in attesa. Il professore sottolinea che il waitC rilascia automaticamente il lock del monitor, permettendo cosi ad altri processi di chiamare set() per fornire il dato.

Semaphore vs. Condition Variable

Signaling disciplines

Quando un processo esegue signalC, sia il signaller che il signalled potrebbero essere pronti a proseguire nel monitor, ma solo uno puo avere accesso esclusivo. Le tre discipline classiche differiscono per l'ordine di priorita tra signaller (S), waiting (W) ed external processes (E — processi bloccati sulle procedure del monitor):

Il professore nota che la scelta della disciplina ha implicazioni pratiche: con Signal & Continue, dopo un waitC(cond) e consigliabile usare while (!condizione) invece di if (!condizione) per gestire possibili risvegli spuri (il signalled potrebbe trovare la condizione ancora falsa perche un altro processo l'ha cambiata nel frattempo).

19. Producer-Consumer con Monitor

Ecco l'implementazione del bounded buffer come monitor, che incapsula automaticamente la mutua esclusione sull'accesso al buffer e la sincronizzazione tramite variabili condizione:

monitor BoundedBuffer {
  ElemType buffer := <EmptyBuffer>
  cond notFull, notEmpty;

  procedure put(ElemType elem) {
    if (buffer is full)
      waitC(notFull);
    append(buffer, elem);
    signalC(notEmpty);
  }

  procedure take(): ElemType {
    if (buffer is empty)
      waitC(notEmpty);
    ElemType el := head(buffer);
    signalC(notFull);
    return el;
  }
}

producer:
  loop
    ElemType el := produce
    BoundedBuffer.put(el)

consumer:
  loop
    ElemType el := BoundedBuffer.take()
    consume(el)

Il codice produttore e consumatore diventa estremamente semplice: chiamano rispettivamente put e take sul monitor, senza preoccuparsi di lock espliciti o semafori. La variabile condizione notFull blocca il produttore se il buffer e pieno; notEmpty blocca il consumatore se il buffer e vuoto. Quando un produttore aggiunge un elemento, segnala notEmpty per sbloccare un eventuale consumatore in attesa; quando un consumatore preleva, segnala notFull per sbloccare un eventuale produttore.

Il professore commenta: "Questa soluzione e molto piu semplice e chiara rispetto a quella con semafori. Il monitor gestisce automaticamente la mutua esclusione sul buffer, e le variabili condizione notFull/notEmpty gestiscono la sincronizzazione."

20. Readers-and-Writers con Monitor

L'implementazione del RWLock come monitor mostra la potenza delle variabili condizione per gestire politiche di sincronizzazione complesse. Ecco la versione con disciplina Signal & Continue:

monitor RWLock {
  int nr, nw = 0;
  cond okToRead, okToWrite;

  procedure request_read() {
    while (nw > 0)
      waitC(okToRead);
    nr := nr + 1;
  }

  procedure release_read() {
    nr := nr - 1;
    if (nr = 0)
      signalC(okToWrite);
  }

  procedure request_write() {
    while (nr > 0 or nw > 0)
      waitC(okToWrite);
    nw := nw + 1;
  }

  procedure release_write() {
    nw := nw - 1;
    signalC(okToWrite);
    signalAllC(okToRead);
  }
}

L'invariante: (nr == 0 or nw == 0) and (nw <= 1) — o ci sono solo reader, o solo un writer (o nessuno). release_write() fa due segnalazioni: signalC(okToWrite) per sbloccare un writer in attesa (se c'e), e signalAllC(okToRead) per risvegliare tutti i reader in attesa.

Il professore mostra anche una seconda versione, piu compatta, che usa il pattern "cascading signal": dopo startRead(), il primo reader sbloccato chiama a sua volta signalC(okToRead) per risvegliare il successivo, creando una catena. Questa versione elimina il while e torna a usare if per il controllo delle condizioni.

procedure startRead() {
  if writers != 0
    waitC(okToRead);
  readers := readers + 1;
  signalC(okToRead);    { risveglia il prossimo reader in cascata }
}

procedure endWrite() {
  writers := writers - 1;
  if emptyC(okToRead)
    then signalC(okToWrite)   { se nessun reader aspetta, sblocca un writer }
    else signalC(okToRead);   { altrimenti sblocca il primo reader }
}

21. Implementare i Monitor con semafori

I monitor possono essere realizzati usando semafori come building blocks di livello piu basso. Per ogni monitor servono:

• Un semaforo mutex (inizializzato a 1) per garantire la mutua esclusione: wait(mutex) in prologo, signal(mutex) in epilogo di ogni operazione
• Per ogni variabile condizione cond, un semaforo condsem e un contatore condcount per tracciare quanti processi sono in attesa

Le due discipline si implementano cosi:

Prologo per ogni operazione:
  wait(mutex)
Epilogo per ogni operazione:
  signal(mutex)

waitC(cond) =
  condcount++;
  signal(mutex);     { rilascia il lock del monitor }
  wait(condsem);     { si blocca sulla condizione }
  wait(mutex);       { quando si risveglia, riacquisisce il lock }

signalC(cond) =
  if (condcount > 0) {
    condcount--;
    signal(condsem); { sblocca un processo in attesa }
  }

Prologo per ogni operazione:
  wait(mutex)
Epilogo per ogni operazione:
  signal(mutex)

waitC(cond) =
  condcount++;
  signal(mutex);
  wait(condsem);     { si blocca — verra sbloccato da signalC }

signalC(cond) =
  if (condcount > 0) {
    condcount--;
    signal(condsem); { sblocca il processo in attesa }
    wait(mutex);     { il signaller si mette in attesa del lock }
  }

Implementare un semaforo con un monitor

Chiudendo il cerchio, si puo anche implementare un semaforo usando un monitor, dimostrando l'equivalenza espressiva dei due costrutti:

monitor Semaphore {
  integer s := <InitValue>
  cond notZero;

  procedure wait() {
    if s = 0
      waitC(notZero);
    s := s - 1;
  }

  procedure signal() {
    s := s + 1;
    signalC(notZero);
  }
}

Il professore mostra anche una versione alternativa che separa il caso in cui s > 0 (decrementa senza bloccare) dal caso s = 0 (si blocca). Entrambe le versioni sono corrette.

22. Model Checking e verifica formale

Data l'esplosione del numero di scenari nei programmi concorrenti, il testing tradizionale non basta. Il professore introduce due approcci principali di verifica formale, anticipando che nella prossima lezione mostrera esempi pratici con Java Path Finder.

Model Checking

Il model checking e una tecnica automatica che esplora esaustivamente tutto lo spazio degli stati di un sistema per verificare se certe proprieta sono soddisfatte. Se la proprieta e violata, produce un controesempio — una traccia di esecuzione completa che porta alla violazione, utilissima per identificare e correggere bug.

Strumenti principali:

• SPIN: model checker per sistemi concorrenti e distribuiti, usa il linguaggio PROMELA per modellare i sistemi. Estremamente efficiente, usato in ambito accademico e industriale
• Java Path Finder (JPF): JVM speciale sviluppata dalla NASA che esegue programmi Java lungo tutti i possibili percorsi di esecuzione, verificando deadlock, eccezioni non catturate, violazioni di proprieta. Se trova un errore, riporta l'intera esecuzione che ci porta. E un progetto open source mantenuto dalla comunita

Inductive Proof of Invariants

Un approccio alternativo, puramente matematico: invece di esplorare tutti gli stati, si dimostra che una proprieta (invariante) 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

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

Tecniche per gestire l'esplosione degli stati

Il problema principale del model checking e la dimensione dello spazio degli stati. Le tecniche moderne includono:

• Regole di riduzione: variabili modellate con un numero limitato di valori
• Costruzione incrementale: si esplora solo lo spazio raggiungibile, fermandosi se si trova una violazione
• Model checking simbolico: si lavora con insiemi di stati invece che singoli stati

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.

Verifica le tue conoscenze