Weryfikacja IEEE 1394 Tree Identify Protocol
IEEE 1394, znana także jako "FireWire", to szyna o wysokiej przepustowości używana do przesyłania cyfrowego dźwięku i obrazu w sieci multimedialnych systemów i urządzeń. Posiada skalowalną architekturę i działa na zasadzie Hot-Plug, co oznacza, że urządzenie może być w łatwy sposób odłączone lub dołączone do sieci w dowolnym momencie.
Cały system składa się z wielu komponentów, komunikujących się ze sobą, za pomocą różnych protokołów zależnie od zadania (np.: transfer danych pomiędzy węzłami, przydział szyny, wybór lidera).
Właściwie IEEE 1394 Tree Identify Protocol jest protokołem wyboru lidera, który jest wykorzystywany po każdym resecie szyny w sieci (np.: kiedy węzeł jest dodawany lub usuwany z sieci). Natychmiast po resecie wszystkie węzły w sieci mają taki sam status i znają tylko węzły, do których mają bezpośrednie połączenia. Lider (root) musi zostać wybrany, aby wykonywać zadania menedżera szyny w kolejnych fazach 1394. Protokół jest zaprojektowany dla spójnych, acyklicznych sieci. W wypadku wykrycia cyklu przekazywany jest raport o błędzie.
Każdy węzeł pracuje w dwóch fazach, zależnie od ilości dzieci c
i sąsiadów n. Gdy n - c > 1 węzeł czeka na wiadomość
"be my parent" od któregoś z sąsiadów. Jeżeli n - c = 1 węzeł
wysyła "be my parent" do sąsiada, który nie jest dzieckiem i nie
otrzymał jeszcze od niego "be my parent". Implikuje to fakt, że pierwsze
ze swoim sąsiadami komunikują się liście i od liści rozpoczyna się budowa drzewa
rozpinającego graf.
Pewien kłopot sprawia fakt, że żądanie "be my parent" nie jest atomowe
i może się zakończyć porażką. W rzeczywistości po "be my parent" następuje
potwierdzenie i potwierdzenie potwierdzenia. Skoro wiadomości te nie są atomowe, może
nastąpić pewnego rodzaju kolizja: dwa węzły wzajemnie do siebie wyślą
"be my parent". Niestety tylko jeden węzeł może zostać liderem i w związku
z tym problem ten musi być rozwiązany. FireWire przewiduje następujący schemat
postępowania: każdy z węzłów niederministycznie wybiera okres czasu (długi albo krótki),
przez który będzie czekał. Jeśli po upływie tego czasu okaże się, że otrzymał wiadomość
"be my parent" staje się on rootem. Jeśli taka wiadomość nie nadeszła
retransmituje on wiadomość. Oczywiście problem może się powtórzyć.
MODULE node
VAR
s: {T0, T1, T2, T3_1, T3_2, T3_3, S0};
port: array 0..2 of port;
rnd: boolean;
ASSIGN
init(s) := T0;
next(s) := case
s = T0 &
((!(port[0].role = unknown) &
!(port[1].role = unknown)) |
(!(port[0].role = unknown) &
(port[2].role = unknown)) |
(!(port[1].role = unknown) &
(port[2].role = unknown))): T1;
s = T1: {T1, T2};
s = T2: {T2, S0, T3_1};
s = T3_1 & rnd: T3_2;
s = T3_1 & !rnd: T3_3;
s = T3_2: T3_3;
s = T3_3: {T1, T2};
1 : s;
esac;
Jest to przełożenie schematu blokowego na kod SMV. Niestety kod modelu jest pozbawiony komunikacji między węzłami. Należy oczekiwać, że rzeczywisty model jest nieco bardziej skomplikowany. Zwraca uwagę fakt, że kod jest przystosowany do węzła mającego nie więcej niż 3 sąsiadów. Rozszerzenie tak zaimplementowanego modelu jest kłopotliwe.
start:
atomic{
assert((counter==N)&&(message==nullmessage)&&(partnerid==N)&&
(self_in==null)&&(self_out==null));
if
::(adj[selfid]-child[selfid]==0)->elected=selfid; goto finish
::(adj[selfid]-child[selfid]==1)->counter=0; goto parent_request
::else->counter=0;goto wait_for_request
fi
};
Model jest niestrukturalny, dzięki czemu jest prostym odbiciem schematu blokowego przedstawionego wcześniej. Dla zmniejszenia ilości stanów w czasie weryfikacji czynności są atomowe.
chan zerotwo=[1] of {mtype}; chan twozero=[1] of {mtype};
chan onetwo=[1] of {mtype}; chan twoone=[1] of {mtype};
chan twothree=[1] of {mtype}; chan threetwo=[1] of {mtype};
chan threefive=[1] of {mtype}; chan fivethree=[1] of {mtype};
chan fourfive=[1] of {mtype}; chan fivefour=[1] of {mtype};
Standardowo odbywa się kanałami. Wydaje się, że rozszerzanie tak zbudowanego modelu nie będzie łatwe.
gcc -E tree.c -o tree.smv). Makro:
#define map_in_out(n, p) ( \
case \
peer[n][p].node = 0: \
case \
peer[n][p].port = 0: node[0].port[0].cout; \
peer[n][p].port = 1: node[0].port[1].cout; \
peer[n][p].port = 2: node[0].port[2].cout; \
esac; \
...
esac \
)
I jego zastosowanie:
(!peer[0][0].node = -1 -> node[0].port[0].cin = map_in_out(0, 0)) (!peer[0][1].node = -1 -> node[0].port[1].cin = map_in_out(0, 1)) (!peer[0][2].node = -1 -> node[0].port[2].cin = map_in_out(0, 2)) ...
byte adj[N]; byte child[N];
typedef array { byte to[N] }; array connect[N];
Natomiast wyjścia i wejścia są mapowane w locie na bieżące potrzeby komunikacji przy pomocy funkcji:
inline converter(id1,id2,chanin,chanout)
/* takes a pair of ids and finds the corresponding in and out channels */
{if
:: (id1==0)-> assert((id2==2)); chanin=twozero;chanout=zerotwo
:: (id1==1)-> assert((id2==2)); chanin=twoone;chanout=onetwo
:: (id1==2)-> assert((id2==0)||(id2==1)||(id2==3));
if
:: (id2==0)->chanin=zerotwo;chanout=twozero
:: (id2==1)->chanin=onetwo;chanout=twoone
:: (id2==3)->chanin=threetwo;chanout=twothree
fi
...
Niestety funkcja jest ściśle zależna od topologii. A zatem dla nowego układu węzłów trzeba pisać nową funkcję. Warto zwrócić uwagę na asercje w kodzie funkcji. Gdyby ich nie było to w wypadku błędu przy definiowaniu topologii mogło by dojść do blokady w czasie konwersji identyfikatorów na odpowiednie kanały.