Home

Federica EU

1/19

Adriano Peron » 6.FSM e Parallelismo

Rappresentazione del parallelismo

I formalismi FSM precedentemente studiati sono intrinsecamente sequenziali e non consentono la rappresentazione esplicita del parallelismo.

La rappresentazione esplicita del parallelismo permette la naturale rappresentazione di sistemi concorrenti, distribuiti e comunicanti.

Ad esempio:

rappresentazione sia di un sistema reattivo sia dell’ambiente che lo sollecita (evoluzione concorrente e comunicazione);
rappresentazione di moduli di uno stesso sistema che evolvono indipendentemente a meno di sincronizzazioni puntuali (concorrenza e comunicazione);
rappresentazione di sistemi spazialmente distribuiti che evolvono indipendentemente a meno di trasferimento di informazioni (concorrenza, distributezza, comunicazione).

La rappresentazione esplicita del parallelismo enfatizza il concetto di modularità (orizzontale) e facilita lo sviluppo modulare delle specifiche.

Modello semantico del parallelismo

In letteratura sono presenti due categorie di modelli semantici per formalismi che permettono la rappresentazione del parallelismo:

interfogliazione (Interleaving): nel modello semantico le azioni che vengono eseguite in parallelo sono eseguite sequenzialmente mediante interfogliazione (vengono rappresentatate tutte le possibili sequenzializzazioni);
- Idea: programmi paralleli eseguiti su di una macchina con un solo processore;
reale concorrenza (True Concurrency): nel modello semantico viene esplicitamente rappresentata l’esecuzione concorrente.

Comunicazione

Nella rappresentazione esplicita del parallelismo assumono rilievo le forme di comunicazione tra le componenti parallele.

Comunicazione mediante canale ed invio di messaggi:

Handshacking (comunicazione uno a uno):

orientata: dal sender verso il receiver;
canale condiviso: le due parti hanno visibilità del nome del canale (non necessariamente privato);
sincrona: l’azione del sender deve essere simultanea a quella del receiver e l’indisponibiltà di una delle parti blocca la possibilità di trasmissione.

Broadcast (comunicazione uno a molti):

orientata: dal sender verso i receiver;
asincrona: l’azione del sender non presuppone la simultanea disponibilità alla ricezione e può avvenire in assenza di riceventi; la ricezione può avvenire (in presenza di strutture di memorizzazione) in tempi successivi alla trasmissione.

Comunicazione (segue)

La forma di comunicazione via canale può essere:

pura: si astrae dal contenuto del messaggio;
con valore: la comunicazione trasmette un messaggio con valore.

(se il numero dei possibili valori di un messaggio è finito si può simulare la comunicazione con valore mediante comunicazione pura predisponendo un canale per ogni messaggio).

Comunicazione mediante condivisione di variabili:

orientata: dal mittente (accesso in modifica delle variabili) al destinatario (accesso in lettura delle variabili);
asincrona: la lettura e la modifica simultanea delle variabili non è possibile (meccanismo meno strutturato rispetto alla comunicazione via canale che consente comunque di simulare forme di handshacking e di broadcast).

Semantica ad Interleaving

Adozione del modello interleaving

Rappresentazione esplicita del parallelismo nella specifica.

Rappresentazione implicita del paralleismo nel modello semantico mediante sequenzializzazione e non-determinismo.

Possibile esplosione del numero degli stati dell’LTS dovuta alla natura combinatorica dell’interfogliazione.

Fig.1 Interleaving di due transizioni parallele.

Automi paralleli senza comunicazione

Introduzione del parallelismo nelle FSM.

Un automa parallelo è un collezione ordinata di automi sequenziali
$\begin{array}{c}A_1 \| A_2 \| \ldots \| A_n \mbox{ con } \\A_i= \langle\Sigma,Q_i, q_{0,i}, \Delta_i ,F_i \rangle, \mbox{ per } 0\leq i\leq n.\end{array}$

Gli automi condividono il medesimo alfabeto. Non è prevista una forma di comunicazione tra le componenti.

Possono essere dotati di due modelli semantici diversi:

modello sincrono: le transizioni attive che hanno lo stesso trigger scattano sincronamente (in reale concorrenza);
modello asincrono: le transizione attive che hanno lo stesso trigger scattano asincronamente (interleaving).

Semantica degli automi paralleli

Una possibile semantica è data dal seguente LTS

$\langle S,S_0,\Delta \rangle$ ,

$\begin{array}{llll}S &= &Q_1 \times \ldots \times Q_n \\S_0 & = & (q_{0,1},\ldots ,q_{0,n})\\\Delta & = &\{(s_1,a,s_2) : &s_1 = (q_{1},\ldots ,q_{n}), \\&&& \mbox{esiste } K \subseteq \{1,\ldots,n\}, K\neq \emptyset \mbox{ t.c.} \\&&& (q_i,a,q'_i) \in \delta_i \mbox{ per ogni } i\in K\\&&& s_2 = (p_{1},\ldots ,p_{n}) \mbox{ e } \\&&& p_i = q'_i \mbox{ se } i\in K \mbox{ e } p_i =q_i \mbox{altrimenti }\}.\end{array}$

Osservazioni

Uno stato in $Q_1 \times \ldots \times Q_n$ descrive lo stato corrente in ciascuna delle componenti.

L’insieme K descrive il sottoinsieme delle componenti che fanno uno scatto simultaneo essendo stimolate dallo stesso simbolo.

A seconda della scelta dell’insieme K si possono avere diverse semantiche:

completamente sincrona se K è scelto sempre come insieme massimale; tutte le transizioni che possono scattare in parallelo deve scattare. E’ la semantica preferibile (modello a reale concorrenza);

completamente asincrona se K è un singoletto. Solo una della transizioni che possono scattare scatta (modello ad interleaving).

Se non ci sono condizioni su K il sincronismo non è forzato e la scelta sull’insieme delle transizioni che, essendo abilitate scattano, è non-deterministica.

Esempio

Per la semantica dell’esempio si assume una semantica completamente sincrona (scatto dell’insieme massimale delle transizioni abilitate).

$A_1$ e $A_2$ sono due copie della stessa macchina che lavorano in parallelo.

Alla richiesta di inizio lavoro (segnale init) una macchina decide non-deterministicamente se svolgere il servizio oppure restare inattiva.

L’avanzare del servizio è regolato dal segnale do e la terminazione del servizio dal segnale exit.

Nel caso in cui entrambe le macchine accettino la richiesta evolvono in maniera perfettamente sincrona.

La scelta non-determinsitica iniziale permette di sfasare tra loro i comportamenti delle due macchine altrimenti sempre costrette ad una evoluzione perfettamente sincrona.

Esempio: Automa parallelo sincrono

Fig.2 Due copie della stessa macchina evolvono in parallelo.

Parallelismo e comunicazione

L’assenza di forme di comunicazione tra le componenti parallele rende scarsamente utilizzabile il formalismo come strumento di specifica.

Nel prosieguo si prenderà in considerazione la composizione parallela di macchine con l’aggiunta di forme alternative di comunicazione.

I casi considerati sono:

comunicazione sincrona mediante canali (comunicazione uno-a-uno handshaking);
comunicazione asincrona mediante canali (comunicazione uno-a-uno con buffer);
comunicazione mediante condivisione di variabili.

Le tre forme di rappresentazione di parallelismo e comunicazione verranno studiate nell’ambiente di verifica SPIN considerando:

Codifica degli automi paralleli comunicanti mediante il linguaggio testuale PROMELA.

Esecuzione delle specifiche mediante il motore di SPIN.

Parallelismo e comunicazione sincrona mediante canali

La forma di comunicazione tra le componenti parallele è un handshaking: una coppia di automi comunica in modo sincrono, l’uno inviando un messaggio, l’altro ricevendo il messaggio.

$\begin{array}{c}A_1 \| A_2 \| \ldots \| A_n \mbox{ con } \\A_i= \langle\Sigma_{I,i},\Sigma_{O,i},Q_i, q_{0,i}, \Delta_i ,F_i \rangle, \mbox{ per } 0\leq i\leq n.\end{array}$

Canali
I canali di comunicazione sono puri (non trasmettono messaggi e rappresentano il solo evento comunicativo).
Ogni automa $A_i$ vede un insieme di canali $\Sigma_i= \Sigma_{O,i}\cup \Sigma_{I,i}$ .

Direzionalità della comunicazione

Per rappresentare la direzionalità della comunicazione (invio e ricezione) l’alfabeto $\Sigma_i$ di un automa viene ripartito in due sottoinsiemi disgiunti dei simboli di input $\Sigma_{I,i}$ (ricezioni) e di output $\Sigma_{O,i}$ (invii).

Tipologie di eventi comunicativi

Ricezione proveniente dall’ambiente esterno

Elemento $a \in \Sigma_{I,i}$ che non viene comunicato da nessuna componente parallela: $a \not\in \bigcup_{j\neq i} \Sigma_{O,j}$ .

L’insieme delle ricezioni dall’ambiente esterno è denotato da $Env_I$ .

Invio all’ambiente esterno

Elemento $a \in \Sigma_{O,i}$ che non viene comunicato a nessuna componente parallela: $a \not\in \bigcup_{j\neq i} \Sigma_{I,j}$

L’insieme degli invii all’ambiente esterno è denotato da $Env_O$ .

Invio o ricezione tra componenti parallele

Elemento $a \in \Sigma_{I,i} \cap \Sigma_{O,j}$ oppure $a \in \Sigma_{O,i} \cap \Sigma_{I,j} \mbox{ per qualche } j\neq i$ .

Semantica: idee

Interfogliazione (scatto asincrono) delle transizioni degli automi che possono evolvere indipendentemente dalle altre componenti (ricezioni e invii rispetto all’ambiente esterno ed azioni interne alle singole componenti); le transizioni sono osservabili dall’esterno.

Scatto sincrono per coppie di transizioni che ricevono da o comunicano a componenti parallele; ogni transizione di invio o ricezione interna ha bisogno dello scatto sincrono di una transizione dall’azione complementare sullo stesso canale (rappresentazione in reale concorrenza dello scatto della coppia di transizioni).

Le transizioni di comunicazione interna che non possono osservare lo scatto di una transizione complementare rimangono bloccate in attesa.

La sincronizzazione di due transizioni complementari dà luogo ad una transizione non osservabile dall’esterno etichettata da $\tau$ .

Semantica: definizione

La semantica è espressa dall’LTS $\langle S,S_0,\Delta \rangle$

$\begin{array}{lll}S & = & Q_1 \times \ldots \times Q_n\\S_0 &=& \{(q_{0,1},\ldots , q_{0,n})\}\\\Delta & = & \mbox{unione dei seguenti insiemi}\\&& \{((q_1, \dots ,q_i, \ldots ,q_n),a,(q_1, \dots ,q'_i, \ldots ,q_n)) : \\\mbox{esterne}&&a\in (ENV_I \cup ENV_O), (q_i,a,q'_i) \in \delta_i \mbox{ per } 1\leq i \leq n \}\\\mbox{interne}&& \{((q_1, \dots ,q_i, \ldots ,q_n),\tau,(q_1, \dots ,q'_i, \ldots ,q_n)) : \\&&(q_i,\tau ,q'_i) \in \delta_iper $ 1\leq i \leq n\}\\\mbox{sincrone}&& \{(\tpl{q_1, \dots ,q_i, \ldots, q_j,\ldots ,q_n},\tau,\tpl{q_1, \dots ,q'_i, \ldots, q'_j, \ldots ,q_n}) :\\&&\mbox{ o } a\in \Sigma_{I,i} \cap \Sigma_{O,j} \mbox{ o }a\in \Sigma_{O,i} \cap \Sigma_{I,j} \mbox{ e }\\&& (q_i,a ,q'_i) \in \delta_i \mbox{ e } (q_j,a ,q'_j) \in \delta_j\mbox{ per } 1\leq i < j \leq n \}.\end{array}$

Esempio: registro di scorrimento

La prima cella riceve in ingresso un segnale $a_1$ dall’ambiente.

Il segnale viene shiftato e restituito all’ambiente sotto forma di $a_{n+1}$ .
Il registro permette di memorizzare fino a n istanze del segnale $a_1$ inoltrato dall’ambiente.

L’automa ha la forma $A_1 \| A_2 \| \ldots \| A_n$
con $A_1= \langle\Sigma_i \cup\{\tau \},Q_i, q_{0,i}, \Delta_i \rangle, \mbox{ per } 0\leq i\leq n \mbox{ dove }$

$\begin{array}{lll}\Sigma_{I,i} &=& \{a_i\}\\\Sigma_{O,i} &=&\{a_{i+1}\}\\Q_i &=& \{q_{0,i},q_{1,i}\}\\\delta_i &=& \{\langle q_{0,i},a_i,q_{1,i}\rangle,\langle q_{1,i},a_{i+1},q_{0,i}\rangle\}.\end{array}$