Definitions of "shareable"/"state shareable" and sufficient conditions for them

[calebmkim]

A component is "state shareable" if:
For any Calyx program, given two instances of the component, c1 and c2: if the live ranges of c1 and c2 do not overlap at all, then we can replace every use of c2 with c1 and the behavior of the program will not change. (Live range of a component, meaning the groups in which the value assigned to the components could potentially be read before the component is written to next).

A rough draft for sufficient criteria for state shareability for a given comp that @sampsyo have thought have (subject to change):

• Cannot have any uses of non-state shareable components (for example, it cannot read a component that counts the number of times it has been used. Thinking about it more, I actually think it is probably ok to write, just not read, to such non-state shareable components, but I'm not 100 percent sure...)
• For every instance of a state-shareable component, any read from that component must have been preceded by a write to that component. The idea behind this is: each time a stateful instance provides information to any of this component's outputs, it must have already "forgotten" -- i.e., been overwritten-- the information it learned from the previous time this component was invoked. Also, if the first read and write occur within the same group (e.g., something like r = r + 2) then that obviously should not be state shareable.

A component comp is "shareable" if:
For any Calyx program, given two instances of comp, c1 and c2, if c1 and c2 are guaranteed never to be used at the same time as each other, then we can replace every use of c2 with c1 and the behavior of the program will not change.

Potential criteria for shareability (should be improved):

• State shareable criteria
• All of the values for the output ports must die in the group that they were created in

An interesting thought @sampsyo and I discussed was this: it seems that shareability requires that any time you want to read a shareable component, you must also write to it in the same group. If you don't do this, then the output the component gives could be anything. Then, If I wrote a program using what I thought was a shareable component, but it turns out it was actually state shareable component, then my program still should behave as I intended it to.

(edit to add examples):
Example of state_shareable:

component add_5(in: 32) -> (out: 32) {
  cells {
    r = std_reg(32);
    add_32 = std_add(32);
  }
  wires {
    group A {
      add_32.left = in; 
      add_32.right = 32'd5; 
      r.in = add_32.out;
      r.write_en = 1'd1;
      count[done] = r.done;
    }
    out = r.out;
  }
  control {
    A;
  }
}

Example of non-shareable:

component count(in: 32) -> (out: 32) {
  cells {
    r = std_reg(32);
    add_32 = std_add(32);
  }
  wires {
    group A {
      add_32.left = r.out; 
      add_32.right = 32'd1; 
      r.in = add_32.out;
      r.write_en = 1'd1;
      count[done] = r.done;
    }
    out = r.out;
  }
  control {
    A;
  }
}

[sampsyo]

Thank you for the writeup, @calebmkim! As some additional context for others, I asked @calebmkim to jot this down as a draft for a page we will add to the documentation to define the semantics of the @share and @state_share annotations (and so that we can be sure we're on the same page about them before we do so).

The apparent need for two annotations came up in the context of #1042, which is further explained in #1039. Take a look at the latter for details but the high-level motivation is that sharing for std_add and sharing for std_reg work differently in a few important ways. If our goal is to have a general sharing pass that addresses both of them, then we had better be clear about what those differences are. As an added bonus, we would like for user-defined components to be able to opt into the same sharing behavior as std_reg; it should be possible to define your own component that gets shared in the same way std_reg does.

[sampsyo]

To formalize this bit:

it seems that shareability requires that any time you want to read a shareable component, you must also write to it in the same group. If you don't do this, then the output the component gives could be anything. Then, If I wrote a program using what I thought was a shareable component, but it turns out it was actually state shareable component, then my program still should behave as I intended it to.

The assertion here is that @share is a strictly stronger property than @state_share. In terms of the responsibility of optimizations, if something has a @share property, then this unlocks strictly more sharing opportunities than if it were annotated as @state_share. In other words, there is a little lattice at work here:

@share > @state_share > unannotated

A way to operationalize this is to say that the sharing pass is always allowed to treat a @share-annotated component as if it were @state_share instead, but not the other way around. This seems true to me, but creative counter-examples would be welcome.

[sampsyo]

One final thing: @calebmkim, I don't quite understand what this assertion means in the sufficient condition for @share:

All of the values for the output ports must die in the group that they were created in

Namely, I'm not sure what "the values for the output ports" are, and I'm not sure what "die" means.

With an eye toward writing this up as a documentation page, maybe some concrete examples of @share, @state_share, and unshareable components would help illustrate the points.

[rachitnigam]

A couple of things:

• I think we should assume all components are non-combinational. I think Calyx programs should be able to assume that a component invoke takes at least one cycle.
• If all components are non-combinational, then I think the best they can get is state_share and not share itself. The semantics of share and state_share are still blurry to me because I can't think of cases where a non-combinational component can be share.

[sampsyo]

Right. Good point. One working hypothesis (which I don't have a lot of confidence in yet) is:

The only kind of thing that wants @share as defined above is combinational components. At the moment, only primitives may be combinational—never Calyx definitions. So there is no sense in trying to infer the @share annotation for Calyx definitions. If someday we introduce combinational component definitions, then as ever, there is nothing to be done either—combinational-ness is a sound and precise criterion for @share. Therefore, our hypothetical inference pass need only worry about the weaker @state_share property.

[calebmkim]

I was looking at some of the test cases for resource-sharing and minimize-regs and it got me thinking (and I think @sampsyo might have mentioned this last week when we were discussing):
What if someone wanted to define a Calyx component that could add 3 numbers? They could just use 2 combinational adders , and that would be an @share user defined Calyx component (I think).
A simple way of detecting the @share off the top of my head would be something like this: it is sufficient criteria for a component to be shareable if the component only has combinational cells instantiated in it.

[rachitnigam]

This is not documented anywhere but one assumption the compiler often makes that components are non-combinational, i.e., they take at least one cycle.

[sampsyo]

Yes, that's right. @calebmkim, I think this restriction slipped my mind when I made up that "add 3 numbers" example! For now, only primitives (i.e., "external" Verilog-implemented components) are allowed to be combinational. We would like to be able to define combinational components in Calyx but we haven't figured out how to do that.

@calebmkim, as a historical note, you may be interested in the point where @rachitnigam introduced combinational groups (and primitives), in #635.

The upshot for the current work is that we believe (without 100% certainty) that the current definition of share is 1-1 equivalent to combinational-ness. And because we can't implement combinational components in Calyx, there is nothing for a share inference pass to do. (state_share, on the other hand, is a different story.)

Because it seems like a good idea to track for "someday" work, I'm going to open an issue on this topic…