Java Threads mailing list archive

Re: A CSP model for Java threads

On Fri, 6 Aug 1999, P.H.Welch wrote:

> 
> Jeremy,
> 
> I want to argue about the LEFT versus LEFT-RIGHT model for JCSPCHANNEL ...

...

I said

>
> > Well I don't think we can go this far. You are modelling the read() method
> > as a single atomic event that may only take place after the corresponding
> > write(), whereas my channel model more accurately allows the read to start
> > before the corresponding write(), and even before the previous write() has
> > terminated.
> >
> > That this is an important aspect of the behaviour is illustrated by my
> > previous example of using the basic JCSP channel as part of an ALT.
> > I think that your version here is wrong because it does not exhibit the
> > same ALT deadlock that I described above.

You said 

> 
> But that's why I think my version is right :-) ... the deadlock should *not*
> occur in the example you give ... the LEFT-RIGHT model is wrong because it
> *does* exhibit the deadlock!  The fact that the read in the LEFT-RIGHT model
> can start before the corresponding write starts is not relevant ... it will
> not proceed beyond the `ready' event in those circumstances and that `ready'
> is going to be hidden to the rest-of-the-world.
> 

But FDR says that my LEFT/RIGHT model is exactly equivalent to the
JCSPCHANNEL. So how would you argue against that?

Of course the deadlock that I described cannot happen in Java as
there is no equivalent construct to the CSP []. But if java
did have a [] construct then the deadlock would be possible and that is
the point.

So how do we move forward? What we really want is to be able
to verify JCSP programs by replacing all calls to read() and
write() with atomic communication statements. So we need to
formulate a set of design rules for where it is safe to 
do this replacement. The fact that I have shown that the JCSP
channel is equivalent to a simple intermediate form should be
helpful with that. 

I'm not sure when I'll get a chance to look at the ALT stuff. 
Tasks are beginning to pile up again.

Jeremy

 -------------------------------------------------------------------------
                            Dr J. M. R. Martin                
 Oxford Supercomputing Centre                          Tel: (01865) 273849
 Wolfson Building                                      Fax: (01865) 273839
 Parks Road                           Email: jeremy.martin@comlab.ox.ac.uk
 Oxford OX1 3QD                         WWW: http://users.ox.ac.uk/~jeremy