Denotational semantics of the Actor model

Last updated

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].

Contents

Actor fixed point semantics

The denotational theory of computational system semantics is concerned with finding mathematical objects that represent what systems do. Collections of such objects are called domains. The Actor uses the domain of event diagram scenarios. It is usual to assume some properties of the domain, such as the existence of limits of chains (see cpo) and a bottom element. Various additional properties are often reasonable and helpful: the article on domain theory has more details.

A domain is typically a partial order, which can be understood as an order of definedness. For instance, given event diagram scenarios x and y, one might let "x≤y" mean that "y extends the computations x".

The mathematical denotation for a system S is found by constructing increasingly better approximations from an initial empty denotation called S using some denotation approximating function progressionS to construct a denotation (meaning ) for S as follows:

It would be expected that progressionS would be monotone, i.e., if x≤y then progressionS(x)≤progressionS(y). More generally, we would expect that

If ∀i∈ω xixi+1, then

This last stated property of progressionS is called ω-continuity.

A central question of denotational semantics is to characterize when it is possible to create denotations (meanings) according to the equation for DenoteS. A fundamental theorem of computational domain theory is that if progressionS is ω-continuous then DenoteS will exist.

It follows from the ω-continuity of progressionS that

progressionS(DenoteS) = DenoteS

The above equation motivates the terminology that DenoteS is a fixed point of progressionS.

Furthermore, this fixed point is least among all fixed points of progressionS.

Compositionality in programming languages

An important aspect of denotational semantics of programming languages is compositionality, by which the denotation of a program is constructed from denotations of its parts. For example, consider the expression "<expression1> + <expression2>". Compositionality in this case is to provide a meaning for "<expression1> + <expression2>" in terms of the meanings of <expression1> and <expression2>.

The Actor model provides a modern and very general way the compositionality of programs can be analyzed. Scott and Strachey [1971] proposed that the semantics of programming languages be reduced to the semantics of the lambda calculus and thus inherit the denotational semantics of the lambda calculus. However, it turned out that concurrent computation could not be implemented in the lambda calculus (see Indeterminacy in concurrent computation). Thus there arose the problem of how to provide modular denotational semantics for concurrent programming languages. One solution to this problem is to use the Actor model of computation. In Actor model, programs are Actors that are sent Eval messages with the address of an environment (explained below) so that programs inherit their denotational semantics from the denotational semantics of the Actor model (an idea published in Hewitt [2006]).

Environments

Environments hold the bindings of identifiers. When an environment is sent a Lookup message with the address of an identifier x, it returns the latest (lexical) binding of x.

As an example of how this works consider the lambda expression <L> below which implements a tree data structure when supplied with parameters for a leftSubTree and rightSubTree. When such a tree is given a parameter message "getLeft", it return leftSubTree and likewise when given the message "getRight" it returns rightSubTree.

 λ(leftSubTree, rightSubTree)    λ(message)      if (message == "getLeft") then leftSubTree      else if (message == "getRight") then rightSubTree

Consider what happens when an expression of the form "(<L> 1 2)" is sent an Eval message with environment E. One semantics for application expressions such as this one is the following: <L>, 1 and 2 are each sent Eval messages with environment E. The integers 1 and 2 immediately reply to the Eval message with themselves.

However, <L> responds to the Eval message by creating a closure Actor (process) C that has an address (called body) for <L> and an address (called environment) for E. The Actor "(<L> 1 2)" then sends C the message [1 2].

When C receives the message [1 2], it creates a new environment Actor F which behaves as follows:

  1. When it receives a Lookup message for the identifier leftSubTree, it responds with 1
  2. When it receives a Lookup message for the identifier rightSubTree, it responds with 2
  3. When it receives a Lookup message for any other identifier, it forwards the Lookup message to E

The Actor (process) C then sends an Eval message with environment F to the following actor (process):

   λ(message)      if (message == "getLeft") then leftSubTree      else if (message == "getRight") then rightSubTree

Arithmetic expressions

For another example consider the Actor for the expression "<expression1> + <expression2>" which has addresses for two other actors (processes) <expression1> and <expression2>. When the composite expression Actor (process) receives an Eval message with addresses for an environment Actor E and a customer C, it sends Eval messages to <expression1> and <expression2> with environment E and sends C a new Actor (process) C0. When C0 has received back two values N1 and N2, it sends C the value N1+N2. In this way, the denotational semantics for process calculi and the Actor model provide a denotational semantics for "<expression1> + <expression2>" in terms of the semantics for <expression1> and <expression2>.

Other programming language constructs

The denotational compositional semantics presented above is very general and can be used for functional, imperative, concurrent, logic, etc. programs (see [Hewitt 2008a]). For example, it easily provides denotation semantics for constructs that are difficult to formalize using other approaches such as delays and futures.

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,yDiagrams, 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
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: P[D] 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 P[D] 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
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 *) are applied are ω-complete. It happens that defining Actor semantics as in Clinger [1981] does not require solving any recursive equations involving the power domain.
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
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
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 [2006b] 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 ⊔D exists; furthermore ⊔D 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

Concurrency Representation Theorem

An Actor computation can progress in many ways. Let d be a diagram with next scheduled event e and X ≡ {e’ | e ─≈→1-message e’} (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) ≡ {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(⊔iεω Mi) = ⊔iεω ProgressionS(Mi)

Furthermore, the least fixed point of ProgressionS is given by the Concurrency Representation Theorem as follows:

iεω 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

iεω 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.

The criterion of continuity for the graphs of functions that Scott used to initially develop the denotational semantics of functions can be derived as a consequence of the Actor laws for computation as shown in the next section.

Related Research Articles

<span class="mw-page-title-main">Finite-state machine</span> Mathematical model of computation

A finite-state machine (FSM) or finite-state automaton, finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number of states at any given time. The FSM can change from one state to another in response to some inputs; the change from one state to another is called a transition. An FSM is defined by a list of its states, its initial state, and the inputs that trigger each transition. Finite-state machines are of two types—deterministic finite-state machines and non-deterministic finite-state machines. A deterministic finite-state machine can be constructed equivalent to any non-deterministic one.

In computer science, denotational semantics is an approach of formalizing the meanings of programming languages by constructing mathematical objects that describe the meanings of expressions from the languages. Other approaches providing formal semantics of programming languages include axiomatic semantics and operational semantics.

<span class="mw-page-title-main">State diagram</span> Diagram of behavior of finite state systems

A state diagram is a type of used in computer science and related fields to describe the behavior of systems. State diagrams require that the system described is composed of a finite number of states; sometimes, this is indeed the case, while at other times this is a reasonable abstraction. Many forms of state diagrams exist, which differ slightly and have different semantics.

In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi, based on message passing via channels. CSP was highly influential in the design of the occam programming language and also influenced the design of programming languages such as Limbo, RaftLib, Erlang, Go, Crystal, and Clojure's core.async.

Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms. Operational semantics are classified in two categories: structural operational semantics formally describe how the individual steps of a computation take place in a computer-based system; by opposition natural semantics describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.

Domain theory is a branch of mathematics that studies special kinds of partially ordered sets (posets) commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer science, where it is used to specify denotational semantics, especially for functional programming languages. Domain theory formalizes the intuitive ideas of approximation and convergence in a very general way and is closely related to topology.

In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax.

In mathematics, the phrase complete partial order is variously used to refer to at least three similar, but distinct, classes of partially ordered sets, characterized by particular completeness properties. Complete partial orders play a central role in theoretical computer science: in denotational semantics and domain theory.

<span class="mw-page-title-main">Concurrency (computer science)</span> Ability execute a task in a non-serial manner

In computer science, concurrency is the ability of different parts or units of a program, algorithm, or problem to be executed out-of-order or in partial order, without affecting the final outcome. This allows for parallel execution of the concurrent units, which can significantly improve overall speed of the execution in multi-processor and multi-core systems. In more technical terms, concurrency refers to the decomposability of a program, algorithm, or problem into order-independent or partially-ordered components or units of computation.

The actor model in computer science is a mathematical model of concurrent computation that treats actor as the universal primitive of concurrent computation. In response to a message it receives, an actor can: make local decisions, create more actors, send more messages, and determine how to respond to the next message received. Actors may modify their own private state, but can only affect each other indirectly through messaging.

In theoretical computer science, Actor model theory concerns theoretical issues for the Actor model.

In computer science, the Actor model and process calculi are two closely related approaches to the modelling of concurrent digital computation. See Actor model and process calculi history.

Concurrent computing is a form of computing in which several computations are executed concurrently—during overlapping time periods—instead of sequentially—with one completing before the next starts.

In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation.

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 serviced. Unbounded nondeterminism became an important issue in the development of the denotational semantics of concurrency, and later became part of research into the theoretical concept of hypercomputation.

In denotational semantics and domain theory, power domains are domains of nondeterministic and concurrent computations.

Indeterminacy in concurrent computation is concerned with the effects of indeterminacy in concurrent computation. Computation is an area in which indeterminacy is becoming increasingly important because of the massive increase in concurrency due to networking and the advent of many-core computer architectures. These computer systems make use of arbiters which give rise to indeterminacy.

The actor model and process calculi share an interesting history and co-evolution.

In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. This article reports on the middle history of the Actor model in which major themes were initial implementations, initial applications, and development of the first proof theory and denotational model. It is the follow on article to Actor model early history which reports on the early history of the Actor model which concerned the basic development of the concepts. The article Actor model later history reports on developments after the ones reported in this article.

In computer science, a loop variant is a mathematical function defined on the state space of a computer program whose value is monotonically decreased with respect to a (strict) well-founded relation by the iteration of a while loop under some invariant conditions, thereby ensuring its termination. A loop variant whose range is restricted to the non-negative integers is also known as a bound function, because in this case it provides a trivial upper bound on the number of iterations of a loop before it terminates. However, a loop variant may be transfinite, and thus is not necessarily restricted to integer values.

References