A Few Notes on Undefinedness

[sampsyo]

Calyx, like every language, has some problems with undefined values. To summarize the status quo:

• The compiler inserts a bunch of "if not otherwise defined, then the value is zero" assignments into the RTL.
• The interpreter uses zero pervasively for things that are not assigned.

However, everybody agrees that this is not a great situation. Some things we would like include:

• The interpreter stops with an error when someone does something bad with undefined values. "Bad" things are sort of unclear but would be like writing them into an output memory, at least.
• The compiler doesn't need to generate a bunch of extra assignments to make things zero (which could lead to more efficient hardware).
• Programmers know exactly when values are required to be defined, and they are encouraged/required to be careful to distinguish between zero and undefined values.

To nail down a more consistent story for undefinedness in Calyx semantics, we need these things:

• A "propagation" policy for combinational primitives. This is probably pretty easy: the output is defined iff all the inputs are defined.
• Some policy for std_mem primitives. Roughly speaking, when the address port is defined, the output value is defined. When write_en is defined, then the value and address inputs must also be defined (otherwise it is a dynamic error).
• Harder: Decide what to do about guard expressions. It is probably the case that every guard expression is defined iff its subexpressions are defined. Then, we want to establish a policy for assignments. I can see two options:
  • If g is undefined in a = g ? b, then a is undefined (regardless of b).
  • It is an error for g to ever be undefined in a = g ? b. This is probably the way to go. But if it is, there are probably lots of wrong Calyx programs, so we would need to carefully figure out what they need to be fixed.
• Decide on a policy for go signals (and write_en signals, which are morally the same). We probably want to require them to be defined always. But we have been sloppily relying on the fact that undefined go signals "default" to zero throughout many Calyx programs, so there is probably plenty to be fixed here too.

After nailing down some of these questions, we probably have some hacking to do:

• Remove those "default to zero" assignments in the compiler.
• Update the interpreter. The environment would need to make all values "optional," i.e., they can either be a bitstring or a distinct "undefined" value. Then it would need to follow the propagation rules above. And finally, it would want to catch errors according the policies mentioned above.

Beyond all this, it would be interesting to think about a type system or other static analysis that could soundly rule out errors that arise because of undefinedness.

[sampsyo]

Just a quick note summing up some thoughts on recent synchronous conversations about undefinedness. First, it would be useful to hammer out a few criteria for how to evaluate potential solutions to this problem. Some ideas that come to mind are:

1. How "footgun-y" do we think the new semantics are, i.e., how many problems do we think they will cause in practice?
2. What are the implications for "optimizability," i.e., what optimizations that we would like to do are prohibited?
3. What are the implications on hardware efficiency when we generate the hardware to implement the policy? [This one's hard to talk much about without actual measurement, but we can make some guesses.]
4. How much of a change would this entail to existing code and passes? [Probably the lowest priority.]
5. What are the implications for interface signals (i.e., go & done ports, and the enable ports on registers)?

The categories of options I currently see (not necessarily exhaustive) include:

• Undriven signals are zero (the de facto behavior of the interpreter).
• An error (either crash or undefined behavior) immediately when reading any undefined value. (This one seems bad.)
• Some fairly intricate system of undefined behavior, where assignments can "propagate" an undefined value without immediately rendering the entire program undefined.

Thinking about the first option---stick with zeroes---I briefly mentioned the other day that I don't think it scores all that well among all the above criteria. It's very clearly optimal on the "don't change existing code" and "what to do about interface signals" dimensions. But it seems fairly footgun-y, prevents optimizations like #1010, and probably (without evidence) has a nonzero hardware cost. So it seems worthwhile to spin out a possible design for an "undefined propagation" semantics to see if we can convince ourselves it's better/worse.

[sampsyo]

[Just linking this thread to #1013, which asks similar questions, for the permanent record.]

[sampsyo]

This is an attempt to, as I briefly proposed above more than a year ago, write down the semantics for "undefinedness propagation." This question is relevant now for the implementation of Cider 2.0, but it of course has wider implications for optimizations, etc.

Background: Evaluating Calyx Programs

Recall the semantic model for running Calyx components, which we can state as a super idealized pseudocode loop nest:

for group in comp.control_program.iter_groups():  # The "control loop."
  while not group[done]:  # The "cycle loop."
    env = init_env()
    while env is still changing:  # The "stabilization loop."
      for asgt in groups:  # Arbitrary order.
        eval_asgt(env, asgt)
      for cell in comp.cells:  # Also aribtrary order.
        eval_comb(env, cell)

    for cell in comp.seq_cells:  # Yep, arbitrary order.
      eval_seq(env, cell)

Where env is a mapping from ports to values. We use these subroutines, not shown:

• eval_asgt(env, asgt): Run an assignment of the form lhs = cond ? rhs by evaluating rhs and cond in env and then, if the condition is true, updating env to assign lhs to the result of evaluating rhs.
• eval_comb(env, cell): Invoke the "combinational behavior" of a cell, updating the cell's output ports in env based on the input ports. We do this for all cells, both combinational and non-combinational (sequential). For example, if cell is an adder, then running this will update that adder's output port to be equal to the sum of the two input port values in env. If cell is a std_reg, then it will make its output port in env equal to its internal state.
• eval_seq(env, seq_cell): "Advance" the execution of each non-combinational (sequential) subcell by one cycle. For example, the std_reg primitive would "save" its input-port value to its internal state. Calyx-defined subcells will just "advance" their cycle loop by one iteration. env is not updated; we are about to throw it away anyway.

Strawperson: Zero-By-Default

What should init_env() do? It "clears the table" for the new execution of the stabilization loop. What should the value of every port be initially, before we evaluate any subcells or assignments?

One answer, and the current answer for Cider 1.0, is that every port gets a zero value. For example, if we were to run this group:

eq.left = add.out;
eq.right = 32'd0;
reg.in = eq.out ? 32'd42;
reg.write_en = 1'd1;
// note no assignments to add.left or add.right

…then, under this interpretation, we'd be semantically guaranteed write the value 42 into our register reg. That is, our adder add will get zeroes on its input ports by default; the sum 0+0 is 0; the comparator eq "returns true."

There are a few problems with "just use zeroes":

1. It feels icky. Having the zero value do "double duty" as both an "unknown" value and an actual value that happens to be one less than one seems like an unfortunate collision.
2. It hides bugs. I think we can all agree that the group above is not a great idea, but Cider 1.0 is powerless to throw an error in this situation (because it can't tell the difference between when you meant to use a zero vs. when you accidentally did by just not providing a value).
3. It has an intrinsic hardware cost. To implement these semantics, we would have to produce hardware that implements these "default" values. We have never directly measured what this costs, but it surely costs something.
4. It prevents optimizations we would like to do. Guard Canonicalization is invalid #1010 contains an important example. Here's another: should we be able to optimize lhs = cond ? rhs to simply lhs = rhs if it is the only assignment to lhs anywhere in the entire program? I would like for this to be allowed, because it only changes the value of lhs when cond is false, when it seems like nobody should be paying attention to lhs anyway. But under the "default to zero" semantics, it would not be, because other code could be depending on lhs being zero at times when cond is false.
5. It makes it harder for the interpreter to detect conflicts. That is, we want the interpreter to signal an error when foo = 1 and foo = 2 are active simultaneously. But when all signals default to zero, it's hard to distinguish between a true conflict (e.g., foo = 0 and foo = 1 are active at the same time) vs. a spurious one (e.g., only foo = 1 is active but foo's default value is 0).

This reasoning is roughly how we got to the concept of "data vs. control ports," as described in #1169. Control ports have default-zero behavior because we think it is dangerous for stuff like go and done to ever be undefined. Data ports do not and have more interesting semantics. We distinguish between the two with @data and @control attributes. The rest of this discussion is mostly about data ports (the non-default-zero kind), because we have decided we can pay the above costs for control ports (at least for now) and that makes the story pretty simple for those.

Semantics With an Undefined Value

The alternative to zero-by-default is to have a special, distinguished "undefined" value that is distinct from any actual, concrete bit-vector value. Let's call this value ⊥. That is, in the env environment from the above psuedocode, every port would map to, conceptually, Option<BitVec> instead of just BitVec, where None corresponds to ⊥. init_env() would set all ports to ⊥ instead of zero.

The point of this discussion is to decide exactly how our main "workhorse" semantic functions (eval_asgt, eval_comb, and eval_seq above) work in the presence of ⊥. Without implying that I have thought this through all that clearly, I want to jot down one proposal for the interesting cases, which we can then debate/revise/ratify.

Assignment Evaluation

For eval_asgt, follow these rules when the condition is true (i.e., lhs = true ? rhs) to determine the new value of the LHS based on the old value of the LHS and the incoming RHS:

old LHS	RHS	new LHS
⊥	⊥	⊥
⊥	v	v
v	⊥	(error)
v	v'	(error)

…where v and v' denote any defined (non-⊥) value. The last row is an error even when v == v' and is labeled as a conflict. (When I say "error" in this writeup, I mean that the interpreter should stop with an error, and compiled hardware is allowed to do whatever it wants, including either stopping with an error or exhibiting arbitrary behavior.) (NB: I am most uncertain about the third row; we should consider it carefully.)

This strategy (and the second row in particular) is important so that statement evaluation remains order-insensitive. That is, we don't want this group:

add.left = 32'd12;
add.right = 32'd30;
foo.in = add.out;

to depend on the order we visit these expressions in, and we want it to be equivalent to this group:

foo.in = add.out;
add.left = 32'd12;
add.right = 32'd30;

That is, if we happen to pick the foo.in assignment to evaluate first, it should be safe to run (and not cause an error), even though add.out will be ⊥ at this point. Then, later, after add.out eventually has a chance to become 42, then when we re-evaluate foo.in = add.out, we'll "upgrade" foo.in from ⊥ to 42 using the second row.

In lhs = cond ? rhs, evaluating the cond expression "propagates" ⊥ in the natural way, e.g., v + ⊥ is ⊥. (NB: Unclear what to do about logical short-circuiting, e.g., 0 & ⊥ or 1 | ⊥.)

It is always an error for cond to evaluate to ⊥. This effectively means that programs should either only use control ports (not data ports) at the leaves of conditions, or else they need to be very careful to otherwise somehow ensure that "transient" ⊥ values never affect the result of evaluating a condition. (NB: The alternative is that lhs = ⊥ ? rhs just stores ⊥ into lhs. Not sure this is workable but we should think about it.)

Combinational Evaluation

For eval_comb, I think every primitive will have to decide for itself how exactly it deals with ⊥ on input ports. The usual thing for combinational primitives should be that ⊥ gets propagated, again in the "natural" way. For example, if either input to std_add is ⊥, then its output should be ⊥.

Sequential Evaluation

It's a similar situation for eval_seq: primitives need to decide on a case-by-case basis what to do with ⊥. Registers and memories, for example, should probably flag an error whenever they would write ⊥ into their internal state (e.g., when reg.in = ⊥ and reg.write_en = 1).

[sampsyo]

Here are a few outcomes from today's synchronous discussion.

a decision on "row 3"

First, we talked quite a bit about what we think of row 3 in the assignment evaluation table, i.e., the conclusion that, during stabilization, assigning x = ⊥ when x is already defined should immediately signal an error. (An "error" being a crash in the interpreter and arbitrary UB in the compiler.) We thought about where this case can actually arise and came up with two scenarios:

1. Somehow, a primitive "changes its mind" during stabilization and, after outputting v for a while, suddenly starts deciding to output ⊥. It was roundly agreed that this is implausible and a poor match for the intuition that signals only get monotonically "more defined" over time during stabilization.
2. Due to @hackedy: You have conflicting assignments, x = y and x = z. Both y and z will eventually be defined, at which point triggering these assignments will cause an error. By an accident of the arbitrary order of evaluation, imagine that y is defined but z is not yet, i.e., it's still ⊥. The row as-is means that we will signal an error earlier, before the concrete-value conflict (row 4) actually happens later on. This one is harder to think about. If we could convince ourselves that this situation always indicated a row-4 conflict would happen in the future, then this would be fine. But it definitely doesn't always predict a later row-4 conflict (imagine z is never assigned), complicating things a bit.

Very relatedly, however, we tried to think about the optimization implications. The example I gave above is this one: transform x = c ? y to x = y when it is the only assignment to x. @rachitnigam gave a generalization, which is roughly: transform this:

l = c1 ? r1;
l = c2 ? r2;

into:

l = c1 ? r1;
l = not c1 ? r2;

or, at the RTL backend level, l = c1 ? r1 : r2. We noticed that the common thread in these optimizations is that they refine the semantics of the input program: i.e., the output program is like the input program on error-free executions but some executions that were previously errors might now succeed just fine or whatever. And they achieve this is essentially by taking some values that, at some points during the stabilization loop, used to be ⊥ and making them concrete values instead. That is, this category of optimizations makes values "more defined" and we want to allow such shenanigans.

With this in mind, these optimizations seem to want to keep that row 3 as it is! These "make-stuff-more-defined" optimizations work by taking a ⊥ in the RHS and sometimes making it a v'. So some assignments in the stabilization loop will move from row 3 to row 4. So it is comforting for these optimizations to know that they are taking an already-erroring program and making it still produce an error. If we changed row 3 to produce v as the new LHS, for example, these optimizations would be introducing errors, which is bad. (It might still be viable to have row 3 produce a new LHS of ⊥, instead of signaling an immediate error, but this would require a different and maybe harder argument to establish the correctness of the above optimizations by saying that an error was guaranteed to happen eventually anyway.)

control ports still have a problem

We identified that we still have a subset of the problems with the default-zero semantics listed above for control ports (which, you may recall, keep still have default-zero semantics as a kind of special case). The biggest problems, to me, are:

• Item 5 on the list in the comment above (it makes it hard for the interpreter to detect conflicts, because there will be some spurious "transient" conflicts due solely zero initialization).
• This sentence from my proposal above is too simple: "It is always an error for cond to evaluate to ⊥." Requiring conditions to always evaluate to ⊥ on every iteration of the stabilization loop seems very restrictive. It would mean all ports used in conditions would need to have default-zero behavior, not even zeroes propagated in one step (even through a std_wire from a constant, for example). It would be better if we could instead require conditions to eventually be defined, by the time the stabilization loop terminates.

@rachitnigam remembered that the original goal with the whole @control/@data separation was to eventually revisit the ad-hoc-ness of @control. Namely, you can frame the central issue there as being that we implement default-zero semantics in the Verilog backend in a way that is pretty backend-specific and is therefore kinda hard to model in Calyx. The goal was (and probably should still be) to someday make these zero assignments explicit in Calyx code. If we can manage this, we can have one style of semantics to rule them all (the one for @data ports outlined in this discussion) and remove the special case from the backend.

So this implies that we should push another item onto our agenda for deep thinking along these lines: what would it take to realize that vision (to get rid of implicit zero-defaulting and make it explicit somewhere)? Let's make a plan for this, even if it might be hard to implement, so we kinda have a roadmap for how to proceed.

And meanwhile, @EclecticGriffin needs to know what to do for @control ports in Cider 2.0. Item 2 above is a pretty serious problem here, because it doesn't suffice to just hack the stabilization loop to make all control ports replace ⊥ with 0 all the time. The problem is a program like this:

w = std_wire(1);
...
w.in = 1;
catch_fire.in = w.out ? 0;
catch_fire.in = !w.out ? 1;

That is, a dangerous port catch_fire.in is enabled as the inverse of the wire w's output. Before we propagate through w, the strawperson default-zero scheme will make w.out == 0, which could then immediately catch things on fire. But we actually want both catch_fire.in assignments to be no-ops until we have actually calculated w.in to a defined value (which will then be 1, preventing any conflagration).

So that simple solution won't do. We want to adhere as much as possible to the semantics we're developing for @data ports that will eventually apply to every port, but we don't want to break lots of programs that work just fine on the Verilog backend. Keeping in mind that what we need here is a temporary hack and not a beautiful solution, @EclecticGriffin proposes this modification to the semantic model, inserted after the stabilization loop:

for p in env.control_ports():
  if env[p] == ⊥:
    env[p] = 0
(then run the stabilization loop again)

This at least addresses the std_wire/catch_fire example above, and we kinda think this might match the Verilog backend's behavior in general? But I think that may be a question that has to be answered empirically.

[rachitnigam]

One possible trickiness with the hack for making the semantics of control ports work is the potential that the definition of "stabilization" might depend on the values assumed by control ports. For the hack to work, we should convince ourselves that the definition of a stabilized set of assignments doesn't itself require constraints on control ports.

[hackedy]

A simpler way of phrasing the assignment evaluation table is that an assignment l := r sets l to F(l, r) where

F(⊥, v) = v
F(x, v) = (error)  [when x != ⊥]

[hackedy]

If we view our values as living in a lattice we can make some observations about F.

  (error)
  /  |   \
 /   |    \
v0   v1 .. vn
 \   |    /
  \  |   /
   \ |  /
     ⊥

The function F is not symmetric (F(x,y) = F(y,x) for all x), but it is monotone (if x<=x' and y<=y' then F(x, y) <= F(x', y')). It preserves meets and joins.

Exercise for me to work out: justify the optimization

l = c1 ? r1 : c2 ? r2 : \undef
==>
l = c1 ? r1 : c2 ? r2 : r2
===>
l = c1 ? r1 : r2

in terms of the properties of F. Show why making F(v, ⊥) = (error) is necessary.

[sampsyo]

Yes, that is nicer!

[sampsyo]

And one other random thought that occurred to me: because F is monotone, every value in env travels "upward" in this lattice while the stabilization loop is running. That is, env is initialized to map all ports to ⊥. Executions of the stabilization loop use F to move some of the values "up" to either concrete vs or errors (⊤). But nothing ever moves back down from a concrete v to ⊥ or from ⊤ to anywhere else (errors are a black hole).

[hackedy]

Unfortunately I think if you use this lattice to understand the stabilization loop as a kind of fixed point you'll always end up at (error)

[hackedy]

So it might be better to treat (error) specially

[sampsyo]

tangent: why are we bothering anyway?

Let's think about the reason the guarded assignments language exists at all. It feels weird that we are creating a language where conflicts are endemic and then trying to come up with a way to rule out conflicts again. Why are we doing this?

First, the reason we don't like conflicts is that the target we hope to compile to (i.e., actual hardware) can't have conflicts. Here's one way of putting it: imagine a target language, named NL, that models target hardware description. The syntax of NL is just (x <- e)* where each variable x can occur only once on the LHS. Expressions e have, like, normal bit-vector math ops and an ITE, written e1 ? e2 : e3. The "single assignment" restriction is because NL models netlists, where each "port" can be connected to exactly one other "port". ITEs correspond to hardware muxes.

Basically, we want to have a translation from the Calyx guarded assignment language to NL. As in, this Calyx snippet:

x = c1 ? e1;
x = c2 ? e2;

Translates to this NL code:

x = c1 ? e1 : (c2 ? e2 : nevermind);

If we give ourselves a special nevermind value that is tantamount to not assigning anything at all.

This transaction to NL is only possible when the Calyx program is conflict-free. Or, more reasonably: I don’t know how to translate Calyx guarded assignments to NL if we have to account for conflicts in the former with any semantics other than “error.”

So why do we have guarded assignments at all? Why are we not happy to just use an NL-like language in Calyx instead? The reason is composability. Calyx really want to be able to combine little snippets of code together, namely when compiling control.

Here's one way of thinking about that composition: let $g$ denote a sequence of Calyx guarded assignments (if you like, a Calyx group). $g_1 ; g_2$ is composition, i.e., just concatenating all the assignments from $g_1$ and $g_2$ to get a new sequence of guarded assignments. We like having a theorem with this impressionistic statement. If $g_1 ; g_2$ is conflict-free, then:

$$[[ g_1 ; g_2 ]] = [[ g_1 ]] \circ [[ g_2 ]] = [[ g_2 ]] \circ [[ g_1 ]]$$

i.e., in the absence of conflicts, you can get the semantics of $g_1 ; g_2$ by getting the semantics of $g_1$ and $g_2$ and composing them. (The actual domain and the meaning of $\circ$ here are left undefined; that's the impressionistic part.)

Hopefully this is semi-relevant to the discussion about what conflict freedom is supposed to do for us. It enables compilation to hardware (like NL) with compositional reasoning.

[sampsyo]

Chatting synchronously with @hackedy was extremely clarifying and (we think) yielded a satisfying solution, which should be workable both for a real implementation in Cider 2.0 and for formalization/verification.

updating the evaluation pseudocode

The upshot is that we need to explicitly track the "winner" who got to write to every port. Here's how to amend the pseudocode loop nest above. Before the stabilization loop, and right next to where we initialize env, initialize a new writer map:

env = init_env()
writer = {}

eval_asgt and eval_comb must be amended to get access to writer and to contain pseudocode like this:

if writer[asgt.dest] != asgt.id:
  report conflict
writer[asgt.dest] = asgt.id

That is, assignments (and cells, I guess) need IDs, and writer[asgt.id] keeps track of the ID of the assignment that "won" the privilege of defining env[asgt.dest]. Conflict detection does not use env at all; it uses the writer IDs.

intuition

Here is a way that was helpful for me to think about it. To evaluate a block of guarded assignments, you have to pick the subset of those assignments that will take effect—and that subset must be conflict-free. That is, imagine you have these guarded assignments:

x = c1 ? v1;
x = c2 ? v2;
y = c3 ? v3;
y = c4 ? v4;

You can think of the evaluator as picking the winning subset of assignments, which must contain at most one assignment per variable (statically). Since you have decided the winners, they are no longer conditional---they can just be written as plain assignments. Like, maybe these assignments win:

x = v1;
y = v4;

Remember, in this "winner set," there can only be one assignment to x and one assignment to y. So this is a plain dataflow graph, and it contains none of the hazards of conflicts or undefinedness that the language guarded assignments does.

To summarize, the idea is that evaluation of a guarded-assignment block ought to pick a single winning DFG from the family of DFGs the block could possibly admit. It does that by tracking the winning assignments in writer, and they must be unique per variable. Critically, we have to identify the winners by the identity of the assignments, not by the values of the expressions, because---at a hardware level---even different assignments that produce the same value must be realized as distinct physical pathways.

theory implications

I think this means that you want to define the meaning of a guarded-assignment block, $[[g]]$, to be a function $V \times W \rightarrow V \times W$, where $V$ corresponds to env and $W$ corresponds to writer.

Values in $V$ are either concrete bitvectors or ⊥; there is no ⊤ (error) value.

Writers in $W$ are assignment IDs, ⊥, or ⊤. As in the value mapping, ⊥ means "not yet known." But we also have ⊤, which indicates a conflict. Attempting to set a winner in $W$ when a different winner already exists yields ⊤. "Repeatedly" setting the same winner in $W$ leaves the winner unchanged and does not yield ⊤, which resolves the problem we were having with, uh, "non-idempotent" assignments.

We think you can (without much trouble) construct, for a guarded-assignment block $g$, a function $f$ so that the least fixed point of $f$ is the desired semantics of $g$.

[hackedy]

wait, is the writer of the assignment the assignment statement itself or the rhs of the assignment? I think I had it as the rhs port but I could see the case for it being asgt.id.

[sampsyo]

Good question. If we tracked the RHS, then would we be depending on equality of RHS expressions? Like, if I have a program like:

x = something ? y;
x = something_else ? y;

…then they are both allowed to "win," because the expressions y and y are equal.

I think we don't want that, mostly because—thinking about the hardware target—this situation still seems to correspond to a mux with two inputs enabled, which is a no-no, even though both inputs are wired up to the same subcircuit.

(In an interpreter implementation, it also seems a bit easier to keep track of assignment indices than to have some kind of structural equality on RHSes.)

[sampsyo]

I see what you mean, though… especially since, in Calyx, RHS expressions can just be a single port. So in the intuition where you just want to keep track of "where did the data come from," tracking the RHS's identity makes sense. And you can imagine resolving my little example above by imagining that compilation to hardware will involve coalescing assignments with identical RHSes, so the above would produce a mux with the condition something | something_else. So yeah, I could see it working that way too.