In computer science, unbounded nondeterminism (sometimes called 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. Computer science is the study of the theoretical foundations of information and computation and their implementation and application in computer systems. ... Wikiquote has a collection of quotations related to: Edsger Dijkstra In computer science, concurrency is a property of systems which consist of computations that execute overlapped in time, and which may permit the sharing of common resources between those overlapped computations. ... In computer science, denotational semantics is an approach to formalizing the semantics of computer systems by constructing mathematical objects (called denotations or meanings) which express the semantics of these systems. ...

Originally thought to be impossible to implement

Edsger Dijkstra [1976] argued that it is impossible to implement systems with unbounded nondeterminism. Since it was widely assumed at the time that unbounded nondeterminism was unimplementable, Tony Hoare [1978] suggested that "an efficient implementaton should try to be reasonably fair." This gave rise to the controversy over unbounded nondeterminism. Portrait of Edsger Dijkstra (courtesy Brian Randell) Edsger Wybe Dijkstra (Rotterdam, May 11, 1930 – Nuenen, August 6, 2002) was a Dutch computer scientist. ... Sir Charles Antony Richard Hoare (Tony Hoare or C.A.R. Hoare, born January 11, 1934) is a British computer scientist, probably best known for the development of Quicksort, the worlds most widely used sorting algorithm, and perhaps even the worlds most widely used algorithm of any kind... In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ...

Arguments for dealing with unbounded nondeterminism

Carl Hewitt argued otherwise (the Actor model has the property of unbounded nondeterminism): Carl Hewitt is a US scientist who is an emeritus professor from MIT. He is known for his design of Planner that was the first Artificial Intelligence programming language based on procedural plans that were invoked using pattern-directed invocation from assertions and goals. ... In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ...

• There is no bound that can be placed on how long it takes a computational circuit called an arbiter to settle (see metastability in electronics). Arbiters are used in computers to deal with the circumstance that computer clocks operate asynchronously with input from outside, e.g.., keyboard input, disk access, network input, etc. So it could take an unbounded time for a message sent to a computer to be received and in the meantime the computer could traverse an unbounded number of states.

• Electronic mail enables unbounded nondetermism since mail can be stored on servers indefinitely before being delivered.

• Communication links to servers on the Internet can be out of service indefinitely.

Arbiters are used in Asynchronous circuits to deal correctly with metastability. ... Metastability in electronics is the ability of a non-equilibrium electronic state to persist for a long period of time (see asynchronous circuit). ... Electronic mail, abbreviated e-mail or email, is a method of composing, sending, and receiving messages over electronic communication systems. ... Channel, in communications (sometimes called communications channel), refers to the medium through which information is transmitted from a sender (or transmitter) to a receiver. ... In computing, a server is a software application that carries out some task (i. ...

Nondeterministic automata

Nondeterministic Turing machines have only bounded nondeterminism. Sequential programs containing guarded commands as the only sources of nondeterminism have only bounded nondeterminism [ Edsger Dijkstra 1976]. Briefly, choice nondeterminism is bounded. Gordon Plotkin gave a proof in his original paper on power domains [1976]: Portrait of Edsger Dijkstra (courtesy Brian Randell) Edsger Wybe Dijkstra (Rotterdam, May 11, 1930 – Nuenen, August 6, 2002) was a Dutch computer scientist. ...

Now the set of initial segments of execution sequences of a given nondeterministic program P, starting from a given state, will form a tree. The branching points will correspond to the choice points in the program. Since there are always only finitely many alternatives at each choice point, the branching factor of the tree is always finite. That is, the tree is finitary. Now König's lemma says that if every branch of a finitary tree is finite, then so it the tree itself. In the present case this means that if every execution sequence of P terminates, then there are only finitely many execution sequences. So if an output set of P is infinite, it must contain [a nonterminating computation].

There is also a theorem of set theory called Königs theorem. ... In mathematics or logic, a finitary operation is one, like those of arithmetic, that take a number of input values to produce an output. ...

Indeterminacy versus nondeterministic automata

Will Clinger [1981] provided the following analysis of the above proof by Plotkin: The neutrality of this article is disputed. ...

This proof depends upon the premise that if every node x of a certain infinite branch can be reached by some computation c, then there exists a computation c that goes every node x on the branch. ... Clearly this premise follows not from logic but rather from the interpretation given to choice points. This premise fails for arrival nondeterminism [in the arrival of messages in the Actor model] because of finite delay [in the arrival of messages]. Though each node on an infinite branch must lie on a branch with a limit, the infinite branch need not itself have a limit. Thus the existence of an infinite branch does not necessarily imply a nonterminating computation.

Unbounded nondeterminism in the original and later version of CSP

Consider a program written in CSP [1978]: In computer science, Communicating Sequential Processes (CSP) is a language for describing patterns of interaction. ...

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

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: either the stop message is accepted from X, in which case continue is set to false, or a go message is accepted from Y, in which case n is incremented and Y is sent the value of continue. If Z ever accepts the stop message from X, then X terminates. Accepting the stop causes continue to be set to false, so after Y sends its next go message, Y will receive false as the value of its guard and will terminate. When both X and Y have terminated, Z terminates because it no longer has live processes providing input.

As the author of CSP points out, therefore, if the repetitive guarded command in the definition of Z were required to be fair, this program would have unbounded nondeterminism: it would be guaranteed to halt but there would be no bound on the final value of n. In actual fact, the repetitive guarded commands of CSP are not required to be fair, and so the program may not halt [Hoare 1978]. This fact may be confirmed by a tedious calculation using the semantics of CSP [Francez, Hoare, Lehmann, and de Roever 1979] or simply by noting that the semantics of CSP is based upon a conventional power domain and thus does not give rise to unbounded nondeterminism.

However, the modern theoretical CSP ([Hoare 1985] and [Roscoe 1988 and 2005]) explicitly provides unbounded nondeterminism. In computer science, unbounded nondeterminism (also called unbounded indeterminacy, a title preferred by Carl Hewitt following Niels Bohr; see fairness) 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... In computer science, Communicating Sequential Processes (CSP) is a language for describing patterns of interaction. ...

Power domain semantics

According to Clinger [1981]

The reason unbounded nondeterminism does not appear in conventional power domain semantics is that each element of the power domain is interpreted as a finitely generable subset of the underlying ω-complete domain [see Power domains from incomplete domains ]. In the ω-complete domains that have been proposed (previous to the publication of Clinger [1981]), finitely generable subsets are either finite or contain an element representing a nonterminating or undefined computation, for essentially the same reason that choice nondeterminism is bounded [Plotkin 1976]. In the Actor event diagram domain and its completion, however, the augmented diagrams contain information that can distinguish computations that violate finite delay [of message arrival] from other nonterminating computations. Intuitively, the Actor event diagram domain is incomplete because the computations that violate finite delay [in the arrival of messages] have been thrown out.

In the mathematical area of order theory, completeness properties assert the existence of certain infima or suprema of a given partially ordered set. ... In computer science, denotational semantics is an approach to formalizing the semantics of computer systems by constructing mathematical objects (called denotations or meanings) which express the semantics of these systems. ...

Indeterminacy in the Actor model

According to Clinger [1981] The neutrality of this article is disputed. ...

To return to the proof that choice nondeterminism is bounded and to see why that proof does not work for arrival nondeterminism [of messages in the Actor model], it is first of all not clear that the tree of initial segments of executions sequences of a concurrent program is always finitary, since the alternatives may for example correspond to the wait times allowed by finite delay [Lynch and Fisher 1979; see also Back 1980]. Secondly, an infinite branch does not necessarily indicate a nonterminating computation since the path may violate the requirement of finite delay [in the arrival of messages] and thus not have a limit.

Apparently the designer of CSP stopped short of requiring fairness because at the time languages with unbounded nondeterminism were widely regard an unimplementable [Hoare 1978]. Additionally unbounded nondeterminism would have precluded giving a conventional power domain semantics for CSP.

In contrast indeterminacy is an inherent part of the Actor model (see Indeterminacy in computation). In computer science, unbounded nondeterminism (also called unbounded indeterminacy, a title preferred by Carl Hewitt following Niels Bohr; see fairness) 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... The neutrality of this article is disputed. ...

No unbounded nondeterminism in Concurrent Processes of Milne and Milner

According to Clinger [1981]

Another important proposal, based like CSP on message passing but more abstract than a programming language, is Concurrent Processes [Milne and Milner 1979]. The semantics of Concurrent Processes also uses conventional power domains, so there is no unbounded nondeterminism and a fair merge cannot be specified.

Robin Milner is a prominent British computer scientist. ... In computer science, unbounded nondeterminism (also called unbounded indeterminacy, a title preferred by Carl Hewitt following Niels Bohr; see fairness) 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...

Semantics versus implementation

According to Dana Scott [1980]: This article needs cleanup. ...

It is not necessary for the semantics to determine an implementation, but it should provide criteria for showing that an implementation is correct.

According to Clinger [1981]::

Usually, however, the formal semantics of a conventional sequential programming language may itself be interpreted to provide an (inefficient) implementation of the language. A formal semantics need not always provide such an implementation, though, and to believe that semantics must provide an implementation leads to confusion about the formal semantics of concurrent languages. Such confusion is painfully evident when the presence of unbounded nondeterminism in a programming language's semantics is said to imply that the programming language cannot be implemented.

Fairness

Discussion of unbounded nondeterminism tends to get involved with discussions of fairness.

Hewitt argued that issues in fairness derive in part from the global state point of view. The first models of computation (e.g.. Turing machines, Post productions, the lambda calculus, etc.) are based on mathematics that makes use of a global state to represent a computational step. Each computational step is from one global state of the computation to the next global state. The global state approach was continued in automata theory for finite state machines and push down stack machines including their nondeterministic versions. All of these models have the property of bounded nondeterminism that is: if a machine always halts when started in its initial state, then there is a bound on the number of states in which it halts. The Turing machine is an abstract machine introduced in 1936 by Alan Turing to give a mathematically precise definition of algorithm or mechanical procedure. As such it is still widely used in theoretical computer science, especially in complexity theory and the theory of computation. ... The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ... The factual accuracy of this article is disputed. ... Fig. ... Stack in computing refers to: Stack (data structure) Stack-based memory allocation as opposed to Heap-based memory allocation in computing architecture. ... In the theory of computation, a nondeterministic algorithm is a hypothetical algorithm where computation can branch, choosing among different execution paths in a way that does not depend only on the input and current execution state. ...

Hewitt argued that there is a fundamental difference between choices in global state nondeterminism and the arrival order indeterminacy (nondetermism) of the Actor model. In global state nondeterminism, a "choice" is made for the "next" global state. In arrival order indeterminacy, arbitration locally decides each arrival order in an unbounded amount of time. While a local arbitration is proceeding, unbounded activity can take place elsewhere. There is no global state and consequently no "choice" to be made as to the "next" global state. In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ...

Of course, there is also local fairness as in flipping a "fair" coin by which it is understood that it is possible (all be it extraordinarily unlikely) for the outcome always to be heads.

Questions of fairness are involved in the merging of streams. Clinger [1981] argued

It appers that a fair merge cannot be written as a nondeterministic data flow program operating on streams. The reason is that for any monotonic function

merge: S × S → P[S]

from pairs of input streams to set of possible output stream it must be that

merge(⊥,1^ω)⊆ merge(0,1^ω)

where ⊥ is the empty stream. Since the only fair merge of ⊥ and 1^ω is 1^ω, 1^ω should be an element of merge(⊥,1^ω), but that would mean 1^ω must be an element of merge(0,1^ω) also.

Of course it is easy to define and implement an Actor that behaves as a fair merge of two stream Actors. Merge algorithms are a family of algorithms that run sequentially over multiple sorted lists, typically producing more sorted lists as output. ...

Recent developments in the semantics of CSP

Recently Stephen Brookes [2005] has published a further development of the semantics of CSP which presents solutions to some of the semantic issues that have been encountered. However some significant issues remain. For example, in the semantics of Brookes [2005], the concurrent assignment of a value to a variable is semantically equivalent to a program which terminates abnormally, i.e., In computer science, Communicating Sequential Processes (CSP) is a language for describing patterns of interaction. ...

 [(x:=1)||(x:=2)] = [abort] 

In contrast, for the Actor semantics of Clinger [1981], concurrently sending two write messages with values 1 and 2 to an Actor x acting as a storage would result in x storing 1 and then storing 2 or vice versa and execution would continue normally.

References

• Carl Hewitt, Peter Bishop and Richard Steiger. A Universal Modular Actor Formalism for Artificial Intelligence IJCAI 1973.
• Robin Milner. Processes: A Mathematical Model of Computing Agents in Logic Colloquium 1973.
• 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. Behavioral Semantics of Nonrecursive Control Structure Proceedings of Colloque sur la Programmation, April 1974.
• Irene Greif. Semantics of Communicating Parallel Professes MIT EECS Doctoral Dissertation. August 1975.
• Gordon Plotkin. A powerdomain construction SIAM Journal of Computing September 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.
• Gilles Kahn and David MacQueen. Coroutines and networks of parallel processes IFIP. 1977
• Henry Baker. Actor Systems for Real-Time Computation MIT EECS Doctoral Dissertation. January 1978.
• Michael Smyth. Power domains Journal of Computer and System Sciences. 1978.
• George Milne and Robin Milner. Concurrent processes and their syntax JACM. April, 1979.
• CAR Hoare. Communicating Sequential Processes CACM. August, 1978.
• Nissim Francez, CAR Hoare, Daniel Lehmann, and Willem de Roever. Semantics of nondeterminism, concurrency, and communication Journal of Computer and System Sciences. December 1979.
• Nancy Lynch and Michael Fischer. On describing the behavior of distributed systems in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Jerald Schwartz Denotational semantics of parallelism in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• William Wadge. An extensional treatment of dataflow deadlock Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Ralph-Johan Back. Semantics of Unbounded Nondeterminism ICALP 1980.
• David Park. On the semantics of fair parallelism Proceedings of the Winter School on Formal Software Specification. Springer-Verlarg. 1980.
• Dana Scott. What is Denotational Semantics? MIT Laboratory for Computer Science Distinguished Lecture Series. April 17, 1980.
• Will Clinger, Foundations of Actor Semantics. MIT Mathematics Doctoral Dissertation, June 1981.
• Stephen Brookes, Tony Hoare and Bill Roscoe A Theory of Communicating Sequential Processes JACM. July 1984.
• Carl Hewitt. The Challenge of Open Systems Byte Magazine. April 1985.
• Bill Roscoe. Unbounded nondeterminism in CSP in `Two papers on CSP', technical monograph PRG-67, Oxford University Computing Laboratory. July 1988.
• A. W. Roscoe<sup>1998</sup> : The Theory and Practice of Concurrency, Prentice-Hall, ISBN 0-13-674409-5.
• David A. Schmidt, The Structure of Typed Programming Languages. MIT Press, Cambridge, Massachusetts, 1994.
• Butler, M. J. and Morgan, C. C. Action Systems, Unbounded Nondeterminism, and Infinite Traces Formal Aspect of Computing. 1995
• Luca Aceto and Andrew D. Gordon (editors). Algebraic Process Calculi: The First Twenty Five Years and Beyond' Process Algebra. Bertinoro, Forl`ı, Italy, August 1–5, 2005
• Stephen Brooke. Retracing CSP in Algebraic Process Calculi: The First Twenty Five Years and Beyond. August 2005.
• ^- A. W. Roscoe: The Theory and Practice of Concurrency, Prentice-Hall, ISBN 0-13-674409-5. Revised 2005.