|
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. 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. Arguments for dealing with unbounded nondeterminism Carl Hewitt 2006 argued otherwise (the Actor model has the property of unbounded nondeterminism): 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: 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 in 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. Unbounded nondeterminism in the original and later version of Communicating sequential processes|CSP Consider a program written in CSP 1978: | 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. 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 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. Indeterminacy in computation|Indeterminacy in the Actor model 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). 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 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. Semantics versus implementation 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. 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. Hewitt argued that there is a fundamental difference between choices in global state nondeterminism and the arrival order indeterminacy (nondeterminism) 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 → PS 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. 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., |(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. | |||||||
|
| ||||||||
 |
|
| |