Actor model theory
Encyclopedia
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
.
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].
). 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).
The combined ordering is obviously transitive by definition.
In [Baker and Hewitt 197?], it was conjectured that the above laws might entail the following law:
Theorem. The Law of Finite Chains Between Events in the Combined Ordering does not follow from the previously stated laws.
Proof. It is sufficient to show that there is an Actor computation that satisfies the previously stated laws but violates the Law of Finite Chains Between Events in the Combined Ordering.
However, we know from physics that infinite energy cannot be expended along a finite trajectory (see for example Quantum information and relativity theory). Therefore, since the Actor model is based on physics, the Law of Finite Chains Between Events in the Combined Ordering was taken as an axiom of the Actor model.
In fact the previous two laws have been shown to be equivalent:
The law of discreteness rules out Zeno machine
s and is related to results on Petri net
s [Best et al. 1984, 1987].
The Law of Discreteness implies the property of unbounded nondeterminism
. The combined ordering is used by [Clinger 1981] in the construction of a denotational model of Actors (see denotational semantics
).
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
, Actor model theory concerns theoretical issues for the Actor model
Actor model
In computer science, the Actor model is a mathematical model of concurrent computation that treats "actors" as the universal primitives 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...
.
Actors are the primitives that form the basis of the Actor model
Actor model
In computer science, the Actor model is a mathematical model of concurrent computation that treats "actors" as the universal primitives 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...
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
Denotational semantics of the Actor model
The denotational semantics of the Actor model is the subject of denotational domain theory for Actors. The historical development of this subject is recounted in [Hewitt 2008b].-Actor fixed point semantics:...
.
Events and their orderings
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.
Activation ordering
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 relativisticallyGeneral relativityGeneral relativity or the general theory of relativity is the geometric theory of gravitation published by Albert Einstein in 1916. It is the current description of gravitation in modern physics...
invariantInvariant (physics)In mathematics and theoretical physics, an invariant is a property of a system which remains unchanged under some transformation.-Examples:In the current era, the immobility of polaris under the diurnal motion of the celestial sphere is a classical illustration of physical invariance.Another...
; 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 referenceFrame of referenceA frame of reference in physics, may refer to a coordinate system or set of axes within which to measure the position, orientation, and other properties of objects in it, or it may refer to an observational reference frame tied to the state of motion of an observer.It may also refer to both an...
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.
Arrival orderings
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 arbiterArbiter (electronics)
-Asynchronous arbiters:An important form of arbiter is used in asynchronous circuits, to select the order of access to a shared resource among asynchronous requests. Its function is to prevent two operations from occurring at once when they should not...
). The arrival events of an Actor are on its world line
World line
In physics, the world line of an object is the unique path of that object as it travels through 4-dimensional spacetime. The concept of "world line" is distinguished from the concept of "orbit" or "trajectory" by the time dimension, and typically encompasses a large area of spacetime wherein...
. 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.
Combined ordering
The combined ordering (denoted by →) is defined to be the transitive closure of the activation ordering and the arrival orderings of all Actors.- The combined ordering is relativistically invariant because it is the transitive closure of relativistically invariant orderings. I.e., 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 Combined Ordering: For no event does e→e.
The combined ordering is obviously transitive by definition.
In [Baker and Hewitt 197?], it was conjectured that the above laws might entail the following law:
- Law of Finite Chains Between Events in the Combined Ordering: There are no infinite chains (i.e., linearly ordered sets) of events between two events in the combined ordering →.
Independence of the Law of Finite Chains Between Events in the Combined Ordering
However, [Clinger 1981] surprisingly proved that the Law of Finite Chains Between Events in the Combined Ordering is independent of the previous laws, i.e.,Theorem. The Law of Finite Chains Between Events in the Combined Ordering does not follow from the previously stated laws.
Proof. It is sufficient to show that there is an Actor computation that satisfies the previously stated laws but violates the Law of Finite Chains Between Events in the Combined Ordering.
- Consider a computation which begins when an actor Initial is sent a Start message causing it to take the following actions
- Create a new actor Greeter1 which is sent the message SayHelloTo with the address of Greeter1
- Send Initial the message Again with the address of Greeter1
- Thereafter the behavior of Initial is as follows on receipt of an Again message with address Greeteri (which we will call the event Againi):
- Create a new actor Greeteri+1 which is sent the message SayHelloTo with address Greeteri
- Send Initial the message Again with the address of Greeteri+1
- Obviously the computation of Initial sending itself Again messages never terminates.
- The behavior of each Actor Greeteri is as follows:
- When it receives a message SayHelloTo with address Greeteri-1 (which we will call the event SayHelloToi), it sends a Hello message to Greeteri-1
- When it receives a Hello message (which we will call the event Helloi), it does nothing.
- Now it is possible that Helloi -Greeteri→ SayHelloToi every time and therefore Helloi→SayHelloToi.
- Also Againi -≈→ Againi+1 every time and therefore Againi → Againi+1.
- Furthermore all of the laws stated before the Law of Strict Causality for the Combined Ordering are satisfied.
- However, there may be an infinite number of events in the combined ordering between Again1 and SayHelloTo1 as follows:
- Again1→...→Againi→...
...→Helloi→SayHelloToi→...→Hello1→SayHelloTo1
However, we know from physics that infinite energy cannot be expended along a finite trajectory (see for example Quantum information and relativity theory). Therefore, since the Actor model is based on physics, the Law of Finite Chains Between Events in the Combined Ordering was taken as an axiom of the Actor model.
Law of Discreteness
The Law of Finite Chains Between Events in the Combined Ordering is closely related to the following law:- Law of Discreteness: For all events e1 and e2, the set {e|e1→e→e2} is finite.
In fact the previous two laws have been shown to be equivalent:
- Theorem [Clinger 1981]. The Law of Discreteness is equivalent to the Law of Finite Chains Between Events in the Combined Ordering (without using the axiom of choice.)
The law of discreteness rules out Zeno machine
Zeno machine
In mathematics and computer science, Zeno machines are a hypothetical computational model related to Turing machines that allows a countably infinite number of algorithmic steps to be performed in finite time...
s and is related to results on Petri net
Petri net
A Petri net is one of several mathematical modeling languages for the description of distributed systems. A Petri net is a directed bipartite graph, in which the nodes represent transitions and places...
s [Best et al. 1984, 1987].
The Law of Discreteness implies the property of unbounded nondeterminism
Unbounded nondeterminism
In computer science, unbounded nondeterminism or unbounded indeterminacy is a property of concurrency by which the amount of delay in servicing a request can become unbounded as a result of arbitration of contention for shared resources while still guaranteeing that the request will eventually be...
. The combined ordering is used by [Clinger 1981] in the construction of a denotational model of Actors (see denotational semantics
Denotational semantics
In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
).
Denotational semantics
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.See also
- Actor model early historyActor model early historyIn computer science, the Actor model, first published in 1973 , is a mathematical model of concurrent computation. This article is about the early history of the Actor model...
- Actor model and process calculiActor model and process calculiIn computer science, the Actor model and process calculi are two closely related approaches to the modelling of concurrent digital computation...
- Actor model implementationActor model implementationIn computer science, Actor model implementation concerns implementation issues for the Actor model.-Cosmic Cube:The Cosmic Cube was developed by Chuck Seitz et al. at Caltech providing architectural support for Actor systems...