-- FDR analysis of Peter Welch's CSP model of Java threads and -- the JCSP implementation of a channel and (2-way) alternation. -- Author: Jeremy M. R. Martin -- Date: June, 2000. -- Note: this script was developed *before* the visual explanation of how -- it works was created. That visual explanation is presented in the slides -- accompanying this script, which needs updating to bring it into line with -- those images. How that visualisation relates to this script is described -- (along with much else) in the paper: -- "Formal Analysis of Concurrent Java Systems", P.H.Welch and J.M.R.Martin. -- In P.H.Welch and A.W.P.Bakkers (editors), -- Communicating Process Architectures 2000, -- Volume 58 of Concurrent Systems Engineering, -- Pages 275-301. WoTUG, IOS Press (Amsterdam), September 2000. -- (ISBN 1-58603-077-9) include "compression.csp" -- -- We shall model a system consisting of a set of Java objects and threads. -- Objects = {0,1,2} Threads = {0,1,2} -- -- We define a collection of channels to model the synchronisation -- events. -- channel claim, release, waita, waitb, notify, notifyall: Objects.Threads -- -- System processes: LOCK(o) controls locking of object o's monitor and -- SWAIT controls its auxilliary pool of waiting threads ts. -- 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) alphaLOCK(o) = { claim.o.t,release.o.t,notify.o.t,notifyall.o.t,waita.o.t | t <- Threads } -- -- A notify event results in one thread being non-deterministically -- selected from the waiting pool and reactivated; a notifyall -- event results in all the threads being activated in some -- non-deterministic order (changed from PHW's original). -- SWAIT(o,ts) = ( waita.o?t -> SWAIT(o,union(ts, {t})) ) [] ( notify.o?t -> if (card(ts) > 0) then |~| s:ts @ waitb.o!s -> SWAIT(o,diff(ts,{s})) else SWAIT(o,{}) ) [] ( notifyall.o?t -> RELEASE(o,ts) ) RELEASE(o,ts) = if (card(ts) > 0) then |~| t:ts @ waitb.o!t -> RELEASE(o,diff(ts,{t})) else SWAIT(o,{}) alphaSWAIT(o) = { waita.o.t,waitb.o.t,notify.o.t,notifyall.o.t | t <- Threads } -- -- The monitor is defined as the parallel composition of the two system -- processes. Initially the auxiliary wait queue is empty. -- MONITOR(o) = SWAIT(o,{}) [ alphaSWAIT(o) || alphaLOCK(o) ] LOCK(o) alphaMONITOR(o) = union(alphaSWAIT(o),alphaLOCK(o)) -- -- Now we define the standard programmer's interface to monitors. -- Note that the WAIT procedure has been modified from Peter's original -- CSP definition. An object needs to join the wait queue, by issuing -- a waita event, prior to releasing the monitor otherwise it might miss -- being notified. This was revealed by FDR in an early run. -- -- For the moment we'll prohibit multiple locks by a particular thread -- on a particular object. This could easily be handled by using processes -- to represent the relevant lock counts (as Peter has shown). -- STARTSYNC(o,me) = claim.o.me -> SKIP ENDSYNC(o,me) = release.o.me -> SKIP WAIT(o,me) = waita.o.me -> release.o.me -> waitb.o.me -> claim.o.me -> SKIP NOTIFY(o,me) = notify.o.me -> SKIP -- -- Now let's build a more realistic version of STARTSYNC and ENDSYNC -- -- We need to store a count associated with each thread and each lock -- maxcount = 3 channel getcount:Objects.Threads.{0..maxcount} channel upcount,downcount:Objects.Threads COUNT(o,t) = COUNT2(o,t,0) COUNT2(o,t,n) = if n < maxcount then upcount.o.t -> COUNT2(o,t,n+1) else STOP [] if n > 0 then downcount.o.t -> COUNT2(o,t,n-1) else STOP [] getcount.o.t!n -> COUNT2(o,t,n) alphaCOUNT(o,t) = {getcount.o.t.d,upcount.o.t,downcount.o.t | d <- {0..maxcount}} Threadseq = <0,1,2> COUNTLIST(o) = <(COUNT(o,t),alphaCOUNT(o,t)) | t <- Threadseq> COUNTS(o) = ListPar(COUNTLIST(o)) alphaCOUNTS(o) = {getcount.o.t.d,upcount.o.t,downcount.o.t | d <- {0..maxcount}, t <- Threads} STARTSYNC2(o,t) = getcount.o.t?n -> if n == 0 then claim.o.t -> upcount.o.t -> SKIP else if n < maxcount then upcount.o.t -> SKIP else STOP ENDSYNC2(o,t) = getcount.o.t?n -> if n == 1 then release.o.t -> downcount.o.t -> SKIP else if n > 1 then downcount.o.t -> SKIP else STOP MONITOR2(o) = (SWAIT(o,{}) [ alphaSWAIT(o) || alphaLOCK(o) ] LOCK(o)) [ union(alphaSWAIT(o),alphaLOCK(o)) || alphaCOUNTS(o) ] COUNTS(o) alphaMONITOR2(o) = union(union(alphaSWAIT(o),alphaLOCK(o)),alphaCOUNTS(o)) -- -- JCSP Implementation of channel: -- -- This is translated from "P.H.Welch, Java Threads in the light of -- occam/CSP, Proceedings of WoTUG21 1998", page 274. -- -- The JCSP channel object has three variables (channel_empty, channel_hold -- and local), which we shall model as processes always ready both to -- have their value reset or to report it to any willing thread. We -- assume, for simplicity, that each channel has the same `boolean' type. -- datatype Variables = channel_empty | channel_hold datatype Bool = TRUE | FALSE channel getvar, setvar: Objects.Variables.Threads.Bool -- -- Variables are initialised as TRUE. -- VARIABLE(o,v) = VARIABLE2(o,v,TRUE) VARIABLE2(o,v,d) = ( [] t:Threads @ getvar.o.v.t!d -> VARIABLE2(o,v,d) ) [] ( [] t:Threads @ setvar.o.v.t?x -> VARIABLE2(o,v,x) ) alphaVARIABLE(o,v) = { getvar.o.v.t.d, setvar.o.v.t.d | t <- Threads, d <- Bool } VARIABLES(o) = VARIABLE(o,channel_empty) [alphaVARIABLE(o,channel_empty) || alphaVARIABLE(o,channel_hold)] VARIABLE(o,channel_hold) alphaVARIABLES(o) = union(alphaVARIABLE(o,channel_empty), alphaVARIABLE(o,channel_hold)) -- -- One purpose of JCSP is to seal off the thread/monitor synchronisation -- calls from the programmer. Instead a read/write interface is provided -- by two simple methods. -- -- We shall model this interface with the following events: -- write.o.t.d - thread t activates java method write(d) of object o, -- message d is supplied for transmission. -- ack.o.t - call to write(d) terminates, -- ready.o.t' - Thread t' activates method read() of object o. -- read.o.t'.d - call to read() terminates, message d is returned -- -- The JCSP channel should behave like a synchronised channel. Each -- successful communcation requires that at some point both threads -- are simultaneously involved. -- channel read, write: Objects.Threads.Bool channel ready, ack: Objects.Threads -- -- We model the JCSP read method as a process which repeatly waits to be -- activated by a ready event and then executes the monitor sychronisation -- code to receive a message. -- READ(o,t) = ready.o.t -> claim.o.t -> getvar.o.channel_empty.t?c -> ( if (c == TRUE) then setvar.o.channel_empty.t!FALSE -> WAIT(o,t); NOTIFY(o,t) else setvar.o.channel_empty.t!TRUE -> NOTIFY(o,t) ) ; getvar.o.channel_hold.t?mess -> release.o.t -> read.o.t!mess -> READ(o,t) alphaREAD(o,t) = { claim.o.t, getvar.o.v.t.d, notify.o.t, notifyall.o.t, setvar.o.v.t.d, read.o.t.d, release.o.t, waita.o.t, waitb.o.t, ready.o.t | v <- Variables, d <- Bool } -- -- Here is the alternative CJT version of Gerald Hilderink -- GREAD(o,t) = ready.o.t -> claim.o.t -> getvar.o.channel_empty.t?c -> (if (c == TRUE) then WAIT(o,t) else SKIP); setvar.o.channel_empty.t!TRUE -> NOTIFY(o,t); getvar.o.channel_hold.t?mess -> release.o.t -> read.o.t!mess -> GREAD(o,t) -- -- The JCSP write method is similarly modelled as a repeating process, -- activated by the write event. -- WRITE(o,t) = write.o.t?mess -> 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 -> ack.o.t -> WRITE(o,t) alphaWRITE(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 <- Bool } -- -- Here is the CJT version -- GWRITE(o,t) = write.o.t?mess -> claim.o.t -> setvar.o.channel_empty.t!FALSE -> setvar.o.channel_hold.t!mess -> NOTIFY(o,t); WAIT(o,t); release.o.t -> ack.o.t -> GWRITE(o,t) -- -- The JCSP channel is then modelled as the parallel composition of -- processes which model its monitor, three variables, and read and write -- methods. -- JCSPCHANNEL(o,t1,t2) = ( READ(o,t1) [alphaREAD(o,t1) || alphaWRITE(o,t2)] WRITE(o,t2) ) [union(alphaREAD(o,t1),alphaWRITE(o,t2)) || union(alphaMONITOR(o),alphaVARIABLES(o))] ( MONITOR(o) [alphaMONITOR(o) || alphaVARIABLES(o)] VARIABLES(o) ) alphaJCSPCHANNEL(o,t1,t2) = union(union(alphaMONITOR(o),alphaVARIABLES(o)), union(alphaREAD(o,t1),alphaWRITE(o,t2))) -- -- Here is the CJT version -- GJCSPCHANNEL(o,t1,t2) = ( GREAD(o,t1) [alphaREAD(o,t1) || alphaWRITE(o,t2)] GWRITE(o,t2) ) [union(alphaREAD(o,t1),alphaWRITE(o,t2)) || union(alphaMONITOR(o),alphaVARIABLES(o))] ( MONITOR(o) [alphaMONITOR(o) || alphaVARIABLES(o)] VARIABLES(o) ) -- -- Now we shall define a simplified model of how the JCSP channel -- should work, and then, hopefully, use FDR to show that this is -- equivalent to the JCSP implementation. -- -- The simple channel consists of two parallel processes, LEFT and RIGHT, -- to handle input and output respectively. The processes are joined -- by a hidden channel transmit. -- channel transmit:Objects.Bool LEFT(o,t) = write.o.t?mess -> transmit.o!mess -> ack.o.t -> LEFT(o,t) RIGHT(o,t') = ready.o.t' -> transmit.o?mess -> read.o.t'!mess -> RIGHT(o,t') alphaLEFT(o,t) = {write.o.t.m, transmit.o.m, ack.o.t | m <- Bool} alphaRIGHT(o,t') = {ready.o.t', transmit.o.m, read.o.t'.m | m <- Bool} CHANNEL(o,t,t') = ( LEFT(o,t') [alphaLEFT(o,t') || alphaRIGHT(o,t)] RIGHT(o,t) ) \ {transmit.o.m | m <- Bool} alphaCHANNEL(o,t,t') = {write.o.t'.m, ack.o.t', ready.o.t, read.o.t.m | m <- Bool} -- -- In order to compare this specification with the JCSP implementation -- we need to conceal all the additional events in the alphabet -- of JCSPCHANNEL -- Private = diff(alphaJCSPCHANNEL(0,0,1),alphaCHANNEL(0,0,1)) -- -- Assert that JCSPCHANNEL(o,t1,t2) \ Private is equivalent to -- CHANNEL(o,t1,t2) in the Failures/Divergences model (by asserting -- refinement in both directions). -- assert CHANNEL(0,0,1) [FD= JCSPCHANNEL(0,0,1) \ Private assert JCSPCHANNEL(0,0,1) \ Private [FD= CHANNEL(0,0,1) assert CHANNEL(0,0,1) [FD= GJCSPCHANNEL(0,0,1) \ Private assert GJCSPCHANNEL(0,0,1) \ Private [FD= CHANNEL(0,0,1) -- -- That works fine with the current system when only two threads -- are in existence, but when we increase the number of threads in the -- system beyond two, perhaps by defining Threads = {0,1,2}, we find that -- the above pair of assertions no longer holds. FDR reveals that this is -- because the new threads may `fiddle' with the state of the channel -- implementation. -- -- So how do we stop other threads from interfering with the channel object? -- -- In CSP we can add a parallel process to the channel implementation which -- blocks access to any of the the relevant events! (Unfortunately this is -- not supported by the actual Java implementation, and so must be -- regarded as a usage rule for JCSP.) -- PROTECTION(o,t,t') = STOP alphaPROTECTION(o,t,t') = { claim.o.t'', setvar.o.v.t''.d, getvar.o.v.t''.d, waita.o.t'' | t'' <- diff(Threads,{t,t'}), v <- Variables, d <- Bool } SAFEJCSPCHANNEL(o,t,t') = JCSPCHANNEL(o,t,t') [ alphaJCSPCHANNEL(o,t,t') || alphaPROTECTION(o,t,t') ] PROTECTION(o,t,t') SAFEGJCSPCHANNEL(o,t,t') = GJCSPCHANNEL(o,t,t') [ alphaJCSPCHANNEL(o,t,t') || alphaPROTECTION(o,t,t') ] PROTECTION(o,t,t') assert CHANNEL(0,0,1) [FD= SAFEJCSPCHANNEL(0,0,1) \ Private assert SAFEJCSPCHANNEL(0,0,1) \ Private [FD= CHANNEL(0,0,1) assert CHANNEL(0,0,1) [FD= SAFEGJCSPCHANNEL(0,0,1) \ Private assert SAFEGJCSPCHANNEL(0,0,1) \ Private [FD= CHANNEL(0,0,1) -- -- This pair of assertions is indeed found to hold when the number of threads -- is increased beyond 2. -- -- -- Summary: -- -- We have shown how to reduce the CSP model of the JCSP channel -- implementation to a far simpler equivalent form. Further work -- would be useful to analyse the JCSP implementation of alternation. -- -- Jeremy Martin 30th July 1999 -- -- -- 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')) SHAREDCHANNEL(o,t,t',t'') = ( LEFT'(o,t',t'') [alphaLEFT'(o,t',t'') || alphaRIGHT(o,t)] RIGHT(o,t) ) \ {transmit.o.m | m <- Bool} alphaSHAREDCHANNEL(o,t,t',t'') = {write.o.t'''.m, ack.o.t''', ready.o.t, read.o.t.m | m <- Bool, 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 <- Bool, 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}) JCSPSHAREDCHANNEL(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) ) alphaJCSPSHAREDCHANNEL(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 JCSPSHAREDCHANNEL -- Private2 = diff(alphaJCSPSHAREDCHANNEL(0,1,0,1,2),alphaSHAREDCHANNEL(0,0,1,2)) -- -- Assert that JCSPSHAREDCHANNEL(o,o',t1,t2,t3) \ Private2 is equivalent to -- SHAREDCHANNEL(o,t1,t2,t3) in the Failures/Divergences model (by asserting -- refinement in both directions). -- assert SHAREDCHANNEL(0,0,1,2) [FD= JCSPSHAREDCHANNEL(0,1,0,1,2) \ Private2 assert JCSPSHAREDCHANNEL(0,1,0,1,2) \ Private2 [FD= SHAREDCHANNEL(0,0,1,2) -- 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 -- above 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, 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 shared channels, to establish the full correctness of JCSP. To do this, -- It will be useful to formulate an alternative definition of the -- SHAREDCHANNEL which doesn't use process interleaving, and has two internal -- 1-1 channels combined with an external choice. -- channel transmit':Objects.Bool LEFT''(o,t) = write.o.t?mess -> transmit'.o!mess -> ack.o.t -> LEFT''(o,t) RIGHT''(o,t') = ready.o.t' -> ( transmit.o?mess -> read.o.t'!mess -> RIGHT''(o,t') [] transmit'.o?mess -> read.o.t'!mess -> RIGHT''(o,t') ) alphaLEFT''(o,t) = {write.o.t.m, transmit'.o.m, ack.o.t | m <- Bool} alphaRIGHT''(o,t') = {ready.o.t', transmit.o.m, transmit'.o.m, read.o.t'.m | m <- Bool} SHAREDCHANNEL''(o,t,t',t'') = ( (LEFT(o,t') [alphaLEFT(o,t') || alphaLEFT''(o,t'')] LEFT''(o,t'')) [union(alphaLEFT(o,t'),alphaLEFT''(o,t'')) || alphaRIGHT''(o,t)] RIGHT''(o,t) ) \ {transmit.o.m, transmit'.o.m | m <- Bool} alphaSHAREDCHANNEL''(o,t,t',t'') = alphaSHAREDCHANNEL(o,t,t,t'') assert SHAREDCHANNEL(0,0,1,2) [FD= SHAREDCHANNEL''(0,0,1,2) assert SHAREDCHANNEL''(0,0,1,2) [FD= SHAREDCHANNEL(0,0,1,2) -- -- June 2000: -- -- Now we consider JCSP implementation of an ALT -- -- The channel read method is a before but the write contains a -- call to Alt.schedule. -- -- -- Convention -- Writing threads are t and t' -- reading and alting thread is t'' -- Channels are o and o' -- Alt object is o'' -- -- We need an extra variable to include in the channel to represent -- the alt variable. -- channel getalt, setalt: Objects.Threads.Bool ALTING(o'') = ALTING2(o'',FALSE) ALTING2(o'',d) = ( [] t:Threads @ getalt.o''.t!d -> ALTING2(o'',d) ) [] ( [] t:Threads @ setalt.o''.t?x -> ALTING2(o'',x) ) alphaALTING(o'') = { getalt.o''.t.d, setalt.o''.t.d | t <- Threads, d <- Bool } -- -- The write method calls the schedule methods for object o''. -- These are coded up as `buddy' processes belonging to the ALT -- process, for convenience. -- channel startsched, endsched: Objects.Threads WRITE2(o,t,o'') = write.o.t?mess -> 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 -> getalt.o.t?alt -> if (alt == TRUE) then ( startsched.o''.t -> endsched.o''.t -> WAIT(o,t) ) else ( WAIT(o,t) ) ) else ( setvar.o.channel_empty.t!TRUE -> NOTIFY(o,t); WAIT(o,t) ) ) ; release.o.t -> ack.o.t -> WRITE2(o,t,o'') alphaWRITE2(o,t,o'') = { 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, startsched.o''.t, endsched.o''.t, getalt.o.t.d | v <- Variables, d <- Bool } -- -- A channel also needs enable/disable methods (called by the -- same thread as the reading thread. -- channel startenable, startdisable: Objects.Threads channel endenable, enddisable: Objects.Threads.Bool ENABLE(o,t'') = ( startenable.o.t'' -> claim.o.t'' -> getvar.o.channel_empty.t''?c -> if (c == TRUE) then setalt.o.t''.TRUE -> release.o.t'' -> endenable.o.t''!FALSE -> ENABLE(o,t'') else release.o.t'' -> endenable.o.t''!TRUE -> ENABLE(o,t'') ) [] ( startdisable.o.t'' -> claim.o.t'' -> setalt.o.t''.FALSE -> getvar.o.channel_empty.t''?c -> if (c == TRUE) then release.o.t'' -> enddisable.o.t''!FALSE -> ENABLE(o,t'') else release.o.t'' -> enddisable.o.t''!TRUE -> ENABLE(o,t'') ) alphaENABLE(o,t'') = {startenable.o.t'', endenable.o.t''.c, startdisable.o.t'', enddisable.o.t''.c, setalt.o.t''.c, claim.o.t'', release.o.t'', getvar.o.channel_empty.t''.d| c <- Bool, d <- Bool} -- -- Combine the new WRITE process with the alt variable (ALTING) and -- the enable/disable code (ENABLE) -- WRITE3(o,t,o'',t'') = ALTING(o) [alphaALTING(o) || union(alphaWRITE2(o,t,o''),alphaENABLE(o,t''))] (WRITE2(o,t,o'') [alphaWRITE2(o,t,o'')||alphaENABLE(o,t'')] ENABLE(o,t'')) alphaWRITE3(o,t,o'',t'') = union( alphaALTING(o), union(alphaENABLE(o,t''),alphaWRITE2(o,t,o''))) -- -- There is a complication in assembling the modified channel, because -- processes READ and WRITE3 must have interleaved access to -- getvar.o.channel_empty.t''?c, and also claim.o.t'' and release.o.t''. -- We have to use a carefully constructed form of interfaced parallel to put -- those two processes together. -- interface(o,t,o'',t'') = diff( inter(alphaREAD(o,t''),alphaWRITE3(o,t,o'',t'')), {getvar.o.channel_empty.t''.c, claim.o.t'', release.o.t'' | c <- Bool} ) JCSPCHANNEL2(o,t,t'',o'') = ( READ(o,t'') [|interface(o,t,o'',t'')|] WRITE3(o,t,o'',t'') ) [union(alphaREAD(o,t''),alphaWRITE3(o,t,o'',t'')) || union(alphaMONITOR(o),alphaVARIABLES(o))] ( MONITOR(o) [alphaMONITOR(o) || alphaVARIABLES(o)] VARIABLES(o) ) alphaJCSPCHANNEL2(o,t,t'',o'') = union(union(alphaMONITOR(o),alphaVARIABLES(o)), union(alphaREAD(o,t''),alphaWRITE3(o,t,o'',t''))) -- -- Now to code up the ALT object. -- -- -- First we make processes to represent the three variables: -- state, selected, and i. -- (this section could be tidied up a little) -- datatype State = ENABLING | WAITING | READY | INACTIVE channel getstate, setstate: Objects.Threads.State Selector = {0,1,99999} channel getselected, setselected: Objects.Threads.Selector Ivals = {0,1,2} channel geti, seti: Objects.Threads.Ivals -- -- State is initialised as INACTIVE. -- SSTATE(o'') = SSTATE2(o'',INACTIVE) SSTATE2(o'',d) = ( [] t:Threads @ getstate.o''.t!d -> SSTATE2(o'',d) ) [] ( [] t:Threads @ setstate.o''.t?x -> SSTATE2(o'',x) ) alphaSSTATE(o'') = { getstate.o''.t.d, setstate.o''.t.d | t <- Threads, d <- State } I(o'') = I2(o'',0) I2(o'',d) = ( [] t:Threads @ geti.o''.t!d -> I2(o'',d) ) [] ( [] t:Threads @ seti.o''.t?x -> I2(o'',x) ) alphaI(o'') = { geti.o''.t.d, seti.o''.t.d | t <- Threads, d <- Ivals } SELECTED(o'') = SELECTED2(o'',0) SELECTED2(o'',d) = ( [] t:Threads @ getselected.o''.t!d -> SELECTED2(o'',d) ) [] ( [] t:Threads @ setselected.o''.t?x -> SELECTED2(o'',x) ) alphaSELECTED(o'') = { getselected.o''.t.d, setselected.o''.t.d | t <- Threads, d <- Selector } STATE(o'') = I(o'') [alphaI(o'') || union(alphaSSTATE(o''), alphaSELECTED(o''))] (SSTATE(o'') [alphaSSTATE(o'') || alphaSELECTED(o'')] SELECTED(o'')) alphaSTATE(o'') = union(alphaI(o''),union(alphaSSTATE(o''), alphaSELECTED(o''))) -- -- Now for the scheduling code -- SCHEDULE(o'',t) = startsched.o''.t -> claim.o''.t -> getstate.o''.t?state -> ( if (state == ENABLING) then setstate.o''.t!READY -> SKIP else if (state == WAITING) then setstate.o''.t!READY -> NOTIFY(o'',t) else SKIP ); endsched.o''.t -> release.o''.t -> SCHEDULE(o'',t) alphaSCHEDULE(o'',t) = {startsched.o''.t, getstate.o''.t.s, setstate.o''.t.s, endsched.o''.t, notify.o''.t, claim.o''.t, release.o''.t | s <- State} -- -- Now for the selecting code -- channel query: Objects.Threads channel return: Objects.Threads.Selector SELECT(o'',t'',o,o') = query.o''.t'' -> setselected.o''.t''!99999 -> setstate.o''.t''!ENABLING -> seti.o''.t''!0 -> startenable.o.t'' -> endenable.o.t''?enabled0 -> (if (enabled0 == TRUE) then ( setstate.o''.t''!READY -> setselected.o''.t''!0 -> SKIP ) else ( seti.o''.t''!1 -> startenable.o'.t'' -> endenable.o'.t''?enabled1 -> if (enabled1 == TRUE) then ( setstate.o''.t''!READY -> setselected.o''.t''!1 -> SKIP ) else ( seti.o''.t''!2 -> SKIP ) )); claim.o''.t'' -> getstate.o''.t''?state -> (if (state == ENABLING) then ( setstate.o''.t''!WAITING -> WAIT(o'',t''); setstate.o''.t''!READY -> SKIP ) else ( SKIP )); release.o''.t'' -> geti.o''.t''?i -> (if (i == 2) then ( startdisable.o'.t'' -> enddisable.o'.t''?enabled1 -> (if (enabled1 == TRUE) then ( setselected.o''.t''!1 -> SKIP ) else ( SKIP )); seti.o''.t''!1 -> SKIP ) else ( SKIP )); geti.o''.t''?i -> (if (i == 1) then ( startdisable.o.t'' -> enddisable.o.t''?enabled0 -> (if (enabled0 == TRUE) then ( setselected.o''.t''!0 -> SKIP ) else ( SKIP )); seti.o''.t''!0 -> SKIP ) else ( SKIP )); setstate.o''.t''!INACTIVE -> getselected.o''.t''?n -> return.o''.t''!n -> SELECT(o'',t'',o,o') alphaSELECT(o'',t'',o,o') = { query.o''.t'', setselected.o''.t''.d, setstate.o''.t''.e, startenable.o.t'', endenable.o.t''.b, startenable.o'.t'', endenable.o'.t''.b, startdisable.o.t'', enddisable.o.t''.b, startdisable.o'.t'', enddisable.o'.t''.b, getstate.o''.t''.e, waita.o''.t'', waitb.o''.t'', notify.o''.t'', notifyall.o''.t'', getselected.o''.t''.d, return.o''.t''.d, claim.o''.t'', release.o''.t'', seti.o''.t''.i, geti.o''.t''.i | d <- Selector, e <- State, b <- Bool, i <- Ivals } -- -- Piece together ALT object: one SELECT process and two SCHEDULEs -- plus the STATE variables and MONITOR -- JCSPALT(o'',t'',o,t,o',t') = ((SELECT(o'',t'',o,o') [alphaSELECT(o'',t'',o,o') || union(alphaSCHEDULE(o'',t), alphaSCHEDULE(o'',t'))] (SCHEDULE(o'',t) [ alphaSCHEDULE(o'',t) || alphaSCHEDULE(o'',t') ] SCHEDULE(o'',t'))) [union( alphaSELECT(o'',t'',o,o'),union(alphaSCHEDULE(o'',t), alphaSCHEDULE(o'',t'))) || alphaSTATE(o'')] STATE(o'')) [union(union( alphaSELECT(o'',t'',o,o'),union(alphaSCHEDULE(o'',t), alphaSCHEDULE(o'',t'))),alphaSTATE(o'')) || alphaMONITOR(o'')] MONITOR(o'') alphaJCSPALT(o'',t'',o,t,o',t') = union(alphaMONITOR(o''), union(alphaSTATE(o''), union(alphaSELECT(o'',t'',o,o'),union(alphaSCHEDULE(o'',t), alphaSCHEDULE(o'',t'))))) -- -- Add in the two channel processes -- JCSPALTSYSTEM(o'',t'',o,t,o',t') = (JCSPCHANNEL2(o,t,t'',o'') [alphaJCSPCHANNEL2(o,t,t'',o'') || alphaJCSPCHANNEL2(o',t',t'',o'')] JCSPCHANNEL2(o',t',t'',o'')) [union(alphaJCSPCHANNEL2(o,t,t'',o''),alphaJCSPCHANNEL2(o',t',t'',o'')) ||alphaJCSPALT(o'',t'',o,t,o',t')] JCSPALT(o'',t'',o,t,o',t') alphaJCSPALTSYSTEM(o'',t'',o,t,o',t') = union(union(alphaJCSPCHANNEL2(o,t,t'',o''), alphaJCSPCHANNEL2(o',t',t'',o'')),alphaJCSPALT(o'',t'',o,t,o',t')) -- -- Now we shall define a simplified model of how the JCSP two-channel -- alternation should work, and then, hopefully, use FDR to show that this -- is equivalent to the JCSP implementation. -- -- -- The specification consists of two standard channels together with -- an ALT process which snoops the write channels to know when a -- channel is holding a message, and provides a selection interface -- to the reading thread. -- ALT(o'',t'',o,t,o',t',ready0,ready1,waiting) = write.o.t?mess -> ALT(o'',t'',o,t,o',t',TRUE,ready1,waiting) [] write.o'.t'?mess -> ALT(o'',t'',o,t,o',t',ready0,TRUE,waiting) [] ( if (waiting == TRUE) then ( if (ready0 == TRUE and ready1 == TRUE) then ( (return.o''.t''!0 -> ALT(o'',t'',o,t,o',t',FALSE,ready1,FALSE)) |~| (return.o''.t''!1 -> ALT(o'',t'',o,t,o',t',ready0,FALSE,FALSE)) ) else if (ready1 == TRUE) then ( return.o''.t''!1 -> ALT(o'',t'',o,t,o',t',ready0,FALSE,FALSE) ) else if (ready0 == TRUE) then ( return.o''.t''!0 -> ALT(o'',t'',o,t,o',t',FALSE,ready1,FALSE) ) else STOP ) else ( query.o''.t'' -> ALT(o'',t'',o,t,o',t',ready0,ready1,TRUE) )) alphaALT(o'',t'',o,t,o',t') = {write.o.t.mess, write.o'.t'.mess, query.o''.t'', return.o''.t''.s | mess <- Bool, s <- Selector} ALTSYSTEM(o'',t'',o,t,o',t') = ((CHANNEL(o,t'',t) [alphaCHANNEL(o,t'',t) || alphaCHANNEL(o',t'',t')] CHANNEL(o',t'',t')) [union(alphaCHANNEL(o,t'',t),alphaCHANNEL(o',t'',t')) || alphaALT(o'',t'',o,t,o',t')] ALT(o'',t'',o,t,o',t',0,0,0)) \ {transmit.o.mess, transmit.o'.mess | mess <- Bool } alphaALTSYSTEM(o'',t'',o,t,o',t') = {write.o.t.m, ack.o.t, ready.o.t'', read.o.t''.m, write.o'.t'.m, ack.o'.t', ready.o'.t'', read.o'.t''.m, query.o''.t'', return.o''.t''.s | m <- Bool, s <- Selector} -- -- We need to add a usage rule to reflect the way in which alt.select -- and channel.read are used. This is an additional parallel -- process which controls the ordering of the read interface events. -- USAGE(o'',t'',o,o') = query.o''.t'' -> return.o''.t''?c -> if (c == 0) then ( ready.o.t'' -> read.o.t''?mess -> USAGE(o'',t'',o,o') ) else ( ready.o'.t'' -> read.o'.t''?mess -> USAGE(o'',t'',o,o') ) alphaUSAGE(o'',t'',o,o') = {query.o''.t'', return.o''.t''.c, ready.o.t'', read.o.t''.mess, ready.o'.t'', read.o'.t''.mess | c <- Selector, mess <- Bool} JCSPALTSYSTEM2(o'',t'',o,t,o',t') = JCSPALTSYSTEM(o'',t'',o,t,o',t') [alphaJCSPALTSYSTEM(o'',t'',o,t,o',t') || alphaUSAGE(o'',t'',o,o')] USAGE(o'',t'',o,o') ALTSYSTEM2(o'',t'',o,t,o',t') = ALTSYSTEM(o'',t'',o,t,o',t') [alphaALTSYSTEM(o'',t'',o,t,o',t') || alphaUSAGE(o'',t'',o,o')] USAGE(o'',t'',o,o') -- -- We also need some protection against illegal events, e.g the -- thread which writes to the first channel is not allowed to -- alter the state of the second channel. -- PROTECTION2(o'',t'',o,t,o',t') = STOP alphaPROTECTION2(o'',t'',o,t,o',t') = {setvar.o.v.t'.d, getvar.o.v.t'.d, setvar.o'.v.t.d, getvar.o'.v.t.d, notify.o.t', notify.o'.t, waita.o.t', waita.o'.t, waita.o''.t, waita.o''.t', notifyall.o''.t, notifyall.o''.t', notifyall.o.t', notifyall.o'.t, claim.o.t', claim.o'.t, startenable.o.t, startenable.o.t', startenable.o'.t, startenable.o'.t', geti.o''.t.i, geti.o''.t'.i, seti.o''.t.i, seti.o''.t'.i, getselected.o''.t.q, getselected.o''.t'.q, setselected.o''.t.q, setselected.o''.t'.q, getalt.o.t'.d, setalt.o.t'.d, getalt.o'.t.d, setalt.o'.t.d, setalt.o.t.d, getalt.o.t''.d, setalt.o'.t'.d, getalt.o'.t''.d | v <- Variables, d <- Bool, s <- State, q <- Selector, i <- Ivals} JCSPALTSYSTEM3(o'',t'',o,t,o',t') = JCSPALTSYSTEM2(o'',t'',o,t,o',t') [alphaJCSPALTSYSTEM(o'',t'',o,t,o',t') || alphaPROTECTION2(o'',t'',o,t,o',t')] PROTECTION2(o'',t'',o,t,o',t') -- -- Now we compare the two systems: the specification and JCSP implementation -- -- In order to compare this specification with the JCSP implementation -- we need to conceal all the additional events in the alphabet -- Private3 = diff(alphaJCSPALTSYSTEM(0,0,1,1,2,2),alphaALTSYSTEM(0,0,1,1,2,2)) assert JCSPALTSYSTEM3(0,0,1,1,2,2)\Private3 [FD= ALTSYSTEM2(0,0,1,1,2,2) assert ALTSYSTEM2(0,0,1,1,2,2) [FD= JCSPALTSYSTEM3(0,0,1,1,2,2)\Private3 -- -- That works fine. Now we look at a previous broken version of the -- JCSP Alt. -- -- -- Bad version of write: reads the value of the alt variable right -- at the beginning -- BADWRITE2(o,t,o'') = write.o.t?mess -> claim.o.t -> getalt.o.t?tmp_alt -> setvar.o.channel_hold.t!mess -> getvar.o.channel_empty.t?c -> ( if (tmp_alt == TRUE) then ( setvar.o.channel_empty.t!FALSE -> startsched.o''.t -> endsched.o''.t -> WAIT(o,t) ) else 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 -> ack.o.t -> BADWRITE2(o,t,o'') -- -- Bad version of ENABLE: disable is not synchronised -- BADENABLE(o,t'') = ( startenable.o.t'' -> claim.o.t'' -> getvar.o.channel_empty.t''?c -> if (c == TRUE) then setalt.o.t''.TRUE -> release.o.t'' -> endenable.o.t''!FALSE -> BADENABLE(o,t'') else release.o.t'' -> endenable.o.t''!TRUE -> BADENABLE(o,t'')) [] ( startdisable.o.t'' -> setalt.o.t''.FALSE -> getvar.o.channel_empty.t''?c -> if (c == TRUE) then enddisable.o.t''!FALSE -> BADENABLE(o,t'') else enddisable.o.t''!TRUE -> BADENABLE(o,t'')) -- -- Bad version of SELECT: entire method is synchronized -- BADSELECT(o'',t'',o,o') = query.o''.t'' -> claim.o''.t'' -> setselected.o''.t''!99999 -> setstate.o''.t''!ENABLING -> seti.o''.t''!0 -> startenable.o.t'' -> endenable.o.t''?enabled0 -> (if (enabled0 == TRUE) then ( setstate.o''.t''!READY -> setselected.o''.t''!0 -> SKIP ) else ( seti.o''.t''!1 -> startenable.o'.t'' -> endenable.o'.t''?enabled1 -> if (enabled1 == TRUE) then ( setstate.o''.t''!READY -> setselected.o''.t''!1 -> SKIP ) else ( seti.o''.t''!2 -> SKIP ) )); getstate.o''.t''?state -> (if (state == ENABLING) then ( setstate.o''.t''!WAITING -> WAIT(o'',t''); setstate.o''.t''!READY -> SKIP ) else ( SKIP )); geti.o''.t''?i -> (if (i == 2) then ( startdisable.o'.t'' -> enddisable.o'.t''?enabled1 -> (if (enabled1 == TRUE) then ( setselected.o''.t''!1 -> SKIP ) else ( SKIP )); seti.o''.t''!1 -> SKIP ) else ( SKIP )); geti.o''.t''?i -> (if (i == 1) then ( startdisable.o.t'' -> enddisable.o.t''?enabled0 -> (if (enabled0 == TRUE) then ( setselected.o''.t''!0 -> SKIP ) else ( SKIP )); seti.o''.t''!0 -> SKIP ) else ( SKIP )); setstate.o''.t''!INACTIVE -> getselected.o''.t''?n -> release.o''.t'' -> return.o''.t''!n -> BADSELECT(o'',t'',o,o') -- -- Now we put it all together -- BADWRITE3(o,t,o'',t'') = ALTING(o) [alphaALTING(o) || union(alphaWRITE2(o,t,o''),alphaENABLE(o,t''))] (BADWRITE2(o,t,o'') [alphaWRITE2(o,t,o'')||alphaENABLE(o,t'')] BADENABLE(o,t'')) BADJCSPCHANNEL2(o,t,t'',o'') = ( READ(o,t'') [|interface(o,t,o'',t'')|] BADWRITE3(o,t,o'',t'') ) [union(alphaREAD(o,t''),alphaWRITE3(o,t,o'',t'')) || union(alphaMONITOR(o),alphaVARIABLES(o))] ( MONITOR(o) [alphaMONITOR(o) || alphaVARIABLES(o)] VARIABLES(o) ) BADJCSPALT(o'',t'',o,t,o',t') = ((BADSELECT(o'',t'',o,o') [alphaSELECT(o'',t'',o,o') || union(alphaSCHEDULE(o'',t), alphaSCHEDULE(o'',t'))] (SCHEDULE(o'',t) [ alphaSCHEDULE(o'',t) || alphaSCHEDULE(o'',t') ] SCHEDULE(o'',t'))) [union( alphaSELECT(o'',t'',o,o'),union(alphaSCHEDULE(o'',t), alphaSCHEDULE(o'',t'))) || alphaSTATE(o'')] STATE(o'')) [union(union( alphaSELECT(o'',t'',o,o'),union(alphaSCHEDULE(o'',t), alphaSCHEDULE(o'',t'))),alphaSTATE(o'')) || alphaMONITOR(o'')] MONITOR(o'') BADJCSPALTSYSTEM(o'',t'',o,t,o',t') = (BADJCSPCHANNEL2(o,t,t'',o'') [alphaJCSPCHANNEL2(o,t,t'',o'') || alphaJCSPCHANNEL2(o',t',t'',o'')] BADJCSPCHANNEL2(o',t',t'',o'')) [union(alphaJCSPCHANNEL2(o,t,t'',o''),alphaJCSPCHANNEL2(o',t',t'',o'')) ||alphaJCSPALT(o'',t'',o,t,o',t')] BADJCSPALT(o'',t'',o,t,o',t') BADJCSPALTSYSTEM2(o'',t'',o,t,o',t') = BADJCSPALTSYSTEM(o'',t'',o,t,o',t') [alphaJCSPALTSYSTEM(o'',t'',o,t,o',t') || alphaUSAGE(o'',t'',o,o')] USAGE(o'',t'',o,o') BADJCSPALTSYSTEM3(o'',t'',o,t,o',t') = BADJCSPALTSYSTEM2(o'',t'',o,t,o',t') [alphaJCSPALTSYSTEM(o'',t'',o,t,o',t') || alphaPROTECTION2(o'',t'',o,t,o',t')] PROTECTION2(o'',t'',o,t,o',t') assert BADJCSPALTSYSTEM3(0,0,1,1,2,2)\Private3 [FD= ALTSYSTEM2(0,0,1,1,2,2) assert ALTSYSTEM2(0,0,1,1,2,2) [FD= BADJCSPALTSYSTEM3(0,0,1,1,2,2)\Private3