[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: x2AnyChannels do not allow alting
> > In CSP, the PAR operator is defined in terms of external choice (sort of
> > ALTing). In occam, we all know the following equivalencees:
> > PAR == ALT
> > in0 ? x0 in0 ? x0
> > in1 ? x1 in1 ? x1
> > in1 ? x1
> > in0 ? x0
> I didn't!
> Maybe it's a question of what "==" means, see below.
It means equivalent under the denotational semantics for occam (or, in its
CSP form, for CSP). See the Transputer Communications article for the full
definitions ;-) ...
At least, I'm pretty sure that's right - confirmation please from Oxford?
> My interpretation ...
> The ALT case indicates that we either do SEQ( in0?x0; in1?x1 ) or
> SEQ( in1?x1; in0?x0 ) which give the same result as each other and as
> concurrent execution of both inputs. So, the ALT form is a valid
> IMPLEMENTATION of PAR, but not the only one - true concurrency is also
But, also, the PAR form is a valid implementation of that ALT and a clever
compiler targetting a multiprocessor or silicon could choose to do that