[concurrency-interest] Re: CSP, the pi-calculus and CPA-2005
miles at milessabin.com
Fri Sep 2 04:16:59 EDT 2005
> Thanks to Miles Sabin and Peter Soper for their replies.
> Miles wrote:
> > I think you'll find that many of the people on this list have an
> > interest in process algebras in one way or another. But I'm not
> > quite so surprised that they don't get discussed here ... the
> > process algebra approach to concurrency is very different from the
> > threads, locks and shared state approach that's hard-wired into
> > Java and reflected in JSR 166.
> No, there's a misunderstanding here about what process algebra
> Regarding threads, locks and shared state there is plenty on offer -
> like formal characterisations that allow formal reasoning and
> automated model-checking. In turn, this leads to precise design of
> the various high-level locking mechanisms you want, correct
> implementation, correct low-level code generation ... all the way
> down to correct and fast hardware support ... all the way up to
> correct applications.
No argument here ... if you look at the Java Memory Model documents
produced by JSR 133 you'll find exactly that. But this only takes us
from the machine level to a level somewhat below that addressed by JSR
> CSP/pi mechanisms are extremely primitive, have a rich mathematics
> and can be formed into patterns that capture any synchronisation
> mechanism you fancy - some will be more useful than others, of
> course! For instance, CSP "events" are the basis for channel
> communications (all sorts), barriers (multiway synchronisation) and
> pretty much anything.
> Again, the point is that it's easy to express this stuff formally and
> that we should do so. Apart from anything else, it makes their
> implementation and applications using them amenable to automated model
> checking ... which can save months/years of debugging.
Understood. But this isn't much practical help to the people who are the
intended consumers of java.util.concurrent. From there up to the
application level things get much more complicated, hence much harder
to specify formally, particularly when you lack first-class language
support for your formalism or programming model of choice.
One of the most common problems here is that typical applications have
to deal not just with the intrinsic sources of concurrency supported by
a particular programming language, but also with concurrency due to
network interaction. This isn't particularly well integrated in Java
(you can't, for example, _directly_ wait on both a monitor and I/O), or
in any other mainstream programming language that I'm aware of (Erlang
comes close, but I'm not sure it could really be characterized as
Systematic handling of failure and cancellation are probably the next
two most common problems, and whilst they're non-negotiable for
production quality systems, they're rarely handled smoothly by
Speaking anecdotally, I've found the concurrent hierarchical state
machines model extremely helpful when designing network applications.
But the translation from a formal specification to running Java code is
an extremely delicate process, one which is most certainly not
In summary: I actually agree with almost all you say, I just don't think
that Java (but not just Java) provides an environment which supports
the direct application of these techniques other than as informal
> Miles added:
> > FWIW, JSR 121, the Java Isolation API, has a CSP/pi-ish feel to it:
> > communication is based on message passing rather than shared state,
> > communication channels can be passed across communication channels
> > for scope extrusion. Pete Soper's collected various things you
> > might find interesting here,
> Thanks for this! With Isolates, I guess you were forced into a
> CSP/pi-like channel mechanism, :).
> Yes, there is a nice, happy and useful relationship. The Link
> mechanism is a little different to both CSP and pi - being bound to
> both Isolates (one at each end). In CSP/pi (and in JCSP/occam-pi),
> channels are independent entities usable by any process that lays its
> hands on them. When you create them, you just create them -
> processes can use them if they can see them and can take it in turns,
> which is a bit more flexible. Language (algebra) rules prevent
Yes, we were aware of this at the time. There are a variety of
implementation reasons which make unbound Links problematic. I hope a
revision of JSR 121 will support them one day, but for now I'd just
like to see a release of what we've done so far.
If you have any comments on the isolation API we'd be delighted to hear
them ... the best place would probably be the isolate-interest list ...
subscription details here,
More information about the Concurrency-interest