Re: A CSP model for Java threads

[Jeremy Martin <jeremy.martin@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>]

> 
> > ...........................................  But I don't know exactly
> > how one would express that in the CSP syntax, because the "user interface"
> > to your channels looks very different from using a channel directly.
> 
> Not sure what you mean here?
> 
>   CSP                                         JCSP
>   ---                                         ----
>     
>   c ! x --> P                                 c.write (x); P
> 
>   c ? x --> P                                 x = (Thing) c.read (); P
> 

I didn't explain myself very well.

If you translate your JCSP on the RHS to CSP, using your model, you will
get some very complicated CSP code involving locks. How will you get
from there to the LHS? 

How will you prove that your channel implementation, using locks,
will behave exactly like a CSP channel when embedded in some arbitrarily
complex network?

That strikes me as being difficult.

Jeremy