Blokada w multi-procesowym systemie poczty elektronicznej
Przedmiotem krótkiej prezentacji będzie problem jaki wystąpił w sieciowym systemie poczty elektronicznej VAX/VMS Uniwersytetu Barkley. Powstanie problemu było skutkiem działalności "Dr Who Fan Club". Jeden z użytkowników sieci otrzymywał korespondencję elektroniczną od Dr Who, która przychodziła do niego ze USA. Następnie kopie listów przy pomocy automatycznego przesyłania, przekazywane około 20 różnym osobom w całej Wielkiej Brytanii. Pewnej nocy po okresie przestoju w amerykańskim systemie pocztowym około 30 przesyłek pojawiło się w krótkim przedziale czasowym. Spowodowało to, oprócz spodziewanego krótkotrwałego dużego obciążenia, zupełną blokadę systemu, którą odkryto następnego dnia.
Aby wyjaśnić jak mogło dojść do blokady, należy w zarysie przedstawić strukturę systemu. Miał on multi-procesową implementację, z następującymi składowymi procesami:
Aby zdiagnozować przyczynę blokady i zapewnić, że przyszłe systemu będą od niej wolne, zdecydowano się zamodelować system w CCS. Model składa się z czterech procesów i trzech buforów między-procesowych:
Koła na rysunku to procesy, natomiast prostokąty symbolizują bufory. Etykiety składowych są takie same, jak identyfikatory agentów z CCS modelujących poszczególne elementy. Strzałki wskazują kierunek przepływu danych, z czego cztery symbolizują komunikację między systemem a światem zewnętrznym (pliki zawierające pocztę są odbierane z i wysyłane do sieci - lewa strona, przesyłki pocztowe są zbierane od użytkowników i dostarczane im - prawa strona).
Zamodelowany system może wykonywać dwa rodzaje zewnętrznych operacji wejścia: otrzymanie poczty z sieci i otrzymanie poczty od użytkownika. Podobnie może wykonywać operacje wyjścia: wysłanie poczty do sieci i wysłanie poczty do użytkownika. Główny agent jest zdefiniowany jako czterej równolegle działający podagenci odpowiadający procesom i trzej podagenci symulujący bufory. Dodatkowo nałożone jest ograniczenie, aby nie była widoczna komunikacja wewnętrzna.
set Internals = {cm_insert, cm_remove, cm_empty, md_start, md_stop, mf_insert,
mf_remove, mf_empty, fm_insert, fm_remove, fm_empty};
agent Old_System = (Collect | Deliver | CollectMail | Mail | MailFile | FileMail | File)\Internals;
Agenci odpowiadający buforom (CollectMail, MailFile, FileMail) zostali zamodelowani
przez przemianowanie standardowych buforów:
agent Buffer = insert.'remove.Buffer + 'empty.Buffer; agent CollectMail = Buffer[cm_insert/insert, cm_remove/remove, cm_empty/empty]; agent MailFile = Buffer[mf_insert/insert, mf_remove/remove, mf_empty/empty]; agent FileMail = Buffer[fm_insert/insert, fm_remove/remove, fm_empty/empty];
W każdej chwili dowolna liczba procesów użytkowników może wysyłać pocztę przez umieszczenie
jej w buforze CollectMail. Zostało to zamodelowane przez pojedynczego agenta,
który może wciąż odbierać przysyłaną pocztę (letter_posted oznacza otrzymanie
wiadomości wysłanej przez użytkownika).
agent Collect = letter_posted.'cm_insert.Collect;
Nowy proces był tworzony, gdy miała być dostarczona przesyłka użytkownikowi. Następnie
system czekał na zakończenie działania nowego procesu i wtedy wznawiał pracę. W modelu
odpowiada za to pojedynczy agent, który potrafi wielokrotnie dostarczać pocztę. Komunikuje
się z agentem Mail rozgłaszając md_start i md_stop
dla każdej wiadomości. Poczta może być wysłana do użytkownika, lub gdy ten ustawił taką
opcję automatycznie przesyłana dalej do wskazanych systemów, co może spowodować, że system
ma wysłać jedną lub więcej przesyłek z powrotem do sieci. Dla uproszczenia w modelu przesyłanie
dalej może spowodować wygenerowanie tylko jednej wychodzącej przesyłki.
agent Deliver = md_start.(tau.'letter_deliver.'md_stop.Deliver + tau.'cm_insert.'md_stop.Deliver);
Agent Mail jest odpowiedzialny zarówno za przychodzącą pocztę w buforze
FileMail, jak i wychodzącą w CollectMail. W rzeczywistości
proces ten po obsłużeniu jakiejkolwiek wiadomości natychmiast zajmował się obsługą wszystkich
wiadomości z CollectMail, aby zapewnić, że nie są one niepotrzebnie opóźniane.
W teorii prowadzi to głodzenia przychodzącej poczty, jednak praktycznie taka sytuacja jest
bardzo mało prawdopodobna. Kiedy proces otrzymuje pocztę może dostarczyć ją do użytkownika,
lub w przypadku, gdy zawiera ona błędy wysłać ją z powrotem do sieci. Agent wygląda tak:
agent Mail = fm_remove.(tau.'md_start.md_stop.Mail1 + tau.'mf_insert.Mail1) + cm_remove.'mf_insert.Mail1; agent Mail1 = cm_empty.Mail + cm_remove.'mf_insert.Mail1;
Wreszcie ostatni proces odpowiedzialny za obsługę protokołu przesyłania plików, obsługujący zarówno
pliki przychodzące/wychodzące z/do sieci. Proces był tak zaprogramowany, że mógł obsługiwać przychodzącą
pocztę przed obsłużeniem wychodzącej. Była to niezamierzona cecha wewnętrznej organizacji, która podobnie
jak w przypadku FileMail teoretycznie mogła prowadzić do głodzenia, przez przyjmowanie nowych
zleceń z zewnątrz przed uporaniem się z zalegającą w systemie pocztą wychodzącą. Agent modelujący to zachowanie
jest następujący:
agent File = file_received.'fm_insert.File + mf_remove.'file_send.File;
Plik ze definicjami CWB znajduje się tutaj.
A tutaj można znaleźć grafy działania niektórych agentów.
W tak skonstruowanym agencie CWB znajduje następujące blokady (fd Old_System):
--- file_received tau tau tau tau tau file_received tau file_received letter_posted tau letter_posted
---> ('cm_insert.Collect | 'cm_insert.'md_stop.Deliver |
('remove.Buffer)[cm_empty/empty,cm_insert/insert,cm_remove/remove] |
md_stop.Mail1 | MailFile |
('remove.Buffer)[fm_empty/empty,fm_insert/insert,fm_remove/remove] |
'fm_insert.File)\Internals
--- file_received tau file_received letter_posted tau tau tau letter_posted tau tau letter_posted tau letter_posted
---> ('cm_insert.Collect | Deliver |
('remove.Buffer)[cm_empty/empty,cm_insert/insert,cm_remove/remove] |
'mf_insert.Mail1 | ('remove.Buffer)[mf_empty/empty,mf_insert/insert,mf_remove/remove] |
('remove.Buffer)[fm_empty/empty,fm_insert/insert,fm_remove/remove] |
'fm_insert.File)\Internals
--- file_received tau file_received letter_posted tau tau tau tau tau tau tau tau tau file_received letter_posted tau
letter_posted --->
('cm_insert.Collect | 'cm_insert.'md_stop.Deliver |
('remove.Buffer)[cm_empty/empty,cm_insert/insert,cm_remove/remove] |
md_stop.Mail1 | ('remove.Buffer)[mf_empty/empty,mf_insert/insert,mf_remove/remove] |
('remove.Buffer)[fm_empty/empty,fm_insert/insert,fm_remove/remove] |
'fm_insert.File)\Internals
--- file_received tau file_received letter_posted tau tau tau tau tau tau tau tau tau tau letter_posted tau letter_posted
'file_send file_received --->
('cm_insert.Collect | 'cm_insert.'md_stop.Deliver |
('remove.Buffer)[cm_empty/empty,cm_insert/insert,cm_remove/remove] |
md_stop.Mail1 | Buffer[mf_empty/empty,mf_insert/insert,mf_remove/remove] |
('remove.Buffer)[fm_empty/empty,fm_insert/insert,fm_remove/remove] |
'fm_insert.File)\Internals
Okazuje się że mechanizm powstania blokad pierwszej i czwartej jest taki sam, chociaż prowadzi do niego inna
ścieżka (MailFile = Buffer[mf_empty/empty,mf_insert/insert,mf_remove/remove]), i możemy zapisać trzech agentów reprezentujących możliwe zakleszczenia:
agent Dead1 = ('cm_insert.Collect | Deliver | 'cm_remove.CollectMail |
'mf_insert.Mail1 | 'mf_remove.MailFile | 'fm_remove.FileMail |
'fm_insert.File)\Internals;
agent Dead2 = ('cm_insert.Collect | 'cm_insert.'md_stop.Deliver |
'cm_remove.CollectMail | md_stop.Mail1 | MailFile |
'fm_remove.FileMail | 'fm_insert.File)\Internals;
agent Dead3 = ('cm_insert.Collect | 'cm_insert.'md_stop.Deliver |
'cm_remove.CollectMail | md_stop.Mail1 | 'mf_remove.MailFile |
'fm_remove.FileMail | 'fm_insert.File)\Internals;
Wynika z tego, że mamy do czynienia z dwoma typami blokady. W przypadku Dead1 mamy do czynienia
z zakleszczeniem pomiędzy Mail i File. Bufory MailFile i FileMail
są pełne, a wspomniani agenci próbują wysłać sobie wzajemnie dane. W sytuacjach, które reprezentują Dead2
i Dead3, dochodzi do blokady pomiędzy Mail i Delivery ponieważ ten drugi
próbuje wysłać pocztę przesyłaną dalej, ale bufor CollectMail jest pełny, a pierwszy czeka na zakończenie
przez niego pracy. Różnica między Dead2 i Dead3 jest tylko taka, że w przypadku tego
drugiego bufor MailFile jest pełny, ale nie ma to związku z samą blokadą.
Zaobserwowane wcześniej zakleszczenie to przypadek Dead1. Pozostałe dwa nie zostały napotkane
w praktyce. Aby zbadać przyczyny zakleszczeń przeprowadzono dodatkowe eksperymenty.
Przychodzącą pocztę możemy wyeliminować przez ograniczenie agenta File tak, aby tylko wysyłał pocztę:
agent File = mf_remove.'file_send.File; agent No_incoming = (Collect | Deliver | CollectMail | Mail | MailFile | FileMail | File)\Internals; Command: fd No_incoming; None.
Jak widać taki system nie ma blokad (choć jego funkcjonalność jest "nieco" ograniczona). Z drugiej strony możemy pozbyć
się poczty przychodzącej od użytkowników, usuwając agenta Collect, co nie poprawia sytuacji, ale jest
wskazówką gdzie należy szukać przyczyn zakleszczenia.
agent No_user_mail = (Deliver | CollectMail | Mail | MailFile | FileMail | File)\Internals;
Command: fd No_user_mail;
--- file_received tau tau tau tau tau file_received tau tau tau tau tau tau tau file_received tau file_received
---> (Deliver | ...
--- file_received tau tau tau tau tau file_received tau tau tau tau tau file_received tau file_received
---> ('cm_insert.'md_stop.Deliver | ...
--- file_received tau tau tau tau tau file_received tau tau tau tau tau tau file_received tau file_received
---> ('md_stop.Deliver | ...
--- file_received tau tau tau tau tau file_received tau tau tau file_received tau file_received ---> (Deliver |...
Teraz spróbujemy się pozbyć generowania błędów przychodzącej poczty i zwracania wadliwej poczty do sieci.
agent Mail2 = fm_remove.'md_start.md_stop.Mail3 + cm_remove.'mf_insert.Mail3;
agent Mail3 = cm_empty.Mail2 + cm_remove.'mf_insert.Mail3;
agent No_errors = (Collect | Deliver | CollectMail | Mail2 | MailFile | FileMail | File)\Internals;
Command: fd No_errors;
--- file_received tau file_received letter_posted tau tau tau letter_posted tau tau letter_posted tau letter_posted
---> ('cm_insert.Collect | ...
--- file_received tau file_received letter_posted tau tau tau tau tau tau tau tau file_received letter_posted tau
letter_posted ---> ('cm_insert.Collect | ...
--- file_received tau file_received letter_posted tau tau tau tau tau tau tau tau tau letter_posted tau letter_posted
'file_send file_received
---> ('cm_insert.Collect | ...
--- file_received tau tau tau tau file_received tau file_received letter_posted tau letter_posted
---> ('cm_insert.Collect | ...
Ciągle w systemie może dojść do blokady. Jest to zgodne z oczekiwaniami, ponieważ nic nie wskazywało, że zwracanie błędnej poczty było przyczyną zakleszczenia. Następna próba to wyeliminowanie automatycznego przesyłania dalej przychodzącej poczty.
agent Deliver1 = md_start.'letter_deliver.'md_stop.Deliver1;
agent No_forwarding = (Collect | Deliver1 | CollectMail | Mail | MailFile | FileMail | File)\Internals;
Command: fd No_forwarding;
--- file_received tau file_received letter_posted tau tau tau letter_posted tau tau letter_posted tau letter_posted
---> ('cm_insert.Collect | Deliver1 |
('remove.Buffer)[cm_empty/empty,cm_insert/insert,cm_remove/remove] | 'mf_insert.Mail1 |
('remove.Buffer)[mf_empty/empty,mf_insert/insert,mf_remove/remove] |
('remove.Buffer)[fm_empty/empty,fm_insert/insert,fm_remove/remove] | 'fm_insert.File)\Internals
W uzyskanym systemie może dojść do blokady, ale tylko odpowiadającej Dead1. Ten eksperyment
potwierdza, że system przesyłania poczty był wadliwy i przyczynił się do potencjalnego zakleszczenia, ale
nie był bezpośrednią przyczyną zaistniałej blokady, co wcześniej podejrzewano. Wobec tego przeprowadzono
dwa dodatkowe eksperymenty, aby sprawdzić czy zmiany w zachowaniu Mail i File
mogą wyeliminować możliwość blokady. Najpierw zmieniono Mail tak, aby nie obsługiwał wszystkich
wiadomości z CollectMail przez zabraniem się za bufor FileMail.
agent Mail4 = cm_remove.Mail5 + fm_remove.Mail6;
agent Mail5 = 'mf_insert.(fm.empty.Mail4 + fm_remove.Mail6);
agent Mail6 = tau.'md_start.md_stop.Mail7 + tau.'mf_insert.Mail7;
agent Mail7 = cm_empty.Mail4 + cm_remove.Mail5;
agent No_privilege = (Collect | Deliver | CollectMail | Mail4 | MailFile | FileMail | File)\Internals;
Command: fd No_privilege;
--- file_received tau tau tau tau file_received tau file_received letter_posted tau tau
letter_posted tau letter_posted ---> ('cm_insert.Collect | ...
--- file_received tau file_received letter_posted tau tau tau tau tau tau file_received
letter_posted tau letter_posted ---> ('cm_insert.Collect | ...
--- file_received tau file_received letter_posted tau tau tau tau tau tau tau tau file_received
letter_posted tau letter_posted ---> ('cm_insert.Collect | ...
--- file_received tau file_received letter_posted tau tau tau tau tau tau tau tau tau letter_posted
tau letter_posted 'file_send file_received ---> ('cm_insert.Collect | ...
--- file_received tau tau tau tau tau file_received tau file_received letter_posted tau letter_posted
---> ('cm_insert.Collect | ...
Jak widać nie przyniosło to poprawy (jakkolwiek mamy tu do czynienia tylko z jednym rodzajem blokady).
Drugi eksperyment polegał na zmianie w File likwidującej obsługę dowolnej ilości
przesyłek z sieci, przed podjęciem pracy nad wewnętrznym buforem. Niestety i tym razem nie
uniknięto zakleszczenia.
agent File2 = mf_remove.'file_send.File2 + file_received.'fm_insert.File3;
agent File3 = mf_empty.File3 + mf_remove.'file_send.File3;
agent No_net_pri = (Collect | Deliver | CollectMail | Mail | MailFile | FileMail | File2)\Internals;
fd No_net_pri;
--- file_received tau tau tau tau tau tau letter_posted tau letter_posted
---> ('cm_insert.Collect | ...
--- file_received tau tau tau tau tau letter_posted tau letter_posted
---> ('cm_insert.Collect | ...
Po eksperymentach stwierdzono, że nie jest możliwe usunięcie blokady z systemu w dotychczasowym kształcie. Postanowiono zreorganizować procesy systemowe i komunikację między nimi.
Podzielono proces Mail na dwa procesy: Mail_in odpowiedzialny za pocztę przychodzącą z bufora FileMail,
który również obciążono obowiązkiem zwracania przesyłek zawierających błędy, Mail_out odpowiadający za pobieranie poczty z
bufora CollectMail i umieszczający ją w MailFile. Obowiązki procesu File również podzielono między
dwa procesy File_in i File_out odpowiedzialne za odpowiednio odbieranie poczty przychodzącą i umieszczanie
jej w buforze FileMail oraz pobieranie poczty wychodzącej z bufora MailFile i wysyłanie jej do sieci.
Nowy model systemu wygląda następująco:
agent Mail_out = cm_remove.'mf_insert.Mail_out;
agent Mail_in = fm_remove.(tau.'md_start.md_stop.Mail_in + tau.'mf_insert.Mail_in);
agent File_out = mf_remove.'file_send.File_out;
agent File_in = file_received.'fm_insert.File_in;
agent New_System = (Collect | Deliver | CollectMail | Mail_out | Mail_in |
MailFile | FileMail | File_out | File_in)\Internals;
Command: fd New_System;
None.