Introdotti da Edsger Dijkstra nel 1968, i semafori sono il piu classico dei meccanismi di coordinazione tra processi: un costrutto semplice ma estremamente potente, in grado di 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 il flusso dei processi (le auto) a seconda della necessita.
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.
Un semaforo S e un tipo di dato composto con due campi:
| Campo | Descrizione |
|---|---|
S.V | Intero ≥ 0 — il "valore" del semaforo |
S.L | Insieme (o coda) di identificatori di processo bloccati |
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")I nomi originali P e V scelti da Dijkstra derivano dal nederlandese e sono ancora usati in molti testi classici (ad esempio nel libro di Ben-Ari). Nella pratica moderna si preferiscono i nomi inglesi wait/signal o acquire/release.
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.
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.
Signal "ricorda": se un processo fa signal(S) quando nessuno e in attesa, il valore di S.V viene incrementato. Un successivo wait(S) da parte di un altro processo trovera il semaforo verde e passera senza bloccarsi. Questa proprieta distingue i semafori da altri meccanismi piu semplici.
Le due operazioni fianco a fianco, nella formulazione compatta vista a lezione:
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 (verde), viene decrementato. Se e 0 (rosso), il processo viene bloccato e aggiunto alla coda S.L.
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>Se nessun processo e in attesa, il valore viene incrementato. Altrimenti, un processo in attesa viene sbloccato (senza incrementare S.V).
L'atomicita delle operazioni wait e signal e il pilastro su cui si regge l'intero meccanismo. Senza atomicita, due processi potrebbero interferire durante il test e la modifica del valore del semaforo, rompendo ogni garanzia.
Ricordate la differenza fondamentale: wait blocca il processo se il semaforo e a zero e lo accoda; signal o incrementa il contatore (se nessuno e in attesa) oppure sblocca un processo dalla coda (senza incrementare). Questa asimmetria e cruciale per capire il comportamento dei semafori come meccanismo di sincronizzazione.
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).
L'invariante del semaforo: S.V = k + #signal(S) - #wait(S) e S.V >= 0 (dove k è il valore iniziale). Questo teorema è fondamentale per la verifica formale dei programmi concorrenti con semafori.
Il professore distingue tre usi principali, che corrispondono a tre valori di inizializzazione diversi:
| Tipo | Valori di S.V | Inizializzazione | Uso tipico |
|---|---|---|---|
| Mutex (binary) | 0, 1 | k = 1 | Mutua esclusione (come un lock): un permesso, un processo per volta |
| Counting (general/resource) | ≥ 0 | k = N | Gestione risorse multiple: ticket per limitare l'accesso a N processi |
| Event | 0 | k = 0 | Sincronizzazione: un processo segnala un evento, un altro lo aspetta |
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."
Un semaforo e a tutti gli effetti un tipo di dato astratto fornito dalla macchina concorrente. Le tre tipologie nel dettaglio:
Il componente intero può assumere solo due valori: 0 e 1. Tipicamente usato per implementare la mutua esclusione, come un lucchetto (lock): wait acquisisce, signal rilascia. Inizializzato con S = (1, {}), protegge l'accesso a una sezione critica.
Il componente intero può assumere qualsiasi valore ≥ 0. Usato per gestire risorse multiple identiche (es. buffer con N slot, pool di connessioni). Il valore iniziale rappresenta il numero di risorse disponibili: inizializzato con S = (N, {}) dove N e il numero di risorse. E anche detto resource semaphore.
Inizializzato a 0 (S = (0, {})), usato esclusivamente per sincronizzazione tra processi (non per mutua esclusione). Serve a inviare/ricevere un segnale temporale: un processo si blocca in wait finche un altro non fa signal per segnalare che un evento e accaduto.
Rispetto ai lock visti nei moduli precedenti, i semafori sono piu generali: un lock puo fare solo mutua esclusione. Con un semaforo si puo fare sia mutua esclusione che sincronizzazione. Pero proprio per questa generalita, sono anche piu difficili da usare correttamente.
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.
In un semaforo forte, S.L non e un insieme ma una coda FIFO. La wait inserisce in coda, la signal preleva dalla testa. Proprieta importante: no starvation — per qualsiasi numero N di processi, la starvation e impossibile perche i processi vengono serviti in ordine di arrivo.
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 >In un semaforo debole, S.L e un insieme (non ordinato). La signal seleziona un processo arbitrario dall'insieme. Questo significa che non c'e garanzia di assenza di starvation: in teoria, uno scenario sfortunato potrebbe far saltare sempre lo stesso processo e favorire sempre gli altri.
I semafori busy-wait (o spin semaphore) non hanno S.L: non esiste una coda di processi bloccati. Il processo rimane in esecuzione in un ciclo di attesa attiva (spin-loop). Le operazioni sono comunque atomiche.
wait(S) = < await (S.V > 0); S.V := S.V - 1 >
signal(S) = < S.V := S.V + 1 >Non c'e garanzia di freedom from starvation: quando un processo incrementa S.V, non e possibile prevedere quale dei processi in attesa nel ciclo while riuscira per primo a passare. Sono appropriati in sistemi multiprocessore con bassa contesa, dove il costo di un context switch (e quindi di coinvolgere il sistema operativo) e superiore al breve spin-loop.
Il professore avverte: con busy-wait non ho nessuna garanzia di freedom from starvation. Quando incremento, se ci sono piu processi in while loop, non posso prevedere chi passera per primo. E soggetto a starvation.
Una motivazione ulteriore per i busy-wait semaphore: in un sistema multiprocessore il processo in attesa ha il proprio processore e non spreca CPU utilizzabile da altri.
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 }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:
<p2,q2,_>
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
La dimostrazione formale si basa sulla costruzione del grafo degli stati ridotto: lo stato del semaforo fa parte del tuple di stato. Si parte da (p1, q1, S.V=1, S.L={}) e si esplorano tutte le transizioni possibili. La mutua esclusione e verificata se nessuno stato raggiungibile contiene entrambi i processi in CS.
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.
Un secondo punto di vista, per esplorare passo passo gli stati del sistema (compresi quelli in cui un processo e bloccato su S.L):
La soluzione con semaforo debole per N processi NON e immune da starvation. Il docente lo sottolinea: per N processi, se la lista S.L e un insieme, un processo potrebbe essere saltato indefinitamente.
Il diagramma di stato completo dei due processi (con le locazioni p1..p4 e q1..q4) puo essere esplorato in modo interattivo:
La soluzione per due processi e banale; funziona anche per N processi, ma senza garanzia di assenza di starvation se il semaforo e debole.
La soluzione con semafori per la sezione critica vale per N processi (non solo 2). Tuttavia, con semaforo debole e N > 2, si perde la garanzia di freedom from starvation: un processo potrebbe essere sempre scavalcato.
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".
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 metaflowchart 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"]
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.
Durante la lezione, uno studente identifica un bug interessante: se il comportamento e ciclico (cioe sort1, sort2 e merge si ripetono), e se sort1 e sort2 eseguono signal due volte in un ciclo, allora merge ha "diritto" di passare due volte. Questo puo causare un disallineamento che porta a situazioni di blocco. Il professore commenta che e un bug "terribile, nel senso da identificare, che nasce proprio dalle ot..." (dal comportamento ciclico).
Il problema Producer-Consumer e un esempio classico di sincronizzazione (di ordine di esecuzione), onnipresente in informatica. Due tipi di processi cooperano: i produttori creano dati e li inviano, i consumatori li ricevono e li elaborano. Esempi concreti:
| Produttore | Consumatore |
|---|---|
| Browser web (richiede pagine) | Linea di comunicazione (le trasmette) |
| Tastiera (genera tasti) | Sistema operativo (li elabora) |
| Word processor (prepara pagine) | Stampante (le stampa) |
| Programma di gioco (rende frame) | Schermo (li visualizza) |
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.
Nella realta i buffer sono finiti. Con un buffer limitato (dimensione N), 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, inizializzato a N.
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).
L'invariante dei due semafori divisi: availItems.V + availPlaces.V = N. Quando il produttore wait(availPlaces), riduce i posti liberi e automaticamente aumenta la probabilita che il consumatore possa lavorare, e viceversa.
Il pattern del semaforo counting inizializzato a N per implementare un numero di ticket e applicabile in molti contesti. "Ogni volta che devo implementare una situazione in cui voglio fare in modo che qualcuno prenda un ticket per poter fare qualcosa, perche voglio limitare il numero di processi, penso a un semaforo counting o resource, inizializzato al numero di ticket: quando ti serve devi fare wait, quando hai finito lo devi restituire con signal."
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)La stessa soluzione con le locazioni etichettate e i commenti riga per riga:
// 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)
}wait(mutex) e wait(availPlaces), si puo incorrere in deadlock.
Ordine delle wait: prima si fa wait sul semaforo di sincronizzazione (availPlaces/availItems), e poi sul mutex. Invertire questo ordine porta a deadlock: un produttore potrebbe tenere il mutex mentre e bloccato in attesa di un posto libero, impedendo al consumatore di entrare per svuotare il buffer. Il professore sottolinea inoltre: "Se vi dimenticate una signal, si blocca tutto. E molto delicato."
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):
Gli invarianti da rispettare (dove nR e il numero di lettori attivi e nW quello degli scrittori) sono:
nR ≥ 0
nW = 0 oppure nW = 1
(nR > 0 → nW = 0) ∧ (nW = 1 → nR = 0)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.
Un primo tentativo con un singolo semaforo lock serializza tutti gli accessi, anche quelli dei reader. Inutile: serve permettere ai reader di lavorare in parallelo.
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.
Come funziona, in sintesi: 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.
Una soluzione piu semplice ma over-constrained userebbe un singolo semaforo per serializzare tutto, impedendo anche la lettura concorrente — sacrificando le prestazioni.
Questa soluzione da priorita ai reader: se arrivano reader continuamente, i writer potrebbero soffrire di starvation (non riescono mai a ottenere rw). Esistono varianti con priorita ai writer o eque (alternate), ma la struttura di base e questa. E importante capire il ruolo di nr: e il contatore che permette ai reader di condividere rw.
Notate la sottigliezza: se si usasse un unico semaforo per serializzare tutto (una soluzione over-constraining), si perderebbe il vantaggio della lettura concorrente. Il vero problema dei lettori-scrittori e bilanciare il throughput dei lettori con l'equita verso gli scrittori.
Un lock serve solo per la mutua esclusione. Un semaforo e piu generale: puo essere usato sia per mutua esclusione (semaforo binario inizializzato a 1) sia per sincronizzazione (event semaphore inizializzato a 0) sia per gestire risorse multiple (counting semaphore inizializzato a N). I lock sono un sottoinsieme dei semafori, non viceversa: "un lock si puo fare con i semafori".
Dato un valore iniziale k per S.V: S.V = k + #signal(S) - #wait(S) e S.V ≥ 0. Dove #signal(S) e il numero di operazioni signal completate e #wait(S) il numero di wait completate con successo (un processo che si blocca durante la wait non viene contato).
In un semaforo forte, l'insieme S.L dei processi bloccati e organizzato come coda FIFO: la wait inserisce in coda, la signal preleva dalla testa. Questo garantisce no starvation per qualsiasi numero N di processi. In un semaforo debole, S.L e un insieme non ordinato e la signal seleziona un processo arbitrario — non c'e garanzia di assenza di starvation.
Il mutex e inizializzato a 1 e usato per la mutua esclusione (lock). L'event semaphore e inizializzato a 0 e usato per la sincronizzazione (segnalazione). Con un mutex, la prima wait decrementa da 1 a 0; con un event semaphore, la prima wait blocca il processo perche il valore e gia 0. Un mutex puo essere visto come un semaforo counting ristretto a {0,1}.
Due semafori che insieme mantengono un invariante fisso. L'esempio classico e il bounded buffer: availItems + availPlaces = N. availItems conta gli elementi disponibili (inizializzato a 0), availPlaces conta i posti liberi (inizializzato a N). Quando il produttore aggiunge un elemento: wait(availPlaces), signal(availItems). Quando il consumatore preleva: wait(availItems), signal(availPlaces).
1. Mutua esclusione: la risorsa non puo essere usata da piu processi contemporaneamente.
2. Hold and wait: i processi che detengono risorse possono richiederne altre.
3. No preemption: le risorse non possono essere rimosse forzatamente.
4. Circular wait: esiste una catena circolare di processi che attendono risorse detenute da altri nella catena.
Tutte e quattro devono essere vere perche si verifichi deadlock.
Due soluzioni classiche: 1) Ticket (N-1): si introduce un semaforo counting inizializzato a N-1 (4 per 5 filosofi) che limita il numero di filosofi che possono tentare di mangiare contemporaneamente. 2) Ordinamento totale: ogni filosofo acquisisce le forchette in ordine crescente di indice (first = min(i, i+1); second = max(i, i+1)). Entrambe rompono la condizione di circular wait.
Assegnare un ordine totale a tutti i lock e acquisirli sempre nello stesso ordine in tutti i punti del codice. Questo rende impossibile la condizione di circular wait, una delle quattro condizioni necessarie di Coffman. E una regola semplice ma estremamente efficace: se ogni processo acquisisce i lock in ordine crescente, non si puo formare un ciclo di attesa.
wait su semaforo puo non bloccare (se S.V > 0); waitC su variabile condizione blocca sempre (dopo aver rilasciato il lock del monitor). signal su semaforo ha sempre effetto (incrementa S.V o sblocca); signalC non ha effetto se la coda e vuota. signal sblocca un processo arbitrario; signalC sblocca il processo in testa alla coda FIFO. Un processo sbloccato da signal puo proseguire subito; con signalC la ripresa dipende dalla signaling discipline.
Signal & Continue (non-preemptive): il signaller continua la sua esecuzione, il signalled riprendera in un momento successivo. Priorita: processi esterni (E) < processi in attesa su condizione (W) < signaller (S). Signal & Wait (preemptive): il signalled viene eseguito immediatamente, il signaller si mette in attesa e competera ad armi pari con i processi esterni. Priorita: E = S < W. Signal & Urgent Wait: come Signal & Wait, ma il signaller ha priorita sui processi esterni (E < S < W).
Signal & Continue (E < W < S): chi segnala continua, il risvegliato aspetta. Signal & Wait (E = S < W): il risvegliato parte subito, il segnalante aspetta. Signal & Urgent Wait (E < S < W): come S&W ma il segnalante ha priorita sugli altri in attesa di entrare. La scelta influenza se usare if o while per il test della condizione: con S&C il while e obbligatorio.
Safety (operatore [], "sempre"): "le cose cattive non accadono mai". Esempio: [] ¬(p3 ∧ q3) — mai due processi contemporaneamente nella sezione critica. Liveness (operatore <>, "eventualmente"): "le cose buone prima o poi accadono". Esempio: [](p2 → <> p3) — se un processo vuole entrare in CS, prima o poi ci riuscira. Le safety si verificano trovando un singolo stato violatore; le liveness richiedono l'analisi di scenari completi.
Perche lo stesso input puo produrre output diversi a seconda dello scenario di interleaving. Alcuni scenari possono essere corretti, altri no. Eseguire il programma una volta testa un solo scenario, e scelte diverse dello scheduler possono mascherare i bug (fenomeno degli heisenbug). Servono tecniche formali come il model checking o la dimostrazione induttiva di invarianti. Inoltre, il codice di test stesso puo introdurre artefatti di temporizzazione che mascherano i bug.