[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: jeremy.martin@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx*Subject*: Re: A CSP model for Java threads*From*: P.H.Welch@xxxxxxxxx*Date*: Mon, 29 Mar 1999 17:17:33 +0100*Cc*: java-threads@xxxxxxxxx, occam-com@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.

- Prev by Date:
**Re: A CSP model for Java threads** - Next by Date:
**Re: A CSP model for Java threads** - Previous by thread:
**Re: A CSP model for Java threads** - Next by thread:
**Re: A CSP model for Java threads** - Index(es):