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

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

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

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

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

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

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

Закон счетности: Существует не более чем счетное количество событий.

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

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

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

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

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

• Потому что все события по приезду актера Икс случиться на мировой линии Икс, порядок прибытия актера релятивистски инвариантный. Т.е., для всех актеров Икс и события е1.е2, если е1 -x → e2, то время е1 предшествует времени е2 в релятивистских системах отсчета всех наблюдателей.
• Закон конечной прецессии в порядках прибытия: Для всех событий е1 и актеры Икс набор {e | e -x → e1} конечно.

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

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

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

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

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

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

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

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

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

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

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

1. Создать нового актера Приветствующий₁ которому отправлено сообщение Сказать привет с адресом Приветствующий₁
2. послать Исходный сообщение Опять таки с адресом Приветствующий₁

После этого поведение Исходный выглядит следующим образом при получении Опять таки сообщение с адресом Приветствующий_я (которое мы назовем событием Опять такия):

1. Создать нового актера Приветствующий_{я + 1} которому отправлено сообщение Сказать привет с адресом Приветствующий_я
2. послать Исходный сообщение Опять таки с адресом Приветствующий_{я + 1}

Очевидно, что вычисление Исходный посылая себя Опять таки сообщения никогда не заканчиваются.

Поведение каждого актера Приветствующий_я как следует:

• Когда он получает сообщение Сказать привет с адресом Приветствующий_я-1 (которое мы назовем событием Сказать приветя), он отправляет Привет сообщение Приветствующий_я-1
• Когда он получает Привет сообщение (которое мы будем называть событием Приветя), ничего не делает.

Теперь возможно, что Приветя -Приветствующийя→ Сказать приветя каждый раз и поэтому Приветя→Сказать приветя.

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

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

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

Опять таки1→...→Опять такия→...${\displaystyle \infty }$...→Приветя→Сказать приветя→...→Привет1→Сказать привет1

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

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

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

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

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

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

Закон дискретности исключает Машины Zeno и связан с результатами на Сети Петри [Лучший и другие. 1984, 1987].

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

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

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

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

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

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

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