On 1 Oct 2012, at 17:07, Larry Dickson wrote:
NO! In a 'when' construct, any running process is pre-empted by a higher priority one (higher up list), whenever it's guard becomes ready. When the higher pri one terminates then it will resume. Sorry if that was not clear.
The problem arises when you compose PRI constructions in parallel with conflicting priority, which might arise through the pattern of communication across a network of processes. For example:
... respond to b
... respond to a
which deadlocks. (Excuse the tabs. I too favour 2-space indents, but not with variable width font.)
I agree it achieves something similar, but it still presumes concurrency with the lower priority process. Communication with that process will be both contrived and potentially messy. How will the low priority process learn the counter value? We're back to channels between processes of differing priority, which is precisely what I wish to avoid. Combined, these have much more in common with sequential behaviour than concurrent.
Also, what if one of the lower priority processes in the ALT took a long time to complete. We will miss 'ticks'. It's not the behaviour I wanted.
Your proposal is anyway far less transparent than :
event a then
event b then
where 'idle' equates with a SKIP guard. And I prize transparency above all else. The meaning ascribed to priority here is (IMHO) crystal clear.
The relative 'weight' of P and Q are immaterial.
Again, I have not described 'when' very well here, for which I apologise. The idea is that each clause is recursive (remains available after the termination of its guarded process) until it either disables itself or is disabled by a peer. The complete construction terminates only once all its member clauses terminate.
Yes, this does mean shared variables, but 1) we restrict these to a single construct (which can have a danger sign painted on it) and 2) we alleviate the risk with the restriction that only a single 'owner' can assign them. As we know, people have been building such systems around PVI for a very long time, with nothing more than a little care. When it comes to formal correctness, it's my understanding that CSP has difficulty with prioritisation anyway.
And I'd still like to keep prioritisation in a single construct (and thus interpretation) only. You've combined the two.
I'm not saying that my proposal is any way ideal, but just that there is a problem here (which may indeed relate to the difficulty the CSP folk have in dealing with prioritisation). (Incidentally, Bill Roscoe in UCS proposes establishing prioritisation over a system, in the form of a partial order. I'm not sure what the implications are for programming but I think he is saying "program without prioritisation, then impose one", without embellishing the language in any other way, then explore its behaviour (with FDR). I'm still not sure what the implications for programming are.)
PS I shall have very little time from now for a few days, so may have to pass on further discussion, though I shall still read further posts. It's been fun, even if we've failed to convince each other!