[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: A CSP model for Java threads
Hi Peter,
This looks interesting. A few comments...
* 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.
* 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.
* This lack of state in CSP introduces problems for modelling the
sequential parts of the Java code in CSP. A formal semantics for Java in
terms of CSP requires some kind of precisely-defined transformation from
Java code to CSP code, which captures some relevant features of the
behaviour. You could opt to abstract away all the state from the Java code
in the transformation to CSP, but this could introduce additional
non-determinism, perhaps leading to phantom deadlocks. (There's a
paper I've seen by Seidel and Scattergood, about translating from
Occam to CSP, which covers much of this -- in "Transputer Applications
and Systems '94").
* 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. Perhaps one could show that your channel implementation is a
refinement of a standard CSP channel, using FDR. 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.
* Even though this is a hard problem, I think it's very important to
have a go and to see how far you can get.
Best Wishes
Jeremy
-------------------------------------------------------------------------
Dr J. M. R. Martin
Oxford Supercomputing Centre Tel: (01865) 273849
Wolfson Building Fax: (01865) 273839
Parks Road Email: jeremy.martin@xxxxxxxxxxxxxxxx
Oxford OX1 3QD WWW: http://users.ox.ac.uk/~jeremy