Unbounded nondeterminism
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.
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.
Carl Hewitt [2006] argued otherwise (the
Actor model has the property of unbounded nondeterminism):
*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.
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]:
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 is 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].
Indeterminacy versus nondeterministic automata
Will Clinger [1981] provided the following analysis of the above proof by Plotkin:
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.
Consider a program written in CSP [1978]:
[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.
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.
According to Clinger [1981]: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 regarded as 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).
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.
According to
Dana Scott [1980]::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.
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.
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.
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.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.,
[(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.* 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: 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.
*Carl Hewitt. The repeated demise of logic programming and why it will be reincarnated What Went Wrong and Why: Lessons from AI Research and Applications. Technical Report SS-06-08. AAAI Press. March 2006.
