Unbounded nondeterminism

From Wikipedia, the free encyclopedia

You have new messages (last change).

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.

Contents

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

[edit] Arguments for dealing with 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 nondeterminism since mail can be stored on servers indefinitely before being delivered.

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

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

[edit] Unbounded nondeterminism in the original and later version of CSP

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.

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

[edit] 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).

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

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

[edit] 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 → 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.

[edit] 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:=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.

[edit] 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. Roscoe1998 : 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.
  • Carl Hewitt, What is Commitment? Physical, Organizational, and Social COIN@AAMAS. April 27, 2006.
Retrieved from "http://en.wikipedia.org../../../u/n/b/Unbounded_nondeterminism.html"