Closed jclark closed 6 months ago
public function main() {
worker w1 {
if true {
// <channel_w1w3_2.close()>
2 -> w3; // channel: w1w3_1
} else {
3 -> w3; // channel: w1w3_2
}
4 -> w3; // channel: w1w3_3
}
// Case 1
worker w3 {
_ = <- w1; // both w1w3_1 and w1w3_2 match here.
_ = <- w1; // w1w3_3 matches here
}
// Case 2
worker w3 {
_ = <- w1; // w1w3_1 matches here
_ = <- w1; // w1w3_2 matches with NoMessageError
_ = <- w1; // w1w3_3 matches here
}
// Case 3
worker w3 {
_ = <- w1; // w1w3_1 matches here
_ = <- w1|w1; // both w1w3_2 and w1w3_3 match here
}
// Case 4
worker w3 {
_ = <- w1|w2; // both w1w3_1 and w1w3_2 match here
_ = <- w1; // w1w3_3 matches here
}
// Case 5
worker w3 {
_ = <- w1|w2|w3;
}
}
From the above 5 scenarios, what are the valid cases? All sends have a receiver (i'th send in w1 is associated with the i'th channel in w3) except in the first case.
The new concept is that you match up actions (in the syntax tree). Each alternative in an alternate receive matches one send action. So:
We might want to give errors for receives that are guaranteed to give a NoMessage.
Consider the below code:
Here I am matching up the send actions to receives based on the breadth first approach for if-else. Case 1 and case 2 if-else are the same. However, the receive result is different in both cases(depends on where we start). We need to have a the same result for both case 1 and 2 right?. In that case, how do we match the send-receive pairs?
The matching is very simplistic. The i-th send action is matched with the i-th receive action (apart from complication with alternates). No, 1 and 2 aren't the same. (We could disallow the case where two parallel branches both have a send to the same place if we wanted to.)
The specification requires that whenever a worker is executed and execution does not fail, then the same sequence of send actions is executed. Sends in a conditional context are very limited: they are only allowed when both branches execute and send the same value. The current implementation does not allow sends in a conditional context at all.
We want to fix this for #1271 by changing the specification semantics so that sends can happen within a conditional context in a much more flexible way. For cases supported by the implementation, the semantics should be unchanged.