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 16:50:20 +0100
Subject: Re: A CSP model for Java threads
Message-ID: <199903291550.QAA04279@elm.ukc.ac.uk>


Jeremy,

> * Modelling the Java synchronisation primitives in terms of CSP, seems
> to be the "right way around". The high-level `monitors' are described
> in terms of low-level handshaking.

Still an arguable point!  The two systems are equivalent: the JavaPP work
is all about modelling CSP primitives with Java ones and last weekend's
model is just vice-versa.  Which one is the `low-level' one, therefore,
has no real logical significance.  What needs to be done is to show that
if we go once around the cycle -- starting from anywhere -- we get back
to where we started :-)

> * The standard semantics of CSP don't allow for any state, so you
> shouldn't really introduce variables to represent synchronisation count.
> Perhaps you could use processes to represent the count variables.

I know ... I did mention that, perhaps, those counts should be modelled
as processes.  But they belong to the user threads, so I would envisage
the process model of a user thread just to carry this count around as
an extra subscript (or index), which is one way CSP can capture the notion
of state.

> * One important application of this work, of which I'm sure you're aware, 
> could be to prove the correctness of your Java/CSP implementation in some
> sense.

Yes, that's why I decided it was about time to write down this CSP model.
In building a CSP model of our JCSP implementation of a CSP channel and
alternation (choice), state variables play a necessary role: is the channel
`empty', is the status of the alting process enabling, ready or waiting.

Disregarding such state in the CSP model would certainly lead to `phantom'
deadlocks.  Again, the process model I had in mind carries such state around
as an index ... these processes are the user threads writing, reading or
alting over these channels ...

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

where I'm assuming that "c" is an "Object" carrying channel whose message,
therefore, requires appropriate casting at the receiving end.

  []( c[i] ? x  --> P(i) | i in {0..(n-1)})   (see below)

To do the above choice over an array of channel guards, first we construct
an Alternative object to assist:

  Alternative alt = new Alternative (c);

Then, the choice works as follows:

  int i = alt.select ();
  x = (Thing) c[i].read ();
  P(i)

Note: if the above choice is only performed once, the "alt" object could
be constructed on-the-fly in the first of the above three lines.  Normally,
however, such choices are in a loop (or recursive process), so we wouldn't
want to make a new one each time.
  
We have tried to make the "user interface" as CSP-like as possible, without
becoming hoplessly (or even slightly!) inefficient through too great a
disregard for Java control flow ...

Peter.