[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)

  Q -- interrupt handler for P

In the same way we could preempt Q with R.

    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

This also deals with

  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.