[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
RE: Poison
Peter wrote:
>
> Anyway, we have:
>
> P ^ Q
>
> which means a process that behaves like P until Q becomes
> runnable ... at which point it becomes Q. Q is blocked
> initially awaiting some event from its environment. Q's
> triggering event is not in P's alphabet.
> So, the GUARDed process only becomes vulnerable to interrupt
> at input points in its code ... and will be interrupted if
> the interrupting communication is being offered by the enviroment.
A process could interrupt on any event: channel-input, channel-output,
channel-call, channel-accept, termination events.
I guess, the interrupt operator is more likely a PRI PAR than like a PRI
ALT. Say, the interrupt event has higher priority than all other events
in P. This special PRI PAR needs to terminate (or kill) P immediately
when P is preempted by Q.
The GUARD is this special PRI PAR. (In my email I called it INTPAR)
GUARD
P
Q -- interrupt handler for P
In the same way we could preempt Q with R.
GUARD
P
GUARD
Q -- interrupt handler for P
R -- interrupt handler for Q
The interrupt event is not shown in the example and may not be
necessary. This is because all events in Q have higher priority than the
events in P, and all events in R have higher priority than the events in
Q.
This also deals with
GUARD
PAR
P
Q
R
T -- interrupt handler for (P||Q||R)
(= (P||Q||R)^T
GUARD is a process.
I guess, we could inherit the PRI PAR semantics as described by Adrian
to describe the semantics of the '^' operator. Adrian....? I think, I
can build a GUARD using CTJ's PRI PAR implementation.
Gerald.