Teoria modelu aktora

W informatyce teoretycznej teoria modelu aktora dotyczy zagadnień teoretycznych dotyczących modelu aktora .

Aktorzy to prymitywy, które stanowią podstawę modelu Actor współbieżnych obliczeń cyfrowych. W odpowiedzi na otrzymaną wiadomość Aktor może podejmować lokalne decyzje, tworzyć więcej Aktorów, wysyłać więcej wiadomości i wyznaczyć sposób odpowiedzi na następną otrzymaną wiadomość. Teoria modelu aktora obejmuje teorie zdarzeń i struktur obliczeń aktora, ich teorię dowodu i modele denotacyjne .

Zdarzenia i ich kolejność

Z definicji Aktora widać, że ma miejsce wiele zdarzeń: lokalne decyzje, tworzenie Aktorów, wysyłanie wiadomości, odbieranie wiadomości oraz wyznaczanie sposobu odpowiedzi na kolejną otrzymaną wiadomość.

Jednak ten artykuł koncentruje się tylko na tych zdarzeniach, które są nadejściem wiadomości wysłanej do Aktora.

Ten artykuł dotyczy wyników opublikowanych w Hewitt [2006].

Prawo policzalności : Zdarzeń jest co najwyżej policzalnie wiele.

Zamawianie aktywacji

Porządkowanie aktywacji ( -≈→ ) jest uporządkowaniem fundamentalnym, które modeluje jedno zdarzenie aktywujące drugie (musi istnieć przepływ energii w komunikacie przechodzącym od zdarzenia do zdarzenia, które aktywuje).

  • Ze względu na transmisję energii porządek aktywacji jest relatywistycznie niezmienny ; to znaczy dla wszystkich zdarzeń e 1 . e 2 , jeśli e 1 -≈→ e 2 , to czas e 1 poprzedza czas e 2 w relatywistycznych układach odniesienia wszystkich obserwatorów.
  • Prawo ścisłej przyczynowości dla aktywacji Porządkowanie : Dla żadnego zdarzenia e -≈→ e .
  • Prawo skończonego pierwszeństwa w porządku aktywacji : Dla wszystkich zdarzeń e 1 zbiór {e|e -≈→ e 1 } jest skończony.

Zamówienia przyjazdu

Kolejność nadejścia Aktora x ( -x→ ) modeluje (całkowite) uporządkowanie zdarzeń, w których wiadomość dociera do x . Kolejność przybycia jest określana przez arbitraż w przetwarzaniu wiadomości (często z wykorzystaniem obwodu cyfrowego zwanego arbitrem ). Wydarzenia przybycia Aktora są na jego światowej linii . Kolejność przybycia oznacza, że ​​model aktora z natury ma nieokreśloność (zobacz Nieokreśloność w obliczeniach współbieżnych ).

  • Ponieważ wszystkie zdarzenia uporządkowania przybycia aktora x zachodzą na linii świata x , uporządkowanie przybycia aktora jest relatywistycznie niezmienne . Tj . dla wszystkich aktorów x i zdarzeń e 1 . e 2 , jeśli e 1 -x→ e 2 , to czas e 1 poprzedza czas e 2 w relatywistycznych układach odniesienia wszystkich obserwatorów.
  • Prawo skończonej predecesji w porządku przybycia : Dla wszystkich zdarzeń e 1 i Aktorów x zbiór {e|e -x→ e 1 } jest skończony.

Zamówienie łączone

Połączone uporządkowanie (oznaczone przez → ) jest definiowane jako przechodnie domknięcie uporządkowania aktywacji i uporządkowania przybycia wszystkich Aktorów.

  • Połączone uporządkowanie jest relatywistycznie niezmienne, ponieważ jest przechodnim zamknięciem relatywistycznie niezmiennych porządków. To znaczy dla wszystkich zdarzeń e 1 . mi 2 , jeśli mi 1 →e 2 . wtedy czas e 1 poprzedza czas e 2 w relatywistycznych układach odniesienia wszystkich obserwatorów.
  • Prawo ścisłej przyczynowości dla złożonego porządku : Ponieważ żadne zdarzenie nie ma e→e .

Połączone uporządkowanie jest oczywiście przechodnie z definicji.

W [Baker i Hewitt 197?] przypuszczano, że powyższe prawa mogą pociągać za sobą następujące prawo:

Prawo skończonych łańcuchów między zdarzeniami w porządku złożonym : Nie ma nieskończonych łańcuchów ( tj . liniowo uporządkowanych zbiorów) zdarzeń między dwoma zdarzeniami w porządku złożonym →.

Niezależność prawa skończonych łańcuchów między zdarzeniami w złożonym porządku

Jednak [Clinger 1981] nieoczekiwanie udowodnił, że prawo skończonych łańcuchów między zdarzeniami w połączonym porządku jest niezależne od poprzednich praw, tj .

Twierdzenie. Prawo Skończonych Łańcuchów Pomiędzy Zdarzeniami w Połączonym Porządku nie wynika z wcześniej podanych praw.

Dowód. Wystarczy pokazać, że istnieje obliczenie aktora, które spełnia podane wcześniej prawa, ale narusza prawo skończonych łańcuchów między zdarzeniami w złożonym porządku.

Rozważmy obliczenia, które rozpoczynają się, gdy aktor Initial otrzymuje komunikat Start , powodujący podjęcie przez niego następujących działań
  1. Utwórz nowego aktora Greeter 1 , który otrzyma wiadomość SayHelloTo z adresem Greeter 1
  2. Wyślij Zainicjuj wiadomość Ponownie , podając adres powitania 1
Następnie zachowanie Initial jest następujące po odebraniu wiadomości Again z adresem Greeter i (które nazwiemy wydarzeniem Again i ):
  1. Utwórz nowego aktora Greeter i+1 , któremu zostanie wysłana wiadomość SayHelloTo z adresem Greeter i
  2. Wyślij Zainicjuj wiadomość ponownie , podając adres Greeter i+1
Oczywiście obliczenia początkowego wysyłania wiadomości ponownie nigdy się nie kończą.
Zachowanie każdego aktora witającego i jest następujące:
  • Kiedy otrzyma wiadomość SayHelloTo z adresem Greeter i-1 (które nazwiemy zdarzeniem SayHelloTo i ), wysyła wiadomość Hello do Greeter i-1
  • Gdy otrzyma wiadomość Hello (którą nazwiemy zdarzeniem Hello i ), nie robi nic.
Teraz możliwe jest, że Hello i - Greeter i → SayHelloTo i za każdym razem, a zatem Hello i → SayHelloTo i .
Również Ponownie i -≈→ Ponownie i+1 za każdym razem, a zatem Ponownie i → Ponownie i+1 .
Ponadto wszystkie prawa określone przed Prawem Ścisłej Przyczynowości dla Połączonego Porządku są spełnione. Jednak w połączonej kolejności między
Again 1 a SayHelloTo 1 może istnieć nieskończona liczba zdarzeń w następujący sposób:
Znowu 1 →...→ Ponownie ja →... ... → Cześć ja → Przywitaj się z i →...→ Cześć 1 → Przywitaj się z 1

Jednak wiemy z fizyki, że nieskończonej energii nie można wydać wzdłuż skończonej trajektorii. Dlatego, ponieważ model aktora jest oparty na fizyce, prawo skończonych łańcuchów między zdarzeniami w złożonym porządku zostało przyjęte jako aksjomat modelu aktora.

Prawo dyskrecji

Prawo skończonych łańcuchów między zdarzeniami w połączonym porządku jest ściśle związane z następującym prawem:

Prawo dyskretności : Dla wszystkich zdarzeń e 1 i e 2 , zbiór {e|e 1 →e→e 2 } jest skończony.

W rzeczywistości wykazano, że poprzednie dwa prawa są równoważne:

Twierdzenie [Clinger 1981]. Prawo dyskrecji jest równoważne prawu skończonych łańcuchów między zdarzeniami w złożonym porządku (bez użycia aksjomatu wyboru).

Prawo dyskretności wyklucza maszyny Zenona i jest związane z wynikami na sieciach Petriego [Best et al. 1984, 1987].

Prawo dyskretności implikuje właściwość nieograniczonego niedeterminizmu . Połączone uporządkowanie jest używane przez [Clinger 1981] przy konstruowaniu denotacyjnego modelu Aktorów (patrz semantyka denotacyjna ).

Semantyka denotacyjna

Clinger [1981] wykorzystał opisany powyżej model zdarzeń Aktora do skonstruowania modelu denotacyjnego dla Aktorów przy użyciu domen władzy . Następnie Hewitt [2006] rozszerzył diagramy o czasy przybycia, aby skonstruować technicznie prostszy model denotacyjny , który jest łatwiejszy do zrozumienia.

Zobacz też

  • Carla Hewitta i in. Actor Induction and Meta-evaluation Conference Record of ACM Symposium on Principles of Programming Languages, styczeń 1974.
  • Irena Greif. Semantyka komunikowania procesów równoległych Rozprawa doktorska MIT EECS. sierpień 1975.
  • Edsger Dijkstra. Dyscyplina programowania Prentice Hall. 1976.
  • Carl Hewitt i Henry Baker Aktorzy i ciągłe działania funkcjonalne konferencji roboczej IFIP na temat formalnego opisu koncepcji programowania. 1-5 sierpnia 1977.
  • Henry Baker i Carl Hewitt Przyrostowe zbieranie śmieci procesów Proceedings of the Symposium on Artificial Intelligence Programming Languages. Zawiadomienia SIGPLAN 12, sierpień 1977.
  • Carl Hewitt i Henry Baker Prawa dotyczące komunikowania procesów równoległych IFIP-77, sierpień 1977.
  • Aki Yonezawa Techniki specyfikacji i weryfikacji programów równoległych oparte na semantyce przekazywania wiadomości Rozprawa doktorska MIT EECS. grudzień 1977.
  • Peter Bishop Bardzo duża przestrzeń adresowa Modułowo rozszerzalne systemy komputerowe MIT EECS Rozprawa doktorska. czerwiec 1977.
  • Carla Hewitta. Przeglądanie struktur kontrolnych jako wzorców przekazywania wiadomości Journal of Artificial Intelligence. czerwiec 1977.
  • Henryk Baker. Systemy aktorów do obliczeń w czasie rzeczywistym Rozprawa doktorska MIT EECS. styczeń 1978.
  • Carla Hewitta i Russa Atkinsona. Specyfikacja i techniki sprawdzania serializatorów IEEE Journal on Software Engineering. styczeń 1979.
  • Carla Hewitta, Beppe Attardiego i Henry'ego Liebermana. Delegacja w obradach Message Passing of First International Conference on Distributed Systems Huntsville, AL. październik 1979.
  • Russa Atkinsona. Automatyczna weryfikacja serializatorów Rozprawa doktorska MIT. czerwiec 1980.
  • Billa Kornfelda i Carla Hewitta. Metafora społeczności naukowej Transakcje IEEE dotyczące systemów, człowieka i cybernetyki . styczeń 1981.
  • Gerry'ego Barbera. Rozumowanie na temat zmian w kompetentnych systemach biurowych Rozprawa doktorska MIT EECS. sierpień 1981.
  • Billa Kornfelda. Paralelizm w rozwiązywaniu problemów Rozprawa doktorska MIT EECS. sierpień 1981.
  • Willa Clingera. Podstawy semantyki aktora Rozprawa doktorska z matematyki MIT . czerwiec 1981.
  • Eike Best . Zachowanie współbieżne: sekwencje, procesy i aksjomaty Notatki z wykładów z informatyki, tom 197 1984.
  • Gul Agha. Aktorzy: model obliczeń współbieżnych w rozprawie doktorskiej w systemach rozproszonych . 1986.
  • Eike Best i R.Devillers. Sekwencyjne i współbieżne zachowanie w teorii sieci Petriego, informatyka teoretyczna, tom 55/1. 1987.
  • Gul Agha, Ian Mason, Scott Smith i Carolyn Talcott. A Foundation for Actor Computation Journal of Functional Programming, styczeń 1993.
  • Satoshi Matsuoka i Akinori Yonezawa . Analiza anomalii dziedziczenia w obiektowych językach programowania współbieżnego w Kierunki badań w współbieżnym programowaniu obiektowym. 1993.
  • Jayadev Misra. Logika programowania współbieżnego: Safety Journal of Computer Software Engineering . 1995.
  • Luca de Alfaro, Zohar Manna, Henry Sipma i Tomás Uribe. Wizualna weryfikacja systemów reaktywnych TACAS 1997.
  • Thati, Prasanna, Carolyn Talcott i Gul Agha. Techniki wykonywania i rozumowania dotyczące diagramów specyfikacji Międzynarodowa konferencja na temat metodologii algebraicznej i technologii oprogramowania (AMAST), 2004.
  • Giuseppe Milicia i Vladimiro Sassone. Anomalia dziedziczenia: dziesięć lat po obradach sympozjum ACM 2004 na temat informatyki stosowanej (SAC), Nikozja, Cypr, 14–17 marca 2004 r.
  • Petrusa Potgietera. Maszyny Zeno i hiperkomputacje 2005
  • Carl Hewitt Co to jest zaangażowanie? Fizyczne, organizacyjne i społeczne COINS@AAMAS. 2006.
Pobrano z „ https://en.wikipedia.org/w/index.php?title=Actor_model_theory&oldid=1009901428 ”