Andrew C. Greenberg wrote:

>
> The bottom line is this: sequential programming can be verified (proved)
> correct by straight-line Hoare or Dijkstra-style reasoning.  Absent
> simplifying invariants, concurrency without straight-line execution
> requires proof that EVERY ONE of the combinatorial explosion of possible
> executions are correct, or properly sequenced, PLUS an additional proof
> of no deadlock.  Whether or not we attempt to formally validate our
> code, the cerebral effort needs to be made informally.
>
> It is bad enough to try to agonize over the cases of state-change in a
> simple loop (and for beginners, hard enough to comprehend the notion of
> a loop invariant).  Imagine doing this for every line of code!
>

I think you've just provided another argument against adding threads to a
sequential model of computation. Consider in contrast the actor model of
computation pioneered by Carl Hewitt. Since all state is encapsulated in
actors (or concurrent objects if you prefer) and all communication is by
asynchrounous message passing you don't need to consider all possible
interleavings of subprogram executions. The only non-determinism is due to
the arrival ordering of messages. Each actor just pops a message off its
incoming queue and processes it. Reasoning about invariants that an actor
maintains isn't harder than reasoning about invariants in sequential code.

Earlier in this thread there was a discussion of messages like "increment
balance by" rather than "set balance" and "get balance". An important point
underlying this is that "increment balance by" is a commutative operation so
arrival ordering does not affect the resulting state when the actor has
finished processing incoming messages. One can't always stick with
commutative operations but it often simplifies things.

Another recent message mentioned Linda and tuple spaces. I don't like the
lack of modularity and scalability of tuple spaces but the major appeal they
have is that they are insensitive to the order of reads and writes (since
reads that occur too early suspend until the matching write happens). Again
concurrency needn't make it hard to reason about your program if you have a
decent model of concurrent computation.

Best,

-ken kahn ( www.toontalk.com )