[semantics] Semantics of Empty vs Seq/Par(Empty)

[EclecticGriffin]

Imagine a component like:

component main(@go go: 1, @clk clk: 1, @reset reset: 1) -> (@done done: 1) {
  cells {
     ...
  }
  wires {
    \\ 0 or more groups
    \\ no continuous assignments that write to done  
  }
  control {
    seq {}
  }
}

We'll call it version A (empty seq).

Imagine the same program but without the seq (empty control). Call that version B.

These programs are potentially a weird little semantic corner. To elaborate, there are three possible situations for each program:

1. the program terminates instantly
2. the program runs forever
3. the program is invalid

My understanding of Calyx is that ver A (empty seq) falls into 1 (instant termination), while ver B (empty control) falls into one of the latter two options.

It seems "obvious" that the compiler should be able to turn Seq([Empty]) into Empty. This transformation may or may not be an actual optimization, but I'll call it such for the rest of this issue.

Option I (both are invalid)

If this is true it suggests that a program must have exactly one of the following:

• A control program with at least one group enable
• A continuous assignment writing to the done port

This also means our obvious optimization is valid.

Option II (A: terminates, B: runs forever)

This is consistent with my understanding of what a control program means and what a fully structural program means, however this means our optimization is invalid which seems off.

Option III (both run forever)

Optimization remains vaild, this however seems inconsistent with the my notional understanding of what a control program means.

Option IV (Both terminate instantly)

Optimization remains valid, this seems transparently incorrect with respect to the semantics of a control-free program.

---

All other options result in an invalid optimization and possibly clash with the generally understood behavior of Calyx programs.

[sampsyo]

😃 Always a fun kind of edge case to consider.

My gut feeling says Option II (A terminates, B runs forever). The underlying semantic rules would be:

• control {} is a special/exceptional case. "Empty-control" or "fully structural" components need to explicitly/structurally conform to the go/done interface.
• Every other component (regular, control-having components) are done when their control program is done.
• seq { s1; s2; ... }, for any (possibly empty) sequence of statements s*, runs each statement in series and then is done.
• So seq {} is just a normal case of that general rule. Because an empty series of statements is done immediately when it starts, so is seq {}.

You're right that this is makes that seq{}-to-nothing optimization invalid in general, which is annoying. Essentially, there would need to be a special case for when this is the only statement in the program.

An alternative would be for fully-structural components to be distinct from components with no control statements, i.e., control {}. That is, there would be a difference between "no control; this is structural" and "the control is just Empty." Syntactically, we could represent this as there being no control keyword at all vs. having control {}. Does that seem reasonable?

[rachitnigam]

One well formedness rule in calyx, that isn’t enforced, is that all components must take at least one cycle to execute (same as groups) so there are no components that terminate immediately

[rachitnigam]

In my eyes, both programs exhibit undefined behavior because they don’t have any internal signaling to force them to take at least one cucle

[sampsyo]

Yeah, there's a strong argument for that as well. It would address the optimization problem: the seq {}-to-nothing optimization would remain allowed everywhere, because control { seq {} } is equivalent to control {} when there is no structural done assignment (both have UB).

However, we don't necessarily need to decide that control { seq {} } takes zero cycles and is therefore UB. We could also decide that it takes one cycle to become done. On the other hand, that would be pretty bad for static seq.

---

Just for fun, I wanted to see what the compiler currently does, so I tried compiling this:

component main() -> () {
  cells {}
  wires {}
  control { seq {} }
}

With this command (static-promotion currently crashes on this program):

$ cargo run -- -d static-promotion -b verilog t.futil

And we produce:

module main(
  input logic go,
  input logic clk,
  input logic reset,
  output logic done
);
// COMPONENT START: main
wire _guard0 = 1;
// COMPONENT END: main
endmodule

i.e., we do the seq {}-to-nothing optimization, and then we have the invalid fully-structural program that is never done.

[rachitnigam]

A decision about control { seq {} } doesn't have to affect the semantics of control { static seq {} }. The latter is provably a zero-cycle program and can be rejected during compilation. The former allows for rescheduling optimization for fixing it but we should probably still reject it.

Also, static-promotion shouldn't be crashing on this program so let's fix that 🤣

[rachitnigam]

Also, a related issue is #621 which also happens because we haven't really nailed down the timing restrictions for component

[rachitnigam]

Is there anything actionable for this issue? If we've decided on a particular semantics, let's document that in the docs page and close this issue?

[hackedy]

An alternative would be for fully-structural components to be distinct from components with no control statements, i.e., control {}. That is, there would be a difference between "no control; this is structural" and "the control is just Empty." Syntactically, we could represent this as there being no control keyword at all vs. having control {}. Does that seem reasonable?

I think this is a good point. Think about a conditional with Empty in one branch. You have to interpret this Empty differently than you would interpret it at the top level, which is a sign of non-compositional weirdness.

[EclecticGriffin]

Closing since there's nothing actionable here right now