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 )
squeak-dev@lists.squeakfoundation.org