Model aktora i rachunek procesów

W informatyce model aktora i rachunek procesów to dwa ściśle powiązane podejścia do modelowania współbieżnych obliczeń cyfrowych . Zobacz historię modelu aktora i procesu kalkulacyjnego .

Istnieje wiele podobieństw między tymi dwoma podejściami, ale także kilka różnic (niektóre filozoficzne, niektóre techniczne):

  • Jest tylko jeden model aktora (chociaż ma on wiele formalnych systemów projektowania, analizy, weryfikacji, modelowania itp. ); istnieje wiele rachunków procesowych opracowanych w celu wnioskowania o różnych rodzajach współbieżnych systemów na różnych poziomach szczegółowości (w tym rachunki uwzględniające czas, przejścia stochastyczne lub konstrukcje specyficzne dla obszarów zastosowań, takich jak analiza bezpieczeństwa).
  • Model Aktora został zainspirowany prawami fizyki i opiera się na nich dla swoich podstawowych aksjomatów, tj. praw fizycznych (patrz Teoria modelu aktora ); rachunki procesowe były pierwotnie inspirowane algebrą ( Milner 1993 ).
  • Procesy w rachunkach procesów są anonimowe i komunikują się poprzez wysyłanie wiadomości albo przez nazwane kanały (synchroniczne lub asynchroniczne), albo przez otoczenie (które można również wykorzystać do modelowania komunikacji kanałowej ( Cardelli i Gordon 1998 )). Natomiast aktorzy w modelu aktora posiadają tożsamość i komunikują się, wysyłając wiadomości na adresy pocztowe innych aktorów (ten styl komunikacji może być również wykorzystany do modelowania komunikacji kanałowej — patrz poniżej).

Publikacje na temat modelu aktora i rachunków procesów zawierają sporo odsyłaczy, potwierdzeń i wzajemnych cytatów (patrz model aktora i historia rachunków procesów ).

Jak działają kanały

Komunikacja pośrednia z wykorzystaniem kanałów ( np. Gilles Kahn i David MacQueen [1977]) była ważnym zagadnieniem dla komunikacji w obliczeniach równoległych i współbieżnych, wpływającym zarówno na semantykę, jak i wydajność. Niektóre rachunki procesowe różnią się od modelu aktora wykorzystaniem kanałów w przeciwieństwie do bezpośredniej komunikacji.

Kanały synchroniczne

Kanały synchroniczne mają tę właściwość, że nadawca umieszczający wiadomość w kanale musi czekać, aż odbiorca pobierze wiadomość z kanału, zanim nadawca będzie mógł kontynuować.

Proste kanały synchroniczne

Kanał synchroniczny może być modelowany przez aktora, który odbiera komunikację typu put i get . Poniżej przedstawiono zachowanie aktora dla prostego kanału synchronicznego:

  • Każda wysłana komunikacja ma wiadomość i adres, na który wysyłane jest potwierdzenie, gdy wiadomość zostanie odebrana przez komunikację get z kanału w kolejności FIFO .
  • Każda komunikacja get ma adres, na który wysyłana jest odebrana wiadomość.

Kanały synchroniczne w rachunku procesowym

Jednak proste kanały synchroniczne nie wystarczają do obliczeń procesowych, takich jak Communicating Sequential Processes (CSP) [Hoare 1978 i 1985], ponieważ używa się polecenia strzeżonego wyboru (za Dijkstrą) (nazywanego w CSP poleceniem alternatywnym ). W poleceniu wyboru strzeżonego wiele ofert (zwanych strażnikami) może być składanych jednocześnie na wielu kanałach w celu wysyłania i odbierania wiadomości; jednak co najwyżej jeden ze strażników może być wybrany dla każdego wykonania polecenia wyboru strzeżonego. Ponieważ można wybrać tylko jednego strażnika, komenda wyboru chronionego zasadniczo wymaga pewnego rodzaju protokołu zatwierdzania dwufazowego lub być może nawet protokołu zatwierdzania trójfazowego, jeśli dozwolone są przerwy w strażnikach (jak w Occam 3 [1992]) .

Rozważmy następujący program napisany w CSP [Hoare 1978]:

[X :: Z!stop() || Y :: strażnik: wartość logiczna; strażnik := prawda; *[strażnik → Z!go(); Strażnik] || Z :: n: liczba całkowita; n:= 0; *[X?stop() → Y!fałsz; drukuj! n; [] Y?go() → n := n+1; prawda]]

wynika z niepełnej specyfikacji synchronizacji sygnałów między trzema procesami X , Y i Z. Powtarzalne polecenie strzeżone w definicji Z ma dwie alternatywy:

  1. komunikat stop jest akceptowany z X , w takim przypadku Y otrzymuje wartość false , a print otrzymuje wartość n
  2. wiadomość go jest akceptowana z Y , w którym to przypadku n jest zwiększane i Y otrzymuje wartość true .

Jeśli Z kiedykolwiek zaakceptuje komunikat stop od X , wówczas X zakończy działanie. Zaakceptowanie zatrzymania powoduje wysłanie Y fałszu , co po wprowadzeniu jako wartości jego strażnika spowoduje zakończenie Y. Kiedy zarówno X , jak i Y zostały zakończone, Z kończy się, ponieważ nie ma już żywych procesów dostarczających danych wejściowych.

W powyższym programie istnieją kanały synchroniczne od X do Z , Y do Z i Z do Y.

Analogia z problemem koordynacji komitetu

Według Knabe [1992], Chandy i Misra [1988] scharakteryzowali to jako analogiczne do problemu koordynacji komitetu:

Profesorowie na uniwersytecie są przydzielani do różnych komisji. Od czasu do czasu profesor zdecyduje się wziąć udział w posiedzeniu któregoś z jej komitetów i będzie czekał, aż będzie to możliwe. Posiedzenia mogą się rozpocząć tylko przy pełnej frekwencji. Zadanie polega na upewnieniu się, że jeśli wszyscy członkowie komitetu czekają, to przynajmniej jeden z nich weźmie udział w jakimś spotkaniu.
Sedno tego problemu polega na tym, że dwa lub więcej komitetów może mieć jednego profesora. Kiedy ta profesor staje się dostępna, może wybrać tylko jedno ze spotkań, podczas gdy inne nadal czekają.

Prosty protokół rozproszony

W tej sekcji przedstawiono prosty rozproszony protokół dla kanałów w rachunkach procesów synchronicznych. W protokole występują pewne problemy, które omówiono w poniższych sekcjach.

Zachowanie polecenia strzeżonego wyboru jest następujące:

  • Dowództwo wysyła wiadomość do każdego ze swoich strażników, aby się przygotował .
  • Kiedy otrzyma pierwszą odpowiedź od jednego ze swoich strażników, że jest przygotowany, wysyła wiadomość do tego strażnika, aby przygotował się do zatwierdzenia i wysyła wiadomość do wszystkich pozostałych strażników, aby przerwali .
    • Kiedy otrzyma wiadomość od strażnika, że ​​jest gotowy do zatwierdzenia , wysyła strażnikowi wiadomość o zatwierdzeniu . Jeśli jednak strażnik zgłosi wyjątek, którego nie może przygotować do zatwierdzenia , wówczas komenda Guarded Choice rozpoczyna cały proces od nowa.
  • Jeśli wszyscy jego strażnicy odpowiedzą, że nie mogą się przygotować , komenda strzeżona nic nie robi.

Zachowanie strażnika jest następujące:

  • Po otrzymaniu wiadomości o przygotowaniu strażnik wysyła wiadomość o przygotowaniu do każdego kanału, z którym oferuje komunikację. Jeśli strażnik ma takie wartości logiczne, że nie może się przygotować lub jeśli któryś z kanałów odpowie, że nie może się przygotować , wówczas wysyła komunikaty o przerwaniu do innych kanałów, a następnie odpowiada, że ​​nie może się przygotować .
    • Po otrzymaniu komunikatu o przygotowaniu do zatwierdzenia strażnik wysyła komunikat o przygotowaniu do zatwierdzenia do każdego z kanałów. Jeśli któryś z kanałów odpowie, że nie może przygotować się do zatwierdzenia , wysyła komunikaty o przerwaniu do innych kanałów, a następnie zgłasza wyjątek, że nie może przygotować się do zatwierdzenia .
    • Po otrzymaniu komunikatu o zatwierdzeniu strażnik wysyła komunikat o zatwierdzeniu do każdego z kanałów.
    • Po odebraniu wiadomości o przerwaniu , strażnik wysyła wiadomość o przerwaniu do każdego z kanałów.

Zachowanie kanału jest następujące:

  • Po odebraniu komunikatu przygotowania do nawiązania odpowiedz, że jest przygotowany, jeśli komunikat jest w toku przygotowania do odebrania , chyba że odebrano komunikat zakończenia , w którym to przypadku rzuć wyjątek, że nie można przygotować się do nawiązania .
  • Po odebraniu komunikatu przygotowującego do odebrania , odpowiedz, że jest przygotowany, jeśli istnieje komunikat przygotowujący do umieszczenia w toku, chyba że odebrano komunikat kończący , w którym to przypadku rzuć wyjątek, że nie może przygotować się do odebrania .
    • Po odebraniu komunikatu dotyczącego przygotowania do zobowiązania do umieszczenia , odpowiedz, że jest przygotowany, jeśli trwa przygotowanie do zatwierdzenia, aby uzyskać komunikację, chyba że otrzymano komunikat kończący , w którym to przypadku rzuć wyjątek, że nie można przygotować się do zobowiązania do umieszczenia .
    • Po otrzymaniu komunikatu „ready to commit to get” odpowiedz, że jest on przygotowany, jeśli jest „ ready to commit”, aby umieścić komunikat w toku, chyba że otrzymano komunikat zakończenia , w którym to przypadku rzuć wyjątek, że nie można przygotować się do zobowiązania się do odebrania .
      • Po odebraniu komunikatu dotyczącego zatwierdzenia , w zależności od tego, który z poniższych zostanie odebrany:
        • Po odebraniu komunikatu o zatwierdzeniu pobierania , jeśli jeszcze tego nie zrobiono, wykonaj polecenie put and get i oczyść przygotowania.
        • Po odebraniu komunikatu o przerwaniu pobierania anuluj przygotowania
      • Po odebraniu komunikatu dotyczącego zatwierdzenia , w zależności od tego, który z poniższych komunikatów zostanie odebrany:
        • Po odebraniu komunikatu dotyczącego zatwierdzenia , jeśli jeszcze tego nie zrobiono, wykonaj get and put i oczyść przygotowania.
        • Po odebraniu komunikatu o przerwaniu odkładania anuluj przygotowania.
      • Po odebraniu komunikatu o przerwaniu odkładania anuluj przygotowania.
      • Po odebraniu komunikatu o przerwaniu pobierania anuluj przygotowania.

Głód przy pobieraniu z wielu kanałów

Rozważmy ponownie program napisany w CSP (omówiony w części Synchroniczne kanały w obliczeniach procesowych powyżej):

[X :: Z!stop() || Y :: strażnik: wartość logiczna; strażnik := prawda; *[strażnik → Z!go(); Strażnik] || Z :: n: liczba całkowita; n:= 0; *[X?stop() → Y!fałsz; drukuj! n; [] Y?go() → n := n+1; prawda]]

Jak wskazano w Knabe [1992], problem z powyższym protokołem ( Prosty protokół rozproszony ) polega na tym, że proces Z może nigdy nie zaakceptować komunikatu zatrzymania od X (zjawisko zwane głodem ), aw konsekwencji powyższy program może nigdy niczego nie wydrukować.

W przeciwieństwie do tego rozważ prosty system aktorów, który składa się z aktorów X , Y , Z i drukuj gdzie

  • Aktor X jest tworzony z następującym zachowaniem: Jeśli
    • otrzymano wiadomość „start” , wyślij Z wiadomość „stop”
  • aktor Y z następującym zachowaniem:
    • otrzymano wiadomość „start” , wyślij Z wiadomość „go”
    • otrzymano wiadomość true , wyślij Z wiadomość „go”
    • otrzymano komunikat fałsz , nie rób nic
  • 0 Aktor Z jest tworzony z następującym zachowaniem, które początkowo ma liczbę n :
    • pojawi się komunikat „start” , nie rób nic.
    • otrzymano wiadomość „stop” , wyślij Y wiadomość false i wyślij wydrukuj wiadomość count n .
    • Jeśli wiadomość „go” zostanie odebrana, wyślij Y wiadomość true i przetwórz następną odebraną wiadomość z liczbą n wynoszącą n+1 .

Zgodnie z prawami semantyki Aktora, powyższy system Aktorów zawsze się zatrzymuje, gdy Aktorzy X , Y , to Z otrzymują wiadomość „start”, co skutkuje wysłaniem print liczby, która może być nieograniczona duża.

Różnica między programem CSP a systemem Actor polega na tym, że Actor Z nie otrzymuje komunikatów za pomocą polecenia strzeżonego wyboru z wielu kanałów. Zamiast tego przetwarza komunikaty w kolejności przybycia, a zgodnie z prawami dotyczącymi systemów Actor, zatrzymania jest gwarantowany.

Livelock na pobieranie z wielu kanałów

Rozważmy następujący program napisany w CSP [Hoare 1978]:

[Licytant1 :: b: oferta; *[Oferty1?b → proces1!b; [] Oferty2?b → proces1!b;] || Licytant2 :: b: oferta; *[Oferty1?b → proces2!b; [] Oferty2?b → proces2!b;] ]

Jak wskazano w Knabe [1992], problem z powyższym protokołem ( Prosty protokół rozproszony ) polega na tym, że proces Bidder2 może nigdy nie zaakceptować oferty Bid1 lub Bid2 (zjawisko zwane livelock ), a w konsekwencji proces2 może nigdy nie zostać wysłany. Każda próba przyjęcia wiadomości Licytującego 2 , ponieważ oferta złożona przez Licytację1 lub Licytację2 jest zabierana przez Licytant1 , ponieważ okazuje się, że Licytant1 ma znacznie szybszy dostęp do Licytacji1 i Licyt2 niż Licytant2 . W rezultacie Licytant 1 może zaakceptować ofertę, przetworzyć ją i zaakceptować inną ofertę, zanim Licytant 2 będzie mógł zobowiązać się do przyjęcia oferty.

Efektywność

Jak wskazano w Knabe [1992], problemem związanym z powyższym protokołem ( Prosty protokół rozproszony ) jest duża liczba komunikatów, które muszą zostać wysłane w celu przeprowadzenia uzgadniania w celu wysłania wiadomości przez kanał synchroniczny. Rzeczywiście, jak pokazano w poprzedniej sekcji ( Livelock ), liczba komunikacji może być nieograniczona.

Podsumowanie problemów

Powyższe podrozdziały wyartykułowały następujące trzy kwestie związane z wykorzystaniem kanałów synchronicznych do rachunków procesowych:

  1. Głód. Korzystanie z kanałów synchronicznych może powodować głód, gdy proces próbuje uzyskać komunikaty z wielu kanałów w poleceniu wyboru strzeżonego.
  2. Blokada życia. Użycie kanałów synchronicznych może spowodować, że proces zostanie zatrzymany podczas próby pobrania komunikatów z wielu kanałów w poleceniu wyboru chronionego.
  3. Efektywność. Korzystanie z kanałów synchronicznych może wymagać dużej liczby połączeń w celu odebrania komunikatów z wielu kanałów w poleceniu wyboru chronionego.

Należy zauważyć, że we wszystkich powyższych przypadkach problemy wynikają z użycia polecenia strzeżonego wyboru w celu uzyskania wiadomości z wielu kanałów.

Kanały asynchroniczne

Kanały asynchroniczne mają tę właściwość, że nadawca umieszczający wiadomość w kanale nie musi czekać, aż odbiorca pobierze wiadomość z kanału.

Proste kanały asynchroniczne

Kanał asynchroniczny może być modelowany przez aktora, który odbiera komunikację typu put i get . Poniżej przedstawiono zachowanie aktora dla prostego kanału asynchronicznego:

  • Każda wysłana komunikacja ma wiadomość i adres, na który natychmiast wysyłane jest potwierdzenie (bez czekania na odebranie wiadomości przez komunikację get ).
  • Każda komunikacja get ma adres, na który wysyłana jest otrzymana wiadomość.

Kanały asynchroniczne w rachunku procesowym

Język programowania Join-calculus (opublikowany w 1996 r.) Zaimplementował lokalne i rozproszone obliczenia współbieżne. Zawierał kanały asynchroniczne, a także rodzaj kanału synchronicznego, który jest używany do wywołań procedur. Rachunek Aπ Actor Agha ( Agha i Thati 2004 ) jest oparty na maszynowej wersji asynchronicznego rachunku π .

algebry

Zastosowanie technik algebraicznych było pionierem w rachunku procesowym. Następnie w ( Gaspari i Zavattaro 1997 ), ( Gaspari i Zavattaro 1999 ), ( Agha i Thati 2004 ) opracowano kilka różnych rachunków procesowych, które miały zapewnić algebraiczne rozumowanie dotyczące systemów aktora .

Semantyka denotacyjna

Will Clinger (opierając się na pracach Irene Greif [1975], Gordona Plotkina [1976], Henry'ego Bakera [1978], Michaela Smytha [1978] i Franceza, Hoare'a , Lehmanna i de Roevera [1979]) opublikował pierwszą zadowalającą matematyczna teoria denotacyjna modelu aktora wykorzystująca teorię domen w swojej rozprawie w 1981 r. Jego semantyka przeciwstawiała nieograniczonemu niedeterminizmowi modelu aktora ograniczonemu niedeterminizmowi CSP [Hoare 1978] i procesów współbieżnych [Milne i Milner 1979] (patrz semantyka denotacyjna ) . Roscoe [2005] opracował semantykę denotacyjną z nieograniczonym niedeterminizmem dla kolejnej wersji Communicating Sequential Processes Hoare [1985]. Niedawno Carl Hewitt [2006b] opracował semantykę denotacyjną dla aktorów opartą na diagramach czasowych .

Ugo Montanari i Carolyn Talcott [1998] przyczynili się do próby pogodzenia Aktorów z rachunkiem procesowym.

  • Carla Hewitta, Petera Bishopa i Richarda Steigera. Uniwersalny modułowy formalizm aktora dla sztucznej inteligencji IJCAI 1973.
  • Robina Milnera. Procesy: model matematyczny agentów obliczeniowych w Logic Colloquium 1973.
  • Irene Greif i Carla Hewitta. Semantyka aktora PLANNER-73 Konferencja Zapis sympozjum ACM na temat zasad języków programowania. styczeń 1975.
  • Irena Greif. Semantyka komunikowania procesów równoległych Rozprawa doktorska MIT EECS. sierpień 1975.
  • Gordona Plotkina. Budowa powerdomain SIAM Journal on Computing, wrzesień 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.
  • Gillesa Kahna i Davida MacQueena. Współprogramy i sieci procesów równoległych IFIP. 1977
  • Aki Yonezawa Techniki specyfikacji i weryfikacji programów równoległych oparte na semantyce przekazywania wiadomości Rozprawa doktorska MIT EECS. grudzień 1977.
  • Michał Smyth. Domeny mocy Journal of Computer and System Sciences . 1978.
  • George'a Milne'a i Robina Milnera . Procesy współbieżne i ich składnia JACM. kwiecień 1979.
  • SAMOCHÓD Hoare . Komunikacja sekwencyjnych procesów CACM. sierpień 1978.
  • Nissim Francez, CAR Hoare , Daniel Lehmann i Willem de Roever. Semantyka niedeterminizmu, współbieżności i komunikacji Journal of Computer and System Sciences . grudzień 1979.
  • Mathew Hennessy'ego i Robina Milnera. O obserwowaniu niedeterminizmu i współbieżności LNCS 85. 1980.
  • Willa Clingera. Podstawy semantyki aktora Rozprawa doktorska z matematyki MIT . czerwiec 1981.
  • Mateusz Hennessy. Model termiczny dla procesów synchronicznych Wydział Informatyki Uniwersytetu w Edynburgu. CSR-77-81. 1981.
  • JA Bergstra i JW Klop. Algebra procesów dla komunikacji synchronicznej Informacji i Sterowania. 1984.
  • Luca Cardelli. Model implementacji komunikacji rendezvous Seminarium na temat współbieżności. Notatki z wykładów z informatyki 197. Springer-Verlag. 1985
  • Roberta van Glabbeka. Ograniczony niedeterminizm i zasada indukcji aproksymacji w algebrze procesów Sympozjum na temat teoretycznych aspektów informatyki na temat STACS 1987.
  • K. Mani Chandy i Jayadev Misra. Projekt programu równoległego: Fundacja Addison-Wesley 1988.
  • Robina Milnera, Joachima Parrowa i Davida Walkera. Rachunek procesów mobilnych Wydział Informatyki Edynburg. Raporty ECS-LFCS-89-85 i ECS-LFCS-89-86. Czerwiec 1989. Poprawione odpowiednio we wrześniu 1990 i październiku 1990.
  • Robina Milnera. The Polyadic pi-Calculus: A Tutorial Edinburgh University. Raport LFCS ECS-LFCS-91-180. 1991.
  • Kohei Honda i Mario Tokoro. Rachunek obiektowy dla komunikacji asynchronicznej ECOOP 91.
  • José Meseguer. Warunkowe przepisywanie logiki jako ujednolicony model współbieżności w wybranych artykułach z Drugich Warsztatów Współbieżności i kompozycyjności. 1992.
  • Fryderyka Knabe. Rozproszony protokół komunikacji opartej na kanałach z wyborem PARLE 1992.
  • Geoffa Barretta. Podręcznik referencyjny Occam 3 INMOS. 1992.
  • Benjamin Pierce, Didier Rémy i David Turner. Typowany język programowania wyższego rzędu oparty na warsztacie pi-calculus na temat teorii typów i jej zastosowania w systemach komputerowych. Uniwersytet w Kioto. lipiec 1993.
  • Milner, Robin (styczeń 1993), „Elementy interakcji: wykład z nagrodą Turinga”, Communications of the ACM , CACM, 36 : 78–89, doi : 10.1145/151233.151240 .
  • R. Amadio i S. Prasad. Lokalizacje i awarie Konferencja Podstawy technologii oprogramowania i informatyki teoretycznej. 1994.
  • Cedrica Fourneta i Georgesa Gonthiera. Refleksyjna abstrakcyjna maszyna chemiczna i rachunek łączenia POPL 1996.
  • Cédric Fournet, Georges Gonthier, Jean-Jacques Lévy, Luc Maranget i Didier Rémy. Rachunek agentów mobilnych CONCUR 1996.
  • Tatsurou Sekiguchi i Akinori Yonezawa . Rachunek z mobilnością kodu FMOODS 1997.
  • Gaspari, Mauro; Zavattaro, Gianluigi (maj 1997), Algebra aktorów (raport techniczny), Uniwersytet Boloński
  • Luca Cardelli i Andrew Gordon (1998), Maurice Nivat (red.), „Mobile Ambients”, Foundations of Software Science and Computational Structures , Notatki z wykładów z informatyki, Springer, 1378
  • Ugo Montanari i Carolyn Talcott. Czy aktorzy i agenci Pi mogą żyć razem? Notatki elektroniczne w informatyce teoretycznej . 1998.
  • Robina Milnera. Systemy komunikacyjne i mobilne: Pi-Calculus Cambridge University Press. 1999.
  •   M. Gaspari i G. Zavattaro (1999), „An Algebra of Actors”, Formalne metody systemów otwartych obiektów : 3–18, doi : 10.1007 / 978-0-387-35562-7_2 , ISBN 978-1-4757 -5266-3
  • Davide Sangiorgi i David Walker. Pi-Calculus: teoria procesów mobilnych Cambridge University Press. 2001.
  • P. Thati, R. Ziaei i G. Agha. Teoria majowego testowania rachunków asynchronicznych z lokalizacją i bez nazwy pasującej do metodologii algebraicznej i technologii oprogramowania. Springer Verlag. Wrzesień 2002. LNCS 2422.
  • Gul Agha i Prasanna Thati (2004), „Algebraiczna teoria aktorów i jej zastosowanie do prostego języka obiektowego” (PDF) , OO to FM (Dahl Festschrift) LNCS , Springer-Verlag, 2635 , zarchiwizowane z oryginału ( PDF) w dniu 2004-04-20 , pobrane 2005-12-15
  • JCM Baeten, T. Basten i MA Reniers. Algebra procesów komunikacyjnych Cambridge University Press. 2005.
  • He Jifeng i CAR Hoare. Linking Theories of Concurrency Międzynarodowy Instytut Technologii Oprogramowania Uniwersytetu Narodów Zjednoczonych Raport UNU-IIST nr 328. Lipiec 2005 r.
  • Luca Aceto i Andrew D. Gordon (redaktorzy). Obliczenia procesów algebraicznych: pierwsze dwadzieścia pięć lat i więcej algebry procesów . Bertinoro, Forl`ı, Włochy, 1–5 sierpnia 2005.
  •   Roscoe, AW (2005), Teoria i praktyka współbieżności , Prentice Hall , ISBN 978-0-13-674409-2
  • Carl Hewitt (2006b) Czym jest zaangażowanie? Fizyczne, organizacyjne i społeczne COIN@AAMAS. 2006.