Теория модели актера

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

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

События и их порядок [ править ]

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

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

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

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

Порядок активации [ править ]

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

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

Заказы по прибытии [ править ]

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

Потому что все события заказа прихода актера x произойти на мировой линии xпорядок прибытия актора релятивистски инвариантен . Т.е. для всех актеров x и события e₁. e₂, если e₁ -x→ e₂, то время e₁ предшествует моменту e₂ в релятивистских системах отсчета всех наблюдателей.
Закон конечного предшествования в порядке прибытия : для всех событий. e₁ и актеры x набор {e|e -x→ e₁} конечно.

Комбинированный заказ [ править ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Поведение каждого актера- приветствия _i выглядит следующим образом:

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

Теперь возможно, что Hello_i -Greeter_i→ SayHelloTo_i каждый раз и поэтому Hello_i→SayHelloTo_i.

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

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

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

Again₁→...→Again_i→... $\infty$ ...→Hello_i→SayHelloTo_i→...→Hello₁→SayHelloTo₁

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

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

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

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

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

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

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

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

Денотационная семантика [ править ]

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

См. также [ править ]

Ссылки [ править ]

Карл Хьюитт и др. Отчет конференции по индукции и метаоценке актеров симпозиума ACM по принципам языков программирования, январь 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 по системам, человеку и кибернетике. Январь 1981 года.
Джерри Барбер. Рассуждения об изменениях в интеллектуальных офисных системах Докторская диссертация MIT EECS. Август 1981 года.
Билл Корнфельд. Параллелизм в решении задач Докторская диссертация MIT EECS. Август 1981 года.
Уилл Клингер. Основы акторной семантики Докторская диссертация по математике Массачусетского технологического института. Июнь 1981 года.
Эйке Бест . Параллельное поведение: последовательности, процессы и аксиомы. Конспект лекций по информатике, том 197, 1984.
Гуль Ага. Актеры: модель параллельных вычислений в распределенных системах Докторская диссертация. 1986.
Эйке Бест и Р.Девиллерс. Последовательное и параллельное поведение в теории сетей Петри Теоретическая информатика Том 55/1. 1987.
Гул Ага, Ян Мейсон, Скотт Смит и Кэролайн Талкотт. Фонда актерских вычислений, январь 1993 г. Журнал функционального программирования
Сатоши Мацуока и Акинори Ёнедзава . Анализ аномалий наследования в объектно-ориентированных параллельных языках программирования по направлениям исследований в области параллельного объектно-ориентированного программирования. 1993.
Джаядев Мишра. Логика параллельного программирования: Журнал безопасности компьютерной разработки программного обеспечения. 1995.
Лука де Альфаро, Зоар Манна, Генри Сипма и Томас Урибе. Визуальная проверка реактивных систем TACAS 1997.
Тати, Прасанна, Кэролайн Талкотт и Гул Ага. Методы выполнения и рассуждения о диаграммах спецификаций. Международная конференция по алгебраической методологии и технологиям программного обеспечения (AMAST), 2004 г.
Джузеппе Милича и Владимиро Сассоне. Аномалия наследования: десять лет после материалов симпозиума ACM по прикладным вычислениям (SAC) 2004 г., Никосия, Кипр, 14–17 марта 2004 г.
Петрус Потгитер. Машины Зенона и гиперкомпьютеры 2005 г.
Карл Хьюитт Что такое приверженность? Физические, организационные и социальные COINS@AAMAS. 2006.