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

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

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

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

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

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

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

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

Активация заказа

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

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

Прибытие заказов

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1. Создайте нового актера Greeter _i+1 , которому будет отправлено сообщение SayHelloToс адресом Greeter _i
2. Отправить Initial сообщение Againс адресом приветствующего _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}

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

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

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

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

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

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

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

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

Ссылки

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