V&V in AI — Appunti

Settimana 2

✦
Indice← PrecedenteSuccessivo →
Capitolo 4

Capitolo 4 — FTS e SPL

Modellazione di programmi reattivi; fairness debole/forte.

Sistemi di transizione fair - Riassunto

Punti chiave

Argomento centrale

La fairness serve a escludere computazioni irrealistiche in cui un'azione abilitata viene ignorata per sempre.

Rilevanza per V&V in AI

FTS e fairness sono fondamentali per verificare proprieta di liveness in agenti, protocolli e sistemi autonomi non terminanti.

Sistema di transizione fair

Un FTS e' un modello formale per sistemi reattivi, cioe' sistemi che continuano a interagire con l'ambiente e non sono pensati per terminare.

Definizione

Un FTS e' una tupla: $$\langle \mathcal{V},\Theta,\mathcal{T},\mathcal{J},\mathcal{C}\rangle$$

Le variabili includono variabili dati e variabili di controllo. Uno stato e' una valutazione di tutte queste variabili. Una transizione puo essere descritta da una relazione logica $\rho_\tau(\mathcal{V},\mathcal{V}')$, dove le variabili con apice indicano lo stato successivo.

Una transizione e' abilitata in uno stato se esiste almeno un successore che soddisfa la relazione di transizione. L'idling transition mantiene invariati dati e controllo e serve a completare computazioni finite, ma normalmente non richiede fairness.

Fairness

Computazioni

Una P-computation e' una computazione che rispetta inizialita, consequenzialita e condizioni di fairness.

Una run rispetta solo inizialita e consequenzialita; una P-computation e' una run ammissibile anche rispetto a justice e compassion. Uno stato e' P-accessible se compare in almeno una P-computation.

Collegamenti

Linguaggio di programmazione semplice

SPL e' un linguaggio minimale usato per modellare programmi reattivi e concorrenti.

Istruzioni

Le istruzioni si dividono in quattro gruppi:

skip non cambia le variabili dati ma avanza il controllo; l'idling transition, invece, non cambia né dati né controllo. await c è abilitata solo quando la guardia c è vera. request r richiede r > 0 e decrementa il semaforo; release r lo incrementa.

Semantica

Un programma SPL puo essere compilato in un Sistemi di transizione fair, usando variabili di controllo per rappresentare le posizioni del programma.

Le label identificano le istruzioni e le post-location indicano dove si trova il controllo dopo l'esecuzione. Nei programmi paralleli si usa un modello a interleaving: a ogni passo viene scelta una transizione abilitata tra quelle disponibili.

Nella traduzione standard, justice viene richiesta per quasi tutte le transizioni tranne idling e noncritical; compassion viene richiesta soprattutto per comunicazioni e request, dove una risorsa può diventare disponibile infinite volte.

Collegamenti

Approfondimento completo settimana 2 - Fair Transition Systems, SPL e fairness

Questo documento espande il Capitolo 4 della seconda settimana di V&V. Capiremo perché per i sistemi reattivi le logiche classiche non bastano, come si usa SPL per modellarli e, in maniera cruciale, perché il concetto di "Fairness" (giustizia) è fondamentale per non avere falsi negativi durante il model checking.

1. Il problema dei sistemi reattivi

I programmi classici (trasformazionali) si comportano come una funzione matematica: prendono un input $X$, calcolano un risultato e terminano restituendo $Y$. I sistemi reattivi (come i server web, i sistemi di controllo del traffico aereo, o gli scheduler dei sistemi operativi) sono progettati per non terminare mai. Reagiscono continuamente agli input dell'ambiente. Per questo, l'esecuzione di un sistema reattivo non produce un output finale, ma genera una computazione infinita (una sequenza infinita di stati).

Le proprietà che ci interessano per questi sistemi si dividono in:

2. SPL (Simple Programming Language)

Per analizzare matematicamente un sistema reattivo, serve un linguaggio di modellazione: SPL. È un linguaggio minimale che supporta la concorrenza. Ha costrutti familiari come assegnamenti, cicli while, branching, ma soprattutto:

Il codice SPL non viene analizzato direttamente: viene "compilato" semanticamente in una struttura matematica rigorosa chiamata Fair Transition System (FTS).

Classi di istruzioni SPL

Negli appunti delle pagine 20-40, SPL è organizzato in quattro gruppi principali. Questa classificazione è utile perché ogni gruppo genera transizioni FTS in modo leggermente diverso.

Istruzioni basic

Istruzioni schematiche

Istruzioni compound

Istruzioni grouped/composite

Labels, post-location e controllo

In SPL le istruzioni sono etichettate. Una label identifica una posizione del programma, mentre la post-location di un'istruzione è la posizione raggiunta dopo la sua esecuzione. Per una concatenazione, ad esempio, la post-location del primo componente coincide con la posizione iniziale del secondo componente.

Questa idea serve per costruire la variabile di controllo dell'FTS: lo stato non contiene solo i dati del programma, ma anche l'informazione su "dove si trova" ogni processo. In un programma parallelo, la variabile di controllo può contenere un insieme di location attive, una per ogni processo in esecuzione nel modello a interleaving.

Nondeterminismo e interleaving

SPL non assume che i processi paralleli eseguano davvero passi simultanei. Il modello usato è l'interleaving: a ogni passo lo scheduler sceglie una transizione abilitata tra quelle disponibili. La scelta può essere nondeterministica. La fairness serve proprio a evitare computazioni in cui lo scheduler continua a scegliere sempre gli stessi processi e ignora per sempre altri processi pronti.

3. Fair Transition Systems (FTS)

Un FTS è una quintupla $\langle \mathcal{V}, \Theta, \mathcal{T}, \mathcal{J}, \mathcal{C} \rangle$:

  1. $\mathcal{V}$ (Variabili di Stato): Contiene le variabili del programma e le variabili di controllo (che fungono da Program Counter per dire in quale riga di codice si trova un processo). Lo stato del sistema è un'assegnazione di valori a tutte queste variabili.
  2. $\Theta$ (Condizione Iniziale): Una formula logica che specifica in quali stati il sistema può iniziare. Ad esempio: x = 0 AND pc1 = start.
  3. $\mathcal{T}$ (Transizioni): Rappresentano gli step di esecuzione (le singole istruzioni). Sono relazioni matematiche tra lo stato attuale $s$ e i possibili stati successivi $s'$.
  4. Una transizione $\tau$ si dice abilitata in $s$ se esiste almeno un successore $s'$. Ad esempio, un await x > 0 non è abilitato se $x = 0$.
  5. Esiste sempre la transizione di idling (che non fa niente e mantiene lo stato invariato).
  6. $\mathcal{J}$ (Justice - Giustizia o Weak Fairness).
  7. $\mathcal{C}$ (Compassion - Compassione o Strong Fairness).

Transizioni come formule logiche

Una transizione $\tau \in \mathcal{T}$ può essere descritta da una formula di primo ordine:

$$\rho_\tau(\mathcal{V}, \mathcal{V}')$$

Le variabili senza apice descrivono lo stato corrente; le variabili con apice descrivono lo stato successivo. Per esempio, una transizione che incrementa $x$ può essere scritta come $x' = x + 1$ insieme alla preservazione delle altre variabili.

La condizione di abilitazione di una transizione è:

$$En(\tau) \equiv \exists \mathcal{V}' \; \rho_\tau(\mathcal{V}, \mathcal{V}')$$

Quindi $\tau$ è abilitata in uno stato $s$ se esiste almeno uno stato successivo $s'$ che rende vera la relazione di transizione. Questo dettaglio è essenziale: justice e compassion parlano sempre di transizioni abilitate e prese.

Idling e diligent transitions

Ogni FTS include una transizione di idling $\tau_I$, definita da $\mathcal{V}' = \mathcal{V}$. Questa transizione non cambia né le variabili dati né le variabili di controllo. Serve a completare computazioni finite trasformandole in computazioni infinite, ma non richiede né justice né compassion.

Le transizioni diverse dall'idling sono dette diligent transitions. In genere sono quelle che rappresentano veri passi del programma.

Run, P-computazioni e accessibilità

Una run soddisfa solo:

Una P-computation è una run che soddisfa anche le condizioni di fairness. Quando negli esercizi si dice "computazione del programma", spesso si intende proprio una computazione ammissibile/fair.

Uno stato è P-accessible se compare in almeno una P-computation. L'accessibilità negli FTS, quindi, non è solo raggiungibilità nel grafo grezzo: le computazioni considerate devono anche rispettare i vincoli di fairness.

4. Perché serve la Fairness?

Supponiamo di avere due processi paralleli: $P_1$ (che stampa "A") e $P_2$ (che stampa "B"). Vogliamo verificare la proprietà di liveness: "Sia A che B verranno stampati infinite volte". Se modelliamo il sistema senza alcun vincolo di fairness, il Model Checker potrebbe considerare una computazione "valida" quella in cui lo scheduler sceglie sempre e solo di eseguire $P_1$, lasciando $P_2$ bloccato all'infinito ("starvation" totale). In quella computazione, la nostra proprietà fallisce. Ma questa computazione non è realistica! Uno scheduler reale di un SO non ignorerà mai per sempre un processo pronto per essere eseguito.

La fairness è il filtro che dice al Model Checker: "Ignora le computazioni in cui lo scheduler è patologicamente cattivo, e verifica le proprietà solo sulle esecuzioni realistiche". Queste esecuzioni realistiche prendono il nome di P-computazioni (Computazioni Ammissibili).

5. Justice e Compassion spiegate bene

Justice (Weak Fairness)

Compassion (Strong Fairness)

Gerarchia: Richiedere la Compassion è un requisito più forte. Una computazione che soddisfa la Compassion per un evento, garantisce automaticamente la Justice per quell'evento. Il contrario non è vero.

Quali transizioni finiscono in $\mathcal{J}$ e $\mathcal{C}$ in SPL

Nella traduzione standard da SPL a FTS:

Questa distinzione spiega molti esercizi: se una transizione è sempre abilitata e non viene presa, si viola justice; se è abilitata infinite volte ma non viene presa infinite volte, si viola compassion. Se invece una transizione non è in $\mathcal{J}$ né in $\mathcal{C}$, può anche essere ignorata senza rendere la computazione non ammissibile.

6. Dalle P-computazioni al Model Checking

Il flusso concettuale è:

  1. Scrivo il programma in SPL.
  2. Lo traduco in un FTS definendo chiaramente $\mathcal{J}$ e $\mathcal{C}$.
  3. L'FTS genera un albero infinito (o un grafo) di stati possibili.
  4. Applico le regole di Fairness per tagliare i rami del grafo irrealistici, tenendo solo le P-computazioni.
  5. Su queste P-computazioni residue (viste come stringhe o percorsi infiniti) utilizzo logiche temporali come LTL o CTL (capitoli successivi!) per verificare che le specifiche di safety e liveness reggano.

Esempio guida: programma reattivo con await e skip

Un pattern importante negli appunti è un programma con due processi:

La domanda tipica è: esiste una computazione ammissibile in cui $P_1$ non termina mai?

La risposta dipende da quali istruzioni restano abilitate:

Questo è il punto chiave degli esercizi: non basta vedere che un processo "potrebbe" fare un passo; bisogna chiedersi se quel passo è sempre abilitato, abilitato infinite volte, e se la transizione sta in $\mathcal{J}$ o in $\mathcal{C}$.

Esempio guida: mutua esclusione

Nei programmi di mutua esclusione con semaforo, come MUX_SEM, la variabile condivisa $y$ rappresenta la disponibilità della risorsa. Se un processo esegue request y, decrementa $y$ e può entrare nella sezione critica; finché non esegue release y, l'altro processo non può superare la propria request.

Le proprietà da distinguere sono:

In MUX_SEM, la compassion su request è ciò che impedisce di abilitare infinite volte la richiesta di un processo senza concedergli mai la risorsa. In varianti con when o grouped instructions, invece, si può ottenere la mutua esclusione ma perdere l'accessibility forte: il sistema può restare fair pur facendo entrare ripetutamente l'altro processo.

7. Esempio svolto 1: tradurre un programma SPL minimo in FTS

Prendiamo un programma molto piccolo:

P:
  l0: await x = 0;
  l1: x := 1;
  l2: skip

Supponiamo che $x\in\lbrace 0,1\rbrace$.

Variabili

Lo stato dell'FTS deve contenere:

Quindi:

$$\mathcal{V}=\lbrace x,pc\rbrace$$

con:

$$pc\in\lbrace l0,l1,l2,l3\rbrace$$

dove $l3$ è la post-location finale dopo skip.

Condizione iniziale

Se il programma parte da $l0$ e $x=0$:

$$\Theta \equiv (pc=l0 \land x=0)$$

Transizione await x = 0

await non cambia $x$, ma avanza il controllo solo se la guardia è vera:

$$\rho_{await}\equiv pc=l0 \land x=0 \land pc'=l1 \land x'=x$$

Abilitazione:

$$En(\tau_{await})\equiv pc=l0\land x=0$$

Se $pc=l0$ ma $x=1$, la transizione non è abilitata.

Transizione x := 1

L'assegnamento cambia $x$ e avanza il controllo:

$$\rho_{assign}\equiv pc=l1 \land x'=1 \land pc'=l2$$

Se ci fossero altre variabili, dovremmo aggiungere che restano invariate.

Transizione skip

skip non modifica i dati, ma modifica il controllo:

$$\rho_{skip}\equiv pc=l2 \land x'=x \land pc'=l3$$

Idling

L'idling è diverso da skip:

$$\rho_I\equiv pc'=pc \land x'=x$$

skip è una istruzione del programma e consuma un passo. L'idling è il passo artificiale che lascia tutto fermo.

Insieme delle transizioni

$$\mathcal{T}=\lbrace \tau_{await},\tau_{assign},\tau_{skip},\tau_I\rbrace$$

Per un programma così semplice, di solito mettiamo in justice le transizioni diligenti:

$$\mathcal{J}=\lbrace \tau_{await},\tau_{assign},\tau_{skip}\rbrace$$

e nessuna in compassion:

$$\mathcal{C}=\emptyset$$

Questa traduzione è il modo standard di passare dal codice a una struttura matematica verificabile.

8. Esempio svolto 2: quando una run non è fair

Considera due processi:

P1:
  l0: skip;
  l0: skip;
  ...

P2:
  m0: skip;
  m0: skip;
  ...

Entrambi hanno sempre una transizione skip abilitata. Nel modello a interleaving, a ogni passo lo scheduler sceglie una sola transizione.

Una run possibile nel grafo grezzo è:

P1, P1, P1, P1, P1, ...

cioè lo scheduler esegue sempre $P_1$ e mai $P_2$.

È una run?

Sì. Ogni passo è giustificato da una transizione valida.

È una P-computazione fair?

Dipende da $\mathcal{J}$.

Se la transizione di $P_2$ è in justice, allora non è fair. Perché:

Quindi viola justice.

Perché questo importa?

Senza fairness, il model checker potrebbe dire che la proprietà:

"$P_2$ prima o poi esegue un passo"

è falsa.

Con justice, quella computazione patologica viene eliminata. La proprietà può diventare vera sulle sole computazioni fair.

Questo è il senso pratico della fairness: non cambia il grafo delle transizioni, ma cambia quali cammini infiniti sono considerati ammissibili.

9. Esempio svolto 3: justice non basta, serve compassion

Ora considera una risorsa condivisa $r\in\lbrace 0,1\rbrace$ e un processo $P$ con:

l0: request r;
l1: critical;
l2: release r;
l0: ...

La transizione request r è abilitata solo quando:

$$r=1$$

Supponi che lungo una computazione la risorsa diventi libera infinite volte:

r=1, r=0, r=1, r=0, r=1, r=0, ...

ma lo scheduler non sceglie mai la request di $P$ proprio nei momenti in cui $r=1$.

Justice viene violata?

Non necessariamente.

Justice scatta se una transizione è continuamente abilitata da un certo punto in poi. Qui request r è abilitata infinite volte, ma non continuamente: quando $r=0$ si disabilita.

Quindi una computazione del genere può soddisfare justice e comunque far morire di fame $P$.

Compassion viene violata?

Sì, se request r è in $\mathcal{C}$.

Compassion dice:

se una transizione è abilitata infinite volte, allora deve essere presa infinite volte.

Qui request r è abilitata infinite volte e non viene mai presa. Quindi la computazione non è fair rispetto a compassion.

Frase da orale

Justice esclude l'ingiustizia contro azioni sempre disponibili; compassion esclude l'ingiustizia contro azioni disponibili infinite volte ma a intermittenza.

10. Esempio svolto 4: mutua esclusione con semaforo

Considera due processi simmetrici:

P1:
  noncritical;
  request y;
  critical;
  release y;
  repeat

P2:
  noncritical;
  request y;
  critical;
  release y;
  repeat

con semaforo:

$$y\in\lbrace 0,1\rbrace$$

e inizialmente:

$$y=1$$

Safety: mutua esclusione

La proprietà di mutua esclusione dice:

non accade mai che $P_1$ e $P_2$ siano entrambi in critical.

Perché vale?

Quindi i due processi non possono superare entrambi la request senza che qualcuno faccia prima release y.

Liveness: prima o poi entro?

La proprietà:

se $P_i$ richiede la risorsa, prima o poi entra in critical

non dipende solo dal semaforo. Dipende anche dalla fairness.

Se il semaforo viene liberato infinite volte e la request di $P_i$ è in compassion, allora non posso ignorare $P_i$ per sempre ogni volta che la risorsa è libera.

Senza compassion, lo scheduler può scegliere sempre l'altro processo nei momenti favorevoli. La mutua esclusione resta vera, ma la starvation non viene esclusa.

Differenza tra safety e liveness nel caso MUX

Questa distinzione è essenziale perché fairness serve soprattutto per ragionare su liveness, non su safety pura.

11. Esercizi guidati da fare a mano

Esercizio 1: abilitazione di un await

Programma:

l0: await x > 2;
l1: x := x - 1

Stato:

$$pc=l0,\quad x=2$$

Domanda: la transizione await x > 2 è abilitata?

Soluzione: no, perché la guardia $x>2$ è falsa. Non esiste uno stato successivo generato da quella transizione. L'unica transizione sempre disponibile è l'idling, più eventuali transizioni di altri processi.

Esercizio 2: skip contro idling

Stato:

$$pc=l2,\quad x=5$$

Istruzione in $l2$:

l2: skip

Effetto di skip:

$$pc'=l3,\quad x'=5$$

Effetto dell'idling:

$$pc'=l2,\quad x'=5$$

Quindi skip e idling non sono la stessa cosa. Il primo avanza il controllo; il secondo lascia fermo l'intero stato.

Esercizio 3: riconoscere una violazione di justice

Una transizione $\tau\in\mathcal{J}$ è abilitata da un certo istante $N$ in poi, ma non viene mai presa dopo $N$.

La computazione è fair?

Soluzione: no. Questa è esattamente la violazione di justice.

Esercizio 4: riconoscere una violazione di compassion

Una transizione $\tau\in\mathcal{C}$ è abilitata ai tempi pari:

$$0,2,4,6,\ldots$$

ma viene presa solo al tempo 0.

La computazione è fair?

Soluzione: no. La transizione è abilitata infinite volte, ma non viene presa infinite volte.

Esercizio 5: P-accessibilità

Uno stato $s$ è raggiungibile nel grafo grezzo, ma ogni cammino infinito che passa da $s$ viola justice.

$s$ è P-accessible?

Soluzione: no. P-accessible significa che lo stato compare in almeno una computazione fair. La raggiungibilità normale non basta.

Attenzione pero' a una proprieta' degli appunti: ogni prefisso finito di una run e' anche prefisso di qualche computazione fair (puoi sempre "riparare" il futuro eseguendo le transizioni trascurate). Quindi uno stato che occorre in una run e' sempre P-accessible. Il caso dell'esercizio — raggiungibile ma non P-accessible — puo' presentarsi solo se ogni prosecuzione da $s$ viola la fairness, cosa possibile solo in sistemi dove da $s$ in poi certe transizioni juste restano per forza abilitate e mai eseguibili insieme.

Esercizio 6 (il classico d'orale): termina $P_1$?

Questo e' l'esempio svolto a lezione, segnalato come tipica domanda di apertura dell'orale (esercizi "chapter 0").

local x: integer where x = 1

P1 :: l0: [ l0a: await x = 1
            or
            l0b: skip ]
      l1:

P2 :: m0: loop forever do
      m1:   x := -x

$P_2$ non termina mai e alterna $x$ tra $1$ e $-1$. Domanda: esiste una computazione ammissibile in cui $P_1$ non termina mai?

L'unica candidata e' quella in cui lo scheduler esegue solo $P_2$:

$$\langle\pi=\{l_0,m_0\}, x=1\rangle \to_{m_0} \langle\pi=\{l_0,m_1\}, x=1\rangle \to_{m_1} \langle\pi=\{l_0,m_0\}, x=-1\rangle \to_{m_0}\cdots$$

Non e' ammissibile. Davanti alla selection, il controllo e' davanti a entrambe le alternative. La justice per l0a (await) e' rispettata: la guardia $x=1$ va e viene, quindi l0a non e' costantemente abilitata. Ma l0b e' una skip: costantemente abilitata e mai eseguita — justice violata. Quindi in ogni computazione fair $P_1$ termina.

Variante 1: togli la skip (resta solo l0a: await x = 1). Ora la computazione candidata e' ammissibile: l'await non e' costantemente abilitata (la guardia oscilla), quindi justice e' soddisfatta anche senza mai eseguirla. Per forzare l'esecuzione servirebbe compassion (e' abilitata infinite volte). Con sola justice, $P_1$ puo' non terminare.

Variante 2: sostituisci la selection con

l0: if x = 1 then l1: skip else l2: skip; l3:

L'if genera un'unica transizione sempre abilitata ($\rho^T \lor \rho^F$: uno dei due disgiunti vale sempre). Justice la forza prima o poi; poi il controllo e' davanti a una skip costantemente abilitata, e justice forza anche quella. $P_1$ termina in ogni computazione fair.

La morale da dire all'orale: la terminazione dipende interamente da quali transizioni sono abilitate con quale persistenza e da che fairness e' richiesta su di esse — lo stesso programma cambia comportamento spostando un'istruzione da "sempre abilitata" a "abilitata a intermittenza".

12. Come una transizione FTS diventa una formula

Negli appunti il passaggio importante e':

una transizione non e' solo una freccia del grafo; puo' essere rappresentata da una formula logica sulle variabili correnti e sulle variabili next.

Se l'insieme delle variabili e':

$$\mathcal{V}=\{x_1,\ldots,x_n\},$$

si introduce una copia primata:

$$\mathcal{V}'=\{x'_1,\ldots,x'_n\}.$$

Le variabili non primate descrivono lo stato corrente. Le variabili primate descrivono il successore.

Una transizione $\tau$ e' rappresentata da:

$$\rho_\tau(\mathcal{V},\mathcal{V}').$$

Esempio:

$$x'=x+1$$

descrive una transizione che incrementa $x$.

Se ci sono anche variabili di controllo, la formula deve dire anche come cambia il program counter.

Enabling condition

La condizione di abilitazione di $\tau$ si ottiene esistenzializzando lo stato successivo:

$$En(\tau)(\mathcal{V})=\exists \mathcal{V}'.\rho_\tau(\mathcal{V},\mathcal{V}').$$

Perche'?

Perche' $\tau$ e' enabled in uno stato corrente se esiste almeno un successore che soddisfa la relazione di transizione.

Questo e' lo stesso schema che ricompare piu' avanti:

13. Traduzione delle istruzioni SPL in FTS

La semantica di SPL associa alle istruzioni formule di transizione.

Per capire gli esercizi bisogna ricordare la differenza tra:

Indichiamo con:

$$pres(Y)$$

la formula che dice che tutte le variabili dati in $Y$ restano uguali.

skip

l: skip; l^

Effetto:

Formula:

$$move(l,l^\wedge)\land pres(Y).$$

Quindi skip non e' idling: skip avanza il controllo, idling no.

Assegnamento

l: u := e; l^

Effetto:

Formula:

$$move(l,l^\wedge)\land u'=e\land pres(Y-\{u\}).$$

Per assegnamenti multipli si usa la stessa idea vettoriale:

$$\bar u'=\bar e.$$

await c

l: await c; l^

Effetto:

Formula:

$$move(l,l^\wedge)\land c\land pres(Y).$$

Questo spiega perche' justice e compassion vanno ragionate sull'abilitazione: await c puo' essere enabled a intermittenza se $c$ diventa vera e falsa nel tempo.

request r e release r

Per il semaforo:

l: request r; l^

Formula:

$$move(l,l^\wedge)\land r>0\land r'=r-1\land pres(Y-\{r\}).$$

request e' enabled solo se la risorsa e' disponibile.

Per:

l: release r; l^

Formula:

$$move(l,l^\wedge)\land r'=r+1\land pres(Y-\{r\}).$$

release non compete per ottenere la risorsa: la libera.

Per questo negli appunti compassion e' richiesta tipicamente su request, non su release.

Comunicazione su canali: send e receive

SPL ha anche istruzioni per il message passing:

I canali si dichiarano in due modi, e la differenza e' sostanziale:

Nella traduzione in FTS i due casi sono molto diversi.

Canale asincrono: si introduce in $Y$ una variabile $\alpha$ il cui valore e' una lista di elementi del tipo del canale.

Send asincrona (l: α ⇐ e; l^): accoda a destra,

$$move(l,l^\wedge)\land \alpha'=\alpha\cdot e\land pres(Y-\{\alpha\}).$$

Receive asincrona (l: α ⇒ u; l^): preleva da sinistra, ed e' enabled solo a canale non vuoto,

$$move(l,l^\wedge)\land |\alpha|>0\land \alpha = u'\cdot\alpha'\land pres(Y-\{u,\alpha\}).$$

Canale sincrono: non si introduce nessuna variabile. La coppia send/receive

l: α ⇐ e; l^      (in un processo)
m: α ⇒ u; m^      (in un altro processo)

genera un'unica transizione congiunta:

$$\rho_{l,m}:\ move(\{l,m\},\{l^\wedge,m^\wedge\})\land u'=e\land pres(Y-\{u\}).$$

Due osservazioni da orale:

Vincoli sulle grouped instructions con comunicazioni:

Fairness per la comunicazione: l'insieme $\mathcal{C}$ (compassion) include le transizioni di send/receive, le grouped che contengono comunicazioni, e request. Il motivo e' sempre lo stesso: l'abilitazione dipende da una risorsa condivisa (il partner pronto, il canale non vuoto, $r>0$) che puo' andare e venire a intermittenza — justice non basterebbe a garantire il progresso. $\mathcal{J}$ invece include tutte le transizioni tranne l'idling e quelle di noncritical.

14. Selection, cooperation e grouped instructions

Questi tre costrutti sono facili da confondere.

Selection

Una selection:

S1 or S2 or ... or Sk

introduce non determinismo di scelta.

Il controllo e' davanti a piu' alternative, e lo scheduler sceglie una delle transizioni enabled.

La semantica e' una disgiunzione:

$$\rho_{S_1}\lor\rho_{S_2}\lor\cdots\lor\rho_{S_k}.$$

Se una scelta non viene presa, le altre possono restare disponibili.

Cooperation / parallel composition

La composizione parallela:

S1 || S2 || ... || Sk

non significa che tutti i processi eseguono un passo simultaneo.

Nel corso si usa interleaving:

a ogni passo viene eseguita una sola transizione enabled tra quelle dei processi attivi.

Quindi il parallelismo produce molte interleaving possibili, non una vera sincronizzazione globale a ogni istante.

Grouped instructions

Una grouped instruction:

<S>

rende atomico l'effetto complessivo di $S$.

Invece di esporre tutti i passi intermedi come transizioni separate, si calcola una relazione di trasformazione dati:

$$\delta[S](Y,Y').$$

Per una concatenazione:

S1; S2

la trasformazione usa variabili intermedie:

$$\delta[S_1;S_2](Y,Y')= \exists \widetilde{Y}.(\delta[S_1](Y,\widetilde{Y})\land \delta[S_2](\widetilde{Y},Y')).$$

Questo e' lo stesso trucco logico usato spesso nelle transizioni simboliche: introduco variabili intermedie e poi le elimino con quantificazione esistenziale.

Entry step ed exit step della cooperation

Negli appunti la cooperation dentro un programma,

l: [ [l1: S1; l^1:] || ... || [lk: Sk; l^k:] ]; l^

genera due transizioni dedicate:

E' una sincronizzazione iniziale e finale: in mezzo, puro interleaving. Il corpo del programma e' l'unico caso senza entry/exit step: la computazione parte direttamente con il controllo distribuito sui componenti.

Labels, control locations e post-locations: le regole complete

Piu' label possono denotare la stessa posizione del controllo. La relazione di equivalenza $\approx_L$ si genera con tre regole:

Una control location e' una classe di equivalenza $[l]$ di $\approx_L$, ed e' questo (non la singola label) il valore che entra in $\pi$.

La post-location di un'istruzione e' la location raggiunta al termine della sua esecuzione. Regole:

Istruzione Post-location
concatenazione $[l_1{:}S_1;\ldots;l_k{:}S_k]$ $post(S) = post(S_k)$, e $post(S_i) = l_{i+1}$ per $i<k$
cooperation $post(S_i) = [l^\wedge_i]$, tutte diverse (per questo serve l'exit step)
selection $post(S) = post(S_1) = \cdots = post(S_k)$ (se ne esegue una sola)
conditional $post(S) = post(S_1) = post(S_2)$
while $[l{:}$ while $c$ do $S']$ $post(S') = [l]$: il corpo riporta davanti al while; il while stesso non ha una regola unica (dipende da $c$)
blocco $post(S) = post(S')$

L'esempio del corso: il MCD di Euclide

Il programma SPL per il massimo comun divisore,

in  a, b : integer where a > 0, b > 0
local y1, y2 : integer where y1 = a, y2 = b
out g : integer

l0: [
l1:   while y1 ≠ y2 do
l2:     [ l3: when y1 > y2 do l4: y1 := y1 - y2
          or
          l5: when y2 > y1 do l6: y2 := y2 - y1 ]
l7:   g := y1
l8: ]

e' l'esempio standard per labels e locations. Le classi:

L'FTS corrispondente: $\mathcal{V} = \{\pi, a, b, y_1, y_2, g\}$, dove il dominio di $\pi$ e' l'insieme delle parti di $\{[l_1],[l_2],[l_4],[l_6],[l_7],[l_8]\}$, e

$$\theta = a>0 \land b>0 \land y_1=a \land y_2=b \land \pi=\{[l_1]\}.$$

Qui $\pi$ resta sempre un singoletto (un solo processo); diventa un insieme piu' grande appena c'e' una cooperation. Post-locations: $post(l_1) = [l_7]$, $post(l_2) = post(l_4) = post(l_6) = [l_1]$ (si torna davanti al while), $post(l_7) = [l_8]$.

Ancestor, LCA e istruzioni parallele vs in conflitto

Sull'insieme delle istruzioni si definisce la relazione di antenato: $S$ e' antenato di $S'$ se $S'$ e' una sotto-istruzione di $S$ (riflessiva e transitiva). Il least common ancestor (LCA) di $S_1$ e $S_2$ e' l'antenato comune minimo.

La distinzione che ne segue:

Esempio degli appunti, $[S_1; [S_2 \| S_3]; S_4] \| S_5$:

15. Mutua esclusione, accessibility e communal accessibility

Gli esempi MUX_SEM e MUX_WHEN servono per distinguere safety e liveness.

Mutual exclusion

Mutual exclusion e' una proprieta' di safety:

non deve mai accadere che due processi siano contemporaneamente nella sezione critica.

Se il semaforo $y$ vale 1 quando la risorsa e' libera, allora request y decrementa $y$ a 0. Finche' il processo non esegue release y, l'altro processo non puo' eseguire la propria request.

Quindi la safety dipende dall'invariante sul semaforo.

Accessibility

Accessibility e' una proprieta' di progresso:

se un processo arriva alla fine della regione non critica e chiede la risorsa, prima o poi entra nella regione critica.

Qui la fairness e' decisiva.

Se una request e' abilitata infinite volte ma non viene mai presa, justice puo' non bastare se l'abilitazione e' intermittente. Serve compassion.

Per questo MUX_SEM, con compassion sulle request, puo' garantire una forma piu' forte di accesso.

Communal accessibility

MUX_WHEN puo' soddisfare una proprieta' piu' debole:

se un processo arriva a chiedere la risorsa, prima o poi qualche processo entra in sezione critica.

Non necessariamente lo stesso.

Questa e' communal accessibility.

La distinzione e' utile all'orale: mutual exclusion dice "mai due insieme"; accessibility dice "chi chiede entra"; communal accessibility dice "qualcuno entra".

La prova di accessibility di MUX_SEM, per esteso

Vale la pena saper ripetere l'argomento degli appunti. Supponiamo $P_1$ bloccato a $l_2$ (davanti alla request y). Due casi:

  1. $y$ resta costantemente $1$ da un certo punto in poi (cioe' $P_2$ resta per sempre nella regione non critica): allora l2: request y e' costantemente abilitata e mai presa — viola gia' la justice (che e' implicata dalla compassion). Computazione non ammissibile.
  2. $y$ non resta costantemente $1$: allora $P_2$ continua a ciclare (request, critical, release, noncritical, ...) e la computazione visita infinite volte lo stato con $\pi = \{l_2, m_2\},\ y = 1$, in cui $l_2$ e' abilitata. Abilitata infinite volte, presa mai: viola la compassion richiesta su request. Non ammissibile.

In entrambi i casi la computazione "bloccante" non e' fair, quindi accessibility vale. Nota dove serve davvero compassion: nel caso 2 l'abilitazione e' intermittente e justice da sola non basterebbe — ed e' esattamente cio' che succede in MUX_WHEN, dove su when si richiede solo justice e accessibility fallisce (resta solo communal accessibility).

C'e' anche una proprieta' piu' semplice da non dimenticare: $P_1$ non puo' restare per sempre dentro la regione critica, perche' su critical e' richiesta justice (deve terminare).

Producer/consumer e Fair-Merge (cenni dagli appunti)

Gli appunti chiudono il capitolo con due esempi di programmi con canali:

Sono esercizi tipo del "chapter 0": saperli impostare (variabili, canali, fairness richiesta) e' piu' importante che ricordarli a memoria.

16. Mini-scaletta orale

  1. Il contesto: Differenza tra programmi trasformazionali e reattivi (le computazioni qui sono infinite).
  2. Lo strumento di modellazione: SPL, con classi di istruzioni: basic, schematiche, compound e grouped.
  3. Labels e controllo: Spiegare post-location e variabili di controllo, cioè come il programma diventa uno stato FTS.
  4. La struttura formale (FTS): Elencare i 5 elementi $\langle \mathcal{V}, \Theta, \mathcal{T}, \mathcal{J}, \mathcal{C} \rangle$.
  5. Transizioni abilitate: Dire che $\tau$ è abilitata se esiste almeno uno stato successivo che soddisfa $\rho_\tau$.
  6. Il problema dello scheduler patologico: Spiegare perché serve la Fairness (evitare falsi controesempi di liveness dovuti a starvation irreale).
  7. Le due forme di Fairness: Definire precisamente la differenza chiave tra continuamente abilitata (Justice) e abilitata infinite volte (Compassion).
  8. Esercizi tipici: Ragionare su await/skip, request/release, mutua esclusione, accessibility e communal accessibility.

17. Quiz interattivo per l'autovalutazione

Quiz Settimana 2 - Capitolo 4: FTS e Fairness

1. In un FTS, cos'è lo stato di un sistema?




2. Quale delle seguenti definizioni descrive la *Compassion* (Strong Fairness)?




3. Perché in Model Checking applichiamo la fairness ai sistemi reattivi?




18. Fonti usate

Esercizi (piano di studio)

Esercizi e domande — settimana 2

Obiettivo della settimana: capire come si impara un automa e come si modellano sistemi reattivi con fairness.

Esercizi scritti essenziali

  1. MAT framework. Scrivi un esempio completo di dialogo Learner/Teacher per il linguaggio: $$L=\lbrace w\in\lbrace a,b\rbrace^* \mid w \text{ contiene almeno una } a\rbrace$$ Includi almeno 5 membership query, una equivalence query sbagliata e un controesempio.

  2. Observation table L*. Per: $$L=\lbrace w\in\lbrace a,b\rbrace^* \mid w \text{ termina con } a\rbrace$$ costruisci una tabella iniziale con $S=\lbrace \epsilon\rbrace$ e $T=\lbrace \epsilon\rbrace$. Espandila finche diventa chiusa e consistente. Disegna il DFA ipotesi.

  3. Controesempio L*. Supponi che l'ipotesi per il linguaggio precedente accetti tutte le stringhe. Trova un controesempio e mostra come aggiorna la tabella.

  4. T-complete e T-minimal. Prendi una tabella a tua scelta e verifica formalmente se e' T-complete e T-minimal. Se non lo e', indica quale riga o transizione forza l'espansione.

  5. Hankel matrix. Costruisci una porzione della matrice di Hankel per: $$L=\lbrace w\in\lbrace 0,1\rbrace^* \mid \#1(w) \text{ e' pari}\rbrace$$ usando prefissi e suffissi fino a lunghezza 2. Identifica quante righe distinte servono.

  6. Confronto. Scrivi una tabella a due colonne: Myhill-Nerode vs L*. Metti: obiettivo, informazione usata, output, criterio di stop.

  7. FTS formale. Definisci un FTS per un contatore modulo 3 con variabile $x\in\lbrace 0,1,2\rbrace$, iniziale $x=0$, transizione inc, e idling. Specifica $\mathcal{V},\Theta,\mathcal{T},\mathcal{J},\mathcal{C}$.

  8. Justice vs compassion. Costruisci una computazione infinita in cui una transizione e' abilitata infinite volte ma non continuamente abilitata. Usa l'esempio per spiegare perche compassion e' piu forte di justice.

  9. SPL -> FTS. Scrivi un mini programma SPL con due processi: P1: await x=0; x:=1 e P2: await x=1; x:=0. Modellalo come FTS con stati di controllo e transizioni.

  10. Starvation. Descrivi una computazione unfair in cui un processo resta affamato. Poi aggiungi una condizione di fairness che la esclude.

Domande orali secche

  1. Perche le membership query da sole non bastano in modo efficiente?
  2. Che cosa contiene una observation table?
  3. Che rapporto c'e' tra righe della tabella e stati del DFA?
  4. Differenza tra sistema terminante e sistema reattivo.
  5. Differenza tra justice e compassion con un esempio.

Controllo

Hai superato la settimana se riesci a simulare a mano un giro di L* e a spiegare fairness senza confondere "sempre abilitata da un certo punto" con "abilitata infinite volte".

Indice← PrecedenteSuccessivo →