|
The denotational semantics of the Actor model is the subject of mathematical models for Actors based on domain theory.==Clinger's Model== In his doctoral dissertation, Will Clinger developed the first denotation semantics for the Actor model. The domain of Actor computations Clinger 1981 explained the domain of Actor computations as follows: The augmented Actor event diagrams see Actor model theory form a partially ordered set < Diagrams, ≤ > from which to construct the power domain P'''Diagrams''' (see the section on Denotations below). The augmented diagrams are partial computation histories representing "snapshots" relative to some frame of reference of a computation on its way to being completed. For x,y∈Diagrams, x≤y means x is a stage the computation could go through on its way to y. The completed elements of Diagrams represent computations that have terminated and nonterminating computations that have become infinite. The completed elements may be characterized abstractly as the maximal elements of Diagrams see William Wadge 1979. Concretely, the completed elements are those having non pending events. Intuitively, Diagrams is not ω-complete because there exist increasing sequences of finite partial computations x0 ≤ x1 ≤ x2 ≤ x3 ≤ ... in which some pending event remains pending forever while the number of realized events grows without bound, contrary to the requirement of finite arrival delay. Such a sequence cannot have a limit, because any limit would represent a completed nonterminating computation in which an event is still pending. To repeat, the actor event diagram domain Diagrams is incomplete because of the requirement of finite arrival delay, which allows any finite delay between an event and an event it activates but rules out infinite delay. Denotations In his doctoral dissertation, Will Clinger explained how power domains are obtained from incomplete domains as follows: From the article on Power domains: PD is the collection of downward-closed subsets of domain D that are also closed under existing least upper bounds of directed sets in D. Note that while the ordering on PD is given by the subset relation, least upper bounds do not in general coincide with unions. For the actor event diagram domain Diagrams, an element of P'''Diagrams''' represents a list of possible initial histories of a computation. Since for elements x and y of Diagrams, x≤y means that x is an initial segment of the initial history y, the requirement that elements of P'''Diagrams''' be downward-closed has a clear basis in intuition. ... Usually the partial order from which the power domain is constructed is required to be ω-complete. There are two reasons for this. The first reason is that most power domains are simply generalizations of domains that have been used as semantic domains for conventional sequential programs, and such domains are all complete because of the need to compute fixed points in the sequential case. The second reason is that ω-completeness permits the solution of recursive domain equations involving the power domain such as R ≈ S → PS + (S R) which defines a domain of resumptions Gordon Plotkin 1976. However, power domains can be defined for any domain whatsoever. Furthermore the power domain of a domain is essentially the power domain of its ω-completion, so recursive equations involving the power domain of an incomplete domain can still be solved, provide the domains to which the usual constructors (+, , → , and In short, there is no technical impediment to building power domains from incomplete domains. But why should one want to do so? In behavioral semantics, developed by Irene Greif, the meaning of program is a specification of the computations that may be performed by the program. The computations are represented formally by Actor event diagrams. Greif specified the event diagrams by means of causal axioms governing the behaviors of individual Actors Greif 1975. Henry Baker has presented a nondeterministic interpreter generating instantaneous schedules which then map onto event diagrams. He suggested that a corresponding deterministic interpreter operating on sets of instantaneous schedules could be defined using power domain semantics Baker 1978. The semantics presented in Clinger 1981 is a version of behavioral semantics. A program denotes a set of Actor event diagrams. The set is defined extensionally using power domain semantics rather than intensionally using causal axioms. The behaviors of individual Actors is defined functionally. It is shown, however, that the resulting set of Actor event diagrams consists of exactly those diagrams that satisfy causal axioms expressing the functional behaviors of Actors. Thus Greif's behavioral semantics is compatible with a denotational power domain semantics. Baker's instantaneous schedules introduced the notion of pending events, which represent messages on the way to their targets. Each pending event must become an actual (realized) arrival event sooner or later, a requirement referred to as finite delay. Augmenting Actor event diagrams with sets of pending events helps to express the finite delay property, which is characteristic of true concurrency Schwartz 1979. Sequential computations form an ω-complete subdomain of the domain of Actor computations In his 1981 dissertation, Clinger showed how sequential computations form a subdomain of concurrent computations: Instead of beginning with a semantics for sequential programs and then trying to extend it for concurrency, Actor semantics views concurrency as primary and obtains the semantics of sequential programs as a special case. ... The fact that there exist increasing sequences without least upper bounds may seem strange to those accustomed to thinking about the semantics of sequential programs. It may help to point out that the increasing sequences produced by sequential programs all have least upper bounds. Indeed, the partial computations that can be produced by sequential computation form an ω-complete subdomain of the domain of Actor computations Diagrams. An informal proof follows. From the Actor point of view, sequential computations are a special case of concurrent computations, distinguishable by their event diagrams. The event diagram of a sequential computation has an initial event, and no event activates more than one event. In other words, the activation ordering of a sequential computation is linear; the event diagram is essentially a conventional execution sequence. This means that the finite elements of Diagrams x0 ≤ x1 ≤ x2 ≤ x3 ≤ ... corresponding to the finite initial segments of a sequential execution sequence all have exactly one pending event, excepting the largest, completed element if the computation terminates. One property of the augmented event diagrams domain < Diagrams, ≤ > is that if x≤y and x≠y, then some pending event of x is realized in y. Since in this case each xi has at most one pending event, every pending event in the sequence becomes realized. Hence the sequence x0 ≤ x1 ≤ x2 ≤ x3 ≤ ... has a least upper bound in Diagrams in accord with intuition. The above proof applies to all sequential programs, even those with choice points such as guarded commands. Thus Actor semantics includes sequential programs as a special case, and agrees with conventional semantics of such programs. The Timed Diagrams Model Hewitt 2006 published a new denotational semantics for Actors based on Timed Diagrams. The Timed Diagrams model stands in contrast to Clinger 1981 which constructed an ω-complete power domain from an underlying incomplete diagrammatic domain, which did not include time. The advantage of the domain Timed Diagrams model is that it is physically motivated and the resulting computations have the desired property of ω-completeness (therefore unbounded nondeterminism) which provides guarantee of service. Domain of Timed Actor Computations Timed Diagrams denotational semantics constructs an ω-complete computational domain for Actor computations. In the domain, for each event in an Actor computation, there is a delivery time which represents the time at which the message is delivered such that each delivery time satisfies the following conditions: 1. The delivery time is a positive rational number that is not the same as the delivery time of any other message. 2. The delivery time is more than a fixed δ greater than the time of its activating event. It will later turn out that the value δ of doesn’t matter. In fact the value of δ can even be allowed to decrease linearly with time to accommodate Moore’s Law. The Actor event timed diagrams form a partially ordered set <TimedDiagrams, ≤>. The diagrams are partial computation histories representing "snapshots" (relative to some frame of reference) of a computation on its way to being completed. For d1,d2εTimedDiagrams, d1≤d2 means d1 is a stage the computation could go through on its way to d2 The completed elements of TimedDiagrams represent computations that have terminated and nonterminating computations that have become infinite. The completed elements may be characterized abstractly as the maximal elements of TimedDiagrams. Concretely, the completed elements are those having no pending events. Theorem: TimedDiagrams is an ω-complete domain of Actor computations i.e., 1. If D⊆TimedDiagrams is directed, the least upper bound VD exists; furthermore VD obeys all the laws of Actor model theory. 2. The finite elements of TimedDiagrams are countable where an element xεTimedDiagrams is finite (isolated) if and only if D⊆TimedDiagrams is directed and x≤VD, there exists dεD with x≤d. In other words, x is finite if one must go through x in order to get up to or above x via the limit process. 3. Every element of TimedDiagrams is the least upper bound of a countable increasing sequence of finite elements. Power domains Definition: The domain 1. M is downward-closed, i.e., if dεM, then ∀d’εTimedDiagrams d’≤d ⇒ d’εM 2. M is closed under least upper bounds of directed sets, i.e. if D⊆M is directed, then VDεM Note: Although Power'''TimedDiagrams''' is ordered by ⊆, limits are not given by U. I.e., ∀i Mi⊆Mi+1 ⇒ Uiεω Mi ⊆ Viεω Mi E.g., If ∀i diεTimedDiagrams and di≤di+1 and Mi= then Viεω Mi = Uiεω Mi U Theorem: Power '''TimedDiagrams''' is an ω-complete domain. Denotations An Actor computation can progress in many ways. Let d be a diagram with next scheduled event e and X ≡ (see Actor model theory), Flow(d) is defined to be the set of all timed diagrams with d and extensions of d by X such that 1. the arrival all of the events of X has been scheduled where 2. the events of X are scheduled in all possible orderings among the scheduled future events of d 3. subject to the constraint that each event in X is scheduled at least δ after e and every event in X is scheduled at least once in every δ interval after that. (Recall that δ is the minimum amount of time to deliver a message.) Flow(d) ≡ if d is complete. Let S be an Actor system, ProgressionS is a mapping Power'''TimedDiagrams'''→Power'''TimedDiagrams''' ProgressionS(M) ≡ UdεM Flow(d) Theorem: ProgressionS is ω-continuous. I.e., if ∀i Mi⊆Mi+1 then ProgressionS(Viεω Mi) = Viεω ProgressionS(Mi) Furthermore the least fixed point of ProgressionS is Viεω ProgressionSi(⊥S) where ⊥S is the initial configuration of S. The denotation DenoteS of an Actor system S is the set of all computations of S. Define the time abstraction of a timed diagram to be the diagram with the time annotations removed. Representation Theorem: The denotation DenoteS of an Actor system S is the time abstraction of Viεω ProgressionSi (⊥S) Using the domain TimedDiagrams, which is ω-complete, is important because it provides for the direct expression of the above representation theorem for the denotations of Actor systems by directly constructing a minimal fixed point. | |||||||
|
| ||||||||
 |
|
| |