Global State Machines Inadequate (contra Dijkstra and Gurevich et. al.)

Global State Machines are an inadequate foundation for computation (contra Dijkstra and Gurevich et. al.)

A principle limitation relates to the inability of Global State Machines to represent concurrency. See What is computation? Actor Model versus Turing's Model

       Global State Machine References

Andreas Blass, Yuri Gurevich, Dean Rosenzweig, and Benjamin Rossman (2007a)
   Interactive small-step algorithms I: Axiomatization
   Logical Methods in Computer Science. 2007.
Andreas Blass, Yuri Gurevich, Dean Rosenzweig, and Benjamin Rossman (2007b)
   Interactive small-step algorithms II: Abstract state machines and the characterization theorem
   Logical Methods in Computer Science. 2007.

Edsger Dijkstra.
   A Discipline of Programming 
   Prentice Hall. 1976.
Edsger Dijkstra and A.J.M. Gasteren.
   A Simple Fixpoint Argument Without the Restriction of Continuity
   Acta Informatica. Vol. 23. 1986.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Plotkin proof: a global state machine has bounded nondeterminism

Plotkin's proof that a global state machine has bounded nondeterminism:

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.

Consequently, either
* The tree has an infinite path. ⇔ The tree is infinite. ⇔ It is possible that P does not halt.
If it is possible that P does not halt, then it is possible that that the set of outputs with which P halts is infinite.
or
* The tree does not have an infinite path. ⇔ The tree is finite. ⇔ P always halts.

If P always halts, then the tree is finite and the set of outputs with which P halts is finite.

What is unbounded

What is unbounded non-determinism useful for?

I'm not even convinced my languages should be pervasively Turing complete.

What is the use of not being Turing complete?

The only reason to not be Turing-complete I can think of is for theorem provers (which by their nature require total functions), and rejecting Turing-completeness means rejecting a significant set of terminating algorithms without their implementers resorting to dirty hacks like putting decrementing counters in the arguments of recursing functions (and then, if you can put a sufficiently large number in such, such as the largest natural number one can represent reasonably, doesn't that basically defeat the point of not being Turing-complete, as can waiting an unreasonably long but finite period of time (e.g. until the Sun expands and engulfs the Earth) be, from the user's standpoint, functionally equivalent to diverging?) And how can one avoid such hacks resulting in unreasonable waits but by putting an execution time limit on one's computations, but then is going over such a limit not equivalent to diverging anyways?

And is not being Turing-complete not enough, as one is still running one's code on a machine with finite virtual memory space, and is not throwing an out-of-memory exception diverging anyways? I.e. rejecting Turing-completeness does not actually make one's functions total.

(This might be possible if one uses an execution and memory model sufficiently restrictive that one can statically determine a maximum amount of memory that a program will allocate ahead of time, and thus be able to preallocate all the memory needed such as to be able to limit throwing out-of-memory exceptions to the very beginning of program execution (you would have to pre-zero all this memory too so as to avoid problems with overcommiting, so as to force out-of-memory events to occur immediately). However, this is likely to force one to a model as limiting as, say, the memory model of C without malloc() or C++ without new and with recursion being forbidden.)

Not Pervasively Turing complete

A language that is not 'pervasively' Turing complete might still be Turing complete, just not pervasively so. Maybe Turing completeness arises only from an implicit outer-most loop. Such a scenario, for example, may involve a language that models processes as taking steps: we might ensure that each step completes, so we can progress to the next step. Similarly, if we have UI event handlers or observer-pattern callbacks, we might wish to ensure that those operations terminate.

Any algorithm that doesn't fit our 'provably terminating' model can be made incremental: we don't know how many steps it will take, but each step will terminate. This can be advantageous in many ways - e.g. we can show incremental work based on intermediate states, or we can cleanly shut down the sub-process if we decide we don't want it anymore.

waiting an unreasonably long but finite period of time (e.g. until the Sun expands and engulfs the Earth)

There are more extreme forms of being 'not pervasively Turing complete', e.g. where we might control the amount of (per step) computation relative to some polynomial bound. (I've certainly contemplated tracking big-O in the type system.)

And is not being Turing-complete not enough

"Not being Turing complete" is not a goal. Rather, it's a consequence of design decisions with which Turing completeness is inconsistent.

What is the use of being Turing-complete?

Well, since (as you say) your implementation cannot be Turing-capable, which would you rather have, arbitrary implementation restrictions or principled ones? (This is not a rhetorical question.)

Bounded nondeterminism in CSP

Hoare was convinced that unbounded nondeterminism could not be implemented and so the semantics of CSP specified bounded nondeterminism.

[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 := false;
                      Y!continue
              []        
          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.

The upshot was that Hoare was convinced that unbounded nondeterminism is impossible to implement. That's why the semantics of CSP specified bounded nondeterminism. But Hoare knew that trouble was brewing in part because for several years proponents of the Actor Model had been beating the drum for unbounded nondeterminism. To address this problem, he suggested that implementations of CSP should be as close as possible to unbounded nondeterminism! But his suggestion was difficult to achieve because of the nature of communication in CSP using nondeterministic select statements (from nondeterministic state machines, e.g., [Dijkstra 1976]), which in the above program which takes the form [X?stop( ) → ... [] Y?go( ) → ...]. The structure of CSP was fundamentally at odds with guarantee of service.

Using the semantics for CSP, it was impossible to formally prove that a server actually provides service to multiple clients (as had been done previously in the Actor Model). That's why the semantics of CSP were reversed from bounded non-determinism [Hoare CSP 1978] to unbounded non-determinism [Hoare CSP 1985]. Bounded non-determinism was but a symptom of deeper underlying issues with nondeterministic transitions in communicating sequential processes (see [Knabe 1992]).

Implementation

The problem with unbounded nondeterminism is that it requires unbounded memory to implement. In the case of CSP (with fair implementations of guards) it requires counters of unbounded size. In the case of the Actor model it requires the interconnect between nodes to act as a buffer of unbounded size.

There are several real implementations of the CSP semantics in hardware. Removing the requirement for unbounded memory made it possible to implement the model in silicon using constant bounds: the transputer at Inmos, the XMOS core etc. Searching for an implementation of the Actor model I can only find simulations written in high-level languages which rely on unbounded heaps in the language.

Turing Machines cannot be implemented, although they can be simulated. We can simulate a subset of machines in software, but this is not the same as building an artifact that is a real Turing Machine. The Actor Model can be simulated in software, but it cannot be implemented as a real computer any more than a Turing Machine can.

The upshot was that Hoare was convinced that unbounded nondeterminism is impossible to implement.

Hoare was entirely correct, and your model for distributed software would require arbitrarily large buffers between all points on the interconnect. This is not possible to implement and so any theoretic advantages will not translate to practical gains.

Why did Hoare change CSP to unbounded nondeterminism?

Why did Hoare change CSP to unbounded nondeterminism?

Did he?

The only claim that I can find right now is yours - on various websites. Could you provide a more detailed citation / quote to back up your claim. There is a body of work in the early 90s that looks at adding unbounded nondeterminism to CSP. I can't really see how that would fit with the synchronous approach to message passing. More detail would be useful.

Unbounded nondeterminism in CSP

Please see the following book:

Bill Roscoe. The Theory and Practice of Concurrency Prentice-Hall. Revised 2005.

Doesn't help

Roscoe published work on adding unbounded nondeterminism to CSP in 1990. Pointing to a book that he wrote 15 years later doesn't really help. Could you provide a detailed citation (either an article, or a specific quote from a book) to indicate that Hoare did add unbounded nondeterminism to CSP?

Unfortunately I don't know date that CSP changed

Unfortunately, I don't know date that CSP changed to unbounded nondeterminism. Roscoe's book has some historical background.

I'll dig out a copy and take

I'll dig out a copy and take a look. But on the question of implementation - what is your view on how unbounded nondeterminism could be implemented? Is it something "real" that we could physically build and use, or is it simply useful as a modelling technique?

Implementing unbounded systems requires ever more resources

Implementing unbounded systems requires ever more resources.

Configurations versus Global States

Computations are represented differently in State Machines and Actors:
1. State Machine: a computation can be represented as a global state that determines all information about the computation. It can be nondeterministic as to which will be the next global state, e.g., in simulations where the global state can transition nondeterministically to the next state as a global clock advances in time, e.g., Simula [Dahl and Nygaard 1967].
2. Actors: a computation can be represented as a configuration. Information about a configuration can be indeterminate. (For example, there can be messages in transit that will be delivered at some indefinite time.)

Petri nets?

Perhaps I'm off the mark here, but it strikes me as peculiar that there is no mention of Carl Adam Petris dissertation "Kommunikation mit Automaten" or any other reference to Petri nets as a model of concurrent systems. Seems to me that the hypothesis that a global state machine (i.e. a model in which the state is assumed to be global and changes are also assumed to have a global effect as well as depending on the global state) is very similar to the Petris idea that global state when taken to extremes is physically impossible, hence the need for local state and local state changes. And if you are so inclined you can view state machines as just a special case of plain place/transition nets.

Petri Nets are a Global State Model

Petri Nets are a Global State Model because of the transition rule that tokens from physically separated places are removed simultaneously.

What do you do about the arbiters, though?

Hi Carl,

I've been thinking a lot about arbiters and the assumptions we tend to make about arbiters, and how it limits our design options.

Going forward, the speed of light will be our bottleneck. There will no longer be such things as liquid bottlebecks and 'elastic' clouds, because eventually the rubberband snaps.

I attempted to create a programming language based on patterns from control theory, such as Predictive Model Control, but I gave up because the bottleneck to implement many real scenarios is too severe due to physics of the real world; for example, to spin up a new slave server requires creating a copy, which also eats bandwidth and has real propagation delay. Propagation delay is the fundamental issue at the speed of light, as communication protocol design becomes THE dominating factor in system design. Further, most control laws have to be driven by 'human hints' rather than detecting periodicity in a system using characteristic functions such as those found in machine learning... or the system will be vulnerable to 'Black Swans'.

Awhile back, I asked you about exactly this problem, and your answer back then was 'Actor Model will get better'. Have I still stumped you?

Please see discussion of arbiters in "What is Computation?"

Please see discussion of arbiters in What is Computation?

Arbiters can take indefinite time

However, I am asking the opposite scenario. Assume an arbiter working at the speed of light.