From P.H.Welch@ukc.ac.uk Sun Oct 31 15:49:08 2004
From: P.H.Welch@ukc.ac.uk
To: jeremy.martin@computing-services.oxford.ac.uk
Cc: java-threads@ukc.ac.uk, occam-com@ukc.ac.uk
Date: Mon, 29 Mar 1999 17:39:23 +0100
Subject: Re: A CSP model for Java threads
Message-ID: <199903291639.RAA05397@elm.ukc.ac.uk>


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.