Modellazione, Sezione Critica, Verifica Formale, Semafori e Monitor

1. Modellare l'esecuzione concorrente

Per comprendere il comportamento di un programma concorrente non possiamo affidarci all'esecuzione reale: il non-determinismo dell'interleaving fa si che uno stesso input possa produrre output diversi a seconda dello scenario. Servono modelli che astraggano dal tempo e dall'architettura specifica.

Assumiamo la speed independence: non facciamo assunzioni sulla velocita relativa dei processi. Questo rende il modello robusto rispetto a cambiamenti hardware e permette l'analisi formale.

Ogni processo ha un controll pointer (o instruction pointer) che indica la prossima istruzione eseguibile. Lo stato globale del sistema e definito da una tupla contenente il control pointer di ogni processo e il valore di tutte le variabili (sia globali condivise che locali private).

Primo esempio

Due processi P e Q che assegnano valori a una variabile condivisa n:

integer k1 := 1
p1: n := k1

integer k2 := 2
q1: n := k2

integer n := 0

L'esecuzione puo seguire due scenari:

• p1, q1 → n = 2
• q1, p1 → n = 1

Il risultato finale dipende dall'ordine con cui le istruzioni vengono interleave: questo e il cuore del non-determinismo nei programmi concorrenti.

2. Diagrammi di stato

Un diagramma di stato (state diagram) rappresenta formalmente l'esecuzione del programma concorrente: ogni nodo e uno stato del sistema, ogni arco e una transizione causata dall'esecuzione di un'istruzione atomica da parte di un processo.

La tupla di stato contiene un elemento per ogni control pointer e per ogni variabile globale o locale rilevante. Partendo dallo stato iniziale, si applicano tutte le transizioni possibili in modo da generare il grafo completo degli stati raggiungibili.

Il numero di scenari possibili cresce in modo combinatorio. Con 2 processi che hanno ciascuno m azioni atomiche, il numero di scenari possibili e dato da:

(2m)! / (m! m!)

Questa crescita esplosiva e la ragione per cui la verifica manuale dei programmi concorrenti e complessa e per cui servono strumenti automatici come il model checker.

3. Atomicita e non-atomicita

La scelta di cosa e atomico e fondamentale nel modello. Un'istruzione atomica viene eseguita fino al completamento senza possibilita di interleaving con altre istruzioni.

Incremento atomico vs non-atomico

Consideriamo l'incremento di una variabile condivisa n:

{
  Caso atomico:
  p1: n := n + 1    q1: n := n + 1

  Caso non-atomico (a livello macchina):
  integer tmp;
  p1: tmp := n      q1: tmp := n
  p2: n := tmp + 1  q2: n := tmp + 1
}

integer n := 0

Nel caso non-atomico, lo n := n + 1 viene tradotto in due istruzioni (load e store). Se i due processi si interleave tra load e store, si possono ottenere scenari in cui il valore finale di n e 1 invece di 2 — una race condition.

Strutture dati non-atomiche

Il concetto di atomicita si applica anche alle strutture dati. Un oggetto dati atomico puo trovarsi solo in un numero finito di stati corrispondenti ai valori che puo assumere. I tipi primitivi nei linguaggi concorrenti sono tipicamente atomici (eccezione: double in Java).

Per un tipo di dato astratto (ADT) non-atomico, possiamo distinguere:

• Stato interno: significativo per chi definisce il tipo
• Stato esterno: significativo per chi utilizza il tipo

La corrispondenza fra stati interni ed esterni e parziale: esistono stati interni senza corrispondente esterno (stati inconsistenti). In programmazione sequenziale questo non e un problema grazie all'information hiding; in programmazione concorrente, un processo potrebbe osservare un oggetto in uno stato inconsistente mentre un altro processo lo sta modificando.

E necessario introdurre meccanismi che garantiscano che i processi lavorino sempre su oggetti in stati consistenti — da qui nasce l'esigenza della sezione critica.

4. Correttezza: safety e liveness

La correttezza dei programmi concorrenti (anche non terminanti) si definisce in termini di proprieta sulle computazioni, condizioni che devono valere in ogni possibile scenario di esecuzione.

La verifica delle proprieta di safety e piu semplice: basta trovare un stato che violi la proprieta per concludere la non-correttezza. La verifica delle proprieta di liveness richiede di analizzare tutti i possibili scenari, non solo gli stati singoli.

5. Fairness

La fairness e una proprieta di liveness per cui qualcosa di buono accade infinitamente spesso. In pratica, riguarda la politica di scheduling: un'azione che puo essere eseguita, prima o poi verra effettivamente eseguita.

Esistono tre livelli di fairness:

Uno scenario e unconditionally fair se, in ogni stato, un'istruzione che e continuamente abilitata appare prima o poi nello scenario. Consideriamo il programma:

p1: while flag = false
p2:   n := 1 - n

q1: flag := true

integer n := 0
boolean flag := false

Se permettiamo scenari non-fair, il processo P puo loopare all'infinito senza che Q esegua mai q1, e l'algoritmo non termina. Solo in scenari fair, Q viene prima o poi schedulato e la computazione termina.

6. Il problema della sezione critica

Introdotto da Dijkstra nel 1965, il problema della sezione critica (Critical Section problem) e uno dei problemi piu importanti e studiati nella programmazione concorrente, nell'ambito della competizione tra processi.

Definizione: N processi, ciascuno in esecuzione in un loop infinito, eseguono una sequenza di istruzioni divisibile in due parti: la sezione critica (CS) e la sezione non critica (NCS).

P[1..n]:
loop forever
  <non-critical section>
  <entry (o pre-) protocol>
  <critical section>
  <exit (o post-) protocol>
  <non-critical section>

Il compito e progettare i protocolli di entrata e uscita che soddisfino le seguenti proprieta:

Si assume la proprieta di progress per la CS: una volta che un processo inizia la CS, deve prima o poi terminarla. La NCS, invece, non deve necessariamente progredire: un processo puo rimanere in NCS indefinitamente o terminare.

7. Primo tentativo — variabile turn

Il primo tentativo usa una variabile condivisa turn che indica a chi spetta entrare in sezione critica:

integer turn := 1

p                               q
loop forever                    loop forever
p1: NCS                         q1: NCS
p2: await turn = 1              q2: await turn = 2
p3: CS                          q3: CS
p4: turn := 2                   q4: turn := 1

Verifica di mutua esclusione: il diagramma di stato ha 16 stati (con NCS e CS espansi) o 4 stati (versione ridotta rimuovendo NCS e CS). Non esistono stati <p2,q2,_> nella versione ridotta (o <p3,q3,_> in quella completa) — la mutua esclusione e soddisfatta.

Assenza di deadlock: se entrambi vogliono entrare, uno dei due otterra il turno giusto. Anche questa e soddisfatta.

Assenza di starvation: NON soddisfatta. Se il processo P esegue la CS e poi si ferma nella NCS (o termina), Q rimane bloccato in q2: await turn = 2 per sempre, perche turn e rimasto a 2. turn funziona come un permesso di accesso: se chi detiene il permesso non lo rilascia (perche e bloccato in NCS), l'altro processo non potra mai entrare.

8. Tentativi 2, 3, 4

boolean wantp := false, wantq := false

p:                              q:
p1: NCS                         q1: NCS
p2: while wantq skip            q2: while wantp skip
p3: wantp := true               q3: wantq := true
p4: CS                          q4: CS
p5: wantp := false              q5: wantq := false

boolean wantp := false, wantq := false

p:                              q:
p1: wantp := true               q1: wantq := true
p2: await wantq = false         q2: await wantp = false
p3: CS                          q3: CS
p4: wantp := false              q4: wantq := false

p:                              q:
p1: wantp := true               q1: wantq := true
p2: while wantq do              q2: while wantp do
p3:   wantp := false            q3:   wantq := false
p4:   wantp := true             q4:   wantq := true
p5: CS                          q5: CS
p6: wantp := false              q6: wantq := false

Sintesi dell'evoluzione

9. Algoritmi di Dekker e Peterson

Algoritmo di Dekker (1965)

Dekker combina il primo e il quarto tentativo: introduce il turn per risolvere la contesa, ma lo usa solo quando c'e effettiva competizione. Quando l'altro processo non vuole entrare, si procede senza attendere il turno.

L'algoritmo e corretto: soddisfa mutua esclusione, assenza di deadlock e assenza di starvation su architetture che forniscono solo load e store come istruzioni atomiche.

Algoritmo di Peterson (1981)

Peterson propone una soluzione piu concisa, unendo due await in una singola condizione composta:

boolean wantp := false
boolean wantq := false
integer turn := 1

p:                                    q:
loop forever                          loop forever
  NCS                                   NCS
  wantp := true                         wantq := true
  turn := 2                             turn := 1
  await (!wantq or turn = 1)            await (!wantp or turn = 2)
  CS                                    CS
  wantp := false                        wantq := false

10. Istruzioni atomiche composte

Se la macchina concorrente fornisce istruzioni atomiche piu potenti del semplice load/store, il problema della sezione critica si semplifica enormemente. Le principali sono:

Con test-and-set possiamo realizzare un lock semplice:

integer lock := 0

integer was_locked
loop forever
  NCS
  repeat
    test_and_set(lock, was_locked)
  until was_locked = 0
  CS
  lock := 0

La test_and_set e atomica e fa due cose contemporaneamente: copia il vecchio valore di lock in was_locked e setta lock a 1. Se was_locked risultava 0, significa che il lock era libero e il processo puo entrare. Se era 1, qualcun altro ha gia preso il lock e bisogna riprovare (busy-wait).

Questa soluzione funziona con N processi, non solo 2.

In Java: synchronized

Il costrutto synchronized in Java implementa sezioni atomiche usando un lock condiviso:

// processo (thread) A
synchronized (lock) {
  <statement a>
  <statement b>
}

// processo (thread) B
synchronized (lock) {
  <statement c>
  <statement d>
}

Non possono esistere scenari con sequenze come a.c.b.d o c.a.d.b — i blocchi synchronized sullo stesso oggetto lock sono eseguiti in mutua esclusione.

11. Bakery algorithm (ticket)

L'algoritmo del fornaio (bakery algorithm) e una soluzione per N processi che introduce il concetto di biglietto numerato, come in una panetteria: ogni cliente (processo) prende un numero e viene servito in ordine crescente.

int num := 1
int next := 1
turn[1:n] := [0, 0, 0, ...]

p[i]:
loop forever
  NCS
  <turn[i] := num; num := num + 1>    { atomico }
  await turn[i] = next
  CS
  next := next + 1

Problema: overflow aritmetico. I contatori num e next crescono monotonamente e con interi a dimensione finita possono arrivare a overflow, causando il reset a 0 e la violazione della proprieta di ordinamento.

12. Verifica vs test

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.

13. Logica Temporale Lineare (LTL)

Per esprimere proprieta di correttezza in modo rigoroso servono linguaggi formali. La LTL (Linear Temporal Logic), introdotta da Amir Pnueli (1977), estende la logica proposizionale con operatori temporali che permettono di ragionare sull'evoluzione degli stati nel tempo.

Le proposizioni atomiche riguardano il valore delle variabili e dei control pointer. Ad esempio, l'etichetta p3 diventa una proposizione che significa "il control pointer del processo P e a p3".

Operatori principali

Specificare safety con LTL

Mutua esclusione per la sezione critica: lo stato "cattivo" e quando entrambi i processi sono in CS. Usiamo l'operatore [] per dire che non deve mai accadere:

[]! (p3 ∧ q3)

In generale: []p dove p = !q e q descrive lo stato "cattivo".

Specificare liveness con LTL

Progress property (assenza di starvation): se un processo e in attesa (stato p2), deve prima o poi entrare in CS (p3):

[](p2 → <>p3)

La formula dice: "per ogni stato, se il processo P e in p2, allora prima o poi (eventualmente) sara in p3".

Attenzione all'implicazione: P → Q equivale a !P ∨ Q. Se la premessa e falsa (P non e in p2), l'implicazione e vera a prescindere da Q. E la formula cattura correttamente che non ci interessa la starvation se P non ha mai richiesto di entrare.

Proprieta derivate

• Riflessivita: []p → p e p → <>p
• Dualita: ![]p → <>!p e !<>p → []!p
• Sequenze: <>[]p (eventualmente sempre vero) vs []<>p (sempre eventualmente vero)

Teorema importante: ([]<>p ∧ []<>q) → []<>(p ∧ q) e falso. P e Q possono essere veri in infiniti stati, ma mai contemporaneamente. E un errore comune assumere il contrario.

Bounded overtaking

La k-bounded overtaking cattura l'idea che un processo non possa essere "superato" piu di k volte da un altro processo mentre aspetta di entrare in CS. Usando il weak-until:

tryp → (!CSq) W (CSq W ((!CSq) W CSp))

Questa formula esprime il 1-bounded overtaking: dopo il tentativo di P, Q puo entrare in CS al massimo una volta prima che P entri.

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

/* 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. Tecniche allo stato dell'arte includono:

• Riduzione manuale: semplificare il modello eliminando variabili o istruzioni irrilevanti per la proprieta da verificare
• 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

15. Semafori

I semafori, introdotti da Dijkstra nel 1968, sono un costrutto semplice ma potente per risolvere problemi di mutua esclusione e sincronizzazione. Funzionano come un semaforo stradale: bloccano e sbloccano l'esecuzione dei processi.

Definizione

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

• S.V: un intero ≥ 0
• S.L: un insieme di identificatori di processo

Si inizializza con S = (k, {}) dove k ≥ 0.

Fornisce due operazioni atomiche:

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

signal(S) =
<if (S.L = {})
    S.V := S.V + 1
  else
    let q := arbitrary element of S.L
    S.L := S.L - {q}
    q.state := ready>

Invariante del semaforo

Dato k valore iniziale di S.V:

S.V ≥ 0

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

Dove #wait(S) conta solo i wait completati (i processi che si bloccano non hanno completato il wait).

Tipi di semafori

Semafori forti vs deboli

• Strong semaphore: S.L e una coda FIFO. Garanzia di assenza di starvation per qualsiasi N.
• Weak semaphore: S.L e un insieme (selezione arbitraria). Starvation possibile.
• Busy-wait semaphore: nessun S.L, il processo continua a testare in busy-wait. Non c'e garanzia di starvation freedom.

Sezione critica con semaforo (2 processi)

binary semaphore S := (1, {})

p:                              q:
loop forever                    loop forever
  NCS                             NCS
  wait(S)                         wait(S)
  CS                              CS
  signal(S)                       signal(S)

E la soluzione e corretta: mutua esclusione, assenza di deadlock, assenza di starvation (con strong semaphore).

Il diagramma di stato include stati bloccati (p1^B e q1^B) e lo stato del semaforo nella tupla {S.V, S.L}.

16. Produttore-Consumatore

Il problema del Produttore-Consumatore (Producer-Consumer) e un esempio classico di sincronizzazione. Due tipi di processi:

• Produttori: creano dati e li inviano
• Consumatori: ricevono e processano i dati

Pattern ubiquitari: browser + communication line, tastiera + OS, word processor + stampante.

Buffer infinito

Con buffer infinito, l'unica sincronizzazione necessaria e: il consumatore non deve prelevare da un buffer vuoto.

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

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

availItems e un resource semaphore, e vale sempre il numero di elementi nel buffer.

Buffer limitato

Con buffer limitato, serve sincronizzare anche il produttore: non deve scrivere se il buffer e pieno.

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

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 + availPlaces = N (split semaphores).

Con mutua esclusione sul buffer

Se le operazioni append e take non sono atomiche, serve un semaforo mutex aggiuntivo:

BoundedQueue<Item> buffer
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)

Attenzione all'ordine: il wait sul semaforo di sincronizzazione (availPlaces / availItems) viene prima del wait sul mutex. Invertire l'ordine puo portare a deadlock.

17. Deadlock e Filosofi a cena

Condizioni di Coffman

Un deadlock puo verificarsi solo se tutte e quattro le seguenti condizioni valgono simultaneamente (Coffman, 1971):

1. Mutua esclusione — Una risorsa non puo essere usata da piu processi contemporaneamente
2. Hold and wait — Un processo che gia detiene risorse puo richiederne altre
3. No preemption — Una risorsa non puo essere rimossa forzatamente dal processo che la detiene
4. Circular wait — Due o piu processi formano una catena circolare in cui ciascuno attende una risorsa detenuta dal successivo

Deadlock con lock

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 (deadly embrace).

In Java non esiste un meccanismo automatico di rilevazione/recovery dai deadlock. Se i thread si bloccano, "that's all, folks!" — l'unica possibilita e arrestare l'applicazione e analizzare post-mortem.

Il problema dei Filosofi a cena (Dining Philosophers)

Un classico problema di sincronizzazione introdotto da Dijkstra (1971) e reso celebre da Hoare. Cinque filosofi siedono a un tavolo con 5 piatti e 5 forchette. Ogni filosofo alterna pensiero e mangiare; per mangiare servono due forchette (quella a sinistra e quella a destra).

Primo tentativo: ogni forchetta e modellata come un semaforo binario. Il filosofo prende prima la sinistra, poi la destra.

semaphore array[0..4] fork := [1, 1, 1, 1, 1]

philosopher i:
loop forever
  think
  wait(fork[i])                    { forchetta sinistra }
  wait(fork[(i+1) % 5])            { forchetta destra }
  eat
  signal(fork[i])
  signal(fork[(i+1) % 5])

Problema: deadlock. Se tutti i filosofi prendono la forchetta sinistra contemporaneamente, nessuno puo prendere la destra. E un classico circular wait.

Soluzioni

semaphore ticket := (4, {})

loop forever
  think
  wait(ticket)
  wait(fork[i])
  wait(fork[(i+1) % N])
  eat
  signal(fork[i])
  signal(fork[(i+1) % N])
  signal(ticket)

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])

18. Lettori-Scrittori

Il problema dei Lettori-Scrittori (Courtois, Heymans, Parnas, 1971) e simile al problema della sezione critica, ma divide i processi in due classi:

• Lettori: devono escludere gli scrittori, ma non gli altri lettori
• Scrittori: devono escludere sia lettori che altri scrittori

E un'astrazione dell'accesso a database: non c'e pericolo in letture concorrenti, ma la scrittura richiede mutua esclusione totale.

Invarianti:

nR ≥ 0 ∧ nW = 0 ∨ nW = 1

(nR > 0 → nW = 0) ∧ (nW = 1 → nR = 0)

Soluzione con semafori

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

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)

Come funziona: mutexR protegge l'aggiornamento del contatore nr. Il primo lettore acquisisce rw (bloccando gli scrittori). Gli altri lettori incrementano solo nr. L'ultimo lettore rilascia rw. Gli scrittori usano rw direttamente per la mutua esclusione totale.

19. Monitor

I semafori sono potenti ma di basso livello: portano a programmi error-prone. I monitor (Brinch Hansen, 1973; Hoare, 1974) offrono un'astrazione piu alta. Un monitor e un'astrazione dati che incapsula:

• Lo stato (variabili permanenti)
• Le operazioni (procedure)
• La politica di concorrenza (mutua esclusione e sincronizzazione)

Proprieta fondamentali

• Mutua esclusione intrinseca: le procedure del monitor si eseguono automaticamente in mutua esclusione. Al massimo un processo puo essere attivo in una procedura del monitor alla volta.
• Nessuna coda esplicita: non c'e una coda associata alle procedure — la politica di scheduling e left to the implementation.

Variabili condizione

Per la sincronizzazione esplicita, i monitor forniscono le variabili condizione con due operazioni:

Discipline di segnalazione

Legenda: S = segnalante, W = processi in waitC, E = processi bloccati sull'entry del monitor.

Produttore-Consumatore con monitor

monitor BoundedBuffer {
  int[] elems := new int[MAX_ELEMS]
  int first := 0, last := 0
  cond notFull, notEmpty

  procedure put(int elem) {
    if ((last + 1) % MAX_ELEMS = first)
      waitC(notFull)
    elems[last] := elem
    last := (last + 1) % MAX_ELEMS
    signalC(notEmpty)
  }

  procedure take(): int {
    if (first = last)
      waitC(notEmpty)
    int elem := elems[first]
    first := (first + 1) % MAX_ELEMS
    signalC(notFull)
    return elem
  }
}

Semafori vs variabili condizione

Implementazione di un semaforo con monitor

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

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

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

I monitor possono essere implementati con semafori: un semaforo mutex per la mutua esclusione, e per ogni variabile condizione un semaforo condsem e un contatore condcount.

Verifica le tue conoscenze