Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D La Corte in Rete
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

Adriano Peron » 8.FSM e Parallelismo – terza parte


Parallelismo e comunicazione mediante variabili condivise

La forma di comunicazione tra le componenti è quella elementare della condivisione di variabili.

La forma di comunicazione è classificabile come:

  • Uno-a-molti (molte letture possono far seguito ad un aggiornamento);
  • Asincrona;
  • Direzionata (da chi aggiorna verso chi legge).

Per semplicità si assume:

  • Di avere un insieme di variabili Var di tipo intero INT;
  • Per le variabili x in Var sia fissato il valore minimo e massimo (MinInt, MaxInt) che la variabile può assumere.

La limitazione sui valori delle variabili è essenziale per garantire la finitezza degli stati del sistema.

Espressioni aritmetiche

Nella forma più generale, una transizione di una macchina a stato-transizione assume la forma

Stato\ \stackrel{Trigger,Condizione,Azione} {\longrightarrow }\ Stato'.

Nel formalismo preso in considerazione si ha che:

Il Trigger mantiene la forma semplice di uno simbolo appartenente ad un alfabeto;
La Condizione è una espressione booleana sul contenuto delle variabili in Var;
l’Azione è un insieme di assegnazioni di una espressione aritmetica ad una variabile.

Categoria delle espressioni aritmetiche Aexp

La categoria Aexp delle espressioni aritmetiche sull’inseme delle variabili Var è definita come segue:

\psi\ ::=\ c\ |\ x \ |\ \psi + \psi\ |\ \psi - \psi\ |\ \psi * \psi

dove c \in Int, MinInt \leq c \leq MaxInt, \mbox{ e } x \in Var.

Espressioni booleane e assegnamenti

Categoria delle espressioni booleane Bexp

La categoria Bexp delle espressioni booleane sull’insieme delle variabili Var è definita come segue:

\phi\ ::=\ True\ |\ x < \alpha\ |\ x > \alpha\ |\ x=\alpha\ |\ \phi \wedge \phi\ |\ \phi \vee \phi\ |\  \neg \phi

dove \alpha \in Aexp,\mbox{ e } x \in Var.

Categoria delle assegnazioni Assign

La categoria Assign delle assegnazioni è definita dall’insieme delle espressioni della forma

x := \alpha \mbox{ con } x\in Var \mbox{ e } \alpha\in Aexp.

Automi comunicanti mediante condivisione di variabili

Fissato un insieme Var di variabili intere un automa parallelo ha la forma   A_1 \| A_2 \| \ldots \| A_n \mbox{ con }

A_1=\langle\Sigma_i ,Q_1, q_{0,i}, \delta_i \rangle\mbox{, per } 0\leq i\leqn \mbox{ dove}

\delta_i \subseteq Q_i \times \Sigma_i \times Bexp \times 2^{Assign}\times Q_i

Si assume che se (q,a,\phi,A)\in \delta_i in A non possano comparire due assegnazioni alla stessa variabile.

Semantica – Stati LTS

La descrizione dello stato globale di un automa comprende lo stato di controllo di ciascuna delle componenti e la valutazione delle variabili in Var.

La valutazione delle variabili Var è descritta da una funzione (totale) di valutazione

\rho : X \rightarrow Int tale che  MinInt \leq \rho(x) \leq MaxInt \mbox{ per ogni }x \in Var.

Sia \Xi l’insieme delle possibili funzioni di valutazione delle variabili.

La semantica è data dall’LTS \langle S,S_0,\Delta \rangle, \mbox{ dove }

  • S = Q_1 \times \ldots \times Q_n \times \Xi;
  • S_0 = \{(q_{0,1},\ldots , q_{0,n},\rho_0)\};

con \rho_0(x)=0 \mbox{ per ogni } x\in Var.

Semantica – Valutazione espressioni aritmetiche

Preliminare alla definizione della relazione di transizione dell’LTS è la definizione della valutazione di espressioni aritmetiche e booleane.

Per una espressione \alpha \in Aexp \mbox{ e una valutazione } \rho \in \Xi, la funzione di valutazione

val : \Xi \times Aexp \rightarrow Int

è definita induttivamente come segue:

  • val(\rho , c) = c \mbox{ per ogni } c \in Int;
  • val(\rho ,x) = \rho(x) \mbox{ per ogni } x \in Var;
  • val(\rho , \alpha_1 + \alpha_2) = val(\rho , \alpha_1) + val(\rho , \alpha_2)\mbox{ per ogni } \alpha_1,\alpha_2 \in Aexp;
  • val(\rho , \alpha_1 - \alpha_2) = val(\rho , \alpha_1) - val(\rho , \alpha_2)\mbox{ per ogni } \alpha_1,\alpha_2 \in Aexp;
  • val(\rho , \alpha_1 * \alpha_2) = val(\rho , \alpha_1) * val(\rho , \alpha_2)\mbox{ per ogni } \alpha_1,\alpha_2 \in Aexp.

Semantica – Valutazione espressioni booleane

Per una espressione \phi \in Bexp \mbox{ e una valutazione } \rho \in \Xi, la funzione di valutazione

valb : \Xi \times Bexp \rightarrow \{True,False\}

è definita induttivamente come segue:

  • valb(\rho , True) = True;
  • valb(\rho ,x<\alpha) = True \mbox{ se } \rho(x) <  val(\rho,\alpha) e False, altrimenti;
  • valb(\rho ,x>\alpha) = True \mbox{ se } \rho(x) >  val(\rho,\alpha) e False, altrimenti;
  • valb(\rho ,x=\alpha) = True \mbox{ se } \rho(x) =  val(\rho,\alpha) e False, altrimenti;
  • valb(\rho ,\phi_1 \wedge \phi_2) = valb(\rho ,\phi_1) \wedge valb(\rho ,\phi_2);
  • valb(\rho ,\phi_1 \vee \phi_2) = valb(\rho ,\phi_1) \vee valb(\rho ,\phi_2);
  • valb(\rho ,\neg \phi) = \neg valb(\rho ,\phi).

Relazione di transizione dell’LTS

\Delta è data dal seguente insieme di transizioni:  \{((q_1, \dots ,q_i, \ldots ,q_n,\rho),a, (q_1, \dots ,q'_i, \ldots ,q_n,\rho')):

\begin{array}{l}(q_i,a,\phi,A,q'_i) \in \delta_i,\\valb(\rho,\phi)=True,\\A=\{x_1=\alpha_1,\ldots,x_k=\alpha_k\},\\val(\rho , \alpha_j)=m_j \mbox{ con } MinInt \leq m_j \leq MaxInt \mbox{ per ogni } 1\leq j \leq k,\\\rho'(x_j) = m_j \mbox{ per ogni } 1\leq j \leq k,\\\rho'(x) = \rho(x) \mbox{ per ogni } x \not \in \{x_1, \ldots ,x_k\}\}.\end{array}

Il modello di parallelismo adottato è puramente interleaving (scatta una sola transizione alla volta).

Si osservi che l’assegnazione delle variabili devono rispettare i limiti MinInt e MaxInt del dominio di definizione.
Il mancato rispetto ha effetto bloccante sulla transizione.

Esempio di specifica 1

Accesso in mutua esclusione ad una sezione critica: Soluzione 1

Accesso in mutua esclusione ad una sezione critica: Soluzione 1


Esempi di specifica

Fig. 1. Protocollo di accesso in mutua esclusione, Soluzione 1

Fig. 1. Protocollo di accesso in mutua esclusione, Soluzione 1


Esempio di specifica 2

Accesso in mutua esclusione ad una sezione critica: Soluzione 2

Accesso in mutua esclusione ad una sezione critica: Soluzione 2


Soluzione 2. Prima formulazione

Fig. 2. Protocollo di accesso in mutua esclusione, Soluzione 2. Prima formulazione

Fig. 2. Protocollo di accesso in mutua esclusione, Soluzione 2. Prima formulazione


Soluzione 2. Seconda formulazione

Fig. 1. Protocollo di accesso in mutua esclusione, Soluzione 2, Seconda formulazione

Fig. 1. Protocollo di accesso in mutua esclusione, Soluzione 2, Seconda formulazione


Specifiche a confronto

Soluzione 1.

  • Garantisce la mutua esclusione nell’accesso alla sezione critica;
  • Soffre di problemi di deadlock.

Soluzione 2.

Formulazione 1:
Non garantisce la mutua esclusione nell’accesso alla sezione critica.

Nell’entrata nella sezione critica il controllo di flag2 e l’assegnazione di flag1 non sono atomiche e separabili dall’interfogliazione nell’esecuzione delle transizioni.

Formulazione 2:
Garantisce la mutua esclusione nell’accesso alla sezione critica.

Nell’entrata nella sezione critica il controllo di flag2 e l’assegnazione di flag1 sono atomiche (sono fatte nella medesima transizione).

  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion

Fatal error: Call to undefined function federicaDebug() in /usr/local/apache/htdocs/html/footer.php on line 93