Pr-1st-1.1-m08-Slajd15

Twierdzenie 8.1

Twierdzenie 8.1

Algorytm Chandy-Lamporta wyznacza w skończonym czasie konfigurację spójną.

Dowód

Lemat 8.1.1

Jeżeli co najmniej jeden proces zainicjuje algorytm, wszystkie procesy zapiszą swój stan lokalny w skończonym czasie.

Ponieważ każdy proces zapisuje stan i wysyła znacznik co najwyżej raz, algorytm się kończy w skończonym czasie. Jeżeli $P_{i}$ jest procesem, który już zapisał stan, a $P_{j}$ jest sąsiadem $P_{i}$, to $P_{j}$ również zapisał stan. Wynika to z faktu, że znacznik wysłany przez $P_{i}$ i $P_{j}$ odebrany przez wymusza na nim zapisanie stanu, jeżeli wcześniej już tego nie dokonał. Ponieważ co najmniej jeden proces zainicjował algorytm, co najmniej jeden zapisał stan; a ponieważ zakładamy, że wszystkie procesy są połączone (pośrednio lub bezpośrednio) za pomocą sieci komunikacyjnej, implikuje to, że wszystkie procesy zapisały stan.

Należy obecnie wykazać, że wyznaczona konfiguracja jest spójna. Oznacza to, że nie może ona zawierać wiadomości w zapisanym stanie kanałów bądź zdarzeń odbioru wiadomości wysłanych w wyniku pewnego zdarzenia, które by nie zostało zapisane w obrazie stanu globalnego. Przyjmijmy, że Jeżeli proces zapisał swój stan, to wysłał również znacznik do wszystkich sąsiadów. Oznacza to, że każde zdarzenia wysłania przez $P_{i}$ wiadomości $M$ do innego procesu $P_{j}$ po zapisaniu stanu musi być poprzedzone zdarzeniem wysłania znacznika - z własności FIFO kanałów komunikacyjnych oznacza to, że $P_{j}$ otrzyma znacznik przed wiadomością $M$. Z algorytmu wynika, że otrzymania znacznika przez $P_{j}$ wymusza na nim zapisanie stanu – a więc jest niemożliwe, by proces otrzymał tą wiadomość przed zapisaniem stanu. Oznacza to, że wyznaczona konfiguracja nie będzie zawierała żadnej wiadomości, której zdarzenie wysłania nie zostało zapisane w którymś z stanów lokalnych. a więc jest konfiguracją spójną.

<< Poprzedni slajd | Spis treści | Następny slajd >>