Trój-Modularna Redundancja
(Triple-Modular Redundancy - John von Neumann)

 

Opis problemu

W systemach rozproszonych ważną kwestią jest obsługa błędów, które są wadami systemów. Błędy mogą być:

Strategie obsługi błędów to:

TMR jest popularną techniką tolerancji i ewentualnej detekcji błędów. Poprawia niezawodność systemu poprzez połączenie trzech niezależnych instancji systemu przez rozdzielacz (splitter) na wejściu i głosującego (voter) na wyjściu.

Rys. 1 - schemat TMR

Zaletą TMR jest to, że maskuje przed użytkownikiem zarówno przelotne jak i trwałe błędy. Dopóki mamy pewność, że jednocześnie tylko jeden z trzech komponentów może ulec uszkodzeniu, wyjście będzie prawdziwe. TMR można stosować warstwowo i niezależnie od komponentów bazowych systemu (pełna niezależność TMR).

TMR nie radzi sobie błędami projektowymi (programistycznymi). Jednakże w momencie, gdy komponenty spełniają tą samą funkcję ale są zupełnie inaczej zaprojektowane można je zastosować w TMR dla programów.

W większości przypadków w momencie zaistnienia niezgodności na wyjściu chcemy się dowiedzieć, który z modułów dał fałszywy wynik, aby go zastąpić bądź naprawić (realizacja bezpośrednio przez komponent głosujący lub poprzez tzw. detektory niezgodności). Podstawowy model TMR zakłada istnienie trzech modułów, jednak nic nie stoi na przeszkodzie aby dodać dodatkowe, które mogą zastąpić jeden z podstawowych w wypadku awarii. Dość często stosuje się również replikację komponentu głosującego.

Prosty moduł TMR

Rys. 2 - interfejs prostego modułu TMR

Rys. 3 - diagram prostego modułu TMR

"Strawny" kod prostego TMR w VP:

(* model 1 TMR *)

const Val = {0,1} (* wejście, wyjście *)
const I = {1,2,3} (* indeksy modułu *)

label in(Val),out(Val) (* wejścia/wyjścia systemowe *)
label mi_I(Val),mo(Val) (* akcje modułu *)
label ack (* synchronizacja akcji głosującego/dzielącego *)
(* moduł *)
agent M = in(x).('out(x).M + t.sum(y:Val,'out(y).M))
agent M(i:I) = M[mi_i/in,mo/out] (* wersja indeksowana *)

Moduł akceptuje wejście i wylicza wyjście (na podstawie funkcji identyczności), t - to akcja wewnętrzna sygnalizująca błąd (po jej zajściu możemy otrzymać cokolwiek).

(* dzielący *)
agent S = in(x).sum(i:I,'mi_i(x).sum(j:diff(I,{i}),'mi_j(x).sum(k:diff(I,{i,j}),'mi_k(x).ack.S)))

Dzielący dostarcza wejście 3 modułom w określonym porządku. Zakładamy, że jest on niezawodny (tak jak i głosujący). Na następną "kolejkę" czeka do momentu, aż otrzyma ack.

(* głosujący *)
agent V = mo(x1).mo(x2).mo(x3).
              if x1 = x2 then V'(x1) else V'(x3)
agent V'(x:Val) = 'out(x).'ack.V

Głosujący przyjmuje 3 wartości na wejściu i porównuje najpierw pierwsza i drugą, jeśli są takie same to ma juz wynik w przeciwnym przypadku trzecia wartość jest decydująca.

(* trój modularna redundancja (321 stanów) *)
agent TMR1 = (S | M(1) | M(2) | M(3) | V)\{mi,mo,ack}

Model TMR z trzema modułami (komunikacja wewnętrzna jest ukryta), które mogą zawieść - musimy taka sytuację wykluczyć - dlatego musimy mieć model modułu doskonałego nigdy się nie psującego:

(* moduł doskonały *)
agent MP = in(x).'out(x).MP
agent MP(i:I) = MP[mi_i/in,mo/out]
(* TMR z dwoma doskonałymi modułami (149 stanów) *)
agent TMR1' = (S | M(1) | MP(2) | MP(3) | V)\{mi,mo,ack}

Model TMR1' jest już ostateczny - ma w sobie 2 moduły doskonałe i jeden, który może się zepsuć.

Źródło w CCS

Stawiamy pytanie: Czy TMR zachowuje się jak moduł doskonały

 eq (TMR1', MP);    True

W momencie gdybyśmy nie mieli akcji ack między głosującym a dzielącym mogłyby się zdarzyć nieoczekiwane przeploty akcji (dzielący dwukrotnie przesyła sygnał do modułów zanim głosujący po raz pierwszy odpowie...)

 

TMR z wykrywaniem błędów

Rys. 4 - interfejs TMR z wykrywaniem błędów

Rys. 5 - diagram TMR z wykrywaniem błędów

Źródło TMR z wykrywaniem błędów w VP:

(* model 2 TMR *)

const Val = {0,1} (* wartości wejścia, wyjścia *)
const I = {1,2,3} (* indeksy modułu *)

label in(Val),out(Val) (* wejścia/wyjścia systemu *)
label mi_I(Val),mo_I(Val) (* wejścia/wyjścia modułu *)
label do(Val),vo(Val) (* detektor wyjścia, wyjście głosującego *)
label fail_I,detect_I (* uszkodzenie modułu, wykrywanie uszkodzenia *)
label ack,mack_I

Dodane wyjścia tak jak na rysunku 5.

(* dzielący *)
agent S = in(x).sum(i:I,'mi_i(x).sum(j:diff(I,{i}),'mi_j(x).sum(k:diff(I,{i,j}),'mi_k(x).ack.S)))

Dzielący bez zmian.

(* moduł wadliwy *)
agent M(i:I) = mi_i(x).(M'(i,x) + fail_i.sum(y:diff(Val,{x}),M'(i,y)))
agent M'(i:I,x:Val) = 'mo_i(x).mack_i.M(i)

Do modułu dodajemy akcję fail - czyli sprawdzenie czy nastąpił błąd indeksowane po wyjściu (ponieważ chcemy wykrywać błąd w każdym z modułów). Akcja mack jest sygnałem synchronizującym dla wykrywacza.

(* moduł doskonały *)
agent MP(i:I) = M(i)\{fail_i}

To taki zwykły moduł, w którym zakazujemy akcji fail_i.

(* wykrywacz niezgodności *)
agent D(i:I) = mo_i(x).'do(x).D'(i,x)
agent D'(i:I,x:Val) = vo(y).(
           if x <> y then detect_i.'mack_i.D(i)
           else 'mack_i. D(i))

Wysyła wynik modułu do głosującego, czeka na wynik głosowania, sprawdza i jeśli wartości nie są zgodne sygnalizuje wykrycie błędu (detect) i bez względu na wynik czeka na synchronizację z modułem.

(* moduł + detektor *)
agent MD(i:I) = (M(i) | D(i))\{mo_i,mack_i}
(* moduł doskonały + detektor *)
agent MD'(i:I) = (MP(i) | D(i))\{mo_i,mack_i}

Moduł normalny i doskonały połączeni z detektore.

(* głosujący *)
agent V = do(x1).do(x2).do(x3).
           if x1 = x2 then V'(x1) else V'(x3)
agent V'(x:Val) = 'vo(x).'vo(x).'vo(x).'out(x).'ack.V

Głosujący zostaje wzbogacony o akcje wysyłające większościowy wynik do wykrywacza.

(* Trój Modularna Redundancja *)
agent TMR2 = (S | MD(1) | MD'(2) | MD'(3) | V)\{mi,do,vo,ack}

agent Cycler = fail_1.detect_1.Cycler

Podstawowy model rozszerzonego TMR. Cycler symuluje jak powinien działać "doskonale uszkodzony" model - zawsze po awarii, musi zostać ona wykryta (przed wykryciem kolejnej awarii).

(* efekt ukrycia operatora uzyskuje się poprzez zdefiniowanie procesu, który
synchronizuje wszystkie akcje, które mają zostać ukryte *)

agent Hide1 = sum(x:I,'fail_x.Hide1 + 'detect_x.Hide1)
(* TMR2 z wszystkimi akcjami uszkodzenia/wykrywania ukrytymi *)
agent TMR2' = (TMR2 | Hide1)\{fail,detect}

Ponieważ sprawdzamy dwie własności musimy ukryć pewne szczegóły nie rozpatrywane - powyżej ukrywamy wszystkie akcje związane z wykrywaniem i raportowaniem błędów (do sprawdzenia czy model TMR działa zawsze dobrze).

(* TMR2 z wejściami/wyjściami i niektórymi akcjami uszkodzenia/wykrywania ukrytymi *)
agent Hide2 = sum(x:Val,'in(x).Hide2) + out(x).Hide2

agent TMR2'' = (TMR2 | Hide2)\{in,out}

Dla sprawdzenia czy następuje poprawna detekcja błędów ukrywamy wejście i wyjście.

Źródło wCCS

 eq (TMR2', MP);            True

 eq (TMR2'', Cycler);       True

 

Sift-Out Modular Redundancy