[concurrency-interest] Re: CSP, the pi-calculus and CPA-2005

Miles Sabin miles at milessabin.com
Fri Sep 2 04:16:59 EDT 2005


P.H.Welch wrote,
> 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
> offers.
>
> 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 
166.

> 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.
<snip/>
> 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 
mainstream).

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 
specification languages.

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 
correctness-proof-preserving. 

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 
guidelines.

> 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, :).
<snip/>

Indeed.

> 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
> confusion.

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,

  http://www.bitser.net/isolate-interest/

Cheers,


Miles


More information about the Concurrency-interest mailing list