Home

Federica EU

1/21

Adriano Peron » 9.Promela

SPIN

SPIN è un sistema per il model checking per proprietà di programmi software asincroni.

Il sistema è reperibile nel sito Spinroot.

Linguaggio per la scrittura di programmi asincroni.

PROMELA: linguaggio testuale di tipo imperativo con costrutti per la descrizione di processi paralleli e comunicanti.

Manuale in linea

Linguaggio per la scrittura delle proprietà da verificare.

LTL: Linear Temporal Logic.

PROMELA: Variabili e tipi di dato

Variabili dei seguenti tipi di dati di base predefiniti

bit Dimensione 1, Valori 0..1
bool Dimensione 1, Valori 0..1
byte, Dimensione 8, Valori 0..255
short Dimensione 16, Valori $-2^{15}..2^{15}-1$
int Dimensione 32, Valori $-2^{31}..2^{31}-1$
chan (Tipo canale di comunicazione)_

Dichiarazioni variabili

<tipo><variabile>;<tipo><variabile> ; int state; byte msg;

Dichiarazioni array

<tipo><variabile>[dimensione]; byte stato[100] (locazioni 0..99)_

PROMELA: alcune istruzioni di base

Assegnamento

<nome><variabile>=<espressione>;

Es. state = state + 1

Azione nulla

skip

Condizione

(<espressione booleana>)

Es. (a == b)

Una condizione booleana è una istruzione eseguibile.
La condizione è eseguibile se la sua valutazione è vero; se eseguita permette al flusso del controllo di passare all’istruzione successiva.
L’esecuzione di una istruzione booleana con valutazione diversa da vero è sospesa finché la sua valutazione non diviene vero.

PROMELA: Tipi processo

Per eseguire un processo serve

avere la possibilità di nominarlo;
definire il suo tipo;
istanziarlo.

proctype <nome> ([parametri])‏ { <body> }

Il corpo comprende dichiarazioni locali e/o istruzioni.

Esempio: dichiarazione di una variabile globale (statoglobale) e di due processi (A e B).

proctype A (byte parametro)
{ byte statolocale;(parametro==1) ->statolocale=4 }

byte statoglobale

proctype B ()
{ (statoglobale==4)-> statoglobale=statoglobale-1 } ‏

(; e -> sono due separatori di istruzioni tra loro intercambiabili)
Possono essere associati solo parametri di tipo base e non array.

Istanziazione processi

In ogni specifica è necessario dichiarare un processo iniziale

init{ <body>}

(assimilabile ad un main() in un programma C).

Nel processo init è possibile inizializzare variabili globali e instanziare processi

init{ statoglobale=4; run A(1); run B() }

il corpo comprende dichiarazioni locali e/o istruzioni.

Istanziazione di processo

run ([valori parametri])

è un comando sempre eseguibile;
inizializza una copia del tipo di processo;
inizializza i parametri;
restituisce un intero pid (run time process number) che dipende dall’implementazione;
non aspetta che il processo inizializzato termi per terminare;

(Es. dopo aver inizializzato A non si aspetta la terminazione del processo A per inizializzare B).

Istanziazione processi (segue)

Operazione di spawn
- Run può essere usato per istanziare processi in ogni processo, non solo nel processo Init.
- PROMELA modella sistemi a stati finiti e dunque il numero di processi istanziabili è limitato (limite hardware dependent).

Terminazione dei processi
- Un processo in esecuzione termina quando il corpo del processo tipo attivato raggiunde l’istruzione finale;
- Un processo non termina finché tutti i processi che ha istanziato siano terminati.

Attivazione concorrente Init{ statoglobale=4; run A(1); run B() }
- le istanziazioni dei processi A e B sono concorrenti;
- le loro istruzioni sono eseguite in interfogliazione (interleaving).

Interleaving processi

byte stato = 1

proctype A() { (stato ==1)-> stato = stato +1 }

proctype B() { (stato ==1)-> stato = stato - 1 }

init{ run A(); run B() }

Possibili esecuzioni:

A termina prima dell’esecuzione dell’iscruzione condizionale di B: stato=2 e B è di conseguenza bloccato;
B termina prima dell’esecuzione dell’istruzione condizionale di A: stato=0 e A è di conseguenza bloccato;
A e B eseguono l’istruzione condizionale; A esegue l’incremento e poi B il decremento; stato = 1; A e B terminano;
A e B eseguono l’istruzione condizionale; B esegue il decremento e poi A l’incremento; stato = 1; A e B terminano.

Atomicità di sequenze di istruzioni

L’interfogliazione può essere limitata rendendo atomica l’esecuzione di sequenze di istruzioni.

byte stato = 1

proctype A() { atomic {(stato ==1)-> stato = stato +1 }}

proctype B() { atomic {(stato ==1)-> stato = stato -1 }}

init{ run A(); run B() }

Possibili esecuzioni:

A termina prima dell’esecuzione dell’iscruzione condizionale di B: stato=2 e B è bloccato;
B termina prima dell’esecuzione dell’istruzione condizionale di A: stato=0 e A è bloccato;
Solo un processo (scelto in modo non deterministico) ha la possibilità di terminare.

Comunicazione asincrona via canali

PROMELA permette forme di comunicazione sincrona e asincrona mediante canali.

I canali sono tipi di base dichiarati come gli altri tipi di base

chan <nomecanale>= [dim] of { tipo1, .., tipon }

Comunicazione asincrona
- dichiara il nome di un canale;
- il canale è associato ad un buffer di dimensione [dim] > 0 per ospitare messaggi; ciascun valore di messaggio è strutturato come un record con campi di tipo base { tipo1, .. ,tipon }.

Esempio:

chan coda = [10] of { short, short }

I messaggi sono strutturati in coppie di interi. La capacità del buffer è di dieci unità.

Invio e ricezione asincroni su canali

chan <nomecanale> = [dim] of { tipo1, .., tipon }

Comunicazione asincrona (dim > 0)_

Istruzione di Invio

<nomecanale>! <expr1>,..,<exprn>

L’operazione di invio è eseguibile solo se il buffer associato al canale non è pieno.
Il messaggio è memorizzato in coda al buffer;
Se vengono passati solo m < n valori, gli ultimi n-m campi del messaggio hanno valore indefinito.

Istruzione di Ricezione

<nomecanale>? <Var1>,..,<Varn>

L’operazione di ricezione è eseguibile solo se il buffer del canale non è vuoto;
L’operazione estrae il messaggio dalla testa del buffer e memorizza le componenti del messaggio in ordine nelle variabili;
Se sono presenti solo m < n variabili, gli ultimi n-m campi del messaggio sono ignorati.

Invio e ricezione asincroni su canali (segue)

Per verificare il numero di messaggi in coda ad un canale

len (<nomecanale> )

atomic { (len(canale) > 1) -> canale?X }

Per condizionare la ricezione alla presenza di valori specifici nel messaggio

<nomecanale>? <Const1> ,..,<Varn>

Al posto di una variabile si può avere un valore costante;
L’istruzione viene eseguita solo se la componente corrispondente a una costante ha lo stesso valore espresso dalla costante.

Canale?0
eseguibile solo se il messaggio in testa al buffer è 0

Variante in forma di condizione

Canale?[0]
Condizione verificata se Canale? 0 è eseguibile. Non altera il contenuto del buffer.

Invio e ricezione asincroni su canali (segue)

I nomi dei canali per le operazioni di comunicazione possono essere parametrici e comunicati dinamicamente ai processi

proctype A(chan c1)_
{ chan c2 ;
c1?c2;
c2!25
}

sul canale parametrico c1 A riceve il nome di un canale (C2) e su quel canale trasmette 25. Nell’esempio il canale effettivamente usato è “canale”.

Init
{
short X;
chan passaggio = [1] of { chan };
chan canale = [1] of { short };
run A( passaggio );
paggaggio!canale;
canale?X
}

Sequence chart della simulazione dell’esempio della slide precedente:

Ogni blocco rappresenta un processo ed il suo stato di avanzamento;
Ogni freccia rappresenta una comunicazione tra processi;
Esempio 1!2 indica che il processo Init tramite il canale 1 (passaggio) comunica il canale 2 (canale);
Sul canale 2 (canale) il processo A invia poi il valore 25.

Fig.1 Sequence chart

Comunicazione sincrona su canali

chan <nomecanale>[0] of { tipo1, .., tipon }

con dimensione 0 del buffer la comunicazione è sincrona nella forma dell’ HANDSHACKING.

Esempio:

chan canale = [0] of {int}

proctype A (){ canale!125; canale!126 }
proctype B (){ int X; canale?X }
init {run A(); run B()}

Solo il processo B può terminare dopo la prima sincronizzazione.
Il processo A rimane in attesa della seconda sincronizzazione e non può terminare (stato waiting).

Costrutti di controllo

Costrutto di scelta
if
:: istruzione1
:: istruzione 2

:: istruzione n
fi

Tra le istruzioni elencate, viene scelta una istruzione eseguibile; Se più di una istruzione è eseguibile la scelta è non-deterministica; L’istruzione If non è eseguibile quando nessuna delle istruzioni è eseguibile.

Costrutto iterativo

do
:: istruzione1
:: istruzione 2

:: istruzione n
od

Ad ogni iterazione viene scelta una sola istruzione eseguibile con lo stesso criterio del costrutto if;
L’uscita dall’iterazione è attuata mediante l’esecuzione dell’istruzione break.

Esempio

proctype contatore() { int X =1; do :: (X != 0); if :: X=X+1 :: X=X-1 fi :: (X == 0); break od }

Ad ogni iterazione solo una delle istruzioni del ciclo do può essere eseguita;
Se X è pari a zero si termina il ciclo;
Se X è diverso da zero la scelta tra incremento e decremento è non-deterministica;
Non è garantito che il processo termini.

Costrutti di controllo

Costrutto di salto incondizionato

Il salto incondizionato è una istruzione sempre eseguibile;
La scelta dei nomi delle etichette deve essere fatta con cura: le etichette che abbiano i seguenti prefissi “end“, “progress“, “accept” assumono significato specifico chiarito nelle lezioni successive.

Esempi di specifica

Fig. 2 Esempio di specifica: shift register con due posizioni e canali di comunicazione asincroni.

Esempi di specifica (segue)

Fig. 3 Esempio di specifica: shift register con due posizioni e canali di comunicazione sincroni.

Esempio

Processi ricorsivi descritti mediante run (spawn) e canali.
Esempio della definizione per il fattoriale.

proctype fact(int n; chan p)
{ chan child = [1] of { int };
int result;
if :: (n <= 1) -> p!1
:: (n >= 2) -> run fact(n-1, child); child?result; p!n*result
fi }

init { chan child = [1] of { int };
int result;
run fact(4, child);
child?result }

SPIN, permettendo di definire solo programmi a stati finiti, consente solo la creazione di un numero limitato (dall’implementazione) di processi e dunque non consente di calcolare il fattoriale per numeri arbitrari.