Il capitolo in un paragrafo. Per descrivere la dinamica di un sistema concorrente senza partire dal codice servono formalismi rigorosi ma leggibili. Una rete di Petri ha posti, transizioni e token: una transizione scatta quando tutti i suoi posti di ingresso hanno un token, e lo scatto sposta i token. Modellando prima ogni processo e poi la «colla» che li coordina, semafori, sezioni critiche, produttori-consumatori e lettori-scrittori si traducono quasi uno a uno. Sulla rete si analizzano raggiungibilità, limitatezza, vivacità e deadlock. Gli statechart di Harel estendono i diagrammi di stato con gerarchia e ortogonalità, e i diagrammi di attività UML descrivono flussi di lavoro con fork e join.
Di un sistema si descrivono struttura, comportamento e interazioni. In UML il diagramma delle classi dà la struttura statica e il sequence diagram uno scambio di messaggi, ma nessuno dei due descrive la dinamica, che in un sistema concorrente è la parte difficile. I formalismi visuali descrivono con diagrammi rigorosi il comportamento di un sistema, o la struttura dei compiti e le loro dipendenze. Servono per i requisiti, l'analisi e il progetto, e se definiti formalmente permettono un'analisi formale. Il modulo ne presenta tre: reti di Petri, statechart e diagrammi di attività. A differenza dei diagrammi di stato del capitolo 2, che chiudono tutto in un'unica tupla globale, le reti di Petri sono modulari: ogni processo è un pezzo di rete, e l'interazione è un pezzo in più.
Una rete di Petri, introdotta da Carl Adam Petri negli anni '60, è un modello formale del flusso di informazione e di controllo, adatto a sistemi di eventi che possono avvenire in concorrenza ma con vincoli di concorrenza, precedenza o frequenza.
Una transizione è abilitata quando ognuno dei suoi posti di ingresso contiene un token. Una transizione abilitata può scattare (firing): toglie un token da ogni posto di ingresso e ne deposita uno in ogni posto di uscita, in modo istantaneo, cioè atomico. Se ne sono abilitate più d'una, ne scatta una qualsiasi: la scelta è non deterministica. Se nessuna è abilitata, la rete si ferma.
Una transizione sorgente, senza ingressi, produce solo token; una transizione pozzo, senza uscite, li consuma soltanto. Con gli archi pesati, un arco di peso w da p a t richiede e consuma w token di p, e un arco di uscita di peso w ne produce w. L'esempio delle slide è la reazione 2H₂ + O₂ → 2H₂O. Una rete pesata si può sempre riscrivere come rete ordinaria, con molti più nodi.
L'interpretazione di base è per eventi e condizioni: le condizioni che valgono causano eventi, e un evento fa cessare alcune condizioni e ne fa iniziare altre. Un posto è una condizione, un token dice che vale, lo scatto è l'evento. Il formalismo ammette altre letture:
| Posti di ingresso | Transizione | Posti di uscita |
|---|---|---|
| precondizioni | evento | postcondizioni |
| dati in ingresso | passo di calcolo | dati in uscita |
| segnali in ingresso | elaboratore di segnali | segnali in uscita |
| risorse necessarie | compito o job | risorse rilasciate |
| condizioni | clausola logica | conclusioni |
| buffer | processore | buffer |
Si parte da ogni processo, da solo: ogni azione è una transizione, e tra due azioni un posto rappresenta lo stato del processo, come un'etichetta nel modello a interleaving. Un token è il flusso di controllo di un'istanza: due token nello stesso posto sono due processi con lo stesso programma. Poi si aggiunge la colla, i posti e gli archi dell'interazione. Hanno lo stesso aspetto dei posti di controllo ma un altro significato: condizioni, permessi, risorse, messaggi.
if): un posto con due transizioni in uscita, che sono in conflitto. Si può modellare la valutazione della condizione con una transizione, o astrarla del tutto. Il livello di dettaglio lo decide chi modella.fork, start, spawn): una transizione con più posti di uscita che di ingresso. Il token nuovo è il flusso di controllo del nuovo processo.join): una transizione con più posti di ingresso.Un flusso di controllo non deve mai sdoppiarsi dove non c'è una fork: se succede, il modello è sbagliato. E in fase di progetto la rete non va «ottimizzata»: una rete più piccola ed equivalente serve a un model checker, ma quella di progetto deve corrispondere uno a uno a come il sistema è pensato.
Al colloquio Ricci chiede di modellare con una rete di Petri un piccolo sistema di processi, come l'esercizio della sezione 4, e raccomanda questo metodo: prima i processi, poi le interazioni. Anche l'assignment 1 chiede di rappresentare con una rete di Petri la dinamica del proprio sistema, catturando gli aspetti essenziali.
b di Q avviene solo dopo l'azione a di P se un posto di uscita di a è anche un ingresso di b.a e b che devono avvenire insieme diventano un'unica transizione, con in ingresso i posti di controllo di entrambi.wait è una transizione che lo ha in ingresso, signal una che lo ha in uscita; la marcatura iniziale è il valore iniziale, 0 per un semaforo evento e 1 per un mutex (capitolo 5).È la domanda d'esame che segue l'esercizio sui semafori del capitolo 5. Il processo P esegue le azioni atomiche a1, a2; il processo Q esegue b1, b2, b3. Si vuole che b2 avvenga sempre dopo a1. Con un semaforo evento:
semaphore S := (0, {})
P: a1 Q: b1
signal(S) wait(S)
a2 b2
b3La rete si costruisce con il metodo della sezione precedente. Prima i due processi, ciascuno una catena di posti e transizioni con un token nel posto iniziale. Poi il semaforo: un posto S senza token. signal(S) diventa un secondo arco di uscita di a1 verso S, e wait(S) un secondo arco di ingresso di b2. Si potrebbero anche disegnare signal e wait come transizioni a sé: il comportamento sulle azioni a e b è lo stesso.
a1. Sono abilitate a1 e b1 (in blu). b2 ha due ingressi: può scattare solo quando Q ha eseguito b1 e a1 ha messo un token in S.L'errore tipico è collegare il posto dopo a1 sia ad a2 sia a b2. Un posto con due transizioni in uscita è una scelta: l'unico token andrebbe o ad a2 o a b2, e uno dei due processi resterebbe bloccato. Per segnalare serve una transizione con due posti di uscita, che produce un token per ciascuno.
produce e put, il consumatore tra get e consume, e N token iniziali sono N produttori. Il buffer sono due posti: gli item, inizialmente 0, e i posti liberi, inizialmente la capienza. put consuma un libero e produce un item, get fa il contrario. Sono i semafori divisi availItems e availPlaces del capitolo 5, con l'invariante «liberi + item = capienza»; senza i liberi il buffer è illimitato.ai con un token; ogni filosofo ha un posto «pensa» e un posto «mangia». Nella rete delle slide un filosofo prende le due forchette con un'unica transizione, quindi non può restare con una sola forchetta in mano. Se invece le prende una alla volta ricompare il deadlock dell'attesa circolare (capitolo 6), lo stesso della rete «due lock presi in ordine opposto» del laboratorio.Fai scattare le transizioni abilitate (in blu). Analizza esplora tutte le marcature raggiungibili e riporta limitatezza, transizioni vive o morte, deadlock e la proprietà che la rete deve garantire, con lo scenario che la viola. Prova a cambiare la marcatura iniziale: S = 1 nell'esercizio, 2 permessi nella sezione critica, 2 invece di 3 nei lettori-scrittori.
La descrizione formale serve ad analizzare le proprietà del sistema, facendo corrispondere safety e liveness a proprietà della rete. Queste sono strutturali, indipendenti dalla marcatura iniziale, o comportamentali, dipendenti da essa.
C = (P, T, I, O): posti, transizioni, e le funzioni I e O che danno i posti di ingresso e di uscita di ogni transizione.μ : P → ℕ. Una rete marcata è M = (P, T, I, O, μ).δ(μ, t) è parziale: è indefinita se t non è abilitata, altrimenti dà la marcatura dopo lo scatto. Un'esecuzione è μ1 = δ(μ0, tj), μ2 = δ(μ1, tk), …, e le sequenze possibili sono molte.μ′ è immediatamente raggiungibile da μ con uno scatto, raggiungibile con una sequenza di scatti. L'insieme di raggiungibilità contiene tutte le marcature in cui la rete può trovarsi.Con m transizioni (righe) e n posti (colonne): la matrice di ingresso D⁻[i,j] è il peso dell'arco da pj a ti, quella di uscita D⁺[i,j] il peso dell'arco da ti a pj, e la matrice di incidenza è D = D⁺ − D⁻. Con la marcatura M (1 × n) e il vettore T (1 × m) delle transizioni che scattano:
M′ = M + T · D
Nell'esempio delle slide P = {p1, …, p5}, T = {t1, …, t4}, con I(t1) = {p1}, O(t1) = {p2, p3, p5}, I(t2) = {p2, p3, p5}, O(t2) = {p5}, I(t3) = {p3}, O(t3) = {p4}, I(t4) = {p4}, O(t4) = {p2, p3}:
| D | p1 | p2 | p3 | p4 | p5 |
|---|---|---|---|---|---|
| t1 | −1 | +1 | +1 | 0 | +1 |
| t2 | 0 | −1 | −1 | 0 | 0 |
| t3 | 0 | 0 | −1 | +1 | 0 |
| t4 | 0 | +1 | +1 | −1 | 0 |
Da M = (1, 0, 0, 0, 0), lo scatto di t1 (T = (1, 0, 0, 0)) dà M′ = (0, 1, 1, 0, 1): un prodotto tra matrici, facile da calcolare in modo efficiente. Il laboratorio mostra D per ogni rete.
D non basta a decidere se una transizione è abilitata: serve D⁻. In t2 il posto p5 è ingresso e uscita, quindi in D vale 0, ma t2 richiede comunque un token in p5.
Un deadlock è una marcatura raggiungibile senza transizioni abilitate, in un sistema che non dovrebbe fermarsi. Le altre proprietà di correttezza diventano condizioni sull'insieme di raggiungibilità, come «nessuna marcatura con due token nei posti CS» o «liberi + item costante».
Gli strumenti citati nelle slide sono PIPE 2, un editor open source in Java, e TINA (Time Petri Net Analyzer), che esplora le marcature e fa model checking.
Gli statechart sono stati introdotti da David Harel nel 1987 per i sistemi reattivi complessi, e sono entrati in UML come state diagram. Un sistema reattivo reagisce di continuo a stimoli esterni e interni (automobili, reti, sistemi operativi, avionica, interfacce utente), a differenza di uno trasformazionale, che da un input calcola un output. Harel voleva una descrizione del comportamento reattivo chiara e realistica, ma formale, da simulare e analizzare.
Stati ed eventi sono il mezzo naturale: «quando in A avviene α, se vale la condizione C, il sistema passa in B». Ma i diagrammi di stato piatti non scalano: gli stati crescono in modo esponenziale, tutti sullo stesso piano. Gli statechart aggiungono due meccanismi: la gerarchia (raggruppamento e raffinamento, per zoomare tra livelli di astrazione) e l'ortogonalità (sottostati indipendenti e concorrenti, con sincronizzazione).
evento (condizione) / azione. Gli stati si annidano, e le frecce partono e arrivano a qualsiasi livello.…/W su una transizione è un'azione istantanea che genera eventi o cambia condizioni; ci sono anche azioni di ingresso (entry) e di uscita (exit) da uno stato. Un'attività invece dura (un suono, un lungo calcolo), quindi si associa a uno stato: la avvia l'azione di ingresso e la ferma quella di uscita.L'equivalente senza AND di uno stato ortogonale ha il prodotto degli stati: due componenti da 1.000 stati ne danno un milione, tre un miliardo. L'ortogonalità evita questa esplosione, la stessa dei diagrammi di stato del capitolo 2. Statemate è lo strumento di modellazione e simulazione basato sugli statechart, per sistemi embedded complessi: la specifica è eseguibile e si simula graficamente per esplorare scenari «what-if», che diventano poi piani di test per il sistema reale.
I diagrammi di attività sono i diagrammi UML per i flussi di lavoro (workflow) di un sistema. Un diagramma di stato mostra gli stati di un oggetto e le transizioni; uno di attività mette al centro le attività che causano quei cambiamenti. Si legge dall'alto in basso:
In UML 2 la semantica dei diagrammi di attività è definita come un flusso di token, ispirato alle reti di Petri. Una fork è una transizione con più uscite, una join una transizione con più ingressi, un branch un posto con più transizioni in conflitto.
Un modello formale e visuale del flusso di informazione e di controllo, adatto a sistemi concorrenti e asincroni. È un grafo bipartito di posti e transizioni collegati da archi, con token nei posti che ne rappresentano lo stato.
Un posto è un nodo che rappresenta una condizione, uno stato di un processo o una risorsa. Un token in un posto dice che la condizione vale; nel modello dei processi è un flusso di controllo, o un permesso. La marcatura, cioè quanti token ci sono in ogni posto, è lo stato della rete.
È abilitata quando ogni posto di ingresso ha almeno un token (o almeno il peso dell'arco). Scattando, atomicamente, toglie un token da ogni ingresso e ne aggiunge uno a ogni uscita. Tra più transizioni abilitate la scelta è non deterministica.
Il semaforo è un posto con tanti token quanto il suo valore iniziale: wait è una transizione che lo ha in ingresso, signal una che lo ha in uscita. La sezione critica usa un posto-permesso con un token, consumato all'ingresso in CS e restituito all'uscita.
Si disegnano le due catene posto-transizione dei processi, poi un posto S vuoto: a1 ha S come uscita aggiuntiva, b2 lo ha come ingresso aggiuntivo. È il semaforo evento inizializzato a 0.
Il posto dei permessi ha n token, uno per lettore, così più lettori entrano insieme. Lo scrittore deve prenderli tutti: entra solo se nessuno sta leggendo, e finché scrive nessun lettore può entrare.
Morta: nessuna sequenza di scatti la può più abilitare (legata al deadlock). Potenzialmente attivabile: esiste una sequenza che la abilita. Viva: è potenzialmente attivabile da ogni marcatura raggiungibile.
Permettono di far scattare una transizione solo se un posto è vuoto. La rete diventa Turing-equivalente, e molte proprietà, decidibili per le reti ordinarie, diventano indecidibili.
La gerarchia (superstati XOR, raffinamento, stati di default e storia) e l'ortogonalità (componenti AND indipendenti che un evento può sincronizzare), più azioni e attività. Evitano l'esplosione degli stati dei diagrammi piatti.
La fork avvia più attività in parallelo, la join aspetta che siano terminate tutte prima di proseguire. Branch e merge invece aprono e chiudono un'alternativa condizionale.
Slide: module 1.5, Visual Formalisms (reti di Petri, statechart, diagrammi di attività). Lezione: 27 marzo 2026, prima ora (reti di Petri applicate ai processi concorrenti: il metodo, l'esercizio di sincronizzazione, sezione critica, if e fork, produttori-consumatori, lettori-scrittori, archi pesati e inibitori, analisi). Statechart e diagrammi di attività non sono stati svolti a lezione e vengono dalle slide. La mappa completa è in coverage-matrix.json.