Актер модельдерінің теориясы - Actor model theory

Жылы теориялық информатика, Актер модельдерінің теориясы үшін теориялық мәселелерге қатысты Актер моделі.

Актерлер - бұл параллельді цифрлық есептеудің Actor моделінің негізін қалайтын примитивтер. Хабарламаға жауап ретінде актер жергілікті шешімдер қабылдай алады, көптеген актерлер құра алады, көбірек хабарламалар жібере алады және келесі алынған хабарламаға қалай жауап беру керектігін белгілей алады. Актер модельдерінің теориясы оқиғалар мен актерлерді есептеу құрылымдары, оларды дәлелдеу теориясы және денотациялық модельдер.

Іс-шаралар және олардың тапсырыстары

Актер анықтамасынан көптеген оқиғалардың орын алатынын көруге болады: жергілікті шешімдер, актерлер құру, хабарламалар жіберу, хабарламалар қабылдау және келесі алынған хабарламаға қалай жауап беру керектігін белгілеу.

Алайда, бұл мақалада актерге жіберілген хабарламаның келуіне байланысты оқиғаларға ғана назар аударылады.

Бұл мақалада Hewitt-те жарияланған нәтижелер туралы баяндалады [2006].

Есептілік заңы: Ең көп іс-шаралар бар.

Активтендіруге тапсырыс беру

Қосылуға тапсырыс беру (-≈→) - бұл бір оқиғаны екіншісін белсендіретін модельдеудің негізгі реті (оқиғадан ол іске қосатын оқиғаға хабарламада энергия ағыны болуы керек).

  • Энергия берілетіндіктен, активацияға тапсырыс беру керек релятивистік тұрғыдан өзгермейтін; яғни барлық іс-шараларға арналған e1.e2, егер e1 -≈ → e2, содан кейін e1 уақыттан бұрын e2 релятивистік анықтамалық шеңберлер барлық бақылаушылардың.
  • Активтендіруге қатаң себептер заңы: Ешқандай оқиға болмайды e -≈ → e.
  • Белсенділікке тапсырыс берудегі ақырғы алдын-ала заң: Барлық іс-шаралар үшін e1 жиынтық {e | e -≈ → e1} ақырлы.

Келуге тапсырыс

Актердің келуіне тапсырыс х ( -x → ) хабарлама келіп түсетін іс-шаралардың (жалпы) ретін модельдейді х. Келу тәртібі анықталады арбитраж хабарламаларды өңдеу кезінде (көбінесе an деп аталатын цифрлық тізбекті қолдану) төреші ). Актердің келу оқиғалары өз алдына әлемдік желі. Келуге тапсырыс беру - бұл актер моделінің табиғаты бойынша анықталмағандығын білдіреді (қараңыз) Бір уақытта есептеу кезінде анықталмағандық ).

  • Актердің келуіне тапсырыс беру кезіндегі барлық оқиғалар х әлемдік желіде болады х, актердің келуіне тапсырыс релятивистік жағынан өзгермейтін. Яғни, барлық актерлер үшін х және оқиғалар e1.e2, егер e1 -x → e2, содан кейін e1 уақыттан бұрын e2 барлық бақылаушылардың релятивистік анықтамалық шеңберінде.
  • Келу бұйрықтарындағы ақырғы прецедис заңы: Барлық іс-шаралар үшін e1 және актерлер х жиынтық {e | e -x → e1} ақырлы.

Аралас тапсырыс

Аралас тапсырыс (белгіленеді ) деп анықталды өтпелі жабылу барлық актерлерді активтендіру және келу туралы бұйрықтар.

  • Аралас тапсырыс релятивистік тұрғыдан инвариантты, өйткені бұл релятивистік инвариантты бұйрықтардың өтпелі жабылуы. Яғни, барлық іс-шаралар үшін e1.e2, егер e1→ e2. содан кейін e1 уақыттан бұрын e2 барлық бақылаушылардың релятивистік анықтамалық шеңберінде.
  • Аралас бұйрық үшін қатаң себептілік заңы: Ешқандай оқиға болмайды e → e.

Біріктірілген тапсырыс анықтамасы бойынша анық өтпелі болып табылады.

[Бейкер және Хьюитт 197?] Жоғарыда аталған заңдар келесі заңға әкелуі мүмкін деген болжам жасады:

Біріктірілген тәртіптегі оқиғалар арасындағы ақырғы тізбектер заңы: Шексіз тізбектер жоқ (яғни, сызықтық реттелген жиынтықтар) екі реттік оқиғалар арасындағы оқиғалар →.

Біріктірілген тәртіптегі оқиғалар арасындағы ақырғы тізбектер заңының тәуелсіздігі

Алайда, [Клингер 1981] таңқаларлықтай, аралас тәртіптегі оқиғалар арасындағы ақырғы тізбектер заңы алдыңғы заңдарға тәуелсіз, яғни,

Теорема. Біріктірілген тәртіптегі оқиғалар арасындағы ақырғы тізбектер заңы бұрын айтылған заңдардан туындамайды.

Дәлел. Бұрын баяндалған заңдарды қанағаттандыратын, бірақ аралас тәртіптегі оқиғалар арасындағы ақырғы тізбектер заңын бұзатын Актердің есебі бар екенін көрсету жеткілікті.

Актерден басталатын есептеуді қарастырайық Бастапқы жіберіледі Бастау оны келесі әрекеттерді жасауға мәжбүр ететін хабарлама
  1. Жаңа актер жасаңыз Сәлемдеуші1 хабарлама жіберіледі Сәлем мекен-жайы көрсетілген Сәлемдеуші1
  2. Жіберу Бастапқы хабарлама Тағы да мекен-жайы көрсетілген Сәлемдеуші1
Бұдан кейін мінез-құлық Бастапқы алынғаннан кейін келесідей Тағы да мекен-жайы көрсетілген хабарлама Сәлемдеушімен (біз оны шара деп атаймыз Тағы дамен):
  1. Жаңа актер жасаңыз Сәлемдеушіi + 1 хабарлама жіберіледі Сәлем мекен-жайы көрсетілген Сәлемдеушімен
  2. Жіберу Бастапқы хабарлама Тағы да мекен-жайы көрсетілген Сәлемдеушіi + 1
Әрине, есептеу Бастапқы өзін жіберу Тағы да хабарламалар ешқашан тоқтатылмайды.
Әр актердің мінез-құлқы Сәлемдеушімен келесідей:
  • Ол хабарлама алған кезде Сәлем мекен-жайы көрсетілген Сәлемдеушіi-1 (біз оны іс-шара деп атаймыз) Сәлеммен) жібереді Сәлеметсіз бе хабарлама Сәлемдеушіi-1
  • Ол алған кезде Сәлеметсіз бе хабарлама (оны іс-шара деп атаймыз) Сәлеметсіз бемен), ол ештеңе жасамайды.
Енді бұл мүмкін Сәлеметсіз бемен -СәлемдеушіменСәлеммен әр уақытта және сондықтан Сәлеметсіз беменСәлеммен.
Сондай-ақ Тағы дамен -≈→ Тағы даi + 1 әр уақытта және сондықтан Тағы даменТағы даi + 1.
Сонымен қатар, аралас тапсырыс үшін қатаң себептер туралы заңда айтылған барлық заңдар қанағаттандырылады.
Алайда, арасында біріккен тәртіпте оқиғалардың саны шексіз болуы мүмкін Тағы да1 және Сәлем1 келесідей:
Тағы да1→...→Тағы дамен→......→Сәлеметсіз беменСәлеммен→...→Сәлеметсіз бе1Сәлем1

Алайда, біз физикадан шексіз энергияны ақырғы траектория бойынша жұмсауға болмайтынын білеміз. Сондықтан, Актер моделі физикаға негізделгендіктен, Актер моделінің аксиомасы ретінде аралас тәртіптегі оқиғалар арасындағы ақырлы тізбектер заңы қабылданды.

Дискреттілік заңы

Біріктірілген тәртіптегі оқиғалар арасындағы ақырғы тізбектер заңы келесі заңмен тығыз байланысты:

Дискреттілік заңы: Барлық іс-шаралар үшін e1 және e2, жиынтық {e | e1→ e → e2} ақырлы.

Іс жүзінде алдыңғы екі заңның баламалары көрсетілген:

Теорема [Клингер 1981]. Дискреттілік заңы аралас тәртіптегі оқиғалар арасындағы ақырғы тізбектер заңына тең (таңдау аксиомасын қолданбай).

Дискреттілік заңы жоққа шығарылады Zeno машиналары нәтижелерімен байланысты Петри торлары [Ең жақсы т.б. 1984, 1987].

Дискреттілік заңы -ның қасиетін білдіреді шектеусіз нондетерминизм. Біріктірілген тапсырысты [Клингер 1981] актерлердің денотациялық моделін құруда қолданады (қараңыз) денотатикалық семантика ).

Денотатикалық семантика

Клингер [1981] а-ны құру үшін жоғарыда сипатталған Actor оқиғалық моделін пайдаланды қуат домендерін пайдаланатын актерлерге арналған денотатикалық модель. Кейіннен Хьюитт [2006] диаграммаларды а-ны құру үшін келу уақытымен толықтырды техникалық жағынан қарапайым денотациялық модель түсіну оңайырақ.

Сондай-ақ қараңыз

Әдебиеттер тізімі

  • Карл Хьюитт, т.б. Актер индукциясы және мета бағалау Бағдарламалау тілдерінің принциптері бойынша ACM симпозиумының конференция жазбалары, қаңтар 1974 ж.
  • Ирин Грейф. Параллельді процестерді байланыстырудың семантикасы MIT EECS докторлық диссертациясы. 1975 жылдың тамызы.
  • Edsger Dijkstra. Бағдарламалау пәні Prentice Hall. 1976 ж.
  • Карл Хьюитт және Генри Бейкер Актерлер және үздіксіз функционалдар Бағдарламалау тұжырымдамаларын формальды сипаттау бойынша IFIP жұмыс конференциясының жұмысы. 1-5 тамыз 1977 ж.
  • Генри Бейкер және Карл Хьюитт Қоқыстарды көбейту Жасанды интеллект бағдарламалау тілдері бойынша симпозиум материалдары. SIGPLAN хабарламалары 12 тамыз, 1977 ж.
  • Карл Хьюитт және Генри Бейкер Параллельді процестердің байланыс заңдары IFIP-77, 1977 жылғы тамыз.
  • Аки Йонезава Хабарламалық семантикаға негізделген параллель бағдарламаларға арналған спецификация және растау әдістері MIT EECS докторлық диссертациясы. Желтоқсан 1977.
  • Питер епископы Модульдік кеңейтілетін компьютерлік жүйелер MIT EECS докторлық диссертациясы. Маусым 1977.
  • Карл Хьюитт. Хабарламаны жіберудің үлгісі ретінде басқару құрылымын қарау Жасанды интеллект журналы. Маусым 1977.
  • Генри Бейкер. Нақты уақыттағы актерлік жүйелер MIT EECS докторлық диссертациясы. 1978 жылғы қаңтар.
  • Карл Хьюитт пен Расс Аткинсон. Сериализаторларға техникалық сипаттама және дәлелдеу әдістері Бағдарламалық жасақтама бойынша IEEE журналы. 1979 жылғы қаңтар.
  • Карл Хьюитт, Беппе Аттарди және Генри Либерман. Хабарлама жіберу жөніндегі делегация Таратылған жүйелер туралы бірінші халықаралық конференция материалдары, Хантсвилл, АЛ. 1979 ж. Қазан.
  • Расс Аткинсон. Сериализаторларды автоматты түрде тексеру MIT докторлық диссертациясы. Маусым, 1980.
  • Билл Корнфельд пен Карл Хьюитт. Ғылыми қауымдастық метафорасы IEEE жүйелер, адам және кибернетика бойынша транзакциялар. 1981 ж. Қаңтар.
  • Джерри Барбер. Білімді кеңсе жүйелерінің өзгеруі туралы пікірталас MIT EECS докторлық диссертациясы. Тамыз 1981.
  • Билл Корнфелд. Есептер шығарудағы параллелизм MIT EECS докторлық диссертациясы. Тамыз 1981.
  • Уилл Клингер. Актер семантикасының негіздері MIT математика бойынша докторлық диссертация. Маусым 1981.
  • Eike Best. Бір уақытта жүріс-тұрыс: реттіліктер, процестер және аксиомалар Информатикадағы дәріс жазбалары.197 1984 ж.
  • Гүл Ага. Актерлер: Таратылған жүйелерде бір уақытта есептеу моделі Докторлық диссертация. 1986 ж.
  • Eike Best және R.Devillers. Петри Нет теориясындағы дәйекті және қатар жүріс-тұрыс Теориялық информатика Vol.55 / 1. 1987 ж.
  • Гул Ага, Ян Мейсон, Скотт Смит және Кэролин Талкотт. Актерлерді есептеу қоры Функционалды бағдарламалау журналы 1993 ж., Қаңтар.
  • Сатоси Мацуока және Акинори Йонезава. Объектілі-бағытталған параллельді бағдарламалау тілдеріндегі мұрагерлік аномалиясын талдау Бір уақытта объектілі-бағдарлы бағдарламалаудағы зерттеу бағыттары. 1993 ж.
  • Джаядев Мисра. Бір уақытта бағдарламалауға арналған логика: қауіпсіздік Компьютерлік бағдарламалық жасақтама журналы. 1995 ж.
  • Лука де Альфаро, Зохар Манна, Генри Сипма және Томас Урибе. Реактивті жүйелерді визуалды тексеру TACAS 1997 ж.
  • Тати, Прасанна, Кэролин Талкотт және Гүл Аға. Техникалық сипаттама сызбаларын орындау және дәлелдеу әдістері Халықаралық конференция алгебралық әдіснамасы және бағдарламалық қамтамасыз ету технологиясы (AMAST), 2004 ж.
  • Джузеппе Милиция және Владимиро Сассоне. Мұрагерлік аномалиясы: он жылдан кейін 2004 ACM симпозиумының қолданбалы есептеулер (SAC) материалдары, Никозия, Кипр, 14-17 наурыз, 2004 ж.
  • Петрус Потгиетер. Zeno машиналары және гиперкомпьютерлік 2005
  • Карл Хьюитт Міндеттеме дегеніміз не, физикалық, ұйымдастырушылық және әлеуметтік Монеталар @ AAMAS. 2006 ж.