vs.
w konkurencji

Collision Avoidance Protocol

Problem

Collision Avoidance Protocol jest stosowany w Ethernecie jako nakładka na protokoły typu CSMA/CD, czyli opóźniające transmisję w razie możliwości kolizji. Wymagania stawiane omawianemu protokołowi to:
  1. wykluczenie kolizji, a co za tym idzie:
  2. ustanowienie górnego ograniczenia opóźnienia transmisji, pod warunkiem, że są one bezbłędne
  3. dostarczanie wysłanych pakietów do wskazanych adresatów tzn. bez pomyłek
Założenia dotyczące medium są następujące:
  1. medium rozgłasza pakiety do wszystkich podłączonych doń stacji
  2. medium jest zawodne

Rozwiązanie

Prostym rozwiązaniem jest wprowadzenie nadrzędnej stacji, która po kolei (wedle strategii Round-Robin) odpytuje zwykłe stacje, czy chcą nadawać. Pomiędzy kolejnymi zapytaniami czeka przez określony czas.

Model rozwiązania

Wszystkie stacje (zwykłe user i nadrzędna master) oraz medium (medium) są reprezentowane przez oddzielne procesy. Dodatkowo każda stacja zwykła ma swojego sekretarza (slave) pośredniczącego w jej komunikacji z medium. Sekretarz rozdysponowuje nadchodzące pakiety. Przede wszystkim sprawdza, czy są one adresowane do jego stacji i tylko wtedy je rozpatruje. Rozpatrywanie polega na ustaleniu, czy pakiet jest zapytaniem od stacji nadrzędnej czy zwykłym pakietem z danymi od innej stacji. W pierwszym przypadku prosi swojego zwierzchnika o dane, a w drugim mu je przekazuje. Stacja może odrzucić propozycję nadania.
Wszelka komunikacja jest synchroniczna i odbywa się po następujących kanałach:
  1. to_medium - sekretarze i stacja nadrzędna nadają do medium
  2. from_medium - medium rozgłasza do sekretarzy i stacji nadrzędnej
  3. prywatne in - staje zwykłe nadają do swoich sekretarzy
  4. prywatne out - sekretarze nadają do swoich stacji
Zawodność medium (założenie 2.) polega na możliwości nierozgłoszenia niektórych kopii pakietu.

Realizacja modelu w Spinie

Kod źródłowy
Akapit ten można traktować jak zbiór krótkich przewodników pt. "Jak zrobić ... w Spinie".

Komunikacja synchroniczna

Komunikacja synchroniczna została zrealizowana za pomocą kanałów o zerowej pojemności. 
/* format pakietu w sieci: nadawca, adresat, dane */
chan to_medium = [0] of {byte, byte, byte};
chan from_medium[N] = [0] of {byte, byte, byte}; /* rozgłaszanie */

/* sekretarz przekazuje otrzymane dane swojej stacji */
chan out[N] = [0] of {byte};	/* powinno być N-1, ale składnia nie pozwala */

/* sekretarz odbiera od swojej stacji adresata i dane do wysłania */
chan in[N] = [0] of {byte, byte}; /* j.w. */

Sprawdzanie, czy nie zaszła pomyłka

Nagłówek pakietu krążącego w sieci zawiera identyfikator nadawcy i adresata. Treścią pakietu będącego zwykłą wiadomością a nie zapytaniem jest powtórzony identyfikator adresata. Umożliwia to zwykłej stacji sprawdzenie, czy jej sekretarz przekazuje jej właściwe pakiety.

Odrzucenie propozycji nadania

Treścią pakietu będącego zapytaniem od stacji nadrzędnej jest specjalna wartość ENQ. Jako że komunikacja jest synchroniczna, sekretarz odebrawszy taki pakiet od medium, nie przekazuje go zwierzchnikowi, tylko odbiera od zwierzchnika identyfikator adresata i treść wiadomości. Przekształca to w pakiet poprzez dodanie identyfikatora na nadawcy i wysyła do medium. Jeśli stacja zwykła nie jest zainteresowana nadawaniem, to zamiast identyfikatora istniejącego adresata umieszcza INVALID_ID. Pakiet taki nie zostanie nikomu dostarczony. Aby nie zaśmiecać sieci, sekretarz mógłby to sprawdzić przed wysyłaniem do medium. 
proctype user(byte id; chan cin,cout)
{
        byte data;
	byte succ = id%(N-1)+1;	/* następnik */
        do
        :: cout?data ->
           if
           :: data!=id -> goto accept_wrong_data
           :: data==id -> skip
           fi
        :: cin!INVALID_ID,0     /* nie zainteresowany */
        :: cin!succ,succ	/* adresat = treść (dla weryfikacji) */
        od;
accept_wrong_data:
        do
        :: (1) -> skip                          
        od
}

Rozgłaszanie

Kanały komunikacyjne w języku PROMELA nie posiadają rozgłaszania, zostało więc ono zaimplementowane jako nadawanie po kolei po każdym z kanałów w tablicy from_medium. Jako że język nie zezwala na określanie ciągu zawierającego operacje blokujące mianem atomowego, to niepodzielność rozgłaszania modelujemy jako wyłączenie nasłuchu na medium na czas trwania tej operacji. Rozgłaszanie może zatem przepleść się z komunikacją między stacjami a ich sekretarzami, ale nie zaburza to oczekiwanej semantyki tej operacji. 
active proctype medium()
{
        byte sender;
        byte receiver;
        byte data;
        byte i;
        do
        :: to_medium?sender,receiver,data ->
           i=0;
           if
           :: (1) -> do
                     :: i<=N-1 ->
                           if
                           :: i==sender -> skip
                           :: i!=sender -> from_medium[i]!sender,receiver,data
                           fi;
                           i=i+1
                     :: i>N-1 -> break
                     od
           :: to_medium?sender,receiver,data -> goto accept_collision
           fi
        od;
accept_collision: do
                  :: (1) -> skip
                  od               
}

Zawodność medium

Tak jak zaznaczono w modelu, zawodność medium polega na niedostarczeniu niektórych kopii pakietu. Przy powyżej realizacji rozgłaszania wymaga to zatem modelowania zawodności w sekretarzach. Osiągnięto to łatwo - sekretarz odebrawszy pakiet od medium, może go po prostu porzucić. 
proctype slave(byte id)
{
        byte sender;
        byte receiver;
        byte data;
        byte ny_receiver;
        byte ny_data;
        do
        :: from_medium[id]?sender,receiver,data ->
           if
           :: data!=ENQ ->
                 if
                 :: receiver==id -> out[id]!data
                 :: receiver!=id -> skip
                 fi
           :: data==ENQ && receiver==id ->
                 in[id]?ny_receiver,ny_data;
                 to_medium!id,ny_receiver,ny_data
           :: data==ENQ && receiver!=id -> skip
           fi
        :: from_medium[id]?sender,receiver,data          /* gubienie pakietu */
        od
}

Odczekiwanie pomiędzy zapytaniami

Wysławszy zapytanie stacja nadrzędna musi odczekać, aż na łączu zapanuje cisza. Język PROMELA oferuje instrukcję timeout, która blokuje dopóki wszystko w systemie stanie się niewykonywalne i wtedy sama staje się wykonywalna. Stacja nadrzędna zawsze zawiesza się na tej instrukcji przed wysłaniem następnego zapytania, bo cisza może wynikać albo ze zgubienia pakietu albo stąd, że wszyscy odebrali. 
active proctype master()
{
        byte sender;
        byte receiver;
        byte data;
        byte next;
        next=1;
        to_medium!0,next,ENQ;      
        do
        :: from_medium[0]?sender,receiver,data
        :: timeout -> next=next%(N-1)+1;to_medium!0,next,ENQ
        od
}

Weryfikacja w Spinie

Własność pierwsza i trzecia są łatwe do zweryfikowania w Spinie w oparciu o wykluczenie cykli akceptacji z przebiegów. Narzędzie to nie pozwala jednak na tak bezpośrednią weryfikację własności drugiej, ponieważ nie operuje pojęciem czasu.

Brak kolizji

Proces medium wykonuje skok do cyklu akceptacji accept_collision, gdy dwa razy z rzędu odbierze komunikat po kanale to_medium. Przez dwa razy z rzędu rozumiemy bez operacji rozgłaszania pomiędzy.

Dostarczenie do właściwego adresata

Proces zwykłej stacji wykonuje skok do cyklu akceptacji accept_wrog_data, gdy treścią wiadomości jest co innego niż jego identyfikator.

Realizacja modelu w Uppaalu

Landrynkowy interfejs graficzny Uppaala nie daje się sobie oprzeć i zachęca do eksperymentowania z różnymi modelami. Proponuję więc samodzielne przeprowadzanie symulacji w trakcie prezentacji.

Rozgłaszanie

Emulacja rozgłaszania
W chwili powstania pracy, na której jest oparta ta prezentacja, Uppaal nie oferował wbudowanego mechanizmu rozgłaszania. Emulowano je za pomocą ciągu lokacji typu commited, po między którymi przejścia etykietowane były nadawaniem. Wybranie tego typu lokacji zapewniało niepodzielność rozgłaszania.

Podejście to, podobnie jak w Spinie, wymaga modelowania zawodności medium w sekretarzach. Sekretarz może zgubić pakiet, gdy jest zajęty obsługą poprzedniego pakietu. Stąd lokacje ignore1 i ignore2, w których sekretarz przebywa nie dłużej niż do upłynięcia dwóch jednostek czasu od chwili odebrania pakietu.

Wysyłający dowiaduje się o zakończonym rozgłaszaniu dzięki synchronizacji z medium po dodatkowym kanale finished, tak jak robi to stacja nadrzędna.

Warto zwrócić uwagę na czyhające tu niebezpieczeństwo blokady, którego nie dostrzegli (albo które uznali za pozbawione znaczenia) autorzy systemu. Emulacja rozgłaszania za pomocą lokacji typu commited pociąga za sobą konieczność nadania tego atrybutu innym lokacjom pozornie niezwiązanym z rozgłaszaniem. Jeśli stacja nadrzędna nie dokona zaraz po nadaniu do medium przejścia do lokacji wait (tzn. nie ustawi czasomierza), to po zakończeniu rozgłaszania dojdzie do blokady. Przyczyną jest konieczność opuszczenia przez medium lokacji broadcast4, czego jednak zrobić nie może, ponieważ nie ma z kim się zsynchronizować po kanale finished. Analogiczny problem wystąpi, gdy sekretarz zabawi za długo w lokacji dispatch, a obecny model narzuca mu pozostanie tam ze względu na niepodzielność rozgłaszania. Wyjściem z impasu jest przypisanie obu tym lokacjom atrybutu commited. Podobnie jak to było w Spinie mimo że taka modyfikacja lokacji dispatch rozbije atomowość rozgłaszania, nie psuje to modelu. Innym źródłem blokad w Uppaalu jest nieumiejętne zmuszanie procesu do opuszczenia danej lokacji po dokładnie danym czasie. Wyłączne postawienie dozoru z równaniem zegarowym na tranzycji spowoduje, że proces może "przegapić" ten właściwy moment i nie móc się później wydostać. Omawiany system obfituje w takie przypadki. W poprawionej wersji odpowiednie lokacje są zaopatrzone w niezmienniki narzucające ograniczenia czasowe na pozostawanie w lokacji.
Wbudowany mechanizm rozgłaszania
Nowsze wersje Uppaala oferują wbudowany mechanizm rozgłaszania posiadający wiele zalet. Po pierwsze eliminuje on opisane powyżej ryzyko blokady. Po drugie nie wymaga modelowania zawodności medium w sekretarzach, ponieważ wysyłanie do kanału typu broadcast jest nieblokujące. Synchronizują się z nim tylko procesy, które mogą to w danej chwili zrobić. Proponuję zweryfikować własność 
A[] not deadlock
dla systemu z poprzedniego akapitu oraz stworzonego przeze mnie systemu korzystającego z nowego mechanizmu.

Weryfikacja w Uppaalu

Zapytania

Brak kolizji

Proces medium osiąga lokację collision, gdy dwa razy z rzędu odbierze komunikat po kanale to_medium analogicznie do wejścia w cykl akceptacji w Spinie. 
A[] not Medium.collision
Ta podstawowa własność bezpieczeństwa jest bezwarunkowo zachowana tylko przez niezawodne medium, natomiast w bardziej realistycznych modelach jak nasz zależy od limitu, jaki stacja nadrzędna wyznacza na otrzymanie pakietu wysłanego przez zwykłą stację jako odpowiedź na zapytanie. Stacja nadrzędna ustawia czasomierz, który informuje ją komunikatem timeout o przekroczeniu tego limitu.

Jeśli limit zostanie przekroczony za prędko, to stacja nadrzędna zinterpretuje to jako sytuację, w której zgubiono pakiet i wszystkie stacje zwykłe czekają na dane. Oczywiście nie to musi być prawdziwą przyczyną, może bowiem zdarzyć się, że sekretarz jest właśnie w trakcie przekazywania zapytania swojemu zwierzchnikowi. Wtedy może dojść do kolizji wiadomości od tej stacji z kolejnym zapytaniem pochopnie wysłanym przez stację nadrzędną. Dzięki Uppaalowi ustalono, że minimalny limit broniący przed kolizjami to 3. Zachęcam do poeksperymentowania z wartością TO w Global declarations.

Ograniczona żywotność

Własności ograniczonej żywotności nie mogą być bezpośrednio wyrażone w języku weryfikacji Uppaala, dlatego celem ich weryfikacji wprowadza się do systemu dodatkowe automaty obserwujące pozostałe komponenty. Obserwacja odbywa się przez komunikację. Dodatkowe kanały sent i received służą odpowiednio poinformowaniu obserwatora o nadaniu i odbiorze komunikatu przez zwykłą stację.

Czas obiegu
Najpierw przekonamy się, że istnieje dolne ograniczenie czasu pełnego obiegu. Każdy automat Round-trip w nowym systemie obserwuje jedną stację i mierzy czas między kolejnymi dokonanymi przez nią nadaniami. Biorąc pod uwagę pierwszą stację widzimy, że istnieje obieg w 12-stu jednostkach czasu, ponieważ poniższa własność jest spełniona: 
E<> RT0.end and RT0.s == 12
Nie można jednak tego oszacowania polepszyć, gdyż następująca własność już nie zachodzi: 
E<> RT0.end and RT0.s < 11
Co ciekawe, analogiczne własności z wartościami odpowiednio 18 i 17 zachodzą dla systemu zawierającego błędy opisane przy okazji rozgłaszania.
Czas transmisji
Autorzy twierdzą, iż przy założeniu niezawodności medium oraz zainteresowania nadawaniem ze strony każdej zapytanej stacji udało im się ustalić górne ograniczenie opóźnienia transmisji oraz odstępu pomiędzy kolejnymi nadaniami. Automat obserwujący BL osiąga lokację bad_trans, jeśli odbiór nastąpił później niż w T jednostek po nadaniu i lokację bad_int, jeśli interwał pomiędzy nadaniami przez kolejne stacje był dłuższy niż I.

Żądana własność to: 
A[] not (BL.bad_int or BL.bad_trans)
Uogólnienie metody
Te dwa przykłady ilustrują wyrażenie ograniczonej żywotności w terminach osiągalności stanów przez automaty obserwujące. Podobnie jak Spin potrafi generować postulaty never-claim wprost z formuł LTL, tak można automatyzować budowę automatów obserwujących na podstawie własności wyrażonych niektórych logikach np. Safety and Bounded Liveness Logic. Oto prosta logika Simple Time Logic wraz z indukcyjną konstrukcją automatów dla formuł (litery przy formułach odpowiadają literom pod automatami). Formuła jest spełniona wtedy i tylko wtedy, gdy stan bad jest nieosiągalny.
  1. prawda
  2. fałsz
  3. można wykonać akcję a nie później niż po czasie N
  4. każda a-tranzycja wykonana przed upływem czasu N prowadzi do stanu, którym spełniona jest formuła reprezentowana przez automat T
  5. koniunkcja formuł reprezentowanych prze automaty T1 i T2
  6. każdy osiągalny stan automatu spełnia formułę reprezentowaną przez automat T

Wniosek

Tytuły prezentacji jak ten bywają przewrotne, wymienione w nim narzędzia okazały się bowiem wzajemnie komplementarne.

Justyna Sidorska, maj 2004