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

P.H.Welch P.H.Welch at kent.ac.uk
Thu Sep 1 18:03:48 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 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.

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.

Shared state?  Easy!  Let x be a variable visible to many threads.  Then:

  Var (x, value) = load.x!value -> Var (x, value)
                   []
                   store.x?newValue -> Var (x, newValue)

is a process allowing its use by any number of threads (= other processes).
In the above, "Var" is a generic variable process, "x" is an integer specific
to a particular variable (e.g. it may be its address) and "value" is some
initial value for that variable.  The channel names "load" and "store" reflect
the point of view of processes using the variables.

Any process knowing "x" can now use the variable.  For instance, an assignment:

  x = y

is modelled as the CSP process:

  load.y?tmp -> store.x!tmp -> SKIP

which looks interestingly like a compilation to machine code, though to a machine
that is formally specified, :).

Of course, there is absolutely no protection against arbitrary interleaving of
loads and stores on the same variable by multiple processes - the point being
that such problems fall naturally into the scope of CSP.  Fixing them, through
higher level constraints ("healthiness conditions") can now begin.

Another example: variables with various "atomic" update operators ...

  AtomicVar (x, value) =
    load.x!value -> AtomicVar (x, value)
    []
    store.x?newValue -> AtomicVar (x, newValue)
    []
    getAndSet.x?newValue -> getAndSetReply.x!value -> AtomicVar (x, newValue)
    []
    compareAndSet.x?expect?update ->
      (compareAndSetReply.x!true -> AtomicVar (x, newValue) <| expect = value |>
       compareAndSetReply.x!false -> AtomicVar (x, value)
      )

etc.  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.  CSP has the commercial FDR ("Failures-
Divergences-Refinement") model checker of Formal Systems (Europe) Ltd:

  http://www.fsel.com/software.html

It's commercial - you have to pay (I have no relationship with Formal Systems!),
though it's cheap for university research.  But it's really useful.

A while back, we had to build a formal (CSP) model of the standard Java monitor
mechanisms (synchronized/wait/notify/notifyAll).  The trickiest part was making
as sure as possible that we had captured all the informally expressed semantics
from the original "specifications" - an impossible thing to prove, of course.
Anyway, the CSP modelling is quite short - slides 20-36 of:

  http://www.cs.kent.ac.uk/projects/ofa/jcsp/csp-java-model.ppt

The reason we had to do this was to correct the JCSP implementation of CSP
external choice, [] - the JCSP "Alternative", where a process waits passively
for any one of a number of events to occur and reacts accordingly.  We released
JCSP back in 1997 but a bug in its "Alternative" didn't show up till 1999, when
it caused a bit of a panic!  Took a whole week to "fix".  Concerned, we built
the CSP model of Java monitors and could then apply FDR to check that our Java
implementation of choice was equivalent to a direct CSP choice.  Applying the
check to our original implementation threw up the counter-example trace that
yielded the deadlock our users had encountered.  The check took about just
a few (< 5) seconds.  Really should have done that way back!  Anyone interested
can look at the rest of the slides above or read the paper:

  http://www.wotug.org/paperdb/send_file.php?id=44

which also contains the formal model of Java monitors.  This paper is from 2000.
Are there other formal specifications of this?  If not, why ... ?

BTW, JCSP is outlined in the final chapter of Doug Lea's book and is available
from:

  http://www.cs.kent.ac.uk/projects/ofa/jcsp/

Although the page doesn't say so, L-GPL open source is available - just ask!
Must update the website, :(.  The release hasn't been updated for a while ...
but it will be.  There's a distributed JCSP Network Edition from Quickstone:

  http://www.quickstone.com/xcsp/jcspnetworkedition/

that is also going public - when I can get around to integrating it cleanly
with the core release.

For those who have not seen JCSP, this is a library of standard Java packages
giving access to the CSP/occam concurrency model, with a dash of pi-calculus
mobility (mobile channels, barriers and terminated-but-rerunnable-processes)
thrown in.  It integrates seamlessly with standard Java thread-and-locks
concurrency - you choose whatever mix suits your application, though you must
take care to conform to the occam parallel healthiness conditions (that the
Java compiler does not police!).

Again, I'm trying to refute Miles' assertion that:

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

:).

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,
> 
>   http://www.bitser.net/isolate-interest/

and Peter Soper wrote:
>                                          ... and it reminded me of the 
> potential of intersecting CSP and pi with JSR121 isolates. I finally 
> located a copy of slides that include Miles Sabin's pi-related ones (see 
> slide 31) that he presented to a UK university some time ago:
> 
>   http://www.bitser.net/isolate-interest/slides20040623.pdf

Thanks for this!  With Isolates, I guess you were forced into a CSP/pi-like
channel mechanism, :).

Just a few notes on the above slides ("The Java Isolation API").  Slide 23:

  o CSP style programming
     o Always use Isolates instead of Threads
     o Practically suitable only for course-grained designs

The last sub-point is an artifact of the first sub-point.  The first point
is the whole point of Isolates - to give security from one "process" being
messed around by another (either through interference or failure).  This is
absolutely fair and necessary in the context of Java.  But if you can police
the necessary care yourself, JCSP (for example) allows CSP style programming
in Java with as fine-grained design as Threads allow.

occam-pi guarantees against erroneous (unsynchronised) process interference
through language design and rules enforced by the compiler - so no run-time
checks are needed, :).  Security against failure of another process is only
partial.  For the kind of applications for which Isolates are designed,
we would have to do a lot more work.

In a wider context, CSP/pi style programming can be extremely fine-grained.
We are working on a project attempting low-level modelling of nanite assemblies
(artificial blood platelets and blood clotting).  This uses all the dynamic
mobility mechanisms built into occam-pi (an extension of the classical occam
language supporting mobile channels, barriers, processes and much more).
We are aiming at models involving (initially) tens of millions of dynamically
constructed, mobile, location-aware, and self-assembling processes - each
process being pretty tiny!

occam-pi carries overheads of only 8 bytes per process, with around 50 ns
process construction time (using Brinch Hansen's parallel memory allocation
algorithm) and 50 ns channel communication overhead (using all the transputer
tricks) on modern Pentiums 4s ... assuming cache hits, that is, :).
URLs for the curious:

  http://www.cs.kent.ac.uk/projects/ofa/kroc/      (occam-pi home and download)
  http://frmb.org/occ21-extensions.html            (summary of pi-extensions)
  http://rmox.net/prelude/                         (research OS)

Other points: I really liked the pi-calc slides (31 and following).  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.

Many apologies for going on too long.  Summary:

  (1) Formal specification of concurrency synchronisation mechanisms (including
      memory models) should be undertaken for all sorts of very practical
      reasons.  We should have moved away from natural language specs long ago.
  
  (2) Formal specification in CSP is usually pretty easy, if you have a
      reasonably tight informal specification ... and finds you out if you
      haven't.  CSP also allows access to the FDR2 model checker.  [Note:
      we have draft CSP specifications for pi-calc mobile channels and,
      soon, for (occam-pi) mobile processes.]
   
  (3) Both the CSP and pi-calculus process algebras address message passing
      via channels between non-shared-memory processes ... but they do much
      much more than that.  :)

Peter Welch.


More information about the Concurrency-interest mailing list