The with operator

[rachitnigam]

Calyx currently supports a with in three locations: invoke, if, and while. The basic idea is that some operations need to execute a combinational group to make combinational components active during execution before reading values from the output ports of the respective combinational operator.

The current with operator has the following nice properties:

1. Reasoning is local. Since the combinational group is only defined to be active for a specific part of the execution---while the condition is evaluated for if and while and while the component is executed for invoke---it does not disrupt local reasoning of groups and control operators.
2. Easy to compile into normal groups. This is because of (1). All uses of comb groups can be turned into normal groups using the remove-comb-groups pass.

I am going to claim that (1) & (2) are good and probably important properties to maintain when extending the language. There are two competing proposals for a more general with operator in my mind and we can evaluate them using these properties.

Scoped with Operator

This will define a generic with operator that can be used like any control operator and activates a combinational group:

with comb_group {
  while lt.out { 
    seq { g1; g2 } 
  }
}

The semantics of the operator is that assignments within it are active during the entire scope of execution. In my opinion, this approach violates both (1) and (2). For example, when reasoning about g1, the compiler needs to be aware of the entire stack of combinational groups that may be currently active. Additionally, there is no way to compile this operator into simple groups since the values on the inputs in the combinational group may change between execution of internal groups.

Enable with

This is a more modest extension to the language and is in spirit of the other uses of with:

seq {
  g1 with comb_group1;
  g2 with comb_group2;
}

This operator, like previous additions of with, is easy to implement and retains (1) and (2). Compiling away the with operation is as simple as copying all the assignments in the combinational group into the group.

Given this, I'm leaning towards the second proposal but would like to hear other opinions about this. Both of these will allow implementation of inlining of invokes as discussed in #807.

[rachitnigam]

More thoughts from a discussion about these two options: It seems that we've kind of tangled ourselves in this mess because of the way invoke works–it allows for scope execution of continuous assignments. Initially, this was in the form of assignments to its input/output ports and now this includes the combinational group attached to it. So either way, we're in a place where we have to lose the "local" reasoning of groups that we thought we had because we are working in a world where continuous assignments can essentially be lexicaly scoped.

The another comment is that the second proposal, enable-with, cannot express inlining correctly. Consider this program:

par { g1; g2 }

Where both g1 and g2 read from the parent component's input port in. If inlining proceeds the way we're imagining, every group that uses an interface port now needs to additionally invoke a combinational group that provides the assignments to those ports once inlined, g1 and g2 will invoke the same combinational group and therefore has a parallel assignment conflict.

[cgyurgyik]

So either way, we're in a place where we have to lose the "local" reasoning of groups that we thought we had because we are working in a world where continuous assignments can essentially be lexicaly scoped.

I'm not entirely following this; specifically, why scoped assignments would lead to the loss of local reasoning. Can you elaborate / provide an example?

[rachitnigam]

You can't reason about the assignments inside any group in isolation; you have to look at the stack of all active continuous assignments at each group enable to really understand what's going on.

For example, we have a papercut check to ensure that a register's write_en and in port are always driven together in a group. With scoped combinational groups, this no longer a property of a group---it is instead the property of a group enable contextualized by the set of active combinational groups.