[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: A CSP model for Java threads



On Wed, 4 Aug 1999, P.H.Welch wrote:

> 
> Fixing WAIT(o,me) so that it kicks off with the waita.o.me means that this
> can go ahead (putting `me' into the `wait set' for object `o') without having
> first claimed the LOCK(o).  That shouldn't be allowed.  To fix that, we just
> need to extend the alphabet of LOCK(o) to include all the waita.o.me events
> and refuse them when not locked - i.e.
> 
>   alphaLOCK(o) = {claim.o.t, release.o.t, notify.o.t, notifyall.o.t, waita.o.t
>                   | t <- Threads}
> 
>   LOCK(o) = claim.o?t -> LOCKED(o,t)
> 
>   LOCKED(O,t) = release.o.t -> LOCK(o)
>               []
>               notify.o.t -> LOCKED(O,t)
>               []
>               notifyall.o.t -> LOCKED(O,t)
>               []
>               waita.o.t -> LOCKED(O,t)
> 
> [Aside: Java doesn't actually deadlock if you try to do a wait on an object
> you haven't locked - it throws an exception.  I don't know how to try and
> model an exception in CSP, so a deadlock seemed reasonable ... ?]

I've tested that and it works fine. 

> 
> 
> Non-deterministic Release following a Notify/NotifyAll
> ======================================================
> 
> In my version of the WAIT[o][n] process, I maintained just a *count*, n, of
> the threads in the waiting set.  Consequently, when a notify (or notifyall)
> occurred, I had to use the external choice operator, [], to listen for
> wait-b[o][s] across *all* threads s.  An internal choice, |~|, would have
> been wrong as it could chose to go for a wait-b[o][s] where the s was not
> one of those in the wait set.
> 
> Your version, SWAIT(o,ts), maintains the whole wait *set*, ts, which is neat.
> It also allows you to use the (non-determiistic) internal choice operator
> when reacting to a notify/notifyall for a non-null wait set.
> 
> But, in this context, are not [] and [~] equivalent?  All those processes
> in the wait set will be trying (or are about to try) to do the wait.o.t
> events - i.e. the environment is offering *all* the events over which the
> choice is to be made - in which case, [] and [~] look equivalent to me?
> Is there some technical advantage (to do with FDR?) in going for |~|?
> 
> Actually, since we now have the wait set held by the SWAIT(o) process,
> we can simplify the desciption of the RELEASE(o,ts), following a notifyall,
> by simply doing a parallel clearing of all the waitb.o.t events.  I couldn't
> do this before when I maintained just a wait *count*:
> 
>   RELEASE(o.ts) = (|| t:ts @ waitb.o.t -> SKIP) ; SWAIT(o,{})
> 
> if I've got the syntax right?

Yes it looks as if your original did work correctly, after all.

Except for the loss of elegance, there would be an advantage in doing it
your way because the SWAIT process would have many less states. Anyway
I've tested it both ways without any problems.

> Simplifying the (JCSPCHANNEL = CHANNEL) Model and Proof
> ========================================================
> 
> You have proved equivelence between a JCSPCHANNEL and a CHANNEL made up
> from two processes:
> 
>           ________________________________________________
>    write |    __________                   ___________    | read
>   --->---|---|          |    transmit     |           |---|--->---
>          |   |   LEFT   |-------->--------|   RIGHT   |   |
>   -------|---|__________|                 |___________|---|-------
>     ack  |                                                | ready
>          |                    CHANNEL                     |
>          |________________________________________________|
> 
> 
> where, loosely speaking:
> 
>   LEFT  = write?x -> transmit!x -> ack -> LEFT
>   RIGHT = ready -> transmit?x -> read!x -> RIGHT
> 
> The thesis being that:
> 
>       _____________                             _____________
>      |             |                           |             |
>      |             |             c             |             |
>      |      A      |------------->-------------|      B      |
>      |             |                           |             |
>      |_____________|                           |_____________|
> 
> 
> is the same as:
> 
>       _____________                             _____________
>      |             | write  ___________  read  |             |
>      |             |--->---|           |--->---|             |
>      |      A'     |       |  CHANNEL  |       |      B'     |
>      |             |-------|___________|-------|             |
>      |_____________|  ack                ready |_____________|
> 
> where A = A',
> 
>   except that (c!x -> P) from A is replaced by (write!x -> ack -> P) in A'
> 
> and B = B',
> 
>   except that (c?x -> Q) from B is replaced by (ready -> read?x -> Q) in B'.
> 
> Now, this thesis is self-evident (!) ... it would be nice to prove though???


I don't think this thesis is actually true in all situations. Things go
wrong when you introduce alternation.

Suppose A = c?x -> SKIP [] c'?x -> SKIP
        B = c!1 -> SKIP

and alphaA = alphaB = {c,c'}

and A || B = c.1 -> SKIP

BUT your transformation gives us 

       A' = ready -> read?x -> SKIP [] ready' -> read'!x -> SKIP
       B' = write!1 -> ack -> SKIP

then the corresponding process A' || B' || channel || channel'
could deadlock without any data being sent, e.g. after trace
  
             <ready',write!1>

Because process A' has selected the wrong ALT branch, which is
why we need extra code for ALT in JCSP. 

> 
> BUT, can't we simplify the model (and the proof) as follows.  Drop the RIGHT
> process, leaving the channel just as LEFT.  Also, we can drop the ack event
> and reuse the write channel for this purpose.  So, consider:
> 
>           ________________________________________________
>          |                                                |
>    write |                                                | read
>   --->---|                    CHANNEL                     |--->---
>          |                                                |
>          |________________________________________________|
> 
> where:
> 
>   CHANNEL = write?x -> read!x -> write?any -> CHANNEL
> 
> and now our thesis is that:
> 
>       _____________                             _____________
>      |             |                           |             |
>      |             |             c             |             |
>      |      A      |------------->-------------|      B      |
>      |             |                           |             |
>      |_____________|                           |_____________|
> 
> 
> is the same as:
> 
>       _____________                             _____________
>      |             |        ___________        |             |
>      |             | write |           | read  |             |
>      |      A'     |--->---|  CHANNEL  |--->---|      B'     |
>      |             |       |___________|       |             |
>      |_____________|                           |_____________|
> 
> where A = A',
> 
>   except that (c!x -> P) from A is replaced by (write!x -> write!x -> P) in A'
> 
> and B = B',
> 
>   except that (c?x -> Q) from B is replaced by (read?x -> Q) in B'.
> 
> In the READ(o,t) process within JCSPCHANNEL, remove the ready.o.t from its
> alphabet and its first line of code.  In the WRITE(o,t), remove the ack.o.t
> from its alphabet and replace its occurrence in its code with write.o.t?any.
> 
> Now the assertions that JCSPCHANNEL and CHANNEL refine each other should still
> go through ... ;-) ... ???
> 

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.

So sadly I think that my specification is about as simple as we can get
for the 1-1 channel. However this does make it feasible to analyse 
quite complicated JCSP programs using FDR.

> 
> 1-1, Many-1, 1-Many and Many-Many Channels
> ==========================================


I'll have a look at this, but I think it will be a LEFT||RIGHT
specification again that we need.

Jeremy

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