Re: A CSP model for Java threads

[P.H.Welch@xxxxxxxxx]

Jeremy,

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

Yes!  You have stated the theorem that we need to prove!!  Getting from
the very complicated CSP code involving locks back to the simple channel
communication is what I meant by going round the cycle (from CSP to JCSP
and back to CSP).

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

Humm ... if we could prove the RHSs above were the same as the LHSs, all
would be done.  Something to do in a late bar at WoTUG-22?

Cheers,

Peter.