Re: Conflicting Priorities in occam

[<P.H.Welch@xxxxxxxxx>]

Adrian,

> Is occam defined?
> ~~~~~~~~~~~~~~~
> "Lower priority processes may only continue when all higher priority processes
> \emph{are unable to}."
> PRI PAR: from occam 2 Reference Manual, page 71. My \emph.
> 
> So that's all right then:
> 
> PAR                 
>   PRI PAR           
>     b ! 2           
>     a ! 1
>   PRI ALT
>     a ? x
>       SKIP
>     b ? y
>       SKIP
> 
> will always communicate on b? I am confident that is what David(?) meant
> when he wrote it. That is the natural idea when you think of a sequential
> implementation on a microprocessor.

I don't think the above code is undefined - just non-deterministic.
It certainly won't (shouldn't?) deadlock though!

Let's talk about a uniprocessor implementation first.

It all depends on the order in which things get scheduled.  All the
PRI PAR means is that the "b ! 2" will be started before the "a ! 1".
But the ordering between the "a ! 1" and the PRI ALT is not defined.

If the "a ! 1" happens before the PRI ALT, the "a" communication will
be taken by that PRI ALT.  Otherwise, the "b" communication will be.

It's also possible for the PRI ALT to be scheduled before the PRI PAR
process, so that the PRI ALT happens before the "b ! 2".  In which case,
the "b" communication takes place.

So, either of these outcomes is possible and either is correct.

That might mean the occam has a `soft'-PAR, but I'm not sure?  Let's
look at some transformations:

    PAR               is equivalent to       ALT 
      a ? x                                    a ? x
      b ? y                                      b ? y
					       b ? y
						 a ? x

so I guess:


    PRI PAR       should be equivalent to    PRI ALT 
      a ? x                                    a ? x
      b ? y                                      b ? y
					       b ? y
						 a ? x

Is it???  If so, then the same should apply to the above with "!" instead
of "?" - i.e.:

    PAR               is equivalent to       ALT 
      a ! x                                    a ! x
      b ! y                                      b ! y
					       b ! y
						 a ! x

so I guess:


    PRI PAR       should be equivalent to    PRI ALT 
      a ! x                                    a ! x
      b ! y                                      b ! y
					       b ! y
						 a ! x

OK - the output guards aren't kosher occam, but semantically it makes
sense.  By semantically, I mean formally semantically!

In which case, your original example transforms to:

  PAR
    PRI ALT
      b ! 2
	a ! 1
      a ! 1
	b ! 2
    PRI ALT
      a ? x
        SKIP
      b ? y
        SKIP

and ... we are back to your original dilemma.  The above code certainly
requires semantic sorting out into "hard"-PAR (==> deadlock) or "soft"-PAR
(==> non-deterministic choice between either communication).

Current occam implementations (KRoC certainly and, I'm sure, SPoc) will
implement the "soft"-PAR semantics.  Dunno what FPGA (or other real
parallel hardware) will/should do ...

Our shared-memory multiprocessor KRoC will also give "soft"-PAR semantics.
It all depends *when* things happen.  I don't believe it will ever deadlock
... it better not!

Cheers,

Peter.

PS. won't be able to read the rest of your last email till Tuesday :-( ...