Modelli di Esecuzione Concorrente, Correttezza e Sezione Critica

1. Avvisi e organizzazione del corso

Il Prof. Ricci apre la lezione con alcuni avvisi amministrativi. Oltre ai quattro assignment standard, quest'anno viene introdotta una novità pensata per agevolare gli studenti lavoratori: la possibilità di concordare un colloquio personalizzato in cui gli assignment vengono sostituiti o ritagliati su un progetto reale legato all'attività lavorativa dello studente.

Il docente ricorda che le lezioni vengono regolarmente registrate e messe a disposizione proprio per facilitare chi deve organizzarsi in modo flessibile, non solo gli studenti lavoratori.

2. Misurare le performance: speedup, efficienza e legge di Amdahl

Uno degli aspetti fondamentali quando si scrivono programmi concorrenti è capire se l'uso di più thread porta effettivamente a un miglioramento delle prestazioni. Il tempo assoluto di esecuzione è significativo, ma per valutare l'efficacia della parallelizzazione si usano due metriche principali: lo speedup e l'efficienza.

Speedup

Lo speedup S si definisce come il rapporto fra il tempo di esecuzione sequenziale T₁ e il tempo di esecuzione parallelo T_N con N processori:

S = T1 / TN

Uno speedup ideale è lineare: S = N. In pratica è quasi sempre inferiore a causa della parte sequenziale del programma e dei costi di coordinamento.

Legge di Amdahl

La legge di Amdahl pone un limite fondamentale allo speedup ottenibile. Se P è la proporzione del programma che può essere parallelizzata, la parte rimanente (1 − P) è intrinsecamente sequenziale. Lo speedup massimo teorico è:

S = 1 / ((1 - P) + P/N)

Al crescere di N, lo speedup tende a 1 / (1 − P), quindi è la parte sequenziale a dominare il limite massimo.

Efficienza

L'efficienza E normalizza lo speedup rispetto al numero di processori:

E = S / N

L'efficienza ideale è 1 (tutti i processori usati al 100%). Valori inferiori indicano overhead di parallelizzazione, contention o parti sequenziali. In alcuni casi particolari si può osservare uno speedup super-lineare (S > N), ad esempio per effetto della cache.

Fattori che influenzano le misure

Quando si misurano le performance di un programma concorrente, bisogna tenere conto di:

• Altri processi — lanciare il test su una macchina con carico leggero e senza applicazioni pesanti in esecuzione.
• Garbage collector (Java) — il GC può introdurre pause che falsano i tempi. Nelle prime versioni di Java il GC bloccava completamente l'esecuzione («stop-the-world»); nelle versioni moderne è più ottimizzato ma va comunque considerato.
• Tempo di esecuzione sufficientemente lungo — se il test dura pochi millisecondi, i risultati sono dominati da fattori esterni (JIT compilation, scheduling OS).

3. CPU-bound vs IO-bound: esperimenti con i thread

Il docente mostra un esempio pratico chiamato IO-Bound Test per illustrare come il comportamento dei thread cambi radicalmente a seconda del tipo di carico di lavoro.

CPU-bound test

Un worker CPU-bound esegue solo computazione pura: in questo esempio ordina ripetutamente un array per simulare lavoro intensivo sulla CPU. Lanciando più thread CPU-bound su una macchina con, diciamo, 10 core:

• Con 1 thread: il tempo di esecuzione è il massimo (riferimento sequenziale).
• Aumentando i thread fino a 10: il tempo diminuisce linearmente (speedup vicino a N).
• Superati i 10 thread: il tempo si stabilizza o addirittura aumenta per l'overhead di context switch.

Il professore mostra il monitor con Mission Control (o JConsole): si osserva che con 1 thread la CPU usage resta bassa, mentre con più thread sale vicino al 100%, segno che tutti i core sono saturati.

IO-bound test

Un worker IO-bound simula operazioni di input/output (es. sleep, attesa di rete, lettura file). In questo caso i thread passano gran parte del tempo bloccati in attesa. La CPU rimane relativamente scarica anche con molti thread (es. 124 thread mostrano solo 6-9% di CPU usage).

Modello del worker nel test

Il worker nel test è progettato con un ciclo while che alterna casualmente fasi di computazione CPU (ordinamento array) e fasi di I/O (sleep). Questo evita la sincronizzazione perfetta in cui tutti i thread farebbero I/O contemporaneamente, simulando uno scenario più realistico dove alcuni thread computano mentre altri attendono.

// Pseudo-struttura del worker
public void run() {
    while (true) {
        if (casuale()) {
            // Fase CPU-bound: ordina array ripetutamente
            ordinaArray();
        } else {
            // Fase IO-bound: attesa (sleep)
            Thread.sleep(5); // 5 ms di attesa
        }
    }
}

Osservazione con JConsole

Usando JConsole si può monitorare l'utilizzo della CPU in tempo reale. Con workload IO-bound si nota che la CPU rimane poco utilizzata anche con molti thread, mentre con workload CPU-bound si avvicina al 100%. Strumenti più sofisticati come JProfiler (non più open source) o VisualVM permettono di analizzare nel dettaglio il comportamento dei singoli thread, individuando lock contention, thread bloccati e bottleneck di performance.

4. Platform thread e virtual thread in Java

Il docente introduce un tema importante per la programmazione concorrente moderna in Java: la differenza tra thread tradizionali e virtual thread, introdotti come feature preview nelle versioni recenti di Java (Project Loom).

Il docente sottolinea che questa distinzione permette di usare un approccio orientato al problema e al dominio, senza dover ottimizzare manualmente il numero di thread in base all'hardware sottostante.

5. Modelli per programmi concorrenti

In ingegneria del software, i modelli sono descrizioni rigorose della struttura e del comportamento di un programma a un adeguato livello di astrazione. Per i programmi concorrenti, definire modelli appropriati permette di:

• Progettare sistemi complessi con rappresentazioni diagrammatiche.
• Analizzare e verificare formalmente le proprietà del sistema.
• Astrarre dai dettagli di basso livello dell'implementazione reale.

Il modello a interleaving

Il modello classico per l'esecuzione concorrente si basa su due assunzioni fondamentali:

1. Ogni processo è una sequenza di azioni atomiche — ogni azione corrisponde all'esecuzione atomica di un'istruzione.
2. Indipendenza dalla velocità (speed independence) — l'esecuzione concorrente è modellata come una sequenza di azioni ottenuta interlacciando arbitrariamente le azioni atomiche dei processi.

In pratica si immagina un singolo processore globale astratto che esegue tutte le azioni, una dopo l'altra, in un ordine non determinato a priori. Una computazione o scenario è una sequenza di esecuzione che può effettivamente verificarsi come risultato dell'interleaving.

6. Hardware parallelo e tassonomia di Flynn

La lezione richiama le basi hardware della programmazione concorrente, già introdotte nel modulo 1.1. L'evoluzione hardware ha reso la programmazione concorrente non più un'opzione ma una necessità.

Tassonomia di Flynn

La tassonomia di Flynn classifica i sistemi di calcolo in base al numero di flussi di istruzioni e di dati:

Sottocategorie MIMD

I sistemi MIMD si dividono ulteriormente in base all'organizzazione della memoria:

La memoria condivisa si distingue in SMP (Symmetric Multi-Processing, accesso uniforme) e NUMA (Non-Uniform Memory Access, accesso non uniforme). La memoria distribuita include MPP (Massively Parallel Processors), cluster e grid.

Architetture moderne: core ibridi e molti-core

I processori moderni combinano core di diverso tipo:

• P-cores (Performance-cores) — frequenza elevata, massime prestazioni.
• E-cores (Efficient-cores) — più piccoli, minor consumo, per task in background.
• Esempi: Intel Core i9 14th gen (8 P-core + 16 E-core), AMD Zen 5 con chiplet design, Apple Silicon M5 con CPU, GPU, NPU integrati.

Esistono inoltre sistemi dedicati all'AI (es. Cerebras CS-3), supercomputer come Fugaku (7,6 milioni di core), e infrastrutture cloud come AWS EC2, Microsoft Azure, Google App Engine.

7. Interazione fra processi

Ogni programma concorrente non banale si basa su processi che interagiscono. Si distinguono tre tipi fondamentali di interazione:

Race condition

Una race condition si verifica quando due o più processi accedono e modificano risorse condivise contemporaneamente e il risultato finale dipende dall'ordine specifico in cui gli accessi avvengono.

Situazioni critiche

Gli errori nei programmi concorrenti possono portare a tre situazioni critiche principali:

L'analogia del latte e del frigo

Il docente (e le slide) riportano la classica analogia di Alice e Bob che devono comprare il latte quando finisce. Senza coordinamento, possono verificarsi scenari in cui:

• Nessuno compra il latte (entrambi pensano che l'altro lo farà).
• Entrambi comprano il latte (spreco).
• Con bigliettini sul frigo: se i controlli non sono atomici, possono comunque verificarsi errori (Alice guarda, va in bagno, Bob guarda, non vede biglietto, compra latte, Alice torna e compra latte).

Questa analogia illustra chiaramente il problema della sezione critica: servono protocolli di ingresso e uscita per garantire l'accesso esclusivo a una risorsa condivisa.

8. Il modello a interleaving

Il modello base per l'esecuzione concorrente considera ogni processo come una sequenza di azioni atomiche. L'esecuzione concorrente è ottenuta interlacciando arbitrariamente le azioni dei processi, come se ci fosse un unico processore globale che esegue tutto in sequenza.

Primo esempio: assegnazione concorrente

p:                            q:
  integer k1 := 1               integer k2 := 2
  p1: n := k1                   q1: n := k2

  integer n := 0   (variabile globale)

Con due processi e un'azione ciascuno, ci sono solo 2 scenari possibili:

1. p1, q1 ⇒ n finale = 2
2. q1, p1 ⇒ n finale = 1

Il risultato finale dipende dall'ordine di esecuzione delle due azioni atomiche.

Questo esempio fondamentale mostra che lo stesso input può produrre output diversi a seconda dello scenario di interleaving. È questa la radice della difficoltà della programmazione concorrente.

9. Diagrammi di stato ed esplosione degli scenari

L'esecuzione di un programma concorrente può essere rappresentata formalmente con stati e transizioni. Uno stato è definito da una tupla che include:

• Un elemento per ogni processo: l'etichetta (istruzione corrente) a cui si trova il control pointer.
• Un elemento per ogni variabile globale o locale: il valore corrente.

C'è una transizione tra due stati s1 e s2 se l'esecuzione di un'istruzione in s1 porta allo stato s2. Il diagramma di stato contiene tutti gli stati raggiungibili del programma. Gli scenari sono cammini orientati nel diagramma a partire dallo stato iniziale. I cicli rappresentano la possibilità di computazione infinita.

Esempio: due processi con due azioni ciascuno

p:                q:
  p1: print("p1")   q1: print("q1")
  p2: print("p2")   q2: print("q2")

Ci sono 6 scenari possibili. Il diagramma di stato ha 9 stati (considerando anche gli stati intermedi e finali).

Combinatoria degli scenari

Il numero di scenari cresce esplosivamente con il numero di azioni e di processi. La formula generale per m processi ciascuno con n azioni è:

Numero scenari = (m * n)! / (n!)^m

Ecco alcuni valori illustrativi:

Questa crescita esponenziale (chiamata esplosione degli scenari) è uno dei problemi fondamentali della verifica dei programmi concorrenti.

10. L'importanza di essere atomici

Una delle questioni più delicate nella modellazione concorrente è cosa si considera atomico. Il docente mostra la differenza cruciale tra un incremento atomico e uno non atomico.

p: n := n + 1
q: n := n + 1
n iniziale = 0

p:                         q:
  integer tmp                integer tmp
  p1: tmp := n               q1: tmp := n
  p2: n := tmp + 1           q2: n := tmp + 1
n iniziale = 0

Incremento a livello di codice macchina

A livello di macchina, un incremento si scompone in più istruzioni:

• Stack machine: push n, push #1, add, pop n (4 istruzioni).
• Register machine: load R1, n; add R1, #1; store n, R1 (3 istruzioni).

In entrambi i casi, se c'è interleaving tra queste micro-istruzioni, si possono produrre valori inconsistenti.

11. Strutture dati non atomiche

Il concetto di atomicità si estende anche alle strutture dati. Un oggetto dati atomico può trovarsi in un numero finito di stati pari al numero di valori che può assumere. I tipi primitivi nei linguaggi concorrenti sono generalmente atomici (ma non sempre: es. double in Java non è atomico su tutte le piattaforme).

I tipi di dato astratti (ADT) composti da più oggetti semplici sono tipicamente non atomici (es. classi in linguaggi OO, struct in C). Per un ADT si distinguono:

• Stato interno — significativo per chi definisce l'oggetto.
• Stato esterno — significativo per chi usa l'oggetto.

La corrispondenza tra stati interni ed esterni è parziale: esistono stati interni che non hanno un corrispondente stato esterno (stati consistenti).

L'esecuzione di un'operazione su un ADT non atomico può attraversare stati inconsistenti. In programmazione sequenziale questo non è un problema (grazie all'information hiding), ma in programmazione concorrente si crea una situazione pericolosa: un processo potrebbe operare su un oggetto mentre un altro processo lo sta modificando, trovandolo in uno stato inconsistente.

12. Processi ciclici e non-determinismo

Quando i processi contengono cicli (ad esempio while basati su condizioni), il diagramma di stato può contenere cicli, rappresentando computazioni potenzialmente infinite.

Esempio: due processi con while

p:                              q:
  p1: while (n < 1)               q1: while (n >= 0)
  p2:   n := n + 1                 q2:   n := n - 1

  n iniziale = 1

Il diagramma di stato per questo esempio ha molti stati e cicli. Si possono costruire scenari in cui il ciclo in p esegue esattamente una iterazione oppure tre iterazioni, a seconda dell'interleaving con q.

13. Correttezza: safety, liveness, fairness

La correttezza dei programmi concorrenti non può essere verificata con il testing tradizionale: lo stesso input può dare output diversi a seconda dello scenario. Serve un approccio basato su proprietà formali delle computazioni.

Safety properties

Una proprietà di safety deve essere sempre vera in ogni stato di ogni computazione. Viene espressa come invariante della computazione. Tipicamente specifica che «cose brutte non devono mai accadere»:

• Mutua esclusione: mai più di un processo nella sezione critica.
• Assenza di deadlock: nessun processo è in attesa di un evento che non può verificarsi.

Liveness properties

Una proprietà di liveness deve diventare vera prima o poi: in ogni computazione esiste uno stato in cui la proprietà è vera. Specifica che «cose buone devono eventualmente accadere»:

• Assenza di starvation: un processo prima o poi ottiene la risorsa che richiede.
• Assenza di dormienza: un processo in attesa viene prima o poi risvegliato.
• Comunicazione affidabile: un messaggio inviato viene prima o poi ricevuto.

Fairness

La fairness è una proprietà di liveness che richiede che qualcosa di buono accada infinitamente spesso. Si declina in tre livelli:

Un algoritmo può terminare o meno a seconda che si assumano scenari fair o unfair. Ad esempio, se un processo è in un ciclo che attende un flag, uno scenario unfair potrebbe non eseguire mai l'istruzione che setta il flag, portando a non-terminazione.

14. Il problema della sezione critica

Introdotto da Dijkstra nel 1965, il Critical Section Problem è uno dei più importanti e studiati problemi della programmazione concorrente. Si colloca nel contesto della competizione fra processi.

Definizione del problema

Abbiamo N processi, ciascuno esegue un ciclo infinito di istruzioni divisibili in due sottosequenze:

• Sezione critica (CS): sequenza di istruzioni che accede a oggetti condivisi.
• Sezione non critica (NCS): resto del codice.

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

Il problema è progettare i protocolli di ingresso e uscita (entry/exit protocol) che garantiscano tre proprietà:

1. Mutua esclusione: le sezioni critiche di due o più processi non devono essere interlacciate.
2. Assenza di deadlock: se alcuni processi cercano di entrare in CS, uno di essi deve prima o poi riuscirci.
3. Assenza di starvation individuale: se un processo cerca di entrare in CS, deve prima o poi riuscirci.

Si aggiunge la proprietà di bounded waiting (attesa limitata). Inoltre, una volta che un processo inizia la CS, deve completarla (progress property per la CS). La NCS non ha obbligo di progresso (può contenere cicli infiniti).

Primo tentativo: variabile turn

integer turn := 1
p:                              q:
  loop forever                    loop forever
    NCS                             NCS
    await turn = 1                  await turn = 2
    CS                              CS
    turn := 2                       turn := 1

Il diagramma di stato comprende 16 stati. La mutua esclusione è soddisfatta (non esiste stato <p3,q3,_>). L'assenza di deadlock è soddisfatta. Tuttavia, la starvation è possibile: se un processo rimane indefinitamente nella sua NCS, il turn non cambia e l'altro processo non può mai entrare in CS. La soluzione non è corretta.

Secondo tentativo: variabili want

boolean wantp := false, wantq := false

Si introducono variabili separate per indicare l'intenzione di ogni processo di entrare in CS. Ma la mutua esclusione non è garantita: lo stato <p3,q3,true,true> è raggiungibile a causa della non-atomicità del pre-protocollo.

Terzo tentativo: want prima dell'attesa

Spostando l'assegnamento di wantp := true prima dell'await, la mutua esclusione è risolta, ma si introduce un deadlock (più precisamente un livelock): entrambi i processi possono rimanere bloccati con want = true, nessuno dei due può entrare.

Quarto tentativo: rinuncia volontaria

Si richiede a un processo di rinunciare alla sua intenzione se scopre che l'altro è in competizione. Il livelock è risolto, ma rimane la possibilità di starvation in caso di interleaving perfetto (alternanza continua).

15. Algoritmi: Dekker e Peterson

Algoritmo di Dekker

Trovato dal matematico olandese T.J. Dekker nel 1965, è la prima soluzione corretta al problema della sezione critica per due processi. Combina il primo (turn) e il quarto tentativo: il diritto di insistere per entrare (non il diritto di entrare) viene passato esplicitamente tra i processi usando la variabile turn.

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

p:                                    q:
  loop forever                          loop forever
    NCS                                   NCS
    wantp := true                         wantq := true
    while wantq = true                    while wantp = true
      if turn = 2 then                      if turn = 1 then
        wantp := false                        wantq := false
        await turn = 1                        await turn = 2
        wantp := true                         wantq := true
    CS                                      CS
    turn := 2                               turn := 1
    wantp := false                          wantq := false

Dekker soddisfa mutua esclusione, assenza di deadlock e assenza di starvation. Funziona su qualsiasi architettura che fornisca solo load e store come istruzioni atomiche.

Algoritmo di Peterson

Proposto da Peterson nel 1981, è più conciso. Collassa due istruzioni 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

Peterson è corretto e più semplice di Dekker. È spesso usato come esempio didattico di soluzione al problema della sezione critica.

16. Istruzioni atomiche composte e lock

Dekker funziona con solo load/store, ma se il calcolatore concorrente fornisce istruzioni atomiche più potenti, il problema della sezione critica si semplifica enormemente.

Test-and-Set

L'istruzione test-and-set è un'operazione atomica che esegue due operazioni senza possibilità di interleaving:

test-and-set(x, r):
  < r := x, x := 1 >

Usando le parentesi angolari < > per denotare l'atomicità, la sezione critica con test-and-set diventa:

integer lock := 0

p:                                    q:
  integer was_locked                    integer was_locked
  loop forever                          loop forever
    NCS                                   NCS
    repeat                                repeat
      test-and-set(lock, was_locked)        test-and-set(lock, was_locked)
    until was_locked = 0                  until was_locked = 0
    CS                                    CS
    lock := 0                             lock := 0

Altre istruzioni atomiche importanti includono exchange, fetch-and-add, compare-and-swap (CAS).

Lock

Sfruttando istruzioni atomiche composte si può realizzare un meccanismo di lock elementare: due operazioni atomiche (acquire e release) proteggono la sezione critica.

lock sharedlock

p:                                    q:
  loop forever                          loop forever
    NCS                                   NCS
    acquire(sharedlock)                   acquire(sharedlock)
    CS                                    CS
    release(sharedlock)                   release(sharedlock)

synchronized in Java

In Java, blocchi synchronized sullo stesso oggetto lock garantiscono l'atomicità di sequenze di azioni, impedendo interleaving come a.c.b.d o c.a.d.b:

// Processo (thread) A
synchronized (lock) {
    // statement a
    // statement b
}

// Processo (thread) B
synchronized (lock) {
    // statement c
    // statement d
}

Algoritmo del fornaio (Bakery)

Per N processi, l'algoritmo del fornaio introduce biglietti numerati per stabilire il turno:

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

P[i]:
  loop forever
    NCS
    < turn[i] := num; num := num + 1 >
    await turn[i] = next
    CS
    next := next + 1

Potenziali problemi: overflow aritmetico per turn e num (crescono monotonicamente).

17. Verifica formale e LTL

Testing vs Verification

LTL — Linear Temporal Logic

Proposta da Amir Pnueli nel 1977, la logica temporale lineare aggiunge operatori temporali alla logica proposizionale per esprimere proprietà che devono valere in tutti gli scenari possibili.

Operatori temporali base

Proprietà con LTL

• Mutua esclusione (safety): □ ¬(p3 ∧ q3)
• Progress property (liveness): □ (p2 ⇒ ◇ p3)
• Dualità: ¬□ p ⇒ ◇ ¬p

Overtaking

La libertà da starvation può essere una proprietà debole: è vero che ◇ CSp, ma se q entra in CS 1000 volte prima di p, la proprietà è tecnicamente soddisfatta ma il comportamento è insoddisfacente. La proprietà di k-bounded overtaking richiede che un altro processo possa entrare al massimo k volte prima che il processo in attesa entri. Si esprime con l'operatore Weak Until:

tryp ⇒ (¬CSq) W (CSq W ((¬CSq) W CSp))

Per 1-bounded overtaking: da quando p cerca di entrare, q può entrare al massimo una volta prima di p.

18. Model checking e TLA+/PlusCal

Model checking

Il model checking è la tecnica più importante per la verifica automatica di proprietà di correttezza nei sistemi concorrenti. La strategia è basata sull'esplorazione esaustiva di tutto lo spazio degli stati del sistema.

• Le proprietà sono espresse come formule di logica temporale (es. LTL).
• Se il sistema soddisfa la proprietà, il model checker produce una conferma.
• Altrimenti produce un controesempio (traccia di esecuzione che viola la proprietà), utile per identificare bug.

Applicazioni: verifica hardware (Intel dopo il Pentium Bug del 1994), sistemi software critici (NASA dopo l'incidente del Mars Polar Lander nel 1999), Amazon Web Services.

Problema dell'esplosione dello spazio degli stati

Il problema principale del model checking è la dimensione dello spazio degli stati. Tecniche allo stato dell'arte:

• Regole per ridurre il numero di stati (variabili modellabili con un numero limitato di valori).
• Costruzione incrementale del grafo (esplorando solo stati raggiungibili, fermandosi se si trova uno stato falsificante).
• Symbolic model checking: lavora con insiemi di stati, non singoli stati.

SPIN e PROMELA

SPIN è un model checker ampiamente usato in ambito accademico e industriale. PROMELA è il linguaggio di modellazione usato da SPIN per descrivere sistemi concorrenti con un insieme limitato di costrutti.

// Esempio: Dekker in PROMELA (struttura)
proctype P() {
    /* dichiarazioni e codice */
}
proctype Q() {
    /* dichiarazioni e codice */
}

Java Path Finder (JPF)

JPF è un model checker specializzato per la verifica di programmi Java, sviluppato dalla NASA e open source. È una JVM speciale che esegue i programmi teoricamente lungo tutti i possibili scenari (percorsi di esecuzione), verificando violazioni di proprietà come deadlock, eccezioni non catturate, violazioni di assert.

Verifica per induzione di invarianti

Tecnica complementare al model checking: si dimostra che una formula è un invariante (vera in ogni stato di ogni computazione) per induzione:

1. Caso base: l'invariante è vero nello stato iniziale.
2. Passo induttivo: assumendo l'invariante vero in uno stato generico S, si dimostra che è vero in tutti gli stati successivi a S.

Esistono sistemi deduttivi che automatizzano questo processo.

TLA+ e PlusCal

TLA+ (Temporal Logic of Actions) è un linguaggio di specifica formale introdotto da Leslie Lamport, usato per specificare e verificare sistemi reali complessi (es. Amazon Web Services). Una specifica TLA+ descrive l'insieme di tutti i possibili comportamenti legali (trace di esecuzione) di un sistema.

Può descrivere sia le proprietà di correttezza desiderate (il «cosa») sia il progetto del sistema (il «come»). Il model checker TLC verifica le proprietà su specifiche TLA+.

PlusCal (ex +CAL) è un linguaggio algoritmico basato su TLA+ per scrivere algoritmi. Un algoritmo PlusCal viene tradotto in una specifica TLA+, che può essere verificata con TLC.

-- algorithm Peterson {
  variables flag = [ i in {0,1} |-> false ], turn = 0;
  process (proc in {0,1}) {
    a0: while (true) {
      a1: flag[self] := true;
      a2: turn := Not(self);
      a3a: if (flag[Not(self)]) { goto a3b } else { goto cs };
      a3b: if (turn = Not(self)) { goto a3a } else { goto cs };
      cs: skip;  \* sezione critica
      a4: flag[self] := false;
    }
  }
}

Con TLC si può verificare la proprieta di mutua esclusione: MutualExclusion = (pc[0] != "cs") or (pc[1] != "cs"). Per algoritmi con troppi stati, TLC non può verificare esaustivamente e si passa alla dimostrazione deduttiva.

Verifica le tue conoscenze