Wprowadzenie

     Weryfikacja zaprezentowana poniżej dotyczy języka programowania wielowątkowych planów wykonania (a właściwie biblioteki). Język ten, kryjący się pod nazwą ESL (Executive Suport Language – język wsparcia wykonania) jest jednym ze składników NASA’s New Millenium Remote Agent - opartego o sztuczną inteligencję systemu kontroli statku kosmicznego, zastosowanego w misji Deep Space 1.
     Język ESL jest używany do zaprogramowania komponentu wykonawczego Zdalnego Agenta (Remote Agent), odpowiedzialnego za bezpieczne wykonanie prac pokładowych.
     Kod źródłowy ESL został napisany w Lisp’ie i w przed przystąpieniem do analizy został przepisany do PROMELI.

 

Nieformalny opis

     Przegląd

     Komponent wykonawczy Zdalnego Agenta został zaprojektowany, aby wspierać bezpieczne wykonanie, kontrolowanych programowo, zadań na pokładzie statku kosmicznego.

     Kiedy zadanie jest (oczywiście dynamicznie) uruchamiane, jeszcze przed przejściem do swojej głównej funkcji, próbuje najpierw osiągnąć wymagane własności. Jednak właściwości mogą się zmienić w czasie działania, a wtedy zadanie, które od takich zmienionych właściwości zależy musi zostać przerwane. Aby uprościć zaprogramowanie pojedynczego zadania, Zdalny Agent modeluje urządzenia znajdujące się na pokładzie w kategoriach różnych właściwości jakie mogą one posiadać i przechowuje te informacje w bazie danych.

     Komponent wykonawczy zapewnia zarówno mechanizm dla osiągania jaki i zachowywania właściwości, używając blokad w celu zapobiegnięcia równoległego uruchomienia zadania z niezgodnymi wartościami właściwości.

     Kontrolę nad tym ma demon, który kontroluje bazę danych reprezentującą stan statku kosmicznego. Jeśli istnieje niezgodność między danymi znajdującymi się w bazie danych a tablicą blokad właściwości, demon zawiesza wszystkie zadania przypisane do właściwości i stara się przywrócić jej pożądany stan. Demon zwykle działa w tle, a uaktywnia się dopiero w momencie gdy zachodzi jakieś zdarzenie zmieniające stan bazy danych lub tablicę blokad.

     Komponent wykonawczy zezwala przypisanie konkretnej właściwości wielu metod jej osiągnięcia. W momencie zainicjowania takiej metody, wykonawca woła odpowiednia dla stanu metodę, która coś konkretnego robi (jednak ta właściwość nie będzie przedmiotem weryfikacji i dlatego przyjęte zostanie, iż zadanie może osiągnąć właściwość bezpośrednio).
 

     Typy danych

     Właściwości – określają stan statku kosmicznego (nazwa właściwości, wartość właściwości).

     Baza danych – przechowuje aktualizowane na bieżąco informacje o stanie statku (jego właściwościach).

     Tabela blokad właściwości – przechowuje trójki {właściwość, subskrybenci, osiągnięta} (działanie podczas niezgodności z BD opisane powyżej). Subskrybenci są przechowywani ponieważ właściwość o konkretnej własności może spełniać warunki dal wielu zadań.

     Zdarzenia – w momencie zmiany tablicy blokad właściwości lub bazy danych demon monitorujący zostaje o tym poinformowany, aby mógł sprawdzić odświeżony stan systemu. W tym celu wprowadzone zostały listy zdarzeń: zmiany tabeli blokad (Snarf_Event) oraz zmiany bazy danych (Memory_Event). Jakikolwiek proces (zadanie lub demon), który chce czekać na konkretne zdarzenie (zmieniające właściwość) wywołuje procedurę czekania (wait) – zamieszczającą proces w kolejce oczekujących. Kiedy następuje zmiana właściwości w bazie danych wszystkie procesy będące na liście oczekujących zostają o tym poinformowane i restartowane.

     Procesy

     Zadania – przed wykonaniem starają się osiągnąć pożądane wartości właściwości, najpierw je blokując w tabeli blokad (snarfing). Może to nastąpić jedynie gdy jest zgodne z pozostałymi blokadami (nie ma konfliktu dostępu) wpp. zadanie zostaje porzucone. Tworzący blokadę jest jej właścicielem i jest odpowiedzialny za osiągnięcie właściwości – zmianę jej wartości w bazie danych (udane zmienia wartość parametru achived na true, wpp. zadanie zostaje porzucone). Pozostałe zadania wpisane na listę subskrybentów czekają na zmiennej Memory_Event. Przed zakończeniem zadanie jest zobowiązane do sprawdzenia czy nie jest ostatnim blokującym właściwości i ewentualnie ma zdjąć z niej blokadę.

     Demon – gwarantuje zachowanie osiągniętej właściwości w czasie wykonania zadania (zgodność wartości w tabeli blokad i bazie danych). Normalnie demon „śpi” czekając na zdarzenie modyfikujące bazę danych lub tablicę blokad. Kiedy się „budzi” sprawdza wszystkie blokady i dla każdej z polem achived = true sprawdza czy dana właściwość jest w bazie danych. Jeśli jej nie ma wszystkie zadania do niej się odwołujące są zawieszane i zainicjalizowana zostaje procedura mająca przywrócić oczekiwane wartości. Po zbadaniu wszystkich blokad demon „usypia” czekając na kolejne zdarzenie.

Formalne przekształcenie do PROMELI

  Analiza wybranych właściwościi

Właściwości do sprawdzenia

  • Własność zwalniania - zadanie zwalnia wszystkie blokady zanim zakończy działanie
  • Własność przerwania - w wypadku wystąpienia niezgodności między bazą danych a tablicą blokad, wszystkie zadania odwołujące się do blokady zostaną zakończone, bądź przez siebie, bądź przez demona

Sprawdzenie powyższych właściwości za pomocą formuł LTL doprowadziło do odnalezienia 4 poważnych błędów oraz jednego problemu z wydajnością.


Błąd 1 - Własność zwalniania

Kiedy zadanie kończy działanie, oczekujemy, że nie jest już subskrybentem żadnej wartości właściwości.

Przebieg
Zadnie zaczyna działać, wywołana zostaje procedura execute_task, która blokuje, zmienia wartość i wraca, aby kontynuować działanie. Wykonuje activetasks[this].state = TERMINATED i jest gotowa do wykonania zwolnienia blokad (procedura release_locks).
W tym momencie w środowisku występuje niezgodność w bazie danych, powodująca zmianę wartości właściwości używanej przez zadanie. Demon ją wykrywa i przerywa działanie zadania zmieniając jego stan na ABORTED.

W wyniku powyższego przebiegu nie zostają zdjęte blokady używane przez zadanie. Jest to spowodowane brakiem ochrony, dla zadania, w trakcie próby wykonania procedury release_locks.

Rozwiązanie - dodanie ochrony zwalniania blokad, w taki sposób, żeby nie było możliwe przerwanie.

Programiści ocenili możliwość wystąpienia tego błędu w czasie lotu dość wysoko. Dodatkowo potwierdzili, że najprawdopodobniej nie zostałby on odkryty w żaden inny sposób (ponieważ występuje jedynie w wielowątkowym środowisku i bardzo specyficznych okolicznościach).
 

Błąd 2 - Własność przerwania

Jeśli po zmianie wartości właściwości w BD przez zadanie nastąpi zmiana w środowisku to zadanie zostanie zakończone lub przerwane.

Przebieg
Demon zaczyna działać i osiąga stan oczekiwania na zdarzenia. Zadanie blokuje i zmienia wartość, sygnalizując SNARF_EVENT i rozpoczyna powrót. Demon obudzony przez sygnał, nie znajduje niezgodności i decyduje się (jeszcze de facto tego nie robi) aby zasnąć.
W tym momencie środowisko zmienia jedną ze zmiennych i sygnalizuje MEMORY_EVENT. Jednak sygnał ten nie spowoduje niczego, ponieważ demon jeszcze nie wywołał wait_for_events.
Następnie demon nie orientując sie o żadnej zmianie wywołuje wait_for_events.

Rozwiązanie - obwarowanie wewnętrznych działań demona sekcją krytyczną (atomic)

Programiści przyznali się do klasycznego błędu - nie opakowali procedur sekcją krytyczną, podziękowali za wytknięcie im tego błędu i stwierdzili jednocześnie, że wcześniej lub później zostałby odkryty ponieważ takich błędów w kodzie popełnili mnóstwo.
 

Błąd 3 - Własność przerwania

Ponownie sprawdzamy powyższą własność na poprawionym modelu.

Przebieg
Demon zaczyna działać i osiąga stan oczekiwania na zdarzenia. Zadanie blokuje i zmienia wartość, sygnalizując SNARF_EVENT i rozpoczyna powrót. Demon obudzony przez sygnał, wywołuje procedurę check_locks, która zawiera dwie pętle - jedną, która szuka naruszeń i ewentualnie przerywa zadanie oraz drugą, która jedynie szuka naruszeń. Demon przebiega przez pierwszą z pętli i następnie jest gotowy do wejścia do drugiej.
W tym momencie środowisko zmienia jedną ze zmiennych i sygnalizuje MEMORY_EVENT. Jednak demon już działa więc nic się nie dzieje, jedynie licznik MEMORY_EVENT zostaje zwiększony.
Demon rozpoczyna drugi przebieg, znajduje niezgodność i wywołuje procedurę naprawczą (do_automatic_recovery). Ponieważ licznik został zwiększony demon musi ponownie wykonać check_locks, jednak nic nie znajduje i zasypia.

Przez cały czas zadanie działa i nie zostaje przerwane.

Rozwiązanie - w momencie zauważenia tego przebiegu nie został on zakwalifikowany jako błędny (a raczej jako błąd w tłumaczeniu Lisp'a na PROMELE), jednak nawet później nigdy nie udało się go poprawić.

Według programistów jest to znany im błąd modelu (który już był na liście "rzeczy do zrobienia"), powodujący przedłużenie czasu między wystąpieniem niezgodności a poinformowaniem o tym zadania. Jednak weryfikujący dodatkowo zauważyli, że może się zdarzyć iż zadanie może nigdy nie zostać poinformowane... (jednak ten błąd specjalnie nie przejął programistów)

Błąd 4 - Własność przerwania

Poprawiono kod, tak aby nie dochodziło do sytuacji z błędu 3 (zezwolono na jego występowanie). Z takim kodem zapytanie zmieniono na "we wszystkich stanach, jeśli wartość właściwości zostanie nieoczekiwanie zmieniona, to zadanie w końcu zostanie, bądź zakończone, bądź właściwość zostanie naprawiona".

Przebieg
Zadnie zaczyna działać, wywołana zostaje procedura achieve_locks_property, przez którą najpierw zostaje zmieniona BD, a następnie powinna zostać zmieniona wartość achieved w tablicy blokad na true. W przebiegu przechodzimy przez zmianę BD i zatrzymujemy się.
W tym momencie w środowisku występuje niezgodność zmieniająca wartość zablokowanej zmiennej niszcząca wcześniejszą zmianę. Demon obudzony przez sygnał od środowiska, szuka niezgodności - jednak żadnej nie znajduje ponieważ zadanie nie zaktualizowało tablicy blokad.
Następnie zadanie kontynuuje swoje działanie zmieniając tablicę blokad.

W momencie wystąpienia niezgodności, nie zostaje ona odkryta przez demona i zadanie nie zostaje przerwane.

Rozwiązanie - obwarowanie sekcją krytyczną operacji w achieve_locks_property.

Drugi z błędów ocenionych przez programistów jako niewykrywalny przez inne metody.

Błąd 5 - Problem wydajnościowy

W czasie analizowania przebiegów został odkryty piąty błąd występujący w kodzie Lisp'a. W PROMELI dotyczy on kodu procesu demona.

Polega ona na tym, że sprawdzanie blokad następuje dwukrotnie po tym jak demon zasypia i zostaje obudzony przez sygnał. Licznik nadejścia sygnałów od zdarzeń zostaje dwa razy powiększony.

Programiści potwierdzili istnienie tego błędu jednak nadali mu niski priorytet (bo to tylko kwestia wydajności ;) ).
 

Piotr Góra, maj 2004