[moca] shooting from the hip: Mobility FAQ ?

[Martin Berger <martinb@xxxxxxxxxxxxxx>]

> Qu1: "Why the he.. do you have so many different calculi?

(counter-question: why are there so many natural numbers?)

(An1a) because we may not yet have hit upon the right one. we may
have but we are not sure. part of the problem is that the
questions process calculi are the answer to are themselves
not really well defined. semantics is a circular process, the
answers refine the questions and vice versa -- as always in
interesting science!

(An1b) because we model computation at different levels of abstraction
and for different purposes, hence the need for different models.

>       Can you provide a nice comprehensible roadmap to them?

not yet. wait 10 years!

>       Are there any conclusions to be drawn from this variety?"

semantics is hard and interesting!

names are fundamental.

mobile hiding is fundamental.

coinduction is great.

everything is interaction.

composition and hiding are two different concepts that should remain
separate.

unrestricted sums are not a good idea.

observers are always
also processes in the same formalism.

start with an untyped formalism and then remove the processes you don't
want by types.

encodings, encodings, encodings.

labelled bisimulations are a great tool for efficient reasoning about
computations.

> Qu2: "Why the he.. do you have
>       so many bisimulations in the pi-calculus?"

(An2a) a variant of the answer to Qu1: because we may not have found
the right one, or we may have found the right one, but we might not
know it. part of the problem is that the
questions bisimulations are the answer for are themselves
not really well defined. semantics is a circular process, the
answers refine the questions and vice versa -- as always in
interesting science!

(An2b) i do think that the question misrepresents process calculi.
a process calculus should not be confused with the syntax of
its processes. the latter are but a means to define what really matters,
namely the syntax quotiented by the chosen congruence. syntax
without congruence/observation is meaningless. of course it would
be better if we could define something isomorphic to the quotients
directly, without recourse to equivalences, but we just don't know
how to do that.

(An2c) the question is misleading for another reason: there are
only two notions of congruence really: barbed congruence
and reduction congruence, and they even coincide for nice
calculi. the many notions of bisimulations are just a consequence
of the fact that it is difficult to use barbed congruence
and reduction congruence for actual reasoning, so we come up
with sound approximations that are easier on the brain. for example
labelled bisimilarities are neat for  showing that two processes
are identical and traces are the tool of choice if
we want to establish two processes as distinct.

of course this is a bit  whiggish, because historically labelled
bisimulations came first. but we know better now ...

to be sure, in many situations the calculus one gets by quotienting
with barbed/reduction congruence is not what one needs to model
this or that phenomenon. however, this is not a failure of the
congruence, it just shows that you have chosen the wrong calculus
to start with: one of the great features of process calculi is
that the are atheistic, that is, they allow only other processes
as observers, no calculus external notion of observation. I think
this is a great feature of process calculi and should not be
given up lightly. if quotienting with reduction/barbed congruence does
not give you what you want, you need to enrich/reduce/modify the
underlying syntax and/or dynamics.

> Qu3: "What are the (killer-) applications?"

the long term goal is: giving precise and tractable (compositional)
foundations to all of computation (work in progress) form high level
languages to assembly, and possible below.

more mundanely: aiding the development of
better tools, program logics, abstractions and typing systems
for concurrent and distributed programming.

one successful microsoft product (biztalk/xlang) is based on
pi-calculus.

> Qu4: "What practical thing can you do with pi/ambients that
>       you cannot do already with CCS/CSP/ACP?"

counterquestion: is there anything interesting/beautiful that
you can do with with CCS/CSP/ACP?

pi-calculi have been used to fully abstractly encode PCF, system F
and various other well-studied languages. which other formalism
has been used to similar effect?

> Qu5: "What, after all, are the
>       main contributions of >10 years of 'mobility'?"

a much better understanding of the importance of naming and
its role in computation. a well developed and general mathematical
theory of program equivalences/congruences and reasoning tools.
typing systems,  encodings of imperative, functional and OO, logics,
integration of (some) security issues and process calculi.

> Qu6: "Why should pi/ambients be considered
>       more fundamental than CCS/CSP/ACP?"

I don't know about ambient, but the results for pi are just more
profound and beautiful than those for CCS/CSP/ACP. of course
this is just an aesthetic preference and i do not wish to minimise
the insight gleaned from pi's predecessors, but that's my strongly
held feeling!

> Qu7: "Can it be implemented?
>       Has it been implemented?"

yes, yes. but on the whole, process-calculists are not so interested
in coding and coders don't read our papers, so cross fertilisation
has been somewhat lacking.

> Qu8: "How can you use for security?

notions of infomation flow are well-developed for pi. and then
there's spi!

>       Why should it be considered better than others?"

we are ultimately interested in the security of the code we actually
execute. hence we need to be able to reason about that directly, not
about some model. so we need to be able to reason about full languages
like Java or C, not just some tiny fragment. Most other formalisms
have not taken up the challenge to model full languages yet
(ASMs being the exception, but they can't handle concurrency properly
i suspect). pi seems furthest ahead.

> Qu9: "Why all this fuzz about encodings?"

To be able to reason about real systems you will have to deal with
multiple languages. if you have fully abstract encodings of all these
languages into one formalism (the universe), you can compile all your
programs, written in multiple languages, down into the universe, do
reasoning there, using just one formalism, and then push the reasoning
results back up to the original programs, because your encodings are precise.
(things are a bit more complicated then that, but that's the essence). no
encodings, no cross-language reasoning.

martin

 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html