Re: [moca] Locations?

[Sanjiva Prasad <sanjiva@xxxxxxxxxxxxxxxxx>]

Uwe Nestmann write:
> "m" == martinb  <martinb@xxxxxxxxxxxxxx> writes:
>
> m> I would be interested to hear opinions on what "is" the
> m> essence of locations.  my current and simple-minded take
> m> is that locations are units of failures, locations are
> m> partial computations that can fail independently.
>
> I agree with this view, depending on the setting, because we
> also use it (calling it "site") in this sense in our
> forthcoming CONCUR paper.

This was the position taken by Roberto Amadio and me (also colleagues
in the Facile project) in our original paper of 1994 which seems to have
opened this can of worms, and further developed by Roberto in his
subsequent papers which bring together mobility, failure, locality.

At that stage, we  also conceived of "concrete" locations as the units at
which resource allocation and management took place (consider address
spaces or Unix processes if you like, together with some kind of
scheduling over these resources), and as the entities between which
processes migrated.

The DJoin view should properly be seen as an constrained language which
ensures that the expensive distributed consensus is unnecessary.  The
"unit of migration" approach in Djoin was somewhat novel, though in the
Facile implementation we allowed for migration of running processes,  by
"marshalling" and "unmarshalling" (see the work of Fritz Knabe).  The full
extent of location as "unit of mobility" and "admin domain" is highlighted
in the Ambients work and after (M-calc), where you can conceive of
computation as mobility.

Only a part of the programme envisaged by us about 10 years ago (and
enhanced substantially by others) has been studied -- for instance, only
stop/crash models for failure have been explored, and the general
framework of "unit of resource allocation" deserve a lot more work.

> But it has also been used as "unit of migration" (Dist Join).
> In Nomadic Pi and Dpi, locations have yet another twist,
> but I rather let the invontors comment on this. :-)

Yes, the work of Peter Sewell and his collaborators is significant
and also provides important perspectives on the variety of approaches
(not least being Hennessy-Riely).


> And of course one should be aware not to confuse with the
> 80s' version of located process calculi by Hennessy, Kiehn,
> and many others ...

Published in the 90s, actually.  There is an excellent survey
on localities by Ilaria Castellani in Handbook of Process Algebras.

For desserts, consider analysis of an authentication protocol, say
Needham-Schroeder PK in Spi (or even in a subset of the pi calculus with
tables studied by Roberto and me).   For the ANALYSIS, the two
protagonists -- even though they are distributed, i.e., can fail separately
and do not share a namespace --- form one locality (the system)
and the attacker forms another locality (the environment).  Establishing
secrecy amounts to showing "parochiality" -- that certain information
remains local to the system.

Cheers,
Sanjiva



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