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

Эта статья требует дополнительных ссылок для проверки . Пожалуйста, помогите улучшить эту статью , добавив цитаты из надежных источников . Материал, не полученный от источника, может быть оспорен и удален.
Найти источники: «Теория моделей актеров» - новости · газеты · книги · ученый · JSTOR ( август 2011 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения )

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

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

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

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

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

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

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

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

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

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

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

Порядок прибытия Actor 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 _1.
Отправьте Initial сообщение Againс адресом Greeter ₁

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

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

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

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

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

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

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

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

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

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

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

Закон дискретности [ править ]

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

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

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

Теорема [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 г.