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

Boehm, Hans hans.boehm at hp.com
Thu Sep 1 19:11:15 EDT 2005


> 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

As far as I can tell, your CSP model of Java monitors ignores the memory
model
issues (JSR 133), as does most theoretical work that I've seen.  That
doesn't make it
useless by any means, but you have to be careful to remember what you're
modeling,
and what you're not.

If I understand correctly, a number of very common Java concurrency bugs
seem
to just quietly disappear in the CSP translation, e.g. double-checked
locking.
(This doesn't argue that we should all be writing the CSP version.  The
Java
memory model is there for a reason, namely to get reasonable
performance.)

Hans



More information about the Concurrency-interest mailing list