From: P.H.Welch_at_email.domain.hidden
Date: 1999-03-29 16:50:20
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.
This archive was generated by hypermail 2.1.7 on 2004-10-31 20:03:57 GMT
© Copyright WoTUG
All rights reserved