Actor model and process calculi

Last updated

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.

Contents

There are many similarities between the two approaches, but also several differences (some philosophical, some technical):

The publications on the Actor model and on process calculi have a fair number of cross-references, acknowledgments, and reciprocal citations (see Actor model and process calculi history).

How channels work

Indirect communication using channels (e.g. Gilles Kahn and David MacQueen [1977]) has been an important issue for communication in parallel and concurrent computation affecting both semantics and performance. Some process calculi differ from the Actor model in their use of channels as opposed to direct communication.

Synchronous channels

Synchronous channels have the property that a sender putting a message in the channel must wait for a receiver to get the message out of the channel before the sender can proceed.

Simple synchronous channels

A synchronous channel can be modeled by an Actor that receives put and get communications. The following is the behavior of an Actor for a simple synchronous channel:

Synchronous channels in process calculi

However, simple synchronous channels do not suffice for process calculi such as Communicating Sequential Processes (CSP) [Hoare 1978 and 1985] because use of the guarded choice (after Dijkstra) command (called the alternative command in CSP). In a guarded choice command multiple offers (called guards) can be made concurrently on multiple channels to put and get messages; however at most one of the guards can be chosen for each execution of the guarded choice command. Because only one guard can be chosen, a guarded choice command in general effectively requires a kind of two-phase commit protocol or perhaps even a three-phase commit protocol if time-outs are allowed in guards (as in Occam 3 [1992]).

Consider the following program written in CSP [Hoare 1978]:

[X :: Z!stop() ||  Y :: guard: boolean; guard := true;      *[guard  →  Z!go(); Z?guard] ||  Z :: n: integer; n:= 0;        *[X?stop()  →  Y!false; print!n;          [] Y?go()  →  n := n+1; Y!true] ]

According to Clinger [1981], this program illustrates global nondeterminism, since the nondeterminism arises from incomplete specification of the timing of signals between the three processes X, Y, and Z. The repetitive guarded command in the definition of Z has two alternatives:

  1. the stop message is accepted from X, in which case Y is sent the value false and print is sent the value n
  2. a go message is accepted from Y, in which case n is incremented and Y is sent the value true.

If Z ever accepts the stop message from X, then X terminates. Accepting the stop causes Y to be sent false which when input as the value of its guard will cause Y to terminate. When both X and Y have terminated, Z terminates because it no longer has live processes providing input.

In the above program, there are synchronous channels from X to Z, Y to Z, and Z to Y.

Analogy with the committee coordination problem

According to Knabe [1992], Chandy and Misra [1988] characterized this as analogous to the committee coordination problem:

Professors in a university are assigned to various committees. Occasionally a professor will decide to attend a meeting of any of her committees, and will wait until that is possible. Meetings may begin only if there is full attendance. The task is to ensure that if all the members of a committee are waiting, then at least one of them will attend some meeting.
The crux of this problem is that two or more committees might share a professor. When that professor becomes available, she can only choose one of the meetings, while the others continue to wait.

A simple distributed protocol

This section presents a simple distributed protocol for channels in synchronous process calculi. The protocol has some problems that are addressed in the sections below.

The behavior of a guarded choice command is as follows:

The behavior of a guard is as follows:

The behavior of a channel is as follows:

Starvation on getting from multiple channels

Again consider the program written in CSP (discussed in Synchronous channels in process calculi above):

[X :: Z!stop() ||  Y :: guard: boolean; guard := true;      *[guard  →  Z!go(); Z?guard] ||  Z :: n: integer; n:= 0;        *[X?stop()  →  Y!false; print!n;          [] Y?go()  →  n := n+1; Y!true] ]

As pointed out in Knabe [1992], a problem with the above protocol (A simple distributed protocol) is that the process Z might never accept the stop message from X (a phenomenon called starvation) and consequently the above program might never print anything.

In contrast consider, a simple Actor system that consists of Actors X, Y, Z, and print where

By the laws of Actor semantics, the above Actor system will always halt when the Actors X, Y, are Z are each sent a "start" message resulting in sending print a number that can be unbounded large.

The difference between the CSP program and the Actor system is that the Actor Z does not get messages using a guarded choice command from multiple channels. Instead it processes messages in arrival ordering, and by the laws for Actor systems, the stop message is guaranteed to arrive.

Livelock on getting from multiple channels

Consider the following program written in CSP [Hoare 1978]:

[Bidder1 :: b: bid;        *[Bids1?b  →  process1!b;          [] Bids2?b  →  process1!b;] ||  Bidder2 :: b: bid;        *[Bids1?b  →  process2!b;          [] Bids2?b  →  process2!b;]  ]

As pointed out in Knabe [1992], an issue with the above protocol (A simple distributed protocol) is that the process Bidder2 might never accept a bid from Bid1 or Bid2 (a phenomenon called livelock) and consequently process2 might never be sent anything. In each attempt to accept a message, Bidder2 is thwarted because the bid that was offered by Bids1 or Bids2 is snatched away by Bidder1 because it turns out that Bidder1 has much faster access than Bidder2 to Bids1 and Bids2. Consequently, Bidder1 can accept a bid, process it and accept another bid before Bidder2 can commit to accepting a bid.

Efficiency

As pointed out in Knabe [1992], an issue with the above protocol (A simple distributed protocol) is the large number of communications that must be sent in order to perform the handshaking in order to send a message through a synchronous channel. Indeed, as shown in the previous section (Livelock), the number of communications can be unbounded.

Summary of Issues

The subsections above have articulated the following three issues concerned with the use of synchronous channels for process calculi:

  1. Starvation. The use of synchronous channels can cause starvation when a process attempts to get messages from multiple channels in a guarded choice command.
  2. Livelock. The use of synchronous channels can cause a process to be caught in livelock when it attempts to get messages from multiple channels in a guarded choice command.
  3. Efficiency. The use of synchronous channels can require a large number of communications in order to get messages from multiple channels in a guarded choice command.

It is notable that in all of the above, issues arise from the use of a guarded choice command to get messages from multiple channels.

Asynchronous channels

Asynchronous channels have the property that a sender putting a message in the channel need not wait for a receiver to get the message out of the channel.

Simple asynchronous channels

An asynchronous channel can be modeled by an Actor that receives put and get communications. The following is the behavior of an Actor for a simple asynchronous channel:

Asynchronous channels in process calculi

The Join-calculus programming language (published in 1996) implemented local and distributed concurrent computations. It incorporated asynchronous channels as well as a kind of synchronous channel that is used for procedure calls. Agha's Aπ Actor calculus ( Agha and Thati 2004 ) is based on a typed version of the asynchronous π-calculus.

Algebras

The use of algebraic techniques was pioneered in the process calculi. Subsequently, several different process calculi intended to provide algebraic reasoning about Actor systems have been developed in ( Gaspari and Zavattaro 1997 ), ( Gaspari and Zavattaro 1999 ), ( Agha and Thati 2004 ).

Denotational semantics

Will Clinger (building on the work of Irene Greif [1975], Gordon Plotkin [1976], Henry Baker [1978], Michael Smyth [1978], and Francez, Hoare, Lehmann, and de Roever [1979]) published the first satisfactory mathematical denotational theory of the Actor model using domain theory in his dissertation in 1981. His semantics contrasted the unbounded nondeterminism of the Actor model with the bounded nondeterminism of CSP [Hoare 1978] and Concurrent Processes [Milne and Milner 1979] (see denotational semantics). Roscoe [2005] has developed a denotational semantics with unbounded nondeterminism for a subsequent version of Communicating Sequential Processes Hoare [1985]. More recently Carl Hewitt [2006b] developed a denotational semantics for Actors based on timed diagrams.

Ugo Montanari and Carolyn Talcott [1998] have contributed to attempting to reconcile Actors with process calculi.

Related Research Articles

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.

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.

The calculus of communicating systems (CCS) is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel composition, choice between actions and scope restriction. CCS is useful for evaluating the qualitative correctness of properties of a system such as deadlock or livelock.

In theoretical computer science, the π-calculus is a process calculus. The π-calculus allows channel names to be communicated along the channels themselves, and in this way it is able to describe concurrent computations whose network configuration may change during the computation.

In computer science, the process calculi are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent agents or processes. They also provide algebraic laws that allow process descriptions to be manipulated and analyzed, and permit formal reasoning about equivalences between processes. Leading examples of process calculi include CSP, CCS, ACP, and LOTOS. More recent additions to the family include the π-calculus, the ambient calculus, PEPA, the fusion calculus and the join-calculus.

Bunched logic is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about resource composition, which aid in the compositional analysis of computer and other systems. It has category-theoretic and truth-functional semantics, which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgement Γ ⊢ A are tree-like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs. The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic, and in systems modelling, where it provides a way to decompose the resources used by components of a system.

Concurrency (computer science) 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.

In computer science, message passing is a technique for invoking behavior on a computer. The invoking program sends a message to a process and relies on that process and its supporting infrastructure to then select and run some appropriate code. Message passing differs from conventional programming where a process, subroutine, or function is directly invoked by name. Message passing is key to some models of concurrency and object-oriented programming.

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, Actor model implementation concerns implementation issues for the Actor model.

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.

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

In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. This article reports on the later history of the Actor model in which major themes were investigation of the basic power of the model, study of issues of compositionality, development of architectures, and application to Open systems. It is the follow on article to Actor model middle history which reports on the initial implementations, initial applications, and development of the first proof theory and denotational model.

Join-patterns provides a way to write concurrent, parallel and distributed computer programs by message passing. Compared to the use of threads and locks, this is a high level programming model using communication constructs model to abstract the complexity of concurrent environment and to allow scalability. Its focus is on the execution of a chord between messages atomically consumed from a group of channels.

References

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.