[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Robin Milner Space and Motion of Communicating Agents

Hi Frank,

This group is about TLA+ and its tools.  TLA+ is a language, based on
the logic TLA, for precisely describing algorithms and high-level
system designs.  It is unlikely that this group is what you're looking
for.  To advise you if it is or where else you should look, I need to
understand what you are looking for.

You wrote that you became interested in concurrency and want to learn
about its concepts and issues.  The problem is that "concurrency"
meant something completely different for Robin than it does for me. 
To me, the field of concurrency encompasses a body of algorithms and
a few impossibility and complexity results.  Perhaps the most important
of the impossibility results is the Fischer, Lynch, and Paterson (FLP)
theorem that is described on the Web as follows:

   In a distributed system with asynchronous message delivery, no
   algorithm can guarantee to reach a consensus between participating
   nodes if one or more of them can fail by stopping

The preeminent conference on this subject has been PODC. I will call
that subject Dijkstra concurrency, since he began it.  I will let
Milner concurrency be the subject that Robin meant by the term
concurrency.  I believe he originated it with his work on CCS
(Calculus of Concurrent Systems), and I think its preeminent
conference has traditionally been Concur.  I believe that only one of
the 82 papers cited in the book by Robin that you mention has had even
the slightest influence on Dijkstra concurrency.  (That one is Hoare's
paper on CSP, which inspired a handful of long-forgotten papers in the

The relevance of Dijkstra concurrency to practical system building is
obvious, though for quite a few of the algorithms studied it's hard to
see any application yet.  I will leave it to others to comment on the
practical relevance of Milner concurrency.  The only one I've observed
is that it has inspired specification languages and tools that have
seen some use in industry.

TLA, like Robin's bigraphs, is a formalism.  Formalism has played no
significant part in the discovery of any results in Dijkstra
concurrency.  (Results in Milner concurrency seem to be mostly about
formalisms.)  TLA and I/O Automata have had some influence on how
algorithms are described and proved correct.  I've found that TLA has
helped me to think more clearly about what correctness of algorithms
means.  But you can't learn Dijkstra concurrency by studying TLA, nor
by studying any of the formalisms from Milner concurrency.  I intended
the TLA+ Hyperbook to have a track about some simple principles of
Dijkstra concurrency, and it contains one or two chapters of that
track.  However, it's not now a very good introduction to Dijkstra
concurrency, and I don't know if it ever will be.

So, are you interested in Dijkstra concurrency, Milner concurrency, or
something else?