Hi Jeremy, > So far my FDR analysis of JCSP has been met with total silence, perhaps > because most of you are away on holiday ... Sorry - I'm back for a while now but hope to grab a few more days sometime! > Here is an FDR analysis of your model for java threads which shows that > the JCSP channel is equivalent to something very simple in CSP. You have had a very good idea here!! I was getting worried that that CSP model of Java threading wasn't helping ... very well done :-) :-) :-) Error in my CSP model for Java threads ====================================== > I found > a couple of very minor bugs in your initial CSP specification, but > otherwise I stayed true to your definition. And in your last message: > In Peter's CSP model the wait method was defined like this... > > WAIT(o,me) = release.o.me -> waita.o.me -> waitb.o.me -> claim.o.me -> > SKIP > > Using this definition I found that JCSP was incorrect - the channel may > deadlock. The reason is that there is window of time between events > release.o.me and waita.o.me where a thread neither holds the monitor > nor belongs to the auxilliary pool of waiting threads. During this > time interval it is possible for a notify event to be fired and > to miss its target. > > So I redefined the wait method like this... > > WAIT(o,me) = waita.o.me -> release.o.me -> waitb.o.me -> claim.o.me -> > SKIP > > Now everything works out fine, because a thread holds onto the monitor > until after it has joined the waiting pool.. > > But was I right to do this? Or do implementations of Java exist where the > time interval that Peter modelled really does happen? I hope not, because > if that were so JCSP would be prone to arbitrary deadlocks, and we would > all have to go back to the drawing board. YES - you are right to make this change. The JCSP channel implementation stays ... I just got the CSP model of the wait wrong (as you immediately dicovered when you tried to run a proof of the channel correctness through FDR - another win for the use of formal tools). Quoting from Doug Lea's "Concurrent Programming in Java": (Following a wait) the JVM places the thread in an internal and otherwise inaccessible `wait set' associated with the target object. The synchronization lock for the target object is released, but all other locks held by the thread are retained. where the context of the quote implies that the above paragraphs happen in the given sequence. So all JVMs are obliged to follow the sequence of your above revision. [Aside: Doug Lea, whilst not being a part of Sun-JavaSoft, is an authority we can trust on these matters.] However, there is one knock-on from this change that ought to be addressed. When the WAIT(o,me) kicked off with the release.o.me, it was automatically prevented from happening unless the LOCK(o) had been claim.o.me'd. This is because that release.o.me is part of the alphabet of LOCK(o) which, if not claim.o.me'd, would refuse it. [I think an earlier draft of the model had the relase and the waita the right way round ... I think I was tempted astray by this automatic `benefit' :-( ...] 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 ... ?] 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? [Note: I think there's a typo in the model in your first mailing. In your SWAIT(o,ts) and RELEASE(o.ts), you use waitb.o!s and waitb.o!t. In your WAIT(o,me), you also use waitb.o!me. Both sides of the channel are writing! Shouldn't that get rejected by FDR? One side ought to be reading or, as in your last email, just use dots.] [Another typo: in your definition of alphaCHANNEL(o,t,t'), the "t'"s on the write.o/ack.o events should be on the ready.o/read.o ones instead - I think?] 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??? 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 ... ;-) ... ??? 1-1, Many-1, 1-Many and Many-Many Channels ========================================== After your FDR assertions that CHANNEL and JCSPCHANNEL refine each other, you write: -- That works fine with the current system where only two threads -- are in existence, but when we increase the number of threads in the -- system beyond two, perhaps by redefining 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.) The read/write methods you checked were from page 274 of the WoTUG-21 proceedings and are only safe to use for a channel between one reader and one writer (at a time) - i.e. a 1-1 channel. This is a usage rule for occam channels and it is only intended to be secure if we abide by that. In occam, under KRoC, SPoC or a transputer, if we switch off that usage checking and allow more than one process to read from (or write to) a channel in parallel, the channel implementation also fails. So, I'm comfortable with this usage rule. [Have I understood your point here?] I would be interested in your checking the other forms of channel :-) ... A Many-1 channel is an efficient, but restricted, form of (fair) ALTing - just like an occam3 SHARED channel. The Many-1 channel code can be extracted from the code on page 276 of WoTUG-21 - replace the `read' with the `read' from page 274. Page 276 gives the Many-Many channel. A 1-Many channel is the page 276 stuff, but using the `write' from page 274. CSP, of course, doesn't have a Many-1 channel primitive - but it does have choice primitives. What we want to prove is that a Many2OneJCSPCHANNEL is the same as a Many2OneCHANNEL process modelled, in the spirit of the above simplification, by something like: Many2OneCHANNEL(o,t') = [] t:diff(Threads,{t'}) @ write.o.t?mess -> read.o.t'!mess -> write.o.t?any -> Many2OneCHANNEL(o,t') alphaMany2OneCHANNEL(o,t') = {write.o.t.m, read.o.t'.m | t <- diff(Threads,{t'}), m <- Data} The One2ManyCHANNEL model may need to go back to your (LEFT||RIGHT) model, as will certainly the Many2ManyCHANNEL - left for another day. ALTing ====== Many ALTing scenarios can be modelled more simply and efficiently with a Many-1 (SHARED) channel. But ALTing *is* more flexible than Many-1 and probably needs to be retained - for example, sometimes we may want to choose between channels {a,b,c} and other times from {b,c,d}. That can't be supported by a Many-1 concept. But we leave this for later! Cheers, Peter.