Finishing off the proof of JCSP

[Jeremy Martin <jeremy.martin@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>]

Hi Peter,

I think I can now supply the missing link between the intermediate
representation of a JCSP channel, that was verified by FDR, and a
pure CSP channel. It came to me while watching cricket this afternoon.

The correctness of the JCSP channel depends on the fact that the JCSP
implementation offers a slightly restricted form of CSP to the programmer.

For the moment let us consider `ALT-free' JCSP networks that use only
1 to 1 channels and no alternation statements.

Define a JCSP network as a special kind of parallel CSP network
P1 || P2 || .. || Pn, where each Pi is a JCSPPROCESS.

JCSPPROCESSS  =   SKIP
              |   a!x -> JCSPPROCESS
              |   a?x -> JCSPPROCESS(x)
              |   JCSPPROCESS |~| JCSPPROCESS
              |   JCSPPROCESS ; JCSPPROCESS

A usage rule is enforced which is that each channel a is used by exactly
one process Pi for input and exactly one process Pj for output, i.e.
the network is triple-disjoint. (There will be other external events
though to represent things like reading in data and printing out
results).

So we have described the set of CSP processes that we would like to
model using JCSP. However we don't really have any CSP channels 
available for use - we only have JCSP channels, which behave like
extra parallel processes.

JCSPCHANNEL(a) = (LEFT(a) || RIGHT(a)) / {a}

where LEFT(a) = write.a?x -> a!z -> ack.a -> LEFT(a)
and   RIGHT(a) = ready.a -> a?x -> read.a!x -> RIGHT(a)

(This representation of a JCSP channel has been proven correct
using FDR)

We would like to show that if we take some JCSP network V = P1||..||Pn
and transform it in some way that replaces all the CSP channels with
JCSP channel processes, then the external behaviour of the program
is preserved.

Let us define the transformation as follows:

Suppose that network V originally contains a CSP channel a,
which is written to by process Pi and read from by process Pj.
To replace CSP channel a in V we introduce an additional
parallel process JCSPCHANNEL(a), and we transform process
Pi to Pi' by replacing all occurences of 
            a!x -> Process
by
            write.a!x -> ack.a -> Process
and we transform process Pj to Pj' by replacing all occurences of
            a?x -> Process(x)
by
            ready.a -> read.a?x -> Process(x)

Now, because of the nice algebraic laws of CSP, if we can
show that the external behaviour of subnetwork Pi || Pj is
unchanged by this transformation then it follows that there
is no effect on the external behaviour of the network as a whole.

What we actually need to prove is that

(1):   (Pi || Pj) / {a} = 
       (Pi' || JCSPCHANNEL(a) || Pj') / {write.a, ack.a, a, ready.a, read.a}

So let's start with the RHS

(Pi' || JCSPCHANNEL(a) || Pj') / {write.a, ack.a, ready.a, read.a}

= (Pi' || ((LEFT(a) || RIGHT(a)) / {a}) || Pj') / {write.a, ack.a,
                                                   ready.a, read.a}

= (Pi' || LEFT(a) || RIGHT(a) || Pj') / {a, write.a, ack.a, ready.a,
                                                             read.a}

=       (  ((Pi' || LEFT(a)) / {write.a, ack.a}) || 
           (RIGHT(a) || Pj') / {ready.a,read.a}    ) / {a}

So we can establish result (1) if we can prove the following:

(2) (Pi' || LEFT(a)) / {write.a, ack.a} = Pi  and
(3) (RIGHT(a) || Pj') / {ready.a,read.a} = Pj

Let us consider the validity of equation 2. This would not hold true
in general for any CSP process Pi. But due to our restriction on the
syntax of JCSP processes, we can see that it is true as follows.

(i) In moving from Pi to Pi' we replace a!x -> PROCESS with
    write.a!x -> ack.a -> PROCESS
(ii) The effect of putting LEFT(a) in parallel with Pi' is then to
    replace write.a!x -> ack.a -> PROCESS in Pi' with write.a!x -> a!x -> 
    ack.a -> PROCESS 
(iii) The effect of hiding {write.a, ack.a} is to set write.a!x -> a!x ->
    ack.a -> PROCESS back to a!x -> PROCESS, which is what we started
    with. (I think this is the only bit which makes use of the restricted
    syntax.)

Equation 3 is proved similarly and we conclude that the 
transformation to replace CSP channel `a' with JCSPCHANNEL(a)
has not affected the behaviour of the network if the channel is
concealed.

Having applied a transformation to replace one CSP channel `a'
with a JCSP channel we can repeat the step on other channels
until only JCSP channels remain. (This is because the transformation
from Pi and Pj to Pi' and Pj' preserves the restriced syntax
of the JCSP processes). Finally we will have shown that

(P1 || .. || Pn) / {a1, .., an} = 
((P1' || .. || Pn') || (JCSPCHANNEL(a1) || .. || JCSPCHANNEL(an)) /
 {write.a1, ack.a1, ready.a1, read.a1, .., write.an, ack.an, ready.an,
  read.an} 

Which means that the external behaviour of the network (i.e its behaviour
when all internal channels are concealed) is exactly preserved.

So we are then perfectly safe to reason about JCSP programs in their
natural form without the additional baggage of LEFT/RIGHT process
pairs for each channel.

I am confident that this proof can easily be extended to take care
of alternation, to establish the full correctness of JCSP.

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