[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

RE: x2AnyChannels do not allow alting

Marcel wrote:

> 6. It is possible to implement the new *2AnyAltingChannel, but there are
>    three problems:
>    - The implementation will be frightenly complex, and therefore it will be
>      difficult to proof its correctness. [agree, but we also agree that
>      difficult does not mean impossible, in fact I think it should be
>      possible]

Yes - I think it probably is possible ... but I'm still recovering from the
difficulty of writing the mutually interacting monitors that implement the
ordinary *2OneCahnnel ALT.  That's only a page and a bit of source code but
took about three years to get right ... and that still needs proving!

>    - The implementation will be inefficient (Peter writes: possibly
>      a time-consuming policing action is needed to sort things out)
>      [doubtful, I cannot imagine the implementation take more than
>      O(nreaders)]

That may be O(nreaders) per *2AnyAltingChannel branch of the ALT, making
O(nreaders*nbranches) altogether :-( ... the nice thing about doing a
committed input from a *2AnyChannel is that it's O(1) - i.e. independent
from the number of competing readers.

One problem for an implementation of a *2AnyAltingChannel is that a process
will need to be pulled from the queue it is on (along with its competitor
processes for servicing the channel).  In principle, I don't like pulling
things from queues - it's not a queue operation (like enqueue/dequeue) and
takes O(n) time (unless you have back pointers which add an extra, though
fixed overhead to everything).  I'll mention this again when discussing
the Mars Pathfinder mission ...

In fact, both JCSP and CJT implement security in the competition for a shared
channel (reading or writing end) by synchronising on a (reader or writer)
monitor lock.  [Java does not specify that such competition is resolved by
queuing, but almost all -- and all sane -- JVMs do.  The two competitive
proposals for real-time Java do mandate queuing when blocked on trying to
acquire a monitor.]  But no way does Java allow a thread that's tried to invoke
a synchronized method back out of that invocation.  So, to implement an
*2AnyAltingChannel secufely, we would have to do something else ... :-(

>    - It is difficult to think of a usage for the new *2AnyAltingChannel.
>      [interesting point]
>   Imagine a distributed multiprocessor computer system with a number
>   of resources (harddisk, screen, network). Some CPUs have access
>   to a subset of these resources. E.g., two CPUs have network access;
>   two can access the screen, and two can access the harddisk.
>   A CPU can only access one resource at a time. E.g., because a
>   single IO region needs to be used for any of the resource accesses.
>   To access the resources, the new Any2AnyAltingChannel can be
>   used in a natural way.
>   Any2AnyAltingChannel harddisk;
>   Any2AnyAltingChannel screen;
>   Any2AnyAltingChannel network;
>   Process CPU1 {
>     ALT
>       harddisk -> execute(harddisk?);
>       network  -> execute(network?); 
>   }
>   Process CPU2 {
>     ALT
>       harddisk -> execute(harddisk?);
>       screen   -> execute(screen?); 
>   }
>   Process CPU3 {
>     ALT
>       screen -> execute(screen?);
>       network  -> execute(network?); 
>   }
> Is this a convincing example?

Can I assume that each CPU above is offering a repeated service on the two
devices it is looking after?  That is each ALT is enclosed by a WHILE-loop:

   Process CPU1 {
         harddisk -> execute(harddisk?)
         network  -> execute(network?)

This means that this CPU1 would *either* be servicing a harddisk request *or*
a network request - but not both.  Let's make the run-time system do the
scheduling (rather than do it ourselves with an ALT) - e.g.:

   Process CPU1 {
	 harddisk -> execute(harddisk?)
         network  -> execute(network?)

Now, each CPU has two processes and can interleave their execution so that
the two devices may be serviced in parallel.  Each process competes with
a server process on one of the other CPUs - so that there will not be
contention for one device between CPUs.

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

where a symmetric balanced ALT is in fact just a simple PAR.  And that:

  PAR                   ?==?            ALT
    in0 ! x0                              in0 ! x0
    in1 ! x1                                in1 ! x1
				          in1 ! x1
					    in0 ! x0

i.e. if our *output* guards have this symmetric balanced pattern, then we
*can* have them - because they are just a PAR (and efficient).

Your example of ALTing over an *2AnyAltingChannel is similarly (but differently)
regular, and a similar trick seems to work.  The channels now only need to be

The PAR-of-two-WHILEs is not quite the same as the WHILE-of-a-two-branch-ALT,
particularly if there is some state information that needs to be updated and
shared between the PAR processes.  Maybe someone from Oxford (Adrian/Jeremy?)
could fill in the details ...

> ps2. When and where is the next WoTUG conference?

I'll post an announcement next!



PS. I just remembered another reason why JCSP has a One2OneChannel.  A key
    semantic point about occam is that its PAR construct does *not* introduce
    non-determinism.  To do that, we have to be explicit and write an ALT
    (or turn off the parallel usage checking!).  That gives a very comfortable
    basis for working with concurrency - both deterministic (e.g. for the
    supercomputing world) and non-determonistic.  Non-determinism can't sneak
    in by default.  A JCSP parallel network that only uses One2OneChannels
    is the same (almost) as occam - it's deterministic by default unless
    we explicitly introduce an ALT, disregard occam's parallel usage ruless
    (sadly unchecked) or put overwriting buffers in the One2OneChannels
    (non-overwriting buffers are OK).  But as soon as we have an Any-* or
    *-Any channel, we have effectively (but efficiently) introduced a simple
    ALT and its non-determinism.