Semafori, Monitor, Modellazione e Verifica di Programmi Concorrenti

1. Modellare l'esecuzione concorrente

Il primo passo per comprendere un programma concorrente e costruirne un modello. Un modello e una descrizione rigorosa della struttura e del comportamento del sistema a un adeguato livello di astrazione: include le informazioni rilevanti e tralascia gli aspetti secondari. I modelli servono sia per la progettazione (rappresentazioni diagrammatiche) sia per la verifica formale.

Il modello standard per l'esecuzione concorrente si basa su tre assunzioni fondamentali:

• Ogni processo e una sequenza di azioni atomiche, ciascuna corrispondente all'esecuzione atomica di un'istruzione.
• Speed independence assumption: non si fa alcuna ipotesi sulla velocita relativa dei processi. L'esecuzione concorrente e modellata come una sequenza di azioni ottenuta interlacciando (interleaving) arbitrariamente le azioni atomiche dei processi.
• Un singolo processore astratto globale esegue tutte le azioni, una alla volta.

In questo modello, il puntatore di controllo (control pointer) di un processo indica la prossima istruzione eseguibile. Una computazione (o scenario) e una sequenza di esecuzione che puo verificarsi come risultato dell'interleaving. Uno stato e definito da una tupla composta da: un'etichetta per ogni processo (la prossima istruzione da eseguire) e un valore per ogni variabile globale o locale.

Numero di scenari

Il numero di possibili scenari cresce in modo combinatorio. Per due processi con n azioni ciascuno, il numero di scenari possibili e il coefficiente binomiale centrale C(2n, n). La tabella seguente mostra la crescita:

Con 3 processi il numero esplode ancora di piu: con 2 azioni ciascuno si hanno gia 90 scenari possibili. Questo rende evidente perche il testing tradizionale non basta per programmi concorrenti: ogni esecuzione puo seguire uno scenario diverso.

flowchart LR
  subgraph P[Processo P]
    p1["p1: n := k1"]-->p2["p2: (fine)"]
  end
  subgraph Q[Processo Q]
    q1["q1: n := k2"]-->q2["q2: (fine)"]
  end
  INIT["
n=0, k1=1, k2=2
P=p1, Q=q1"]-->p1
  INIT-->q1
  p1-->|"n=1"|Q
  q1-->|"n=2"|P
  Q-->q2
  P-->p2

2. Atomicita e la sua importanza

Il concetto di atomicita e fondamentale. Un'azione atomica viene eseguita fino al completamento senza possibilita di interleaving con altre azioni. Il professore sottolinea che la scelta di cosa considerare atomico e cruciale per la correttezza del modello.

Incremento atomico vs non-atomico

Consideriamo due processi che eseguono n := n + 1 in concorrenza, con n = 0 iniziale.

Strutture non atomiche

Per i tipi di dato astratti non atomici si distinguono due tipi di stato: lo stato interno (significativo per chi definisce la classe) e lo stato esterno (significativo per chi usa la classe). La corrispondenza tra stati interni ed esterni e parziale: esistono stati interni senza corrispondente stato esterno, detti inconsistenti. In programmazione sequenziale questo non e un problema grazie all'information hiding. In programmazione concorrente, invece, e necessario introdurre meccanismi che garantiscano che i processi lavorino sempre su dati in stati consistenti.

flowchart LR
  subgraph HW["A livello macchina (stack)"]
    P1["P: push n"]-->P2["P: push #1"]
    P2-->P3["P: add"]
    P3-->P4["P: pop n"]
  end
  subgraph HW2[" "]
    Q1["Q: push n"]-->Q2["Q: push #1"]
    Q2-->Q3["Q: add"]
    Q3-->Q4["Q: pop n"]
  end

3. Correttezza: safety, liveness e fairness

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

Safety properties

Una proprieta di safety deve essere sempre vera: deve valere in ogni stato di ogni computazione. Si esprimono come invarianti della computazione. Tipicamente specificano che le "cose cattive" non devono mai accadere:

• Mutua esclusione: mai piu di un processo nella sezione critica.
• Assenza di deadlock: nessun processo rimane bloccato ad attendere un evento che non puo verificarsi.

Liveness properties

Una proprieta di liveness deve diventare vera prima o poi: in ogni computazione esiste uno stato in cui la proprieta e vera. Tipicamente specificano che le "cose buone" prima o poi accadono:

• Assenza di starvation: un processo alla fine ottiene la risorsa che gli serve.
• Assenza di dormanza: un processo in attesa viene prima o poi risvegliato.
• Comunicazione affidabile: un messaggio inviato viene prima o poi ricevuto.

Fairness

La fairness e una proprieta di liveness che richiede che qualcosa di buono accada infinite volte. Dipende dalla politica di scheduling. Il professore distingue tre livelli:

4. Il problema della sezione critica

Introdotto da Dijkstra nel 1965, il Critical Section Problem e uno dei problemi piu importanti e studiati nella programmazione concorrente, nel contesto della competizione fra processi. Abbiamo N processi, ciascuno esegue in ciclo infinito una sequenza di istruzioni divisibile in due parti: la sezione critica (CS) e la sezione non critica (NCS). Ogni sezione critica e tipicamente una sequenza di istruzioni che accede a un oggetto condiviso.

Il compito e progettare protocolli di ingresso (entry/pre-protocol) e di uscita (exit/post-protocol) che soddisfino le seguenti proprieta:

Primo tentativo: variabile turn

Si introduce una variabile condivisa turn che funge da "permesso": se turn = 1, tocca a P; se turn = 2, tocca a Q. Entrambi i processi attendono che turn assuma il proprio valore.

Verifica tramite diagramma di stato: la mutua esclusione e soddisfatta (non si raggiunge mai p3 ∧ q3), l'assenza di deadlock e soddisfatta, ma la starvation e possibile: se un processo rimane indefinitamente nella NCS, l'altro non potra mai entrare nella CS perche turn non cambiera mai. La soluzione non e corretta.

5. Algoritmi di Dekker e Peterson

Dopo vari tentativi (secondo tentativo con variabili wantp/wantq che viola la mutua esclusione; terzo tentativo che soffre di deadlock; quarto tentativo che soffre di starvation per interleaving perfetto), si arriva alla soluzione finale.

Algoritmo di Dekker (1965)

Scoperto dal matematico olandese T.J. Dekker, combina il primo e il quarto tentativo: il diritto di insistere per entrare (non il diritto di entrare) viene passato esplicitamente tra i processi tramite la variabile turn. L'algoritmo soddisfa mutua esclusione, assenza di deadlock e assenza di starvation.

Algoritmo di Peterson (1981)

Piu conciso della soluzione di Dekker, collassa le due await in una singola condizione composta:

boolean wantp = false, wantq = false;
int turn = 1;

// Processo P
loop forever {
  p1: NCS
  p2: wantp = true
  p3: turn = 2
  p4: await (!wantq || turn == 1)
  p5: CS
  p6: wantp = false
}

// Processo Q
loop forever {
  q1: NCS
  q2: wantq = true
  q3: turn = 1
  q4: await (!wantp || turn == 2)
  q5: CS
  q6: wantq = false
}

Peterson funziona su qualsiasi architettura che fornisca load e store come istruzioni atomiche. La dimostrazione di correttezza puo essere fatta costruendo il diagramma di stato ridotto (solo le etichette rilevanti per la sincronizzazione) e verificando le tre proprieta.

6. Test-and-set e lock hardware

Il problema della sezione critica puo essere enormemente semplificato se la macchina concorrente fornisce istruzioni atomiche composte. Le principali sono:

• test-and-set (x, r): < r := x, x := 1 >
• exchange
• fetch-and-add
• compare-and-swap (CAS)

Con test-and-set, la sezione critica per N processi diventa semplice:

int lock = 0;

// Processo P
loop forever {
  p1: NCS
  repeat {
    p2: test_and_set(lock, was_locked)
    p3: } until (was_locked == 0)
  p4: CS
  p5: lock = 0
}

Questo meccanismo realizza un lock elementare: due operazioni atomiche, acquire e release. In Java, il blocco synchronized fornisce esattamente questa astrazione: due blocchi synchronized(lock) sullo stesso oggetto non possono essere interlacciati.

Algoritmo del panificio (Bakery algorithm)

Un'alternativa per N processi basata sui "ticket": ogni processo prende un numero e attende il proprio turno. Problema: i contatori turn e num crescono monotonamente, con possibile overflow aritmetico.

7. Verifica formale e LTL

Il testing rivela la presenza di errori solo per scenari selezionati; la verifica dimostra che una proprieta vale per tutti gli scenari possibili. Servono tecniche formali.

La logica temporale lineare (LTL), introdotta da Amir Pnueli nel 1977, permette di esprimere proprieta di correttezza che devono valere in tutti gli stati di tutte le computazioni. I due operatori fondamentali sono:

• [] 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.

Esempi di specifica LTL

Operatori derivati

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

8. Model checking: SPIN, JPF, TLA+

Il model checking e la tecnica piu importante per la verifica automatica di proprieta di correttezza dei sistemi concorrenti. La strategia: esplorare esaustivamente l'intero spazio degli stati del sistema e verificare se certe proprieta sono soddisfatte. Se il sistema viola la proprieta, il model checker produce una traccia (controesempio) utile per identificare i bug.

SPIN e PROMELA

SPIN e un model checker ampiamente usato in ambito accademico e industriale. PROMELA e il linguaggio per scrivere i modelli. Permette di specificare processi concorrenti con un insieme limitato di costrutti, sufficienti per costruire modelli astratti del sistema.

Java Path Finder (JPF)

JPF e un model checker specializzato per programmi Java, sviluppato dalla NASA per software critico. E' una JVM speciale che esegue il programma lungo tutti i possibili scenari (percorsi di esecuzione), verificando violazioni di proprieta come deadlock ed eccezioni non catturate. Se trova un errore, JPF riporta l'intera esecuzione che porta all'errore.

TLA+ e PlusCal

TLA+ (Temporal Logic of Actions) e un linguaggio di specifica formale introdotto da Leslie Lamport. Permette di descrivere sia le proprieta di correttezza desiderate (il "cosa") sia il progetto del sistema (il "come"). Usato in contesti reali come Amazon Web Services. PlusCal (ex +CAL) e un linguaggio algoritmico basato su TLA+ che viene tradotto in specifiche TLA+ e verificato con il model checker TLC.

9. Semafori: tipo di dato e operazioni

I semafori sono stati introdotti da Dijkstra nel 1968 come costrutto generale-purpose potente ma semplice, in grado di risolvere quasi qualsiasi problema di mutua esclusione e sincronizzazione. L'analogia usata dal professore e quella del semaforo stradale: blocca e sblocca il flusso dei processi (le auto) a seconda della necessita.

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

• S.V: intero >= 0 (il valore del semaforo)
• S.L: insieme di identificatori di processo (la coda dei processi bloccati)

Si inizializza con S = (k, {}), dove k >= 0 e il valore iniziale di S.V e {} l'insieme vuoto per S.L. Fornisce due operazioni atomiche:

Operazione wait(S) — anche chiamata P(S)

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

Se il valore del semaforo e > 0 (semaforo "verde"), viene semplicemente decrementato. Altrimenti (semaforo "rosso"), il processo viene bloccato e aggiunto a S.L.

Operazione signal(S) — anche chiamata V(S)

signal(S) = <
  if (S.L = {})
    S.V = S.V + 1
  else
    let q = elemento arbitrario di S.L
    S.L = S.L - {q}
    q.state = ready
>

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

10. Classificazione dei semafori

I semafori si classificano secondo diversi criteri. Il professore presenta tre dimensioni principali:

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

11. Semafori per mutua esclusione e sincronizzazione

I semafori sono costrutti primitivi utilizzabili come mattoncini di basso livello per risolvere quasi qualsiasi problema di interazione tra processi in architettura a memoria condivisa. Due grandi famiglie di utilizzo:

Mutua esclusione

Il caso piu semplice: un semaforo binario inizializzato a 1 funge da lock. Ogni processo esegue wait(S) prima di entrare nella CS e signal(S) dopo averla lasciata. La soluzione per due processi e banale; funziona anche per N processi, ma senza garanzia di assenza di starvation se il semaforo e debole.

Sincronizzazione (event semaphore)

Un semaforo inizializzato a 0 puo essere usato per inviare/ricevere un segnale temporale. Esempio classico: il merge sort concorrente.

Supponiamo di avere tre processi: sort1 ordina la prima meta dell'array e fa signal(S1); sort2 ordina la seconda meta e fa signal(S2); merge fa wait(S1) e wait(S2) e poi fonde le due meta. I semafori S1 e S2 sono event semaphore (inizializzati a 0). Il processo merge si blocca automaticamente fino a quando entrambi i sort non hanno completato.

flowchart LR
  A["Array A"]-->P1
  P1["sort1: ordina 1a meta"]-->|"signal(S1)"|S1
  A-->P2
  P2["sort2: ordina 2a meta"]-->|"signal(S2)"|S2
  S1-->R1["wait(S1)"]
  S2-->R2["wait(S2)"]
  R1-->M
  R2-->M
  M["merge: fonde le due meta"]-->OUT["Array A ordinato"]

12. Producer-Consumer con semafori

Il problema Producer-Consumer e un esempio classico di problema di ordine di esecuzione. Due tipi di processi: i produttori creano dati e li inviano ai consumatori; i consumatori ricevono dati e li elaborano. Pattern onnipresente in informatica: browser-server, tastiera-SO, word processor-stampante, ecc.

Buffer infinito

Con buffer infinito c'e una sola interazione da sincronizzare: il consumatore non deve prelevare da un buffer vuoto. Invariante: nAvailItems.V = #elementi nel buffer. Si usa un resource semaphore availItems inizializzato a 0.

// Produttore
loop forever {
  p1: Item el = produce()
  p2: append(buffer, el)
  p3: signal(availItems)
}

// Consumatore
loop forever {
  q1: wait(availItems)
  q2: Item el = take(buffer)
  q3: consume(el)
}

Buffer limitato

Con buffer limitato (dimensione N), si aggiunge un'altra sincronizzazione: il produttore non deve scrivere in un buffer pieno. Si introducono due semafori split: availItems (elementi disponibili) e availPlaces (posti disponibili), inizializzato a N. Invariante: availItems + availPlaces = N.

Produttori e consumatori multipli

Se ci sono piu produttori e piu consumatori, le operazioni di append e take sul buffer non sono atomiche. Serve un semaforo mutex aggiuntivo per garantire la mutua esclusione sull'accesso al buffer condiviso. L'ordine delle operazioni e importante: prima si attendono i semafori di sincronizzazione, poi si acquisisce il mutex.

// Produttore
loop forever {
  p1: Item el = produce()
  p2: wait(availPlaces)   // aspetta un posto libero
  p3: wait(mutex)         // entra in sezione critica
  p4: append(buffer, el)
  p5: signal(mutex)
  p6: signal(availItems)  // segnala un nuovo elemento
}

// Consumatore
loop forever {
  q1: wait(availItems)    // aspetta un elemento
  q2: wait(mutex)
  q3: Item el = take(buffer)
  q4: signal(mutex)
  q5: signal(availPlaces) // segnala un posto libero
  q6: consume(el)
}

13. Deadlock e Filosofi a Cena

Il problema dei Filosofi a Cena (Dining Philosophers) e stato originato da un problema d'esame di Dijkstra nel 1971 su 5 computer in competizione per 5 unita a nastro, ed e stato trasformato nella versione attuale da Tony Hoare. Cinque filosofi siedono a un tavolo con 5 piatti e 5 forchette; nel centro c'e una ciotola di spaghetti. Ogni filosofo alterna pensiero e mangiare, ma per mangiare servono due forchette (la sinistra e la destra), e puo raccoglierne solo una alla volta.

Primo tentativo: un semaforo per forchetta

Ogni forchetta e modellata come un semaforo binario. Purtroppo questa soluzione deadlocka: se tutti i filosofi raccolgono la forchetta sinistra prima che qualcuno provi a raccogliere la destra, nessuno puo mai mangiare.

semaphore[] fork = [1, 1, 1, 1, 1];

// Filosofo i
loop forever {
  think()
  wait(fork[i])             // forchetta sinistra
  wait(fork[(i+1) % N])     // forchetta destra
  eat()
  signal(fork[i])
  signal(fork[(i+1) % N])
}

Condizioni di Coffman per il deadlock

Il deadlock si verifica solo quando tutte e quattro le seguenti condizioni sono soddisfatte simultaneamente:

1. Mutua esclusione: una risorsa non puo essere usata da piu processi contemporaneamente.
2. Hold and wait: processi che gia detengono risorse possono richiederne di nuove.
3. No preemption: nessuna risorsa puo essere rimossa forzatamente da un processo che la detiene.
4. Circular wait: due o piu processi formano una catena circolare, dove ciascuno attende una risorsa detenuta dal successivo.

Soluzioni

Il professore presenta due soluzioni classiche:

Soluzione 1: ticket (N-1 posti). Si limita il numero di filosofi che possono mangiare simultaneamente a N-1 (4 su 5), introducendo un semaforo ticket inizializzato a N-1. Questo garantisce liveness.

Soluzione 2: rompere la catena (ordinamento delle forchette). L'ultimo filosofo (o tutti) raccolgono le forchette in ordine inverso: prima la destra, poi la sinistra. Equivalentemente, si assegna un ordinamento totale alle risorse (alle forchette) e si acquisiscono sempre nello stesso ordine. Questo rende impossibile il circular wait.

semaphore[] fork = [1, 1, 1, 1, 1];

// Filosofo i — soluzione con ordinamento
int first = min(i, (i+1) % N);
int second = max(i, (i+1) % N);

loop forever {
  think()
  wait(fork[first])    // forchetta con indice minore
  wait(fork[second])   // forchetta con indice maggiore
  eat()
  signal(fork[first])
  signal(fork[second])
}

Deadlock detection e recovery

Nelle basi di dati, il deadlock viene gestito con detection and recovery: si analizza il grafo delle dipendenze "is-waiting" cercando cicli; se trovato, si seleziona una vittima e si abortisce la transazione. In JVM non esiste alcun meccanismo automatico: se i thread deadlockano, la soluzione e solo lo shutdown dell'applicazione. Esiste solo supporto "post-mortem" per la diagnosi.

14. Readers-and-Writers

Il problema dei lettori e scrittori (Courtois, Heymans, Parnas, 1971) e simile alla mutua esclusione, ma divide i processi in due classi: i lettori (che devono escludere gli scrittori ma non altri lettori) e gli scrittori (che devono escludere sia lettori che altri scrittori). E l'astrazione dell'accesso a un database: non c'e pericolo se piu processi leggono simultaneamente, ma la scrittura deve essere in mutua esclusione.

Invarianti del problema

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

dove nR e il numero di lettori e nW il numero di scrittori.

Primo tentativo (over-constrained)

Usare un singolo semaforo rw come lock esclusivo per tutti. Funziona ma serializza anche i lettori, perdendo il vantaggio della lettura concorrente.

Soluzione corretta

I lettori non usano lo stesso lock degli scrittori. Si introduce un mutexR per proteggere il contatore dei lettori nr. Il semaforo rw viene acquisito solo dal primo lettore (quando nr == 0) e rilasciato solo dall'ultimo lettore (quando nr == 0 dopo il decremento).

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

// Lettore
loop forever {
  wait(mutexR)
  if (nr == 0) wait(rw)
  nr = nr + 1
  signal(mutexR)
  Item el = read(dbase)
  wait(mutexR)
  nr = nr - 1
  if (nr == 0) signal(rw)
  signal(mutexR)
}

// Scrittore
loop forever {
  wait(rw)
  write(dbase, el)
  signal(rw)
}

15. Monitor: astrazione di coordinamento

I semafori sono potenti ma di basso livello: programmi soggetti a errori, difficili da usare in programmi complessi. Per questo si introducono i monitor, un costrutto di piu alto livello introdotto da Brinch Hansen (1973) e generalizzato da Hoare (1974).

Un monitor e un'astrazione di dati della programmazione concorrente che incapsula:

• lo stato (variabili permanenti)
• le operazioni (procedure)
• la politica di concorrenza (sincronizzazione e mutua esclusione)

E' una generalizzazione del concetto di kernel dei sistemi operativi (versioni decentrate del monolitico kernel) e del concetto di oggetto nella OOP (classi che incapsulano dati + operazioni + politica di sincronizzazione/mutex).

Proprieta fondamentali

• Mutua esclusione intrinseca: le procedure del monitor si eseguono con mutua esclusione. Al massimo una procedura puo essere attiva alla volta. I processi che trovano il monitor occupato vengono sospesi.
• Sincronizzazione esplicita: attraverso variabili di condizione (condition variables), usate per ritardare un processo che non puo continuare fino a quando lo stato del monitor non soddisfa una certa condizione booleana.

Sintassi astratta

monitor MonitorName {
  // dichiarazione variabili permanenti
  // inizializzazione
  // procedure (o entries)
}

Esempio minimo: contatore thread-safe.

monitor Counter {
  int count;

  procedure inc() {
    count = count + 1
  }

  procedure getValue(): int {
    return count
  }
}

Il professore sottolinea che la mutua esclusione e implicita: non richiede l'uso di semafori o altri meccanismi da parte del programmatore. Le operazioni sono eseguite atomicamente le une rispetto alle altre. Non esiste una coda esplicita associata a una procedura del monitor: questo puo portare a starvation.

16. Variabili di condizione e discipline di segnalazione

Le variabili di condizione sono tipi di dato primitivi che permettono di sospendere (waitC) e riprendere (signalC) processi all'interno di un monitor, rappresentando condizioni (eventi) sullo stato del monitor in attesa di essere soddisfatte. Ogni variabile di condizione e associata a una coda FIFO di processi bloccati.

Operazioni

Discipline di segnalazione

Il professore spiega che quando un processo esegue una signalC, si pone il problema di chi debba continuare: il processo che segnala o quello che viene risvegliato? Le tre discipline classiche sono:

Conseguenza pratica: if vs while

A seconda della disciplina di segnalazione, il test sulla condizione dopo un waitC puo essere un if o un while: l'uso del while e sempre sicuro ed e necessario con Signal and Continue perche la condizione potrebbe essere cambiata da un altro processo tra il risveglio e la riacquisizione del lock.

// Con Signal and Wait (preemptive): if basta (ma while e sempre sicuro)
if (!B) waitC(cond)

// Con Signal and Continue: while necessario!
while (!B) waitC(cond)

17. Monitor: esempi pratici

Il professore dedica ampio spazio a mostrare come i monitor vengono usati per realizzare componenti di sincronizzazione riutilizzabili.

Synchronized Cell

Una cella che permette a un processo di depositare un valore e a un altro di prelevarlo, con sincronizzazione automatica:

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

Semaforo implementato con monitor

BoundedBuffer (Producer-Consumer) 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
  }
}

Read-Write Lock con monitor

monitor RWLock {
  int nr = 0, 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 || nw > 0)
      waitC(okToWrite)
    nw = nw + 1
  }

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

Implementazione dei monitor tramite semafori

I monitor possono essere realizzati usando semafori (il professore mostra sia la semantica Signal and Continue che Signal and Wait). L'idea base: un semaforo mutex per la mutua esclusione; per ogni variabile di condizione, un semaforo condsem e un contatore condcount.

18. Confronto: Semafori vs Variabili di Condizione

Il professore dedica una slide specifica al confronto, che e importante per evitare confusioni:

Verifica le tue conoscenze