Robin Milner Space and Motion of Communicating Agents
fcol...@gmail.com
I'm looking for a way to learn about these concepts and issues. I've come across TLA.
Is there an overlap between Leslie Lamport's work and Robin Milner's work?
I'd like to find an active community which will help me learn.
Is this the right place? Should I look somewhere else? I've searched this group for "Milner" and didn't see anything.
Leslie Lamport
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
80s.)
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?
Leslie
Ron Pressler
Going off on a tangent, but If I were to reduce TLA+ to a (perhaps obscure) buzzphrase, I’d say it is “theory B for (and by) theory A people”. This is felt not only in the choice of the extremely general computational model of abstract state machines as opposed to some more specific algebra (or “calculus”), but also in the emphasis on and interest in how “plain engineers” can (and do) put it to use in practice. I think that this emphasis (and even interest) is sorely lacking in some of the theory B work, which may result in the real-world efficacy of some of its most interesting work remaining forever unknown.
While it is true that TLA+ is completely orthogonal to PL concerns, I do think that there is some real competition here, certainly in the approach (and I’m sorry if I’m stirring a pot which should not be stirred). Even though TLA+ is a formal language, I think — and correct me if I’m wrong — that it is firmly in the verification camp, which basically says “express your program how you like, we’ll give you tools to reason about it”, while the PL camp says, “we’ll give you tools to express programs in a certain way, and if you do, they’ll be easier to reason about”. I guess that the PL people would say that their very approach would inevitably result in fewer of their attempts being adopted (it’s easier to adopt a tool that fits how you already work, than a tool that requires you to change how you work to fit with it), but they hope that those few ideas that eventually do get adopted would have a long lasting, revolutionary impact. In a way, it is a competition between pragmatists and idealists, I think. As a "plain engineer" practitioner, I, for one, would be very interested in seeing a panel discussion between the two different camps.
Leslie Lamport
Ron's post raises two questions. The first is, do we need to specify
programs in a higher-level language before implementing them in a
programming language? People who design PLs would say no, their
languages make what the program does so obvious that no higher-level
description is needed. I think the first PL for which this was
believed to be true was FORTRAN. It's not true for FORTRAN and I don't
think it's true for any existing general-purpose PL--certainly not
when it comes to implementing distributed systems.
It would be nice if there were a PL that made higher-level specs
unnecessary. I think many people working on Milner concurrency have
that as their goal. I believe it would be possible to compile TLA+
specs that use a specific way of describing interprocess communication
into adequate code for a useful class of distributed programming
problems. Testing that belief would be an interesting research
project. I believe that if specs separate from programs are ever made
completely unnecessary, it will not be by PL development. Rather, it
will come through advances in machine learning that allow code to be
generated from something that looks more like a TLA+ spec than like a
program in any currently envisioned language. But that is pure
speculation, and should not be taken seriously.
The current need for specs as well as programs raises the second
question: should those specs look as much as possible like programs to
make them easier for computer engineers to write? I think most
engineers would answer yes. I say no. I think the most important
function of writing a spec is to make the engineer think clearly about
what she is building. I have found conventional programming languages
to be impediments to clear thinking. TLA formalizes the way I learned
over many years to think about concurrent algorithms--the heart of
Dijkstra concurrency. I developed TLA+ to be a language that forces
engineers to think that way about their concurrent systems, rather
than the way PLs lead them to think.
to justify them properly. I would be interested in knowing how
engineers who have used TLA+ in building distributed systems answer
them, and why.
Leslie
Frank Colcord
Frank