[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