[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
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
and what you're not.

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


More information about the Concurrency-interest mailing list