From jeremy.martin@computing-services.oxford.ac.uk Sun Oct 31 15:49:08 2004 From: Jeremy Martin To: P.H.Welch@ukc.ac.uk Cc: jeremy.martin@computing-services.oxford.ac.uk, java-threads@ukc.ac.uk, occam-com@ukc.ac.uk Date: Mon, 29 Mar 1999 17:02:09 +0100 (BST) Subject: Re: A CSP model for Java threads Content-Type: TEXT/PLAIN; charset=US-ASCII MIME-Version: 1.0 Message-ID: > > > ........................................... 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