LANGUAGE DESIGN FOR ATOMICITY DECLARATIVE SYNCHRONIZATION AND...

W 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. Rozważania rozpoczęto od omówienia motywacji i kontrybucji. Opisano algorytmy wersjonowania przeznaczone do sterowania współbieżnością w zadaniach atomowych. Następnie zaprojektowano rachunek 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 podejścia do synchronizacji deklaratywnej: rachunek kombinatorów współbieżności z opartą na typach weryfikacją spełnialności kombinatorów oraz język ograniczeń dla modelu synchronizacji opartego na rolach. 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. Na zakończenie zaprezentowano oparty na klasach obiektowy rachunek wiązań dynamicznych, który posłużył do pokazania zastosowań mechanizmów synchronizacji opisanych w tej książce przy dynamicznym wiązaniu obiektów. W dodatku zamieszczono formalne dowody poprawności szeregu twierdzeń wykazujących trafność systemu typów dla rachunku zadań atomowych, w tym dowód dynamicznej poprawności przykładowego algorytmu wersjonowania.

Wersja do druku Zapytaj Wyślij link Cofnij