Rigor-ifying the language semantics

[sampsyo]

This has no immediate urgency, but with all this work on the interpreter, I got started thinking about nailing down Calyx's semantics. There are various "dark corners" that come up from time to time, and I thought it might be nice to collect them into one place so we can approach the difficult task of defining what we actually mean in each case (rigorously but informally).

Here are the questions that have been bouncing around:

• What is the behavior when you read a signal that is not currently being written to?
  • Consider a group containing this statement, for example: add.left = reg0.out ? const0.out. Imagine there are no other assignments to add.left (and that add.right is connected to a constant). When reg0 holds 1, everything's fine, of course, and the adder invocation proceeds. But what happens when reg0 holds 0?
  • Is this an error because the adder attempts to read a value, add.left, that is never written? That seems way too limiting; surely we shouldn't be required to always have a meaningful value on both inputs to the adder.
  • Should we instead imagine that add.left holds an all-zero bit pattern? That's a little more sensible, but it is not really realistic about what's going on in the hardware: it would require extra circuitry to enforce that unproven signals always go back to zero. And as a practical matter, we would like simulations to be able to distinguish between meaningless values and meaningful zeroes.
  • So perhaps we should consider the add cell to be "inactive" because one of its ports is undriven, and so the add.out port should also be considered undefined. But what is the policy for determining what happens to components in these situations—is it always "any one undefined input means the entire cell is disabled," or do components get to define their own policies? If the latter, do they observe a special "undefined" value on their port? Are we getting dangerously close to Verilog's X at this point?
• What kinds of "overlap" are allowed in par?
  • May well-formed programs ever even activate the same components in different "branches" of a par?
  • I think our current answer should be "no"; any such activations make a program ill-behaved. But because this limitation is quite restrictive, it would be good to have confidence that no current Calyx programs rely on being able to do this.
  • On the other hand, if so, what mechanism ensures that these invocations do not actually conflict? (This question implies the investigation of synchronization primitives.) And further down the "if so" garden path, what happens to state updates in different branches of par? If I write to a register in one branch and read from it in the other branch, when (if ever) does the read see the result of the write?
• We should nail down the specifics of the go/done interface, i.e., the contract between invoking circuitry and the invoked component. Exactly when are go and done required to be "high," etc.? The questions are already well summarized in Precise go/done interface #405.
• A long-standing semantic issue is what to do about combinational components. Currently, there are lots of combinational components implemented in in Verilog, but AFAIK it is impossible to implement one in Calyx—because the required go/done interface is fundamentally sequential. This seems like a shame and implies that we either need (a) a special case for defining combinational components, or (b) a way to generalize the go/done contract to work for combinational logic. My intuition leans toward (a), i.e., there needs to be two different interfaces for the two kinds of logic.

Surely there are more, so we can keep adding to this list.

Here's a very rough proposal for how to think about defining the semantics. There are lots of questions and sketched-out parts in here, but hopefully it's a useful starting point.

Setup

A component definition consists of port declarations, a set of cells, a set of groups, and a control program.

A cell is an instance of a component that includes state, which takes the form of a set of subcells (the prototypes for which come from the component definition). Cell state thus forms a tree. The leaves of the tree are primitive cells, whose state is an arbitrary object instead of a set of subcells. (We will use normal cell to mean a cell that is not a primitive cell.)

The semantics for component evaluation will involve an environment, which maps port names to bit-vector values. The domain of an environment for a given cell is (a subset of) the union of all ports on the component definition itself and on all subcells. For example, consider this Calyx component:

component foo(inp: 32) -> (outp: 32) {
    cells {
        add = std_add(32);
    }
    ....
}

…where the std_add component has the ports left, right, and out. The environment for any cell that is an instance of foo could contain the port names inp, outp, add.left, add.right, and add.out. (We use dot notation to distinguish identically-named ports on different subcells.) The domain for any environment is a subset of this set, i.e., environments are partial maps for this domain.

Program Semantics

There is a distinguished top-level (main) component, which must have no ports. Program execution begins with an initial state where all primitive (leaf) cells get their associated opaque initial state and we build up the rest of the component state tree normally from there up to the main component.

We then begin component execution with the main component.

Component Semantics

To execute a component, we need input port values. For the main component, however, there are no input ports. [TK: Should port values be allowed to change over time? Currently saying no; they are fixed at the start.]

Execution proceeds iteratively according to the control program. In the absence of par, this execution is a straightforward recursive traversal of the control statement tree. par is more complicated. [TK: Actually say more about par.]

At the leaves of the tree, there are group activations. Execution for those proceeds as listed in the next section, using the state rooted at the current component and the component's port values. (There is no environment as input to group evaluation, which always starts with a "fresh" environment. It is impossible to communicate between group invocations via the environment.)

Group Semantics

To run a group using a given state, we iterate cycle evaluation, which is described in the next section. Cycle evaluation produces an environment and possibly mutates the state tree.

Group execution repeatedly executes the cycle evaluation procedure until the resulting environment maps <group>[done] to 1.

[TK: Somewhere in here, we need to "advance" the cycle-level execution of sequential subcells. The policy is something like "for every subcell C, if C.go is 1 in the result environment of a cycle evaluation, then run cycle evaluation for C" but I'm not entirely sure yet...]

Cycle Semantics

Evaluating a single cycle for a group consists of these steps:

1. Initialize a new environment, I, with the input port values only.
2. Create a copy of I, called E, that will be the working environment for the cycle. (This reflects that every cycle starts in a fresh environment; only the state persists across cycles.)
3. While E is still changing, do these steps:
   1. Create a copy of E, called F, that we will update in this iteration.
   2. For each assignment in the group x = c ? e, evaluate c in E. It must produce a 1-bit value. If the result is 1, then evaluate e in E. Then assign x in F to the result of e. If either c or e references a value that is undefined in E during this process, then the assignment "fails" and no change is made to F.
   3. For every combinational subcell [TK: what do you know; a special designation—not sure this is the right thing!] in the component where E contains values for all of the cell's input ports, let the subcell do its thing to produce a set of values for its output ports. Copy these result values into F. For example, this is where registers produce an out value using the stored state and adders produce an out value using their input values.
   4. Set E to F (throwing away the old E at this point).

When E stops changing (i.e., E equals F at the end of the inner evaluation loop), cycle evaluation has finished. (Legal Calyx programs must make this inner loop terminate in a finite number of iterations; divergence here indicates a "combinational cycle.")

[rachitnigam]

What is the behavior when you read a signal that is not currently being written to?

The set of possible solutions here reminds me of the discussion about undef and poison values in the LLVM semantics. Calyx level components can derive policies for these behaviors by looking at the assignments to inputs and outputs; only the primitives (with in the LLVM analogy, the ops) need to have a policy defined for them.

For example, the policy that "any one undefined input means the entire cell is disabled" is manifestly false—std_reg allows .out to be read without .in being driven. On the other hand, a Calyx level component has only one use for IO ports: to connect them (transitively) to some primitive port. Maybe we can come up with some notions of undef and poison style policies for combinational and stateful primitives and use that to specify the policy for Calyx components.

[sampsyo]

Good point about std_reg not obeying the simplest possible policy. I suppose that means we would indeed be stuck with inventing per-primitive policies for undefinedness (which is really not so bad—it would mean, for example, that the primitive implementations in the interpreter would take Options instead of plain values).

Hopefully the simple policy applies in a kind of monadic way to "pure" combinational operations like add so they could just ignore this Optionness.

[sampsyo]

Pasting more on this "undefinedness" question from our discussion on Around today. We listed these options:

• every port must always be written/defined on every cycle [Adrian does not like this]
• it is not allowed to read values that are not written
  • a variation of this where it is OK for combinational logic can somehow "propagate" undefined, so it only eventually becomes an error when it "propagates" to state?
• values that are not written are always zero [in some limited way, this is what Calyx programs sometimes currently assume. it is also what Alma's PR implements and is a good short-term solution.] [but Adrian is worried that it implies needlessly expensive hardware, so maybe worth reevaluating in the long term.]
  • consider exploring an interpreter flag - for unassigned ports

[rachitnigam]

What kinds of "overlap" are allowed in par?

Reprising a previous discussion we had about this, our choices are: "par disallows any conflict" and "par allows every conflict". In the former, par should be statically disallow "may-overlap" behavior: syntactic invocation of the same component in par branches is an error. In the latter, par does no checking whatsoever and allows branches to carefully synchronize and invoke the same component. It is still an error to have multiple driver to the same port on a component in the second case.

I am personally in favor of the second semantics and building a more restrictive version of the operator on top of it.

[sampsyo]

Indeed; one can imagine that, if we had the restrictive version, we would also want the more permissive version. In the more permissive version, though, I think we have quite a bit of thinking to do about what the semantics ought to be—for doubly driven signals, concurrent but safe activations of sequential components, etc. So that's why I mentioned a preference the other way, for making par more restrictive and therefore simpler for now unless we can find Calyx programs we've already written that really depend on these kinds of possibly-conflicting activations.

[sampsyo]

I didn't quite understand this argument:

In the former, par should be statically disallow "may-overlap" behavior: syntactic invocation of the same component in par branches is an error.

Namely, could you expand on why this should be static/syntactic? I'd lean instead for dynamic enforcement, just like any sort of prohibition we invent against acting on undefined signals. The rule would be that, during the execution of par { s1 ; s2 }, you'd track every group actually invoked during the execution of both s1 and s2; if the intersection is nonempty, it's an ill-behaved program.

The dynamic approach would allow this, for example:

par {
  if foo_grp with foo_cond { potential_conflict } ;
  if bar_grp with bar_cond { potential_conflict }
}

…where foo_cond == !bar_cond so the two ifs can never be true simultaneously.

The reason I lean toward dynamic enforcement is that we'd definitely want dynamic enforcement if we ever wanted to introduce synchronization primitives to enforce ordering among different branches of a bar. (Catching conflicts statically in the presence of synchronization would be infeasible.) So starting now with the rule being dynamic seems prudent.

[rachitnigam]

Oh, that’s a good counterexample! I was thinking that the first one was so restrictive that static rejection should be allowed by I’m wrong. We should allow your counterexample.