Hiding boundary nodes

[kasperdokter]

Consider the 'limping alternator' protocol:

LA(a,c) {
   sync(a,c)
   syncdrain(a,b)
   fifo1(b,c)
}

It has one source node, a, and one sink node, c. Node b is not in the interface of LM and is therefore hidden. The expected behavior of the limping alternator is empty. That is, any put operation on a and get operation on c are blocked forever. The reason is that hidden node b is a source node that is not connected to any producer (which is the same as saying that it is connected to a silent producer component that does not output any values).

Unfortunately, the current compiler incorrectly compiles the limping alternator as a plain sync channel. The reason is that the compiler applies existential quantification to the data value observed at node b. However, existential quantification is correct only for mixed nodes. In this case, existential quantification simply matches up the different components that produce values at the mixed node. For boundary nodes (i.e., source and sink nodes), existential quantification acts like a generator that produces random data out of thin air.

To correct the problem, the compiler must first prevent applying existential quantification to boundary nodes, and simply generate and unconnected node in the target code. Then, we obtain the desired behaviour.