What are legal connections between channel instance references? Channels have directional connection semantics. Two value producers cannot be aliased, nor can two consumers.
Q: Should legal programs be restricted to connecting at most one-receiver to one-sender?
A: Yes, until we support shared channels (see below).
Q: Should dangling channels (one-way only) be allowed, rejected, or warned? Does not count definition ports, which are assumed to be connected.
Clarification: Channel directions indicated in port declarations only dictate which direction one cannot connect to locally.
We use the following example program template to answer questions.
defproc inner(chan(bool) A; chan?(bool) B; chan!(bool) C) { ... } defproc outer(chan(bool) P; chan?(bool) Q; chan!(bool) R) { inner x(...), y(...); }
Goal: precise set of rules for channel connections. Q: does it depend on whether or not referenced channel is local vs. port?
Proposal: a read-only port can take a directionless or read-only port (forwarded) channel as an argumnent. (Likewise for send-only ports.) (Update: accepted.)
Should we allow alias connection syntax for channels? Aliasing is a symmetric relation, whereas port connections need not be. Yes, but with the following additional semantic constraints:
Proposal: Unidirectional channels should not be referenceable as aliases, only connected through ports. Only nondirectional channels may use alias syntax. Thus, directional channels may only be connected by passing port arguments. Consequences: every physical channel must be connected to at least one nondirectional channel. A send-receive pair must be connected using a nondirectional channel of the same type. (Status: obsolete, in favor of the proposals below)
Proposal: A nondirectional channel may be connected to only one read-only channel and only one send-only channel. (Update: accepted, with possible exception of explicitly shared channels, proposed below.) The following example would be rejected:
defproc bucket(chan?(bool) S) { ... } chan(bool) R; bucket a(R), b(R);
Implementation detail: As aliases are built using a union-find, make sure the canonical node always knows what direction of channels have been connected (propagation). We will track this with a set of flags indicating whether a channel is already connected to a producer or consumer. Note, however, that send/receive use of a channel in CHP body counts as connecting a consumer/producer, respectively. Thus, channel connection checking should include a final pass over the CHP's unrolled footprint.
Proposal: Reject local channel declarations with directional qualifiers. Rationale: It doesn't make sense to have a uni-directional channel in a local scope because any connection or use thereof would result in a block. (Could this be useful for debugging, e.g. causing intentional deadlock?)
Proposal: Reject dangling channels. Channels that are missing connection to a producer or consumer should be rejected. Basically, when a channel is deduced as dangling, at least a diagnostic should be issued. Resolution: issue warning diagnostic, without rejecting outright. Eventually, it is up to the final tool to accept or reject dangling connections.
Proposal: Shared channels: Thus far, we've described one-to-one channels where producers and consumers are exclusively paired. In some exceptional circumstances one might desire to share a channel among multiple senders or multiple receivers, where exclusive access is to be guaranteed by the programmer. The following semantics are proposed for sharing channels: A channel is allowed to be connected to multiple receivers, if and only if all participating receivers agree to share, by some implementation of `agree.' Likewise, multiple senders may share a channel, if and only if all participating senders agree to share. One end of communication on a channel is indifferent to whether or not the other end is shared; a non-shared sender however may connect to shared receivers, and a non-shared receiver may connect to shared senders; To mix shared and non-shared uses on the same end is considered an error.
Rationale: Since channel sharing is exceptional, we want to prevent inadvertent sharing of channels. Non-shared channels expect exclusive use of the channel, so to share them would violate the fundamental assumption.
Syntax: a port declared with ?? or !! indicates that the channel may be shared (by receiving or sending). A ?? port channel may be connected locally to multiple receivers, and a !! port channel may be connected locally to multiple senders. When referenced externally, as a member of process, ?? ports may share the same channel as multiple receivers, and !! ports may share the same channel as multiple senders.
TODO: examples.
Q: should process aliases be allowed, if processes declare directional channel ports? (Without further modification, they are rejected when attempting to connect ports recursively.)
defproc sink(chan?(bool) X) { } sink x, y; x = y; // results in x.X = y.X
Q: What is the initial `connected' state of a non-directional channel port (inside definition)? A: a read-only port is assumed to be connected to a producer, and a write-only port is assumed to be connected to a consumer.
Q: Should local `connected' state information be propagated from formal collections' aliases to actual collections' aliases? With this, channels that are locally dangling can be properly connected hierarchically. A: Yes, we propagate local connectivity summaries up through formals to initialize the connectivity state of substructure actuals for more precise hierarchical alias analysis. This may help check connectivity of non-directional channels. NOTE: this would also apply to relaxed actuals, and is a necessary step towards properly implementing them (a general mechanism to propagate local information externally). TODO: illustrative examples.
Q: Do we allow a channel (member of an array) to be referenced by both meta-parameter and nonmeta-parameters? No. Rationale: Nonmeta indexed channels introduce another difficulty, as they cannot be analyzed at compile time... Effectively, this restricts mixing of meta-aliasing and nonmeta-referencing, at least for channels, variables may be another issue. This issue is related to alias disambiguation.