Теория актерской модели - Actor model theory

В теоретической информатике , теория Actor модели касается теоретических вопросов для модели Actor .

Акторы - это примитивы, которые составляют основу модели параллельных цифровых вычислений акторов. В ответ на сообщение, которое он получает, Актер может принимать локальные решения, создавать больше Актеров, отправлять больше сообщений и определять, как реагировать на следующее полученное сообщение. Теория модели акторов включает в себя теории событий и структур вычислений акторов, их теорию доказательств и денотационные модели .

События и их порядок

Из определения Актера видно, что происходят многочисленные события: локальные решения, создание Актеров, отправка сообщений, получение сообщений и определение того, как реагировать на следующее полученное сообщение.

Тем не менее, эта статья фокусируется только на тех событиях, которые являются прибытием сообщения, отправленного Актеру.

Эта статья сообщает о результатах, опубликованных в Hewitt [2006].

Закон счетности : событий может быть не более чем счет .

Заказ активации

Порядок активации ( -≈→ ) - это фундаментальный порядок, который моделирует одно событие, активирующее другое (в сообщении должен быть поток энергии, передаваемый от события к событию, которое оно активирует).

• Из-за передачи энергии порядок активации релятивистски инвариантен ; то есть на все события . , если , то время предшествует времени в релятивистских системах отсчета всех наблюдателей. e1e2e1 -≈→ e2e1e2
• Закон строгой причинности для порядка активации : ни одно событие не действует e -≈→ e .
• Закон конечного предшественника в порядке активации : для всех событий набор конечен. e1{e|e -≈→ e1}

Заказы на прибытие

Порядок прибытия Actor x ( -x→ ) моделирует (общий) порядок событий, в которых прибывает сообщение x . Порядок прибытия определяется арбитражем при обработке сообщений (часто с использованием цифровой схемы, называемой арбитром ). События прибытия Актера находятся на его мировой линии . Порядок прибытия означает, что модель Актера по своей природе имеет неопределенность (см. Неопределенность в параллельных вычислениях ).

• Поскольку все события порядка прибытия актера x происходят на мировой линии x , порядок прибытия актера релятивистски инвариантен . Т.е. для всех актеров x и событий . , если , то время предшествует времени в релятивистских системах отсчета всех наблюдателей. e1e2e1 -x→ e2e1e2
• Закон конечного предшественника в порядке прибытия : для всех событий и Актеров набор конечен. e1x{e|e -x→ e1}

Комбинированный заказ

Комбинированный порядок (обозначается → ) определяется как транзитивное закрытие порядка активации и порядков прибытия всех участников.

• Комбинированный порядок является релятивистски инвариантным, поскольку он является транзитивным замыканием релятивистски инвариантных порядков. Т.е. при всех событиях . , если . тогда время предшествует времени в релятивистских системах отсчета всех наблюдателей. e1e2e1→e2e1e2
• Закон строгой причинности для комбинированного упорядочивания : ни одно событие не действует e→e .

Комбинированный порядок, очевидно, транзитивен по определению.

В [Baker and Hewitt 197?] Было высказано предположение, что вышеуказанные законы могут повлечь за собой следующий закон:

Закон конечных цепочек между событиями в комбинированном порядке : не существует бесконечных цепочек ( т. Е. Линейно упорядоченных множеств) событий между двумя событиями в комбинированном порядке →.

Независимость закона конечных цепочек между событиями в комбинированном порядке.

Тем не менее, [Clinger 1981] неожиданно оказалось , что закон конечных цепей между событиями в комбинированном Упорядочение не зависит от предыдущих законов, то есть ,

Теорема. Закон конечных цепочек между событиями в комбинированном порядке не следует из ранее изложенных законов.

Доказательство. Достаточно показать, что существует вычисление Актера, которое удовлетворяет ранее указанным законам, но нарушает закон конечных цепочек между событиями в комбинированном порядке.

Рассмотрим вычисление, которое начинается, когда субъекту Initial отправляется Start сообщение, заставляющее его предпринять следующие действия.

1. Создайте нового участника Greeter _1, которому будет отправлено сообщение SayHelloTo с адресом Greeter _1.
2. Отправьте Initial сообщение Again с адресом Greeter ₁

После этого поведение Initial при получении Again сообщения с адресом Greeter _i (которое мы будем называть событием ) выглядит следующим образом : Againi

1. Создайте нового актера Greeter _{i + 1,} которому будет отправлено сообщение SayHelloTo с адресом Greeter _i.
2. Отправьте Initial сообщение Again с адресом Greeter _{i + 1}

Очевидно, что вычисление начальной отправки Again сообщений никогда не прекращается.

Поведение каждого встречающего актера _i следующее:

• Когда он получает сообщение SayHelloTo с адресом Greeter _i-1 (который мы будем называть событием ), он отправляет сообщение

Greeter _i-1.SayHelloToiHello

Когда он получает Hello сообщение (которое мы назовем событием ), он ничего не делает. Helloi

Теперь возможно, что каждый раз и поэтому . Helloi -Greeteri→ SayHelloToiHelloi→SayHelloToi

Также каждый раз и поэтому . Againi -≈→ Againi+1Againi → Againi+1

Кроме того, выполняются все законы, изложенные до Закона строгой причинности для комбинированного упорядочивания.

Однако может быть бесконечное количество событий в объединенном порядке между и следующим образом: Again1SayHelloTo1

Again1→...→Againi→...${\displaystyle \infty }$...→Helloi→SayHelloToi→...→Hello1→SayHelloTo1

Однако мы знаем из физики, что бесконечная энергия не может быть израсходована по конечной траектории. Следовательно, поскольку модель актера основана на физике, закон конечных цепочек между событиями в комбинированном порядке был взят в качестве аксиомы модели актера.

Закон дискретности

Закон конечных цепочек между событиями в комбинированном порядке тесно связан со следующим законом:

Закон дискретности : для всех событий и набор конечен. e1e2{e|e1→e→e2}

Фактически, предыдущие два закона оказались эквивалентными:

Теорема [Clinger 1981]. Закон дискретности эквивалентен закону конечных цепочек между событиями в комбинированном порядке (без использования аксиомы выбора).

Закон дискретности исключает машины Зенона и связан с результатами на сетях Петри [Best et al. 1984, 1987].

Закон дискретности подразумевает свойство неограниченного недетерминизма . Комбинированный порядок используется [Clinger 1981] при построении денотационной модели Актеров (см. Денотационная семантика ).

Денотационная семантика

Клинджер [Clinger, 1981] использовал модель событий Актера, описанную выше, чтобы построить денотационную модель для Актеров, использующих домены власти . Впоследствии Хьюитт [2006] дополнил диаграммы временем прибытия, чтобы построить технически более простую денотационную модель , более легкую для понимания.

Смотрите также

• Актерская модель ранняя история
• Модель актора и расчеты процесса
• Реализация актерской модели

Рекомендации

• Карл Хьюитт и др. Актерский вводный курс и запись конференции по метаоценке симпозиума ACM по принципам языков программирования, январь 1974 г.
• Ирен Грейф. Семантика взаимодействующих параллельных процессов MIT EECS Докторская диссертация. Август 1975 г.
• Эдсгер Дейкстра. Дисциплина программирования Прентис Холл. 1976 г.
• Карл Хьюитт и Генри Бейкер Актеры и непрерывные функционалы Труды Рабочей конференции IFIP по формальному описанию концепций программирования. 1–5 августа 1977 г.
• Генри Бейкер и Карл Хьюитт «Постепенная сборка мусора процессов» Труды симпозиума по языкам программирования с искусственным интеллектом. Уведомления SIGPLAN от 12 августа 1977 г.
• Законы Карла Хьюитта и Генри Бейкера для связи параллельных процессов IFIP-77, август 1977 г.
• Аки Ёнэдзава Методы спецификации и проверки параллельных программ на основе семантики передачи сообщений. Докторская диссертация MIT EECS. Декабрь 1977 г.
• Питер Бишоп. Модульно расширяемые компьютерные системы с очень большим адресным пространством. Докторская диссертация MIT EECS. Июнь 1977 г.
• Карл Хьюитт. Просмотр структур управления как шаблонов передачи сообщений Журнал искусственного интеллекта. Июнь 1977 г.
• Генри Бейкер. Акторские системы для вычислений в реальном времени. Докторская диссертация MIT EECS. Январь 1978 г.
• Карл Хьюитт и Расс Аткинсон. Спецификация и методы проверки сериализаторов Журнал IEEE по разработке программного обеспечения. Январь 1979 г.
• Карл Хьюитт, Беппе Аттарди и Генри Либерман. Делегация в протоколах передачи сообщений Первой международной конференции по распределенным системам Хантсвилл, Алабама. Октябрь 1979 г.
• Расс Аткинсон. Автоматическая проверка сериализаторов. Докторская диссертация Массачусетского технологического института. Июнь 1980 г.
• Билл Корнфельд и Карл Хьюитт. Метафора научного сообщества Транзакции IEEE о системах, человеке и кибернетике. Январь 1981 г.
• Джерри Барбер. Рассуждения об изменениях в хорошо осведомленных офисных системах. Докторская диссертация MIT EECS. Август 1981 г.
• Билл Корнфельд. Параллелизм в решении проблем, докторская диссертация MIT EECS. Август 1981 г.
• Уилл Клингер. Основы актерской семантики Докторская диссертация по математике Массачусетского технологического института. Июнь 1981 г.
• Эйке Бест . Concurrent Behavior: Sequences, Processes and Axioms Lecture Notes in Computer Science Vol.197 1984.
• Гуль Ага. Актеры: модель параллельных вычислений в распределенных системах докторская диссертация. 1986 г.
• Эйке Бест и Р. Девиллерс. Последовательное и одновременное поведение в теории сетей Петри, теоретической информатике, том 55/1. 1987 г.
• Гул Ага, Ян Мейсон, Скотт Смит и Кэролайн Талкотт. Фонд для вычислений актеров, журнал функционального программирования, январь 1993 г.
• Сатоши Мацуока и Акинори Ёнэдзава . Анализ аномалии наследования в объектно-ориентированных языках параллельного программирования по направлениям исследований в параллельном объектно-ориентированном программировании. 1993 г.
• Джаядев Мишра. Логика для параллельного программирования: Журнал безопасности компьютерной программной инженерии. 1995 г.
• Лука де Альфаро, Зохар Манна, Генри Сипма и Томас Урибе. Визуальная проверка реактивных систем TACAS 1997.
• Тати, Прасанна, Кэролайн Талкотт и Гул Ага. Методы выполнения и рассуждения о спецификационных диаграммах Международная конференция по алгебраической методологии и программным технологиям (AMAST), 2004.
• Джузеппе Милиция и Владимиро Сассоне. Аномалия наследования: десять лет спустя после заседаний Симпозиума ACM 2004 г. по прикладным вычислениям (SAC), Никосия, Кипр, 14–17 марта 2004 г.
• Петрус Потгитер. Машины Zeno и гиперкомпьютеры 2005
• Карл Хьюитт Что такое обязательства? Физические, организационные и социальные COINS @ AAMAS. 2006 г.