Re: A CSP model for Java threads

[Jeremy Martin <jeremy.martin@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>]

Hi Peter,

I've now tackled the two-writer single reader problem in the way
you suggested (but with LEFT and RIGHT components). It all comes out
OK, you'll be pleased to know.

So that just leaves us of the question of under which circumstances
it is safe to replace this intermediate LEFT/RIGHT form with just a
channel.

Jeremy

--
-- We shall model a system consisting of a set of Java objects and threads.
-- 

Objects = {0,1}
Threads = {0,1,2}

...previous code omitted 

-- 
-- Many to one channels (5th July 1999):
--
-- We now model the JCSP channel which allows two concurrent writers
-- but only a single reader.
--

--
-- First the spec:
--

LEFT'(o,t,t') = LEFT(o,t) ||| LEFT(o,t')

alphaLEFT'(o,t,t') = union(alphaLEFT(o,t),alphaLEFT(o,t'))

ALTCHANNEL(o,t,t',t'') = 
  (
      LEFT'(o,t',t'')
    [alphaLEFT'(o,t',t'') || alphaRIGHT(o,t)]
      RIGHT(o,t)
  ) \ {transmit.o.m | m <- Data}

alphaALTCHANNEL(o,t,t',t'') = 
  {write.o.t'''.m, ack.o.t''', ready.o.t, read.o.t.m 
   | m <- Data, t''' <- {t',t''}} 

--
-- Now the implementation (taken from PHW's Java code)
-- An extra object is needed to be the write_monitor
--

WRITE'(o,writemonitor,t) = write.o.t?mess -> 
                           claim.writemonitor.t ->
                           claim.o.t ->  
                           setvar.o.channel_hold.t!mess ->
                           getvar.o.channel_empty.t?c ->
                           (
                             if (c == TRUE) then
                             setvar.o.channel_empty.t!FALSE -> 
                             WAIT(o,t)
                           else
                             setvar.o.channel_empty.t!TRUE -> 
                             NOTIFY(o,t); 
                             WAIT(o,t)
                           );
                           release.o.t ->
                           release.writemonitor.t -> 
                           ack.o.t -> 
                           WRITE'(o,writemonitor,t)

alphaWRITE'(o,o',t) = { 
                        claim.o''.t, getvar.o.v.t.d, notify.o''.t, 
                        notifyall.o''.t, setvar.o.v.t.d, write.o.t.d, 
                        release.o''.t, waita.o''.t, waitb.o''.t, ack.o.t 
                        | v <- Variables, d <- Data, o'' <- {o,o'}
                      }

--
-- The read method is essentially the same as before, except
-- that we need to include certain events in its alphabet to
-- prevent the reading thread from messing with the write monitor.
-- (I only realised this after catching a livelock on an early run.)
--

READ'(o,o',t) = READ(o,t)

alphaREAD'(o,o',t) = union(alphaREAD(o,t),{claim.o'.t})

JCSPALTCHANNEL(o,o',t1,t2,t3) = 
   (
     READ'(o,o',t1) 
       [alphaREAD'(o,o',t1) || 
        union(alphaWRITE'(o,o',t2),alphaWRITE'(o,o',t3))] 
     (WRITE'(o,o',t2) [alphaWRITE'(o,o',t2) || alphaWRITE'(o,o',t3)] 
      WRITE'(o,o',t3))
   )
 [union(alphaREAD'(o,o',t1),union(alphaWRITE'(o,o',t2),
  alphaWRITE'(o,o',t3))) 
  || 
  union(union(alphaMONITOR(o),alphaMONITOR(o')),alphaVARIABLES(o))] 
   (
     (
         MONITOR(o)
       [alphaMONITOR(o) || alphaMONITOR(o')]
         MONITOR(o') 
     )
       [union(alphaMONITOR(o),alphaMONITOR(o')) || alphaVARIABLES(o)]
     VARIABLES(o)
   ) 

alphaJCSPALTCHANNEL(o,o',t1,t2,t3) = 
union(union(alphaREAD'(o,o',t1),union(alphaWRITE'(o,o',t2),
alphaWRITE'(o,o',t3))),union(union(alphaMONITOR(o),alphaMONITOR(o')),
alphaVARIABLES(o)))      

--
-- In order to compare this specification with the JCSP implementation
-- we need to conceal all the additional events in the alphabet
-- of JCSPALTCHANNEL
--

Private2 = diff(alphaJCSPALTCHANNEL(0,1,0,1,2),alphaALTCHANNEL(0,0,1,2))

--
-- Assert that JCSPALTCHANNEL(o,o',t1,t2,t3) \ Private2 is equivalent to 
-- ALTCHANNEL(o,o',t1,t2) in the Failures/Divergences model (by asserting
-- refinement in both directions).
--

assert ALTCHANNEL(0,0,1,2) [FD= JCSPALTCHANNEL(0,1,0,1,2) \ Private2

assert JCSPALTCHANNEL(0,1,0,1,2) \ Private2 [FD= ALTCHANNEL(0,0,1,2)



 -------------------------------------------------------------------------
                            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