Teorie modelu herce - Actor model theory

v teoretická informatika, Teorie modelu herce se týká teoretických otázek pro Herecký model.

Herci jsou primitiva, která tvoří základ hereckého modelu souběžného digitálního výpočtu. V reakci na zprávu, kterou obdrží, může herec provést místní rozhodnutí, vytvořit více aktérů, odeslat více zpráv a určit, jak reagovat na další přijatou zprávu. Teorie modelu herce zahrnuje teorie událostí a struktur hercových výpočtů, jejich teorii důkazů a denotační modely.

Události a jejich uspořádání

Z definice herce je vidět, že dochází k mnoha událostem: místní rozhodnutí, vytváření aktérů, odesílání zpráv, přijímání zpráv a určování, jak reagovat na další přijatou zprávu.

Tento článek se však zaměřuje pouze na ty události, které jsou příchodem zprávy odeslané herci.

Tento článek podává zprávu o výsledcích publikovaných v Hewitt [2006].

Zákon spočitatelnosti: Událostí je nanejvýš spočetně mnoho.

Aktivační objednávání

Objednávka aktivace (-≈→) je základní uspořádání, které modeluje jednu událost aktivující druhou (ve zprávě musí být tok energie, který přechází z události na událost, kterou aktivuje).

Kvůli přenosu energie je pořadí aktivace relativisticky neměnný; to znamená pro všechny události E₁.E₂, pokud E₁ -≈ → e₂, pak čas E₁ předchází čas E₂ v relativistické referenční rámce všech pozorovatelů.
Zákon přísné kauzality pro objednávání aktivace: Pro žádnou událost e -≈ → e.
Zákon konečných předchůdců v objednávce aktivace: Pro všechny události E₁ sada {e | e -≈ → e₁} je konečný.

Objednávky příjezdu

Objednávka příjezdu herce X ( -x → ) modeluje (celkové) řazení událostí, ve kterých zpráva dorazí X. Pořadí příjezdu je určeno arbitráž při zpracování zpráv (často využívající digitální obvod zvaný rozhodce ). Události příjezdu herce jsou na něm světová linie. Pořadí příjezdu znamená, že aktorský model má ve své podstatě neurčitost (viz Neurčitost při souběžném výpočtu ).

Protože všechny události z příjezdu objednání herce X se stalo na světové linii X, objednávka příjezdu herce je relativisticky neměnný. Tj., pro všechny herce X a události E₁.E₂, pokud E₁ -x → e₂, pak čas E₁ předchází čas E₂ v relativistických referenčních rámcích všech pozorovatelů.
Zákon konečných předchůdců v příchozích objednávkách: Pro všechny události E₁ a herci X sada {e | e -x → e₁} je konečný.

Kombinované objednávání

Kombinované řazení (označeno →) je definován jako přechodné uzavření aktivačních objednávek a objednávek příjezdů všech Herců.

Kombinované uspořádání je relativisticky neměnné, protože se jedná o přechodné uzavření relativisticky neměnných uspořádání. Tj., pro všechny události E₁.E₂, pokud E₁→ e₂. pak čas E₁ předchází čas E₂ v relativistických referenčních rámcích všech pozorovatelů.
Zákon přísné příčinné souvislosti pro kombinované objednávání: Pro žádnou událost e → e.

Kombinované uspořádání je zjevně tranzitivní podle definice.

V [Baker a Hewitt 197?] Se předpokládalo, že výše uvedené zákony mohou zahrnovat následující zákon:

Zákon konečných řetězců mezi událostmi v kombinovaném řazení: Neexistují žádné nekonečné řetězce (tj., lineárně uspořádané množiny) událostí mezi dvěma událostmi v kombinovaném pořadí →.

Nezávislost zákona konečných řetězců mezi událostmi v kombinovaném řazení

[Clinger 1981] však překvapivě dokázal, že zákon konečných řetězců mezi událostmi v kombinovaném pořadí je nezávislý na předchozích zákonech, tj.,

Teorém. Zákon konečných řetězců mezi událostmi v kombinovaném řazení nevyplývá z dříve uvedených zákonů.

Důkaz. Stačí ukázat, že existuje výpočet herce, který splňuje dříve uvedené zákony, ale porušuje zákon konečných řetězců mezi událostmi v kombinovaném řazení.

Zvažte výpočet, který začíná, když herec Počáteční je odeslán Start zpráva způsobující, že provede následující akce

Vytvořte nového herce Greeter₁ kterému je zpráva odeslána Řekni Ahoj s adresou Greeter₁
Poslat Počáteční zpráva Znovu s adresou Greeter₁

Poté chování Počáteční po obdržení Znovu zpráva s adresou Greeter_i (kterou budeme nazývat událost Znovu_i):

Vytvořte nového herce Greeter_{i + 1} kterému je zpráva odeslána Řekni Ahoj s adresou Greeter_i
Poslat Počáteční zpráva Znovu s adresou Greeter_{i + 1}

Je zřejmé, že výpočet Počáteční posílá se Znovu zprávy nikdy nekončí.

Chování každého herce Greeter_i je následující:

Když přijme zprávu Řekni Ahoj s adresou Greeter_i-1 (kterou budeme nazývat událost Řekni Ahoj_i), pošle a Ahoj zpráva pro Greeter_i-1
Když obdrží Ahoj zpráva (kterou budeme nazývat událost Ahoj_i), nic nedělá.

Nyní je možné, že Ahoj_i -Greeter_i→ Řekni Ahoj_i pokaždé, a proto Ahoj_i→Řekni Ahoj_i.

Taky Znovu_i -≈→ Znovu_{i + 1} pokaždé, a proto Znovu_i → Znovu_{i + 1}.

Kromě toho jsou splněny všechny zákony uvedené před zákonem přísné příčinné souvislosti pro kombinované objednávání.

V kombinovaném pořadí však může být nekonečné množství událostí Znovu₁ a Řekni Ahoj₁ jak následuje:

Znovu₁→...→Znovu_i→... ${ displaystyle infty}$ ...→Ahoj_i→Řekni Ahoj_i→...→Ahoj₁→Řekni Ahoj₁

Z fyziky však víme, že nekonečnou energii nelze vynaložit po konečné trajektorii. Vzhledem k tomu, že aktorský model je založen na fyzice, byl zákon axiálních řetězců mezi událostmi v kombinovaném pořadí považován za axiom aktorského modelu.

Zákon diskrétnosti

Zákon konečných řetězců mezi událostmi v kombinovaném řazení úzce souvisí s následujícím zákonem:

Zákon diskrétnosti: Pro všechny události E₁ a E₂, sada {e | e₁→ e → e₂} je konečný.

Ve skutečnosti se předchozí dva zákony ukázaly jako rovnocenné:

Věta [Clinger 1981]. Zákon diskrétnosti je ekvivalentní zákonu konečných řetězců mezi událostmi v kombinovaném řazení (bez použití axiomu výběru.)

Zákon diskrétnosti vylučuje Zeno stroje a souvisí s výsledky na Petriho sítě [Nejlepší et al. 1984, 1987].

Zákon diskrétnosti implikuje vlastnictví neomezený nedeterminismus. Kombinované řazení používá [Clinger 1981] při konstrukci denotačního modelu herců (viz denotační sémantika ).

Denotační sémantika

Clinger [1981] použil výše popsaný model události Actor ke konstrukci a denotační model pro herce využívající mocenské domény. Hewitt [2006] následně rozšířil diagramy o časy příjezdu, aby vytvořil a technicky jednodušší denotační model to je snazší pochopit.

Viz také

Reference

Carl Hewitt, et al. Indukce a meta hodnocení herce Záznam z konference ACM Symposium on Principles of Programming Languages, leden 1974.
Irene Greif. Sémantika komunikace paralelních procesů Disertační práce MIT EECS. Srpna 1975.
Edsger Dijkstra. Disciplína programování Prentice Hall. 1976.
Carl Hewitt a Henry Baker Herci a spojité funkce Pokračování pracovní konference IFIP o formálním popisu koncepcí programování. 1. - 5. srpna 1977.
Henry Baker a Carl Hewitt Inkrementální sběr odpadků procesů Sborník ze sympozia o programovacích jazycích umělé inteligence. SIGPLAN Notices 12, August 1977.
Carl Hewitt a Henry Baker Zákony pro komunikaci paralelních procesů IFIP-77, srpen 1977.
Aki Yonezawa Specifikace a ověřovací techniky pro paralelní programy založené na sémantice předávání zpráv Disertační práce MIT EECS. Prosince 1977.
Peter Bishop Modulárně rozšiřitelné počítačové systémy s velmi velkým adresním prostorem Disertační práce MIT EECS. Červen 1977.
Carl Hewitt. Prohlížení řídicích struktur jako vzorů předávání zpráv Journal of Artificial Intelligence. Červen 1977.
Henry Baker. Herecké systémy pro výpočet v reálném čase Disertační práce MIT EECS. Leden 1978.
Carl Hewitt a Russ Atkinson. Specifikace a zkušební techniky pro serializátory IEEE Journal on Software Engineering. Leden 1979.
Carl Hewitt, Beppe Attardi a Henry Lieberman. Delegování při předávání zpráv Sborník z první mezinárodní konference o distribuovaných systémech Huntsville, AL. Říjen 1979.
Russ Atkinson. Automatické ověřování serializátorů Disertační práce MIT. Červen 1980.
Bill Kornfeld a Carl Hewitt. Metafora vědecké komunity Transakce IEEE na systémech, člověku a kybernetice. Leden 1981.
Gerry Barber. Důvod ke změně ve znalostních kancelářských systémech Disertační práce MIT EECS. Srpna 1981.
Bill Kornfeld. Rovnoběžnost při řešení problémů Disertační práce MIT EECS. Srpna 1981.
Will Clinger. Základy herecké sémantiky Doktorská disertační práce z matematiky MIT. Červen 1981.
Jako nejlepší. Souběžné chování: sekvence, procesy a axiomy Přednášky v informatice Vol.197 1984.
Gul Agha. Herci: Model souběžného výpočtu v distribuovaných systémech Disertační práce. 1986.
Eike Best a R. Devillers. Sekvenční a souběžné chování v teorii Petriho sítě Theoretical Computer Science Vol.55 / 1. 1987.
Gul Agha, Ian Mason, Scott Smith a Carolyn Talcott. Nadace pro výpočet herců Journal of Functional Programming, leden 1993.
Satoshi Matsuoka a Akinori Yonezawa. Analýza dědičných anomálií v objektově orientovaných souběžných programovacích jazycích v Výzkum směrů v souběžném objektově orientovaném programování. 1993.
Jayadev Misra. Logika pro souběžné programování: Bezpečnost Journal of Computer Software Engineering. 1995.
Luca de Alfaro, Zohar Manna, Henry Sipma a Tomás Uribe. Vizuální ověření reaktivních systémů TACAS 1997.
Thati, Prasanna, Carolyn Talcott a Gul Agha. Techniky provádění a zdůvodňování specifikačních diagramů Mezinárodní konference o algebraické metodice a softwarové technologii (AMAST), 2004.
Giuseppe Milicia a Vladimiro Sassone. Anomálie dědičnosti: deset let poté Proceedings of the ACM Symposium on Applied Computing (SAC) 2004, Nicosia, Kypr, 14. – 17. Března 2004.
Petrus Potgieter. Zeno stroje a hyperpočítání 2005
Carl Hewitt Co je to závazek? Fyzický, organizační a sociální COINS @ AAMAS. 2006.