Choreographies should be able to figure out choice broadcasting

[ashton314]

Consider this example from the paper:

if ℓ₁.𝑒 then
  ℓ₃.𝑒′ ↝ ℓ₂.𝑥;
  ℓ1 [L] ↝ ℓ2;
  ℓ₂.𝑥 + 2
else
  ℓ₃.𝑒′ ↝ ℓ₂.𝑥;
  ℓ1 [R] ↝ ℓ2;
  ℓ₂.𝑥 + 3

The paper goes on to say that only ℓ₃ never needs to be informed because its behavior is the same down both branches; not so for ℓ₂, since its behavior depends on what ℓ₁ decides at the test in the if.

We should be able to figure out what parties actually need to know what the decision is and automatically add the decision-sending code by looking at the branches and analyzing how actors' behaviors differ. So, I'd like to be able to write:

if ℓ₁.𝑒 then
  ℓ₃.𝑒′ ↝ ℓ₂.𝑥;
  ℓ₂.𝑥 + 2
else
  ℓ₃.𝑒′ ↝ ℓ₂.𝑥;
  ℓ₂.𝑥 + 3

Is this tantamount to asking, "how much can I lift out of the if?"

[ashton314]

Indeed, with commit d714874 I had to do some funny work around branches: whenever you enter an if expression, we switch into processing the branch blocks in a pseudo-CPS mode. This is because the decision communication needs to wrap the rest of the computation together. (See how endpoint projection is defined for 〚ℓ₁[d] ↝ ℓ₂; C〛.)

Since decision communication is scoped to an if expression (i.e. it cannot sensibly appear outside an if) then the if should in principle be able to tell what parties need to know about the decision.

[bennn]

I'm confused. Why do branches need different processing?

Looking at this chunk from sec 5.3, the projection looks local. This translation could happen outside an if:

Is there trouble implementing choose and allow?

[bennn]

HasChor does choice broadcasting automatically: https://doi.org/10.1145/3607849

Sec 3.3 says it's for convenience, but may lead to more communication than necessary.

EDIT: the Choral paper has a longer discussion. https://dl.acm.org/doi/pdf/10.1145/3632398

Broadcasting seems like a very reasonable default! Can Chorex look ahead for choice-broadcast expressions and use the default only if there are none in the branch?