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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Wed, 11 May 2016 22:16:48 -0700 (PDT)*References*: <78da9a98-0d9e-42b8-af55-cc39813bc21c@googlegroups.com>

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

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

**Follow-Ups**:**Re: Robin Milner Space and Motion of Communicating Agents***From:*Ron Pressler

**References**:**Robin Milner Space and Motion of Communicating Agents***From:*fcol . . .

- Prev by Date:
**Robin Milner Space and Motion of Communicating Agents** - Next by Date:
**modeling resets** - Previous by thread:
**Robin Milner Space and Motion of Communicating Agents** - Next by thread:
**Re: Robin Milner Space and Motion of Communicating Agents** - Index(es):