🚀 go-pugleaf

In article <1772@culhua.prg.ox.ac.uk> geraint@prg.ox.ac.uk (Geraint Jones) writes:
>
>The implementation can only be `secure' in the sense that it implements the
>language as defined.

That's all that I said.  Perhaps I should not have implied more than that.
  
>In any non-trivial language with while loops, you
>will never get a mechanical guarantee from the compiler that the program
>terminates.  In the same way, in any dialect of occam with CHAN OF ANY,
>you will not get a mechanically checked guarantee of proper channel use.
>And serve you right.  Of course, you might want a compiler for particular
>applications to reject CHAN OF ANY declarations, but then it wouldn't be
>an occam2 compiler, would it?

Sure enough, you are correct.  That just says that "unsatisfactorily" matched
processes synchronizing via a CHAN OF ANY can be part of a *valid* occam
program.  (Analogously, as you point out, an infinite loop can be part of a
valid Pascal (for instance) program.)

Now, I'm really not familiar with the occam 2 definition of communication
over a CHAN OF ANY, but the fact that such programs are valid seems to lead
to a problem.  Namely, the parallel composition of two deterministic, valid
processes may yield one (overall) process when the composition is within a
single transputer, and may yield a completely different process (STOP, for
example) when the composition involves two transputers.  

Now I haven't checked, but I have been of the impression that the occam 
definition has intended to make PAR and PLACED PAR identical in composing 
two or more processes into a single (overall) process.  (That is, the only 
difference should be in the system's implementation of the composition.  
Abstractly, the composition is identical.)  If this is the case, then the
system would appear to be doing something to violate the definition of 
occam.

If, on the other hand, occam does prescribe such a differentiation, then
the system is fine, but (at least this feature of) occam sure is a mess.
I know I wouldn't want to be working on the semantics for such language
features (so tied to implementation details).

Any thoughts shedding further or better light on this question shall be
greatly appreciated.


Jonathan