| Thank you, Bill! I think I am onto it, where the problem is what is hiding. References are Roscoe, Theory and Practice of Concurrency, and Martin, The Design and Construction of Deadlock-Free Concurrent Systems. It is the failures rule for hiding which (assuming divergence freedom) is failures(P\X)={(s\X,Y)|(s,YUX) in failures(P)} (Roscoe p 199) or for a single hiding, failures(P\x)={(s|\(Sigma-{x}),X)|(s,XU{x}) in failures(P)} (Martin p 18). Repeated applications of Martin's rule gives Roscoe's rule. In either case, multiple different traces of P collapse to a single trace of P\X by "collapsing" states that are connected by members of X, and refusals only count if the refusals in P contain every member of X. It is clear that this is needed to make the algebra work, and we just hope it corresponds to something in real programs - a point not clearly addressed in the references. The notion that they are the refusals of a stable state doesn't seem quite right. (The Roscoe p 94 description of case P2 does not correspond to the picture on p 93, by the way, because hiding should have eliminated c from refusal sets.) Applying the above rule to ((c->a->STOP)[](b->STOP))\c starts with a maximal refusal on the top node before hiding of {a}, and therefore the rule looks only at the node after the c, and you get the sliding choice. However, applying the above rule to ((c->a->STOP)|~|(b->STOP))\c, before the hiding the top node has maximal refusals {a,b} and {a,c} and the latter does make a contribution, as does the node after the c, so you get maximal refusals {a} and {b} after the hiding. The solution to the conundrum seems to be that a process with hiding is not the same as the process without hiding. The solution seems to be that an event that is to be hidden must satisfy both the conditions (i) it is completely under the control of the process and needs nothing from the environment, and (ii) it is promptly on offer where written at a state. Neither of these conditions are required if the event is not to be hidden. In particular, (ii) is replaced with the possibility that the event may be immediately on offer OR it may only be offered after a long time. Thus, the {b} that may be refused in the sliding choice above is really a {b,c} where it counts as refusal if c wins the race, while the {a} that must be accepted is really an {a,c} without the b, so that it has to accept the c, and the a may arrive later and if early stays on offer until c is executed. The second case is easier to understand since the original top may insist on b even though c was on offer, and then get hung on an offer of {a} even if it really means {a,c}; or it may take c and get hung on an offer of {b} after that. I think this links up nicely with my Ground Truth stuff (Fringe, CPA2017), which basically defines "promptly" as a Straight Sweep, which means a continuous stream of executed instructions, without blocking within the process - but allowing overlapping of multiple sub-processes and communication - leads to the event in question. See Active Sweep, Progress, and Straight Sweep in the first Fringe, slides 9 and 10. It refers to Transputers, both soft and hard linked, but the same thing will work for any reasonable processor. Fast, busy execution without divergences will get to the event in microseconds or less, while human-scale events from the environment take a big fraction of a second or more. So the distinction is practically clear, if not theoretically. Larry Dickson On Dec 22, 2018, at 2:00 PM, Bill Roscoe <awroscoe@xxxxxxxxx> wrote:
|