Jump to content

Actor model theory: Difference between revisions

From Wikipedia, the free encyclopedia
Content deleted Content added
m References: Doubled reference.
Rz98 (talk | contribs)
m wikilink
 
(26 intermediate revisions by 23 users not shown)
Line 1: Line 1:
{{Refimprove|date=August 2011}}
In [[theoretical computer science]], '''Actor model theory''' concerns theoretical issues for the [[Actor model]].
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 semantics|denotational models]].
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 semantics of the Actor model|denotational models]].


==Events and their orderings==
==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.
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.
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].
This article reports on the results published in Hewitt [2006].
Line 13: Line 14:


===Activation ordering===
===Activation ordering===
The activation ordering (<tt>-≈→</tt>) 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).
The activation ordering (<code>-≈→</code>) 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 ''[[General relativity|relativistically]] [[Invariant (physics)|invariant]]''; that is, for all events <tt>e<sub>1</sub></tt>.<tt>e<sub>2</sub></tt>, if <tt>e<sub>1</sub> -≈→ e<sub>2</sub></tt>, then the time of <tt>e<sub>1</sub></tt> precedes the time of <tt>e<sub>2</sub></tt> in the relativistic [[Frame of reference|frames of reference]] of all observers.
*Because of the transmission of energy, the activation ordering is ''[[General relativity|relativistically]] [[Invariant (physics)|invariant]]''; that is, for all events <code>e<sub>1</sub></code>.<code>e<sub>2</sub></code>, if <code>e<sub>1</sub> -≈→ e<sub>2</sub></code>, then the time of <code>e<sub>1</sub></code> precedes the time of <code>e<sub>2</sub></code> in the relativistic [[Frame of reference|frames of reference]] of all observers.
*''Law of Strict Causality for the Activation Ordering'': For no event does <code>e -≈→ e</code>.

*''Law of Strict Causality for the Activation Ordering'': For no event does <tt>e -≈→ e</tt>.
*''Law of Finite Predecession in the Activation Ordering'': For all events <code>e<sub>1</sub></code> the set <code>{e|e -≈→ e<sub>1</sub>}</code> is finite.

*''Law of Finite Predecession in the Activation Ordering'': For all events <tt>e<sub>1</sub></tt> the set <tt>{e|e -≈→ e<sub>1<sub>}</tt> is finite.


===Arrival orderings===
===Arrival orderings===
The arrival ordering of an Actor <tt>x</tt> ( <tt>-x-> </tt>) models the (total) ordering of events in which a message arrives at <tt>x</tt>. Arrival ordering is determined by ''arbitration'' in processing messages (often making use of a digital circuit called an [[Arbiter (electronics)|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 computation]]).
The arrival ordering of an Actor <code>x</code> ( <code>-x→ </code>) models the (total) ordering of events in which a message arrives at <code>x</code>. Arrival ordering is determined by ''arbitration'' in processing messages (often making use of a digital circuit called an [[Arbiter (electronics)|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 <tt>x</tt> happen on the world line of <tt>x</tt>, the arrival ordering of an actor is ''relativistically invariant''. ''I.e.'', for all actors <tt>x</tt> and events <tt>e<sub>1</sub></tt>.<tt>e<sub>2</sub></tt>, if <tt>e<sub>1</sub> -x→ e<sub>2</sub></tt>, then the time of <tt>e<sub>1</sub></tt> precedes the time of <tt>e<sub>2</sub></tt> in the relativistic frames of reference of all observers.
*Because all of the events of the arrival ordering of an actor <code>x</code> happen on the world line of <code>x</code>, the arrival ordering of an actor is ''relativistically invariant''. ''I.e.'', for all actors <code>x</code> and events <code>e<sub>1</sub></code>.<code>e<sub>2</sub></code>, if <code>e<sub>1</sub> -x→ e<sub>2</sub></code>, then the time of <code>e<sub>1</sub></code> precedes the time of <code>e<sub>2</sub></code> in the relativistic frames of reference of all observers.
*''Law of Finite Predecession in Arrival Orderings'': For all events <code>e<sub>1</sub></code> and Actors <code>x</code> the set <code>{e|e -x→ e<sub>1</sub>}</code> is finite.

*''Law of Finite Predecession in Arrival Orderings'': For all events <tt>e<sub>1</sub></tt> and Actors <tt>x</tt> the set <tt>{e|e -x→ e<sub>1<sub>}</tt> is finite.


===Combined ordering===
===Combined ordering===
The combined ordering (denoted by <tt>→</tt>) is defined to be the transitive closure of the activation ordering and the arrival orderings of all Actors.
The combined ordering (denoted by <code>→</code>) 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 <tt>e<sub>1</sub></tt>.<tt>e<sub>2</sub></tt>, if <tt>e<sub>1</sub>&rarr;e<sub>2</sub></tt>. then the time of <tt>e<sub>1</sub></tt> precedes the time of <tt>e<sub>2</sub></tt> in the relativistic frames of reference of all observers.


*The combined ordering is relativistically invariant because it is the transitive closure of relativistically invariant orderings. ''I.e.'', for all events <code>e<sub>1</sub></code>.<code>e<sub>2</sub></code>, if <code>e<sub>1</sub>→e<sub>2</sub></code>. then the time of <code>e<sub>1</sub></code> precedes the time of <code>e<sub>2</sub></code> in the relativistic frames of reference of all observers.
*''Law of Strict Causality for the Combined Ordering'': For no event does <tt>e→e</tt>.
*''Law of Strict Causality for the Combined Ordering'': For no event does <code>e→e</code>.


The combined ordering is obviously transitive by definition.
The combined ordering is obviously transitive by definition.
Line 39: Line 36:
In [Baker and Hewitt 197?], it was conjectured that the above laws might entail the following law:
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 &rarr;.
:''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===
===Independence of the Law of Finite Chains Between Events in the Combined Ordering===
Line 48: Line 45:
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.
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 <tt>Start</tt> message causing it to take the following actions
:Consider a computation which begins when an actor ''Initial'' is sent a <code>Start</code> message causing it to take the following actions
:#Create a new actor ''Greeter<sub>1</sub>'' which is sent the message <tt>SayHelloTo</tt> with the address of ''Greeter<sub>1</sub>''
:#Create a new actor ''Greeter<sub>1</sub>'' which is sent the message <code>SayHelloTo</code> with the address of ''Greeter<sub>1</sub>''
:#Send ''Initial'' the message <tt>Again</tt> with the address of ''Greeter<sub>1</sub>''
:#Send ''Initial'' the message <code>Again</code> with the address of ''Greeter<sub>1</sub>''


:Thereafter the behavior of ''Initial'' is as follows on receipt of an <tt>Again</tt> message with address ''Greeter<sub>i</sub>'' (which we will call the event <tt>'''Again<sub>i</sub>'''</tt>):
:Thereafter the behavior of ''Initial'' is as follows on receipt of an <code>Again</code> message with address ''Greeter<sub>i</sub>'' (which we will call the event <code>'''Again<sub>i</sub>'''</code>):
:#Create a new actor ''Greeter<sub>i+1</sub>'' which is sent the message <tt>SayHelloTo</tt> with address ''Greeter<sub>i</sub>''
:#Create a new actor ''Greeter<sub>i+1</sub>'' which is sent the message <code>SayHelloTo</code> with address ''Greeter<sub>i</sub>''
:#Send ''Initial'' the message <tt>Again</tt> with the address of ''Greeter<sub>i+1</sub>''
:#Send ''Initial'' the message <code>Again</code> with the address of ''Greeter<sub>i+1</sub>''
:Obviously the computation of ''Initial'' sending itself <tt>Again</tt> messages never terminates.
:Obviously the computation of ''Initial'' sending itself <code>Again</code> messages never terminates.


:The behavior of each Actor ''Greeter<sub>i</sub>'' is as follows:
:The behavior of each Actor ''Greeter<sub>i</sub>'' is as follows:
:*When it receives a message <tt>SayHelloTo</tt> with address ''Greeter<sub>i-1</sub>'' (which we will call the event <tt>'''SayHelloTo<sub>i</sub>'''</tt>), it sends a <tt>Hello</tt> message to ''Greeter<sub>i-1</sub>''
:*When it receives a message <code>SayHelloTo</code> with address ''Greeter<sub>i-1</sub>'' (which we will call the event <code>'''SayHelloTo<sub>i</sub>'''</code>), it sends a <code>Hello</code> message to ''Greeter<sub>i-1</sub>''
:*When it receives a <tt>Hello</tt> message (which we will call the event <tt>'''Hello<sub>i</sub>'''</tt>), it does nothing.
:*When it receives a <code>Hello</code> message (which we will call the event <code>'''Hello<sub>i</sub>'''</code>), it does nothing.
:Now it is possible that <tt>'''Hello<sub>i</sub>''' -''Greeter<sub>i</sub>''<tt>→ '''SayHelloTo<sub>i</sub>'''</tt> every time and therefore <tt>'''Hello<sub>i</sub>'''→'''SayHelloTo<sub>i</sub>'''</tt>.
:Now it is possible that <code>'''Hello<sub>i</sub>''' -''Greeter<sub>i</sub>''→ '''SayHelloTo<sub>i</sub>'''</code> every time and therefore <code>'''Hello<sub>i</sub>'''→'''SayHelloTo<sub>i</sub>'''</code>.
:Also <tt>'''Again<sub>i</sub>''' -≈→ '''Again<sub>i+1</sub>'''</tt> every time and therefore <tt>'''Again<sub>i</sub>''' → '''Again<sub>i+1</sub>'''</tt>.
:Also <code>'''Again<sub>i</sub>''' -≈→ '''Again<sub>i+1</sub>'''</code> every time and therefore <code>'''Again<sub>i</sub>''' → '''Again<sub>i+1</sub>'''</code>.


:Furthermore all of the laws stated before the Law of Strict Causality for the Combined Ordering are satisfied.
: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 <tt>'''Again<sub>1</sub>'''</tt> and <tt>'''SayHelloTo<sub>1</sub>'''</tt> as follows:
:However, there may be an infinite number of events in the combined ordering between <code>'''Again<sub>1</sub>'''</code> and <code>'''SayHelloTo<sub>1</sub>'''</code> as follows:
:<tt>'''Again<sub>1</sub>'''→...→'''Again<sub>i</sub>'''→...<math>\infty</math>...→'''Hello<sub>i</sub>'''→'''SayHelloTo<sub>i</sub>'''→...→'''Hello<sub>1</sub>'''→'''SayHelloTo<sub>1</sub>'''
:<code>'''Again<sub>1</sub>'''→...→'''Again<sub>i</sub>'''→...<math>\infty</math>...→'''Hello<sub>i</sub>'''→'''SayHelloTo<sub>i</sub>'''→...→'''Hello<sub>1</sub>'''→'''SayHelloTo<sub>1</sub>'''</code>


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.
However, we know from physics that infinite energy cannot be expended along a finite trajectory. 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===
===Law of Discreteness===
The Law of Finite Chains Between Events in the Combined Ordering is closely related to the following law:
The Law of Finite Chains Between Events in the Combined Ordering is closely related to the following law:
:''Law of Discreteness'': For all events <tt>e<sub>1</sub></tt> and <tt>e<sub>2</sub></tt>, the set <tt>{e|e<sub>1</sub>→e→e<sub>2<sub>}</tt> is finite.
:''Law of Discreteness'': For all events <code>e<sub>1</sub></code> and <code>e<sub>2</sub></code>, the set <code>{e|e<sub>1</sub>→e→e<sub>2</sub>}</code> is finite.


In fact the previous two laws have been shown to be equivalent:
In fact the previous two laws have been shown to be equivalent:
Line 77: Line 74:
: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.)
: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]]s and is related to results on Petri nets [Best ''et. al.'' 1984, 1987].
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]]).
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]]).

==Denotational semantics==
Clinger [1981] used the Actor event model described above to construct a [[Denotational semantics of the Actor model#Clinger.27s Model|denotational model for Actors using power domains]]. Subsequently Hewitt [2006] augmented the diagrams with arrival times to construct a [[Denotational semantics of the Actor model#The Timed Diagrams Model|technically simpler denotational model]] that is easier to understand.


==See also==
==See also==
Line 87: Line 87:


==References==
==References==
*Carl Hewitt, '' et. al.'' '''Actor Induction and Meta-evaluation''' Conference Record of ACM Symposium on Principles of Programming Languages, January 1974.
*Carl Hewitt, '' et al.'' '''Actor Induction and Meta-evaluation''' Conference Record of ACM Symposium on Principles of Programming Languages, January 1974.
*Irene Greif. '''Semantics of Communicating Parallel Processes''' MIT EECS Doctoral Dissertation. August 1975.
*Irene Greif. '''Semantics of Communicating Parallel Processes''' MIT EECS Doctoral Dissertation. August 1975.
*Edsger Dijkstra. '''A discipline of programming''' Prentice Hall. 1976.
*Edsger Dijkstra. '''A discipline of programming''' Prentice Hall. 1976.
*Carl Hewitt and Henry Baker '''Actors and Continuous Functionals''' Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1-5, 1977.
*Carl Hewitt and [[Henry Baker (computer scientist)|Henry Baker]] '''Actors and Continuous Functionals''' Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1–5, 1977.
*Henry Baker and Carl Hewitt '''The Incremental Garbage Collection of Processes''' Proceeding of the Symposium on Artificial Intelligence Programming Languages. SIGPLAN Notices 12, August 1977.
*[[Henry Baker (computer scientist)|Henry Baker]] and Carl Hewitt '''The Incremental Garbage Collection of Processes''' Proceedings of the Symposium on Artificial Intelligence Programming Languages. SIGPLAN Notices 12, August 1977.
*Carl Hewitt and Henry Baker '''Laws for Communicating Parallel Processes''' IFIP-77, August 1977.
*Carl Hewitt and [[Henry Baker (computer scientist)|Henry Baker]] '''Laws for Communicating Parallel Processes''' IFIP-77, August 1977.
*Aki Yonezawa '''Specification and Verification Techniques for Parallel Programs Based on Message Passing Semantics''' MIT EECS Doctoral Dissertation. December 1977.
*Aki Yonezawa '''Specification and Verification Techniques for Parallel Programs Based on Message Passing Semantics''' MIT EECS Doctoral Dissertation. December 1977.
*Peter Bishop '''Very Large Address Space Modularly Extensible Computer Systems''' MIT EECS Doctoral Dissertation. June 1977.
*Peter Bishop '''Very Large Address Space Modularly Extensible Computer Systems''' MIT EECS Doctoral Dissertation. June 1977.
Line 104: Line 104:
*Bill Kornfeld. '''Parallelism in Problem Solving''' MIT EECS Doctoral Dissertation. August 1981.
*Bill Kornfeld. '''Parallelism in Problem Solving''' MIT EECS Doctoral Dissertation. August 1981.
*Will Clinger. '''Foundations of Actor Semantics''' MIT Mathematics Doctoral Dissertation. June 1981.
*Will Clinger. '''Foundations of Actor Semantics''' MIT Mathematics Doctoral Dissertation. June 1981.
*Eike Best. '''Concurrent Behaviour: Sequences, Processes and Axioms''' Lecture Notes in Computer Science Vol.197 1984.
*[[Eike Best]]. '''Concurrent Behaviour: Sequences, Processes and Axioms''' Lecture Notes in Computer Science Vol.197 1984.
*Gul Agha. '''[http://hdl.handle.net/1721.1/6952 Actors: A Model of Concurrent Computation in Distributed Systems]''' Doctoral Dissertation. 1986.
*Gul Agha. '''[http://hdl.handle.net/1721.1/6952 Actors: A Model of Concurrent Computation in Distributed Systems]''' Doctoral Dissertation. 1986.
*Eike Best and R.Devillers. '''Sequential and Concurrent Behaviour in Petri Net Theory''' Theoretical Computer Science Vol.55/1. 1987.
*Eike Best and R.Devillers. '''Sequential and Concurrent Behaviour in Petri Net Theory''' Theoretical Computer Science Vol.55/1. 1987.
*Gul Agha, Ian Mason, Scott Smith, and Carolyn Talcott. '''A Foundation for Actor Computation''' Journal of Functional Programming January 1993.
*Gul Agha, Ian Mason, Scott Smith, and Carolyn Talcott. '''A Foundation for Actor Computation''' Journal of Functional Programming January 1993.
*Satoshi Matsuoka and Akinori Yonezawa. '''Analysis of inheritance anomaly in object-oriented concurrent programming languages''' in Research directions in concurrent object-oriented programming. 1993.
*Satoshi Matsuoka and [[Akinori Yonezawa]]. '''Analysis of inheritance anomaly in object-oriented concurrent programming languages''' in Research directions in concurrent object-oriented programming. 1993.
*Jayadev Misra. '''A Logic for concurrent programming: Safety''' Journal of Computer Software Engineering. 1995.
*Jayadev Misra. '''A Logic for concurrent programming: Safety''' Journal of Computer Software Engineering. 1995.
*Luca de Alfaro, Zohar Manna, Henry Sipma and Tomás Uribe. '''Visual Verification of Reactive Systems''' TACAS 1997.
*Luca de Alfaro, Zohar Manna, Henry Sipma and Tomás Uribe. '''Visual Verification of Reactive Systems''' TACAS 1997.
*Thati, Prasanna, Carolyn Talcott, and Gul Agha. '''Techniques for Executing and Reasoning About Specification Diagrams''' International Conference on Algebraic Methodology and Software Technology (AMAST), 2004.
*Thati, Prasanna, Carolyn Talcott, and Gul Agha. '''Techniques for Executing and Reasoning About Specification Diagrams''' International Conference on Algebraic Methodology and Software Technology (AMAST), 2004.
*Giuseppe Milicia and Vladimiro Sassone. '''The Inheritance Anomaly: Ten Years After''' Proceedings of the 2004 ACM Symposium on Applied Computing (SAC), Nicosia, Cyprus, March 14-17, 2004.
*Giuseppe Milicia and Vladimiro Sassone. '''The Inheritance Anomaly: Ten Years After''' Proceedings of the 2004 ACM Symposium on Applied Computing (SAC), Nicosia, Cyprus, March 14–17, 2004.
*Petrus Potgieter. [http://arxiv.org/abs/cs/0412022 '''Zeno machines and hypercomputation'''] 2005
*Petrus Potgieter. [https://arxiv.org/abs/cs/0412022 '''Zeno machines and hypercomputation'''] 2005
*Carl Hewitt [http://www.pcs.usp.br/~coin-aamas06/10_commitment-43_16pages.pdf What is Commitment?Physical, Organizational, and Social] COINS@AAMAS. 2006.
*Carl Hewitt [http://www.pcs.usp.br/~coin-aamas06/10_commitment-43_16pages.pdf What is Commitment?Physical, Organizational, and Social] COINS@AAMAS. 2006.

[[Category:Actor model]]
[[Category:Actor model (computer science)]]
[[Category:Denotational semantics]]
[[Category:Mathematics of computing]]

Latest revision as of 21:28, 2 March 2021

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.

Events and their orderings

[edit]

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

[edit]

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.

Arrival orderings

[edit]

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.

Combined ordering

[edit]

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

[edit]

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
  1. Create a new actor Greeter1 which is sent the message SayHelloTo with the address of Greeter1
  2. 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):
  1. Create a new actor Greeteri+1 which is sent the message SayHelloTo with address Greeteri
  2. 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 -GreeteriSayHelloToi every time and therefore HelloiSayHelloToi.
Also Againi -≈→ Againi+1 every time and therefore AgainiAgaini+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→......→HelloiSayHelloToi→...→Hello1SayHelloTo1

However, we know from physics that infinite energy cannot be expended along a finite trajectory. 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

[edit]

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 machines and is related to results on Petri nets [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).

Denotational semantics

[edit]

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

[edit]

References

[edit]
  • Carl Hewitt, et al. Actor Induction and Meta-evaluation Conference Record of ACM Symposium on Principles of Programming Languages, January 1974.
  • Irene Greif. Semantics of Communicating Parallel Processes MIT EECS Doctoral Dissertation. August 1975.
  • Edsger Dijkstra. A discipline of programming Prentice Hall. 1976.
  • Carl Hewitt and Henry Baker Actors and Continuous Functionals Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1–5, 1977.
  • Henry Baker and Carl Hewitt The Incremental Garbage Collection of Processes Proceedings of the Symposium on Artificial Intelligence Programming Languages. SIGPLAN Notices 12, August 1977.
  • Carl Hewitt and Henry Baker Laws for Communicating Parallel Processes IFIP-77, August 1977.
  • Aki Yonezawa Specification and Verification Techniques for Parallel Programs Based on Message Passing Semantics MIT EECS Doctoral Dissertation. December 1977.
  • Peter Bishop Very Large Address Space Modularly Extensible Computer Systems MIT EECS Doctoral Dissertation. June 1977.
  • Carl Hewitt. Viewing Control Structures as Patterns of Passing Messages Journal of Artificial Intelligence. June 1977.
  • Henry Baker. Actor Systems for Real-Time Computation MIT EECS Doctoral Dissertation. January 1978.
  • Carl Hewitt and Russ Atkinson. Specification and Proof Techniques for Serializers IEEE Journal on Software Engineering. January 1979.
  • Carl Hewitt, Beppe Attardi, and Henry Lieberman. Delegation in Message Passing Proceedings of First International Conference on Distributed Systems Huntsville, AL. October 1979.
  • Russ Atkinson. Automatic Verification of Serializers MIT Doctoral Dissertation. June, 1980.
  • Bill Kornfeld and Carl Hewitt. The Scientific Community Metaphor IEEE Transactions on Systems, Man, and Cybernetics. January 1981.
  • Gerry Barber. Reasoning about Change in Knowledgeable Office Systems MIT EECS Doctoral Dissertation. August 1981.
  • Bill Kornfeld. Parallelism in Problem Solving MIT EECS Doctoral Dissertation. August 1981.
  • Will Clinger. Foundations of Actor Semantics MIT Mathematics Doctoral Dissertation. June 1981.
  • Eike Best. Concurrent Behaviour: Sequences, Processes and Axioms Lecture Notes in Computer Science Vol.197 1984.
  • Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems Doctoral Dissertation. 1986.
  • Eike Best and R.Devillers. Sequential and Concurrent Behaviour in Petri Net Theory Theoretical Computer Science Vol.55/1. 1987.
  • Gul Agha, Ian Mason, Scott Smith, and Carolyn Talcott. A Foundation for Actor Computation Journal of Functional Programming January 1993.
  • Satoshi Matsuoka and Akinori Yonezawa. Analysis of inheritance anomaly in object-oriented concurrent programming languages in Research directions in concurrent object-oriented programming. 1993.
  • Jayadev Misra. A Logic for concurrent programming: Safety Journal of Computer Software Engineering. 1995.
  • Luca de Alfaro, Zohar Manna, Henry Sipma and Tomás Uribe. Visual Verification of Reactive Systems TACAS 1997.
  • Thati, Prasanna, Carolyn Talcott, and Gul Agha. Techniques for Executing and Reasoning About Specification Diagrams International Conference on Algebraic Methodology and Software Technology (AMAST), 2004.
  • Giuseppe Milicia and Vladimiro Sassone. The Inheritance Anomaly: Ten Years After Proceedings of the 2004 ACM Symposium on Applied Computing (SAC), Nicosia, Cyprus, March 14–17, 2004.
  • Petrus Potgieter. Zeno machines and hypercomputation 2005
  • Carl Hewitt What is Commitment?Physical, Organizational, and Social COINS@AAMAS. 2006.