[ In English ]

Projekt języka operacji atomowych, deklaratywnej synchronizacji i dynamicznej aktualizacji w systemach komunikacyjnych Pawel T. Wojciechowski Wydawnictwo Politechniki Poznańskiej, Poznań 2007 Spis treści

Obecnie występuje rosnące zainteresowanie projektowaniem nowych języków programowania, które łączą takie cechy, jak współbieżność (lub równoległość) oraz możliwość dodawania nowego kodu w trakcie działania programu. Dzięki tym cechom możliwości procesorów wielordzeniowych mogą być lepiej wykorzystane, pozwalając przy tym na dynamiczną aktualizację oprogramowania. Przykładowymi aplikacjami są usługi rozproszone, które muszą być dostępne bez przerwy, np. finansowe i telekomunikacyjne, rezerwacje lotów oraz kontrola ruchu lotniczego. Zatrzymanie usług świadczonych "non-stop" powoduje straty finansowe; może także spowodować zagrożenie bezpieczeństwa. Dlatego też usługodawcy muszą móc naprawić, zaktualizować lub rozszerzyć swoje systemy z minimalną ingerencją w dostępność usługi. Dające się dynamicznie aktualizować systemy rozproszone mogą być implementowane z użyciem popularnych języków programowania, które pozwalają na dynamiczne ładowanie i łączenie komponentów kodu. Jednakże, aby usprawnić programowanie oraz zagwarantować niezawodność, potrzebne są nowe abstrakcje programistyczne. Przykładem są konstrukcje do synchronizacji różnych operacji wejścia/wyjścia, wykonywanych lokalnie w maszynie lub globalnie w systemie rozproszonym.

W tej rozprawie zaprojektowano nowe konstrukcje językowe i algorytmy uzyskiwania atomowości, deklaratywnej synchronizacji oraz dynamicznej aktualizacji protokołów. Mogą one służyć do budowy systemów komunikacyjnych z modularnych protokołów, które można zastępować dynamicznie.

• Atomowość (niepodzielność) gwarantuje, że zbiór operacji wykonywanych w miejscu sieciowym (maszynie) może być brany pod uwagę jako pojedyncza jednostka obliczeniowa, niezależnie od jakichkolwiek innych operacji wykonywanych współbieżnie.
• Deklaratywna synchronizacja oznacza sposób implementacji sterowania różnego rodzaju współbieżnymi akcjami lub zdarzeniami w systemie, który polega na zdefiniowaniu polityki synchronizacji (takiej jak atomowość). Definiuje się ją w formie zbioru reguł,  oddzielnie od kodu komponentów. Takie podejście umożliwia ponowne użycie komponentów protokołów w różnych stosach protokołów oraz ułatwia ich dynamiczną zamianę.
• Dynamiczna aktualizacja protokołów oznacza transparentną zamianę protokołów w trakcie działania systemu w taki sposób, że korzystanie z usług implementowanych przez te protokoły nie jest narażone na błędy. Jednoczesna dynamiczna zamiana komponentów protokołów zlokalizowanych w różnych miejscach sieciowych odbywa się pod kontrolą algorytmów przełączania.

Rozprawa ma następującą strukturę:

• Rozpoczęto od przedyskutowania motywacji i kontrybucji. Następnie opisano algorytmy wersjonowania przeznaczone do sterowania współbieżnością w zadaniach atomowych.
• W kolejnym rozdziale zaprojektowano rachunek (ang. calculus) zadań atomowych, tj. transakcji atomowych bez odtwarzania stanu, mogących mieć efekty wejścia/wyjścia. Rachunek ten wyposażony jest w system typów do statycznej weryfikacji danych wymaganych przez dynamiczne wersjonowanie. System typów gwarantuje, że proponowane w rachunku konstrukcje programistyczne są używane w sposób prawidłowy.
• Następnie opisano dwa różne podejścia do synchronizacji deklaratywnej: (1) rachunek kombinatorów współbieżności z opartą na typach weryfikacją spełnialności kombinatorów (co daje gwarancję ich poprawnego zastosowania) oraz (2) język ograniczeń (ang. constraint language) dla modelu synchronizacji opartego na rolach.
• W kolejnym rozdziale opisano model dynamicznej aktualizacji protokołów oraz podano dwa przykładowe algorytmy przełączania protokołów, mające określone pożądane własności.
• W ostatnim rozdziale zaprojektowano oparty na klasach obiektowy rachunek wiązań dynamicznych. Rachunek posłużył do pokazania zastosowań mechanizmów synchronizacji opisanych w tej książce (tj. zadań atomowych i kombinatorów współbieżności) przy dynamicznym wiązaniu obiektów.
• W dodatku zamieszczono formalne dowody poprawności szeregu twierdzeń wykazujących trafność (poprawność) systemu typów (ang. type soundness) dla rachunku zadań atomowych, w tym dowód dynamicznej poprawności przykładowego algorytmu wersjonowania.

Manuskrypt książki jest dostępny w formacie PDF i Postscript. Uwagi dotyczące treści mile widziane.