[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: A CSP model for Java threads
Jeremy,
I want to argue about the LEFT versus LEFT-RIGHT model for JCSPCHANNEL ...
First of all, let's consider the problem you raised with my `thesis':
> > 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!1 -> SKIP
> B = c?x -> SKIP [] c'?x -> SKIP
>
> and alphaA = alphaB = {c,c'}
>
> and A || B = c.1 -> SKIP
>
> BUT your transformation gives us
>
> A' = write!1 -> ack -> SKIP
> B' = ready -> read?x -> SKIP [] ready' -> read'!x -> 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.
[Note: in quoting your reply above, I've swapped your `A' and `B' names
around to bring them consistent with my pictures.]
Later, you write:
> 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.
The fact that the read can start - and hence commit itself to that read -
*before* the corresponding write means that the model's behaviour with
respect to an ALT (external choice, []) involving that read is going to be
wrong. As your example above shows, the B' process commits to the primed
channel (ready' -> read'!x -> SKIP) even though the environment is not
offering any write on it. So, the LEFT-RIGHT channel's behaviour under
an ALT seems to be an internal choice (rather than an external one) and
we can get your deadlock (instead of the acceptance of the unprimed
communication that is being offered). This seems wrong?
Without ALTs, the LEFT-RIGHT model obeys the `thesis'. With ALTs, it doesn't.
But we need this `thesis', or something like it, to give relevance to your
FDR-proof of the equivalence between JCSPCHANNEL and CHANNEL. Before moving
on to verify the correctness of the JCSP Alternative and ALT-supporting
channels, we need to think some more about this ...
I proposed simplifying your LEFT-RIGHT channel model into just a LEFT one:
> > 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.
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.
So, with and without ALTs, the LEFT-only model obeys its (respective) `thesis'
... what d'ya reckon? I'm not sure about all this??
Verifying the JCSP ALT
======================
We could use more-or-less the same model as for the many-1 channel. Set up
an array (sized 2 initially!) of CSP channels (or channel-pairs if you want
to keep the `ack' channels separate) as input to an AltingCHANNEL process.
AltingCHANNEL is a CSP process implemented directly using [] (maybe this
would still be done by an AltingLEFT process that transmits its input via
a RIGHT process). The AltingJCSPCHANNEL has the same inputs/outputs as
AltingCHANNEL but is implemented by:
i = alt.select (write); // write is the array of input channels
x = write[i].read ();
For completeness, AltingCHANNEL and AltingJCSPCHANNEL should output both `i'
and `x'. Then, FDR-prove them equivalent ... :-)
That would be a huge confidence boost (e.g. if you modelled the original ALT
algorithm, a deadlock should be shown), but it's not quite the whole story.
It only shows that the JCSP ALTing works in the cases when we might as well
have used a many-1 channel (except that we do get the extra information
about which writer was accepted).
ALTing comes into its own when, at different times, we need to choose between
different-but-not-disjoint sets of channels. For example, the wot-no-chickens
canteen sometimes ALTs between the `supply' line (from the chef) and the
`service' line (from the philosophers) ... except when it has run out of
chickens and ALTs only on the `supply' line, refusing to `service' orders.
[ALTing on a single channel is, of course, the same as just committing to
read it - but that's not relevant.] This example is not something that can
be programmed using a many-1 channel ... at least, not without getting into
the same difficulties as a monitor-based algorithm (that cannot refuse calls).
So, how do we prove that successive ALTs over different-but-not-disjoint sets
of channels will not interfere with each other? I don't see how they can,
since everything is cleared back to an inactive/disabled state after each ALT.
But then ... that's what I thought about the original algorithm ... and that
deadlocked over successive ALTs over the *same* set of channels ...
Over to you Jeremy!
Cheers,
Peter.