Re: A CSP model for Java threads

[P.H.Welch@xxxxxxxxx]

Jeremy,

Further to your:

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

Did INMOS ever do this for the transputer implementation of a CSP channel?

This seems to be exactly the same problem.  In fact, the `monitor'
implementation in JCSP (now with a correct ALT ;-) is *very* close to
the transputer implementation ... the monitor locks appear in the transputer
as uninterruptable micro-code.  [This throws another angle on the `low'
versus `high' level argument!  Those monitor primitives, including "wait"
and sort of including a "notify" map to micro-code elements that were
used to implement channels etc. in the transputer.  So, those monitor
thingees seem pretty `low-level' in that context :-)].

But, seriously, does anyone know if INMOS ever proved their channels
were CSP ones?  I don't remember anyone ever asking ...

Peter.