Re: Poison

[P.H.Welch@xxxxxxxxx]

Adrian wrote:

> > So, despite the semantic complexities introduced by exception handling,
> > its application (for termination at least) on processes trying to use
> > a poisoned channel seems quite understandable - so there ought to be
> > a (formal) semantics out there that simply captures it ...
> 
> I've been too busy and distracted to follow this thread in detail, but
> as someone else pointed out, there is a formal semantics for an
> interrupt in standard CSP. It just doesn't appear in occam.

We'd better read (re-read!) section 5.4 of Hoare's CSP book (on interrupts,
catastrophic lightning strikes, restarts, checkpointing ...).

One thing that emphasises is that the event triggering the interrupt is
outside the alphabet of the process being interrupted:

  "... this restriction preserves determinism, and reasoning about
   the operators is simplified ..."

That seems fine for describing external KILL channels to a process but
doesn't seem to describe exceptions (which are not generated by the
environment but are the result of internal things going wrong)?

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.

In occam, Q's triggering event could be a channel input.  That channel is
not a SHARED input channel with P (although, maybe P could output to it?).
We could have a syntax:

  GUARD
    P
  WITH
    Q

As Adrian suggested, maybe this is equivalent to a transformed version of P
that has lots of PRI ALTs mixed into it (against the trigger input event
for Q).  For occam, this can of course only be done for input events of P
(which would make this weaker than Hoare's ^ operator).  For example:

  GUARD
    WHILE TRUE        -- successor process
      INT x:
      SEQ
        in ? x
        out ! x + 1
  WITH
    INT any:
    interrupt ? any
    ...  wind-up actions (may involve in and out?)

is equivalent to:

  SEQ
    INITIAL BOOL running IS TRUE:
    WHILE TRUE
      PRI ALT
        INT any:
        interrupt ? any
	  running := FALSE
        INT x:
        in ? x
	  out ! x + 1
    ...  wind-up actions (may involve in and out?)

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.

Humm ... the Q process *has* to be start with a channel input.  So, maybe
the WITH should be dropped and replaced directly with the trigger guard ...
or guards,  In this case, we need a shape like an ALT:

  GUARD
    INTERRUPTIBLE
      P
    interruptA ? any
      Q
    interruptB ? any
      R

So:

  (1) how useful would such a facility be compared to (a) no such facility
      and (b) a general exception mechanism?
  
  (2) how clean are its semantics (compared to a general exception mechanism)?

  (3) implementation costs?

On the last point, implementation via PRI ALTs against all inputs in the
interruptible process would be heavy :-( ... the costs of managing exceptions
(at least when they are not raised) I'm told are very cheap!

On the first point, not taking the interrupt when stuck on output may mean
this may leave a system deadlocked rather than (gracefully) terminated.
I deprecated using KILL channels for termination in that old paper for
that reason.  So maybe the semantics should be equivalent to PRI ALTing
the interrupt inputs against all communications (input and output) in the
interruptible process.  We just have to find a way to implement it.

On the first point again, what does this mean if the interruptible process
is itself a PARallel network?  When the network in interrupted, we need
to propagate that interrupt event down to all the processes in that network.
What if they are not programmed to take interrupts?  This is getting hard ...
in the CSP book, the interruptible process just disappears magically ...
regardless of any internal concurrency ... hmm ... maybe spreading poison
through the already existing application channels is best after all ...

This is fun - but I'm on holiday tomorrow and I've wretched QA monitoring
reports to write on last years' courses beofre I can go :-( :-( :-(

Peter.

PS. this all sounds like the PROTECTED processes supported by the T9000 ... ?