Corso di Elementi di Software Dependability
Proposta di elaborato
A.A. 2012-13
Si richiede la modellazione di un algoritmo distribuito di “leader election”
Si considera un sistema distribuito costituito di un numero n di nodi. I nodi sono anonimi e
uguali tra loro. In particolare i nodi inizialmente non conoscono il numero totale di nodi, ma
conoscono solo la topologia di connessione verso gli altri nodi. Non esiste quindi un
meccanismo predefinito per distinguere i nodi, ma si suppone una topologia ad anello, nel
quale ogni nodo sa trasmettere un messagio al nodo precedente e al nodo successivo
dell’anello.
L’algortimo oggetto dell’elaborato ha come scopo quello di produrre la conoscenza di un
leader, per poi poter instaurare algoritmi di identificazione dei nodi a partire dal nodo leader.
L’algoritmo procede per passi successivi all’aggregazione di cluster di nodi di grandezza via
via crescente, fino ad ottenere un unico cluster di dimensione massima. Avendo un cluster un
primo nodo e un ultimo nodo, Il primo nodo del cluster massimo diventa il leader.
Un cluster C è definito come un insieme di nodi adiacenti della rete (ovvero una porzione di
anello), tale che sono definiti:
- primo(C) il primo nodo in senso orario del cluster,
- ultimo(C) l’ultimo nodo del cluster in senso orario
- ordine(C) il numero di nodi del cluster.
Di conseguenza, un nodo di un cluster si può trovare in uno dei macrostati:
primo nodo
ultimo nodo
nodo intermedio.
Nel caso che ordine(C) =1, il relativo nodo non ha questa distinzione di stato. Nel caso
ordine(C) =2, i nodi del cluster possono solo essere in uno dei primi due stati.
Un nodo, in ogni passo dell’algoritmo, localmente sa di appartenere ad un cluster di cui
conosce l’ordine.
L’algoritmo procede in modo iterativo come segue:
1) Fase iniziale.
2) Round di aggregazione
3) consolidamento delle aggregazioni
4) test di terminazione dell’algoritmo: se negativo, torna a 2)
5) finalizzazione
1) Fase iniziale: Si sono già definite le condizioni iniziali; n cluster di ordine 1, ogni nodo sa
di appartenere ad un cluster di ordine 1.
2) Round di aggregazione: Ogni cluster, indipendentemente, invia al cluster alla sua destra e
al cluster alla sua sinistra una richiesta di aggregazione. Sulla base delle risposte ricevute (ad
esempio, considerando la prima risposta ottenuta) il cluster sceglie se aggregarsi a sinistra o
a destra e consolida questa scelta con il cluster presecelto. Lo schema di funzionamento è
definito come segue (mediante UML SD di UMC) per un cluster di ordine 1, ovvero un nodo.
Si distingue la trasmisisone delle richieste iniziali, eseguita in paralello alla ricezione. La
ricezione stabilisce subito, nondetrministicamente, se il nodo si polarizza a sinistra o destra,
con relativi messaggi di ack per consolidare la decisione tra i nodi.
Il round di aggregazione di un cluster ha un comportamento analogo, e transita quindi per gli
stessi stati, ma poiché il primo e l’ultimo nodo di un cluster lavorano autonomamente, è
necessario assicurare la consistenza della decisione per tutti i nodi del cluster, mediante un
algoritmo di two-phase commit protocol.
3) consolidamento delle aggregazioni
La fase precedente termina con la decisione del primo e dell’ultimo nodo. La fase di
consolidamento ha lo scopo di consolidare l’appartenenza ai cluster, attraverso messagi
all’interno deI cluster: ogni nodo di un cluster precisa il suo stato e acquisice il valore
dell’ordine del cluster.
Inoltre, si noti che l’algoritmo raffigurato per un cluster di ordine 1 invia molti messaggi che
non vengono ricevuti e quindi rimangono (nella semantica UML di UMC) nelle code di
eventi. I messaggi “orfani” devono essere trascurati e anche il nodo che non si è aggregato
deve sapere che la fase di aggrregazione è finita. La fase di conoslidamento ha quindi anche il
compito di assuicurarsi che ogni cluster abbia completato lla fase di aggregzione e che non vi
siano messaggi spuri rimasti pendenti.
4) test di terminazione dell’algoritmo
L’algoritmo è terminato quando una qualsiasi delle seguenti condizioni è verificata:
- un cluster ha ordine uguale ad n
- per un cluster C, succ(ultimo(C)) = primo (C)
- per un cluster C, un messaggio inviato da primo(C), via via inoltrato dagli altri nodi,
e ricevuto da primo(C) incontra una sola frontiera tra cluster (cioè il nodo ultimo(C)
Tutte queste condizioni non possono essere verificate localmente, dal momento che ogni
nodo non conosce n, e non essendoci ancora un identità globale, non è possibile distinguere
un nodo da un altro.
E’ necessario in questo caso fare uso di un nonce, ovvero di un numero casuale univoco
(almeno con alta probabilità…) generato localmente, che quindi identifica univocamnte il
mittente di un messaggio. Può quindi essere utilizzata una tecnica come quella dell’ultimo
punto di cui sopra. Ai fini della modellazione, come nonce si può usare un identificatore
dell’istanza del nodo, identificatore facile da ottenere visto che la moellazione asusme un
numero fissato a priori di nodi (vedi sotto).
5) finalizzazione
In questa fase il primo nodo dell’unico cluster definisce il proprio ID come 0, e lo invia al
nodo a destra. Ogni nodo definisce il proprio ID come quello ricevuto più 1 e, se non è
l’ultimo, lo inoltra a destra. In questo modo viene definita l’identità di ogni nodo. L’ID=0
definisce il ruolo di leader.
Obiettivi dell’elaborato
Modellare ogni nodo con una statechart, e l’intero sistema come una combinazione di
statechart. Ogni statechart che modella un nodo deve essere uguale, a meno dei colelgametni
con i nodi adiacenti, e a meno della generazione del nonce.
Sul modello risultante effettuare delle azioni di verifica tramite simulazione o verifica
formale, a seconda dello strumento utilizzato.
Il modello ottenuto (in modo sostanziamente corretto) può presentare nondeterminismo o
meno, in funzione della modellazione effettuata, ma anche dello strumento di modellazione
utilizzato.
In caso di funzionamento deterministico, si può avere che l'esecuzione vada a buon fine,
oppure che vada in deadlock, o che non termini.
In caso di funzionamento nondeterministico, si può avere che tutte le computazioni vadano a
buon fine, o che alcune vadano a buon fine e le altre in deadlock o non terminino, o che tutte
le computazioni vadano in deadlock o non terminino.
L’oggetto della verifica sarà la presenza o meno di nondetermnismo e il tipo di
comportamento, con gli strumenti di verifica disponibili (simulazione, model-checking).
Altro punto da analizzare sarà l’eventuale presenza di messaggi orfani e il loro impatto sul
funzionamento dell’algoritmo.
A seguito delle analisi effettuate, e basandosi sui relativi risultati, si dovranno individuare
eventuali soluzioni ad eventuali problemi risocntrati.
Un ulteriore punto di studio riguarda la scalabilità del modello.
Infatti la modellazione necessariamente, per prevedere attività di simulazione e verifica
formale, dovrà prevedere un numero dato di nodi. Si suggerisce il numero di 6, anche se si
ammette che in alcui casi potrebbe essere necessario partire da un numero minore. D’altra
parte, per poter simulrae delle situazioni interessanti di aggregazione, non risulta utile un
numero sotto 4.
Nonostante si fissi il numero di nodi, la modellazione deve mantenersi generica, in
particolare i modelli dei nodi non devono fare alcun riferimento al numero dei nodi.
La modellazione generica dovrebbe facilitare in linea di principio la scalabilità a numeri di
nodi maggiori> Scopo dell’analisi è quidni quello di verificare la scalabilità, sia come facilità
di creare sistemi a più nodi, magari automaticamente (con un algoritmo che dato n crea il
modello), sia come limiti di memoria e/o di performance degli strumenti di verifica utilizzati.
Ogni gruppo, formato in genere da due o tre studenti, affronta l’attività di modellazione e
verifica utilizzando un diverso strumento di supporto, per l’accesso e la documentazione del
quale viene data comunicazione separata. Gli strumenti in questione sono:
- SCADE
- Stateflow/Simulink di Matlab
- IBM Rhapsody
- UMC
- STM Radcase
- NuSMV con NuSMVGUI
Effort previsto
Al fine di rispettare i vincoli di ore dedicate all’esame rispetto ai CFU acquisiti, si considera
che l’elaborato deve essere svolto, da ciascuno degli studenti di un gruppo, impiegando da 70
a 85 ore (per l’esame a 9 CFU).
Si suggerisce di impiegare il tempo secondo l’ordine delle fasi:
- modellazione
- verifica
- individuazione della risoluzione dei problemi incontrati
- analisi scalabilità
Tralasciando quindi le ultime fasi in caso di consistente superamento dell’effort previsto.
Nella relazione dell’elaborato deve essere esplicitato nel modo maggiormente preciso
possibile l’effort profuso in ciascuna delle fasi.
Si riporta a titolo di riferimento il codice UMC del primo round dell’algoritmo su tre nodi.
// class definition
Class Node is
Signals
acks,ackd, acks2,ackd2, reqs, reqd;
Vars
nodosx: Node;
nododx: Node;
Primo:bool := False; -- local attributes
Secondo:bool := False;
State Top = SX /DX /REC
State SX = init,final
State DX = init,final
State REC = init,sxacked, dxacked, sxconsreq, dxconsreq, sxconsack, dxconsack
Behavior
Top.SX.init -> Top.SX.final
{-/
nodosx.reqd
}
Top.DX.init -> Top.DX.final
{-/
nododx.reqs
}
Top.REC.init -> Top.REC.sxacked
{ reqs /
nodosx.ackd;
}
Top.REC.init -> Top.REC.dxacked
{ reqd /
nododx.acks;
}
Top.REC.init -> Top.REC.sxacked
{ acks / }
Top.REC.init -> Top.REC.dxacked
{ ackd / }
Top.REC.sxacked -> Top.REC.sxconsreq
{-/
nodosx.ackd2;
}
Top.REC.dxacked -> Top.REC.dxconsreq
{-/
nododx.acks2;
}
Top.REC.sxconsreq -> Top.REC.sxconsack
{ acks2 /
Secondo:= True
}
Top.REC.dxconsreq -> Top.REC.dxconsack
{ ackd2 /
Primo:= True
}
end Node;
// object instatiations
Node1: Node (nodosx -> Node3, nododx -> Node2)
Node2: Node (nodosx -> Node1, nododx -> Node3)
Node3: Node (nodosx -> Node2, nododx -> Node1)
Abstractions {
Action: $1($*)
-> $1($*)
-- observe events with all their params
Action $obj:assign(v1,$index,$value) -> assign
Action: accept($1) -> accepted($1) -- observe dispatching of triggers
State: Node1.Primo=True -> Node1primo
State: Node2.Primo=True -> Node2primo
State: Node3.Primo=True -> Node3primo
State: Node1.Secondo=True -> Node1secondo
State: Node2.Secondo=True -> Node2secondo
State: Node3.Secondo=True -> Node3secondo
}