The Pi Calculus, Mobility and JSR-121: First Thoughts

Why is this subject interesting?

A dream still held by many who can think beyond the next bug fix is provably correct software and the mathematical tools for realizing the dream. If sound mappings can be established between JSR-121⁴ and pi calculi there is the potential for strong assertions about applications using the JSR-121 APIs . This will allow architects and developers to move closer to designing quality in and further from the need to stamp defects out.
JSR-121 associations with pi calculus and pi calculus relevance to mobile agent systems will stimulate interest in the isolation APIs.

Are the JSR-121 Isolation APIs really "pi-derived"?

Link can Link instances ("channel names"), Isolate references ("processes"), (limited) "process state" and arbitrary data expressible as bytes as well as specialized types like DBDs¹ and Isolate state events. Study of Milner² suggests that Link seems to be at least as powerful as a pi calculus channel in terms of what can be sent on it. Also, the key quality of channels supporting the sending and receiving of channel names is supported by Link. So overlap between pi calculus and the Link abstraction seems undeniable.

Isolation APIs clearly support full parallelism apart from the Link send/receive rendezvous (perhaps ameliorated by nonblocking links if LinkChannel⁵ makes it into Java).

It isn't yet clear that isolation APIs provide a complete set of mappings to the pi calculus and it seems doubtful that a complete set of ideal mappings to more relevant calculi like delta pi³ can be defined. On the other hand almost all mappings between delta pi and existing Java have been made without anything more intrusive than a preprocessor, so there is room for optimism.

So yes, JSR121 is clearly pi-derived in the sense that it has at least some direct mappings to pi calculus and the potential for the benefit that stems from them.

Does JSR121 offer strong mobility?

No. Control state cannot be reestablished , let alone namespaces or other resources. But this is no worse than for other mobility systems based on Java.

Does JSR121 support weak mobility?

Yes, but to a degree more limited than weak mobility via Java support already in the literature:

Application state is restricted to the subset that is serializable or otherwise compatible with Link transport. Java objects that might be present in an application that are not serializable cannot be moved. That is, isolation APIs are not magical vis a vis mobility constraints already well understood. So a small superset of existing support for mobility via Java is added by the isolation APIs via the Link class. However:
Movement is only within the scope of an aggregate (typically a single computer system but no larger than a cluster with a "single administrative view") and this is more constrained than most other Java APIs supporting mobility. This is among other things a statement of how Link is not really in competition with RMI.

Link will probably offer intrinsically higher performance than the transport APIs supporting mobility within greater scopes.
So JSR-121 supports mobility that is both weak and "geography constrained" but with higher performance potential than Java APIs supporting a wider scope. That is, no free lunch, no surprises.

Some obvious mappings between JSR-121 and pi calculus terms and partial expressions:

PI Calculus	Isolation APIs
Process	Isolate
Channel	Link
a<x> (output msg x on channel a)	a.send(IsolateMessage.new<type of x>(x))
a(x) (input msg x on channel a)	x = a.receive().get<type of x>()
Restriction (channel creation)	Link object instantiation, e.g. a = Link.newLink()

Conclusions

Finding JSR121 relevance to formal methods is a good thing.
There are strong parallels between certain pi calculi elements and JSR-121 abstractions.
It is a tease to suggest that JSR-121v1 has relevance to the field of mobile agent systems except within a strictly limited scope.
JSR-121 does provide a solid foundation for mobility within its defined scope.
The greatest potential of JSR-121 connections to the pi calculi seems to be for designing provably correct systems.
The more sound mappings that can be established between JSR-121 and pi calculi (e.g. delta pi) the better.

References and Footnotes

Descriptor Bearing Doober: an IsolateMessage that wraps a Java I/O object (e.g. Socket) typically containing an 0pen OS level file descriptor. This cute acronym is meant to draw attention to a novel feature that JSR-121 adds to Java, one that even most Unix and Windows programmers are not familiar with.
Communicating and Mobile Systems, R. Milner, 1999.
Mobile Process Calculus API in Java, Final Report, Daniel Lister, June 2002.
JSR-121 draft specification, http://jcp.org/yadayada
The java.nio.channels.LinkChannel class proposed by JSR-121 for consideration as part of JSR-203 would further close the terminology gap with pi calculus.

Pete@Soper.US February 28, 2003