Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
В теоретической информатике теория акторной модели рассматривает теоретические аспекты акторной модели. Акторы — это базовые элементы, составляющие основу акторной модели параллельных цифровых вычислений. В ответ на полученное сообщение актор может принимать локальные решения, создавать новых акторов, отправлять сообщения и определять способ обработки следующего полученного сообщения. Теория акторной модели включает в себя теории событий и структур акторных вычислений, их теорию доказательств и денотационные модели.
In theoretical computer science, Actor model theory concerns theoretical issues for the Actor model. Actors are the primitives that form the basis of the Actor model of concurrent digital computation. In response to a message that it receives, an Actor can make local decisions, create more Actors, send more messages, and designate how to respond to the next message received. Actor model theory incorporates theories of the events and structures of Actor computations, their proof theory, and denotational models.
События и их последовательность
Из определения Актора следует, что происходит множество событий: локальные решения, создание Актора, отправка сообщений, получение сообщений и определение способа реагирования на следующее полученное сообщение. Однако в данной статье мы сосредоточимся исключительно на событиях, связанных с получением сообщения, отправленного Актору. В статье представлены результаты, опубликованные в Hewitt [2006]. Закон счетности: количество событий не превышает счетного множества.
From the definition of an Actor, it can be seen that numerous events take place: local decisions, creating Actors, sending messages, receiving messages, and designating how to respond to the next message received. However, this article focuses on just those events that are the arrival of a message sent to an Actor. This article reports on the results published in Hewitt [2006]. Law of Countability: There are at most countably many events.
Приказ активации
Порядок активации (≈→) — это фундаментальный порядок, моделирующий активацию одного события другим (передача сообщения от события к активируемому им событию должна сопровождаться потоком энергии). Благодаря передаче энергии, порядок активации релятивистски инвариантен; то есть, для любых событий e1 и e2, если e1 ≈→ e2, то время события e1 предшествует времени события e2 во всех релятивистских системах отсчета наблюдателей. Закон строгой причинности для порядка активации: ни для какого события e не выполняется e ≈→ e. Закон конечного предшествия в порядке активации: для любого события e1 множество {e | e ≈→ e1} конечно.
The activation ordering ( ≈→) is a fundamental ordering that models one event activating another (there must be energy flow in the message passing from an event to an event which it activates). Because of the transmission of energy, the activation ordering is relativistically invariant; that is, for all events e1. e2, if e1 ≈→ e2, then the time of e1 precedes the time of e2 in the relativistic frames of reference of all observers. Law of Strict Causality for the Activation Ordering: For no event does e ≈→ e.
Law of Finite Predecession in the Activation Ordering: For all events e1 the set {e|e ≈→ e1} is finite.
Прибытие заказов
Порядок прибытия актора x (x→) моделирует (полный) порядок событий, в которых сообщение приходит в актор x. Порядок прибытия определяется арбитражем при обработке сообщений (часто с использованием цифровой схемы, называемой арбитром). События прибытия актора лежат на его мировой линии. Порядок прибытия означает, что модель акторов по своей сути обладает недетерминированностью (см. Недетерминированность в параллельных вычислениях). Поскольку все события порядка прибытия актора x происходят на мировой линии x, порядок прибытия актора является релятивистски инвариантным. То есть, для всех акторов x и событий e1, e2, если e1 x→ e2, то время события e1 предшествует времени события e2 во всех релятивистских системах отсчета наблюдателей. Закон конечного предшествования в порядке прибытия: для всех событий e1 и акторов x множество {e | e x→ e1} конечно.
The arrival ordering of an Actor x ( x→ ) models the (total) ordering of events in which a message arrives at x. Arrival ordering is determined by arbitration in processing messages (often making use of a digital circuit called an arbiter). The arrival events of an Actor are on its world line. The arrival ordering means that the Actor model inherently has indeterminacy (see Indeterminacy in concurrent computation). Because all of the events of the arrival ordering of an actor x happen on the world line of x, the arrival ordering of an actor is relativistically invariant. I. e., for all actors x and events e1. e2, if e1 x→ e2, then the time of e1 precedes the time of e2 in the relativistic frames of reference of all observers. Law of Finite Predecession in Arrival Orderings: For all events e1 and Actors x the set {e|e x→ e1} is finite.
Денотационная семантика
Клингер [1981] использовал модель событий Actor, описанную выше, для построения денотационной модели акторов с использованием силовых областей. Впоследствии Хьюитт [2006] расширил диаграммы, добавив время поступления сообщений, чтобы создать технически более простую и понятную денотационную модель.
Clinger [1981] used the Actor event model described above to construct a denotational model for Actors using power domains. Subsequently Hewitt [2006] augmented the diagrams with arrival times to construct a technically simpler denotational model that is easier to understand.