Isolation and stateful “doneness”

[sampsyo]

On Isolating Groups

We were discussing (synchronously) a problem today that I will chicken out of summarizing directly, because it's super tricky to describe, but I want to summarize some thoughts about the problem here.

The underlying issue is about isolating the execution of groups. An important concept in the idea of Calyx groups is that they are supposed to have semantics that are isolated from the execution of other groups. In other words, a group can do whatever it wants "inside" without worrying about interfering effects from "outside." The upshot is that we can reason about programs compositionally: you can understand what each group does once, and then draw conclusions about what the overall program does based on that understanding about the individual groups.

A consequence of this isolation is that it should always be the case that two groups activated in a seq control structure should be able to share cells willy-nilly without interfering with one another. This is the property, for example, enables the program equivalence reasoning that powers our register-sharing pass.

Consider a program whose control looks like this:

seq {
  foo;
  bar;
}

…where foo and bar are groups that use two different registers foo_reg and bar_reg. But they don't actually have data flow between them, in the sense that both of them write to their register before reading from it, so they can't possibly "communicate" through the register's state. Then this program is equivalent to one where both groups share a single register, call it reg, instead. The reason these programs are equivalent relies on the isolation of groups: we know that foo's use of reg has absolutely no bearing on bar's use of the reg. This story is all just to emphasize that we really like this isolation property and the compositional reasoning that it enables.

The unnamed problem that we've been discussing has to do with a violation of this isolation. Namely, groups often (always??) use registers to drive their [done] holes—they frequently use assignments like this:

foo[done] = reg.done;

The problem with this is that the control logic we generate uses foo[done] to decide when to start the execution of the next cycle. So if we want bar to start doing its thing immediately on the cycle that foo[done] becomes true, then bar actually ends up using reg to decide when to start! Which means that foo and bar are actually "sharing" reg during that one cycle, in a kind of invisible way, and the groups can't really rely on isolation. Most perniciously, bar can't rely on reg being useful for driving its own [done] signal, because it needs to be 0 when foo's is 1.

A Modest Proposal

I have no idea if this following proposal will actually solve the problem, but I think discussing it would at least be illustrative. The proposal is to give every group its own ghostly "register" to use just for signaling done-ness. Philosophically, the idea is to acknowledge that our (non-combinational) groups typically (always?) need to declare and use such a register anyway to make sure that they take at least one cycle. So why don't we bake that into the semantics of groups instead of making all groups reinvent the "register for driving [done]" pattern? That way, we can offer an abstraction that ensures that every group appears to own an isolated state element for this purpose and avoid any unpleasantness about accidentally sharing these registers.

How this plays out concretely is left deliberately a little fuzzy, but one what would be to redefine [done] to work more like a register's in port. Namely, outside observers don't see the done signal become true until the cycle after the group assigns 1 to [done].

A straightforward/correct way to compile groups in this hypothetical, proposed world would be to literally generate a single new register for every single group. A basic approach to generating FSMs would read this register from each group, increment the FSM state, and then write back to the FSM state register. This would introduce an extra cycle between group executions—that is, foo would finish up, its doneness register would become true in the next cycle, and the FSM state would only increment (activating bar) in the following cycle. This is wasteful but at least it’s correct in the sense that the groups stay isolated. (And I think it’s the name number of cycles as our current dynamic control compilation??)

A better way, of course, would somehow let the FSM state increment immediately on the cycle after foo writes 1 to its “doneness register.” To do that, we can take advantage of the fact that foo[done] is not a real register and instead implement it using the FSM’s existing state register instead. The very rough idea is to “inline” the [done] assignments into the FSM’s logic. So if foo has this:

foo[done] = whatever;

Then the FSM logic might include something like this:

fsm.in = whatever & fsm.out == 0 ? 1;

The point is that the computation whatever now “goes into” the FSM state register, which takes the place of a literal physical register implementing foo[done]. Instead, bar can now activate immediately after this assignment happens (because its [go] hole is hooked up to the same FSM state register), saving one cycle relative to the naive FSM generation approach above.

[rachitnigam]

Thanks for the summary Adrian! For future context, the relevant issues are #635 & #662.

A different way at looking at the semantics is that using a done signal on its own is meaningless---it must be associated to some "index" (such as an FSM state) to be meaningful. For example, when we write something like:

two[go] = (one[done] & fsm.out == 0) ... ? 1'd1;

We're stating that we're using the value of one[done] at the index fsm.out == 0. Using one[done] from any other index in this context will generate a different program.

One way to reify this notion of the "ghost done signal of a group" is using these indices. Using this, we can say that reading a group[done] signal is only meaningful when it is indexed. If you don't index it, you'll run into trouble.

[rachitnigam]

Compiling Groups and done Signals

Calyx groups provide a relatively strong guarantee about group execution--that changes made in a group are isolated from changes made in other groups not running in parallel.

This means that if you sequence execution of two groups, they are guaranteed to not conflict with each other. This isolation property allows Calyx passes to reason about groups individually and perform optimizations that can, for example, share components between groups without having to reason about any conflicts.

For example, the following two programs are functionally identical in Calyx:

group write_r1 { r1.in = 1'd1; r.write_en = 1'd1; write_r1[done] = r1.done; }
group write_r2 { r2.in = 1'd1; r.write_en = 1'd1; write_r2[done] = r2.done; }
control { seq {
  write_r1; write_r2;
}}

and:

group write_r1 { r1.in = 1'd1; r.write_en = 1'd1; write_r1[done] = r1.done; }
group write_r2 { r1.in = 1'd1; r.write_en = 1'd1; write_r2[done] = r1.done; }
control { seq {
  write_r1; write_r2;
}}

Calyx can determine that since register r1 is not used after the occurrence of write_r1, it reuse the register in write_r2 without changing the functional behavior of the program.

done Signals

The done signal of a signals the completion of the action that the group was trying to run. Calyx's control programs guarantee that when a group is enabled, the assignments within it are only going to be active while the group's done signal is not true. Furthermore, once the done signal does become true, the assignments will not be activated till the group is enabled again.

While it is relatively straightforward to specify these semantics in prose, implementing them using hardware turns out to be challenging.

Lowering seq using FSMs

Calyx control programs are realized in hardware using finite-state machines (FSMs). During lowering, the compilation passes generate an FSM that runs the groups as long as needed and transition when a group is done executing. At first glace, an FSM for the seq operator might look simple:

seq { one; two; }

which can be implemented using the FSM register f and group:

group realize_control {
  // Run groups in the respective FSM state
  one[go] = f.out == 0 & !one[done];
  two[go] = f.out == 1 & !two[done];

  // Transition to new FSM state when group is done.
  f.in = f.out == 0 & one[done] ? 1;
  f.in = f.out == 1 & two[done] ? 2;

  // Control program is done in the FSM's final state
  realize_control[done] = f.out == 2;
}

While functionally correct, this FSM does not accurately capture the cycle-by-cycle semantics of Calyx. Assuming the latencies of groups one and two is t1 and t2 respectively, we will have the following cycle-by-cycle behavior:

• cycle 0: f.out == 0 & !one[done] is true and group one starts executing.
• cycle t1: one[done] is true which means that in this cycle, one is already inactive. However, we still have f.out == 0 which means two is not executing yet.
• cycle t1 + 1: f.out == 1 & !two[done] is true and group[two] starts executing.
• cycle t1 + 1 + t2: two[done] is true and two has stopped executing. However, we still have f.out == 1 so the realize_control will not signal that it is
  done yet.
• cycle t1 + 1 + t2 + 1: f.out == 2 and the control program is done.

This means that a control program that should have taken t1 + t2 cycles to finish execution ends up taking 2 extra cycles. Because of Calyx's group isolation property, this program is correct---it is always safe to delay the sequential execution of groups.

Generating the Fastest FSM

To precisely understand the semantics of Calyx programs, it is important to generate the fastest FSM, in terms of the number of cycles it takes. While the fastest FSM may use more complex logic, it can act as a reference for what semantics deem safe. Any optimization to the FSM, for example to trade-off of number of cycles for simplicity of logic, can then be reasoned about precisely.

From the previous example, we can decide that a possible way to remove the extra transition when lowering seq is enabling the subsequent group in the cycle when the previous group is done. We can generate something like this:

one[go] = f.out == 0 & !one[done];

// Immediately enable two when `one` is done.
two[go] = f.out == 0 & one[done] & !two[done];
// Once the FSM transitions, keep `two` enabled.
two[go] = f.out == 1 & !two[done];

The generation scheme relies on the fact that all Calyx groups must take at least one cycle to execute. This means that if two takes exactly one cycle to perform its computation, only the first two[go] statement will ever need to be active. Any group that runs after two will similarly have its execution coordinated by using two[done] and the FSM register.

Even in these scheme however, the done signal of group realizing the control program will take an unnecessary extra cycle since the FSM will lag behind by one cycle since the done signal is:

realize_control[done] = f.out == 2;

This is a bug and should be fixed.

Leaking done Signals

This new FSM scheme exposes a crucial lie in the group isolation property of Calyx---that done signals of groups, which may come from structural elements like registers, are not isolated and in fact, must be visible outside group boundaries to enable the current style of compilation.

For example, going back to our first example programs:

group write_r1 { r1.in = 1'd1; r.write_en = 1'd1; write_r1[done] = r1.done; }
group write_r2 { r2.in = 1'd1; r.write_en = 1'd1; write_r2[done] = r2.done; }
control { seq {
  write_r1; write_r2;
}}

and:

group write_r1 { r1.in = 1'd1; r.write_en = 1'd1; write_r1[done] = r1.done; }
group write_r2 { r1.in = 1'd1; r.write_en = 1'd1; write_r2[done] = r1.done; }
control { seq {
  write_r1; write_r2;
}}

While Calyx semantics make it perfectly safe to share the storage location of r1, sharing the done signal of r1 is incorrect because it is read outside the group.

Going back to our new FSM schema, we'll generate code that looks like this:

write_r1[go] = f.out == 0 & !write_r1[done];
write_r2[go] = f.out == 0 & write_r1[done] & !write_r2[done];
write_r2[go] = f.out == 1 & !write_r2[done];

which will eventually turn into something like this:

write_r1[go] = f.out == 0 & !r.done;
write_r2[go] = f.out == 0 & r.done & !r.done;
write_r2[go] = f.out == 1 & !r.done;

This program will not allow the execution of write_r2 in the same cycle when write_r1 because the guard will always be false (due to the r.done & !r.done).

The fundamental problem is that replacing write_r2[done] with r.done is incorrect---r.done only represents write_r2[done] when f.out == 1. In other FSM states, it might refer to the done condition of some other group.

Indexed Usage of done Signals

This finally leads us to a way of formalizing the usage of done signals of
groups in a way that isolation properties can be maintained.

We state that using the done signal of a group without an FSM index is incorrect.
Instead, whenever the done signal of a group is used, the compiler must ensure that
the correct FSM index is added.

In its correct, the schema should generate code that looks like this:

write_r1[go] = f.out == 0 & !(write_r1[done] & f.out == 0);
write_r2[go] = (f.out == 0 & write_r1[done]) & !(write_r2[done] & f.out == 1);
write_r2[go] = f.out == 1 & !(write_r2[done] & f.out == 1);

we can simplify guards using boolean transformations and get:

write_r1[go] = f.out == 0 & !write_r1[done];
write_r2[go] = f.out == 0 & write_r1[done];
write_r2[go] = f.out == 1 & !write_r2[done];

Indexing in Presence of par

The par control operator allows for parallel group execution.
Again, since groups may use done signals from the same structural component,
we need to carefully define the "FSM index" for each group's done signal:

seq {
  one;
  par {
    seq { two; three; }
    four;
  }
  five;
}

In this program, let's assume that one, two, and three, all use the
same register r.
During compilation, each child of a par node will instantiate a separate
FSM so that it can independently make progress:

group realize_par {
  // fp1 is the FSM register for the seq { .. } block
  two[go] = fp1.out == 0 & !two[done];

  three[go] = fp1.out == 0 & two[done];
  three[go] = fp1.out == 1 & !three[done];

  fp1.in = fp1.out == 0 & two[done] ? 1;

  // fp2 is the FSM register for `four`
  four[go] = fp2.out == 0 & !four[done];
}
group realize_control {
  one[go] = f.out == 0 & !one[done];

  realize_par[go] = f.out == 0 & one[done];
  realize_par[go] = f.out == 1 & !realize_par[done];
}

If we inline realize_par[go] and replace the group's done signals with r.done,
we get:

group realize_par {
  two[go] = (f.out == 0 & r.done | f.out == 1 & !realize_par[done]) & fp1.out == 0 & !r.done;
  ...
  fp1.in = (f.out == 0 & r.done | f.out == 1 & !realize_par[done]) & fp1.out == 0 & r.done ? 1;
}

Which reduce to:

group realize_par {
  two[go] = f.out == 1 & fp1.out == 0 & !r.done & !realize_par[done] ;
  ...
  fp1.in = (f.out == 0 & r.done | f.out == 1 & !realize_par[done]) & fp1.out == 0 & r.done ? 1;
}

This program will entirely skip the execution of group two.
Assuming one takes t1 cycles, we will have the following cycle-by-cycle
behavior:

• cycle 0: f.out == 0 & !one[done] is true and one starts executing.
• cycle t1: f.out == 0 & r.done is true and the children of par statement should start executing.
  However, the assignment of two[go] is not true because it requires f.out == 1. On the other
  hand, the transition assignment to fp1 is true causing fp1 to transition to state 1.
• cycle t1 + 1: Since fp1 is in state 1, two is not executed and instead three starts executing.

The problematic assignment is this:

two[go] = fp1.out == 0 & !two[done];

which is equivalent to:

two[go] = fp1.out == 0 & !(two[done] & fp1.out == 0);

The use of two[done] is indexed by fp1.out but not by the top-level FSM
f.out.
In order to correct this, we should've instead generated:

two[go] = fp1.out == 0 & !(fp1.out == 0 & f.out == 1 & two[done]);

Which, after inlining par[go] would look like:

two[go] = (f.out == 0 & r.done | f.out == 1 & !realize_par[done]) & !(f.out == 1 & r.done) & fp1.out == 0;
two[go] = f.out == 0 & r.done & !(f.out == 1 & r.done) & fp1.out == 0
        | f.out == 1 & !realize_par[done] & !(f.out == 1 & r.done) & fp1.out == 0;
        = f.out == 0 & r.done & !f.out == 1 & fp1.out == 0
        | f.out == 0 & r.done & !r.done & fp1.out == 0
        | f.out == 1 & !realize_par[done] & !f.out == 1 & fp1.out == 0;
        | f.out == 1 & !realize_par[done] & !r.done & fp1.out == 0;
        = f.out == 0 & r.done & !f.out == 1 & fp1.out == 0
        | f.out == 1 & !realize_par[done] & !r.done & fp1.out == 0;

These assignments ensure that during the early transition, when f.out == 0 & r.done, two will start executing.
When f.out == 1 in the next cycle, two will execute till it r.done
becomes high.

TODO: Implication on groups in par that may use the same structural element to signal done (Can this even happen?)

[sampsyo]

Here is one quick pedantic consideration, which I know is kind of a tangent, but just to point it out for separate discussion… one thing we haven't really settled is whether cycle-level timing is actually part of Calyx's semantics. Your comment started out with an example of "naive" FSM generation, which is simple but inefficient:

This means that a control program that should have taken t1 + t2 cycles to finish execution ends up taking 2 extra cycles. Because of Calyx's group isolation property, this program is correct---it is always safe to delay the sequential execution of groups.

And indeed, we would classify this implementation as "correct" if we give a latency-insensitive semantics to Calyx programs. It would be correct but needlessly slow, and we know there is a faster way to implement the same code that is also correct. However, if we want the actual cycle-level timing to be part of the language's semantics, then this would be "incorrect" by that definition, as this earlier statement implies:

this FSM does not accurately capture the cycle-by-cycle semantics of Calyx

Here are some reason to not make the cycle-level timing behavior part of Calyx's semantics:

• The semantics are simpler this way, enabling easier proofs.
• Higher-level semantics admit a wider range of implementations. Both the slow/naive/simple FSM generation and the fast/possibly-complex FSM generation strategies would remain valid. Or, for example, you can imagine an even faster FSM implementation that uses speculation or something—latency-insensitive semantics would be required to allow that flexibility.
• It leaves room for cycle-level timing guarantees to be part of the semantics for statically timed groups. That is, once you add static annotations, the semantics would be the same but stronger because they would add timing requirements to the existing, simpler semantics.

Anyway, I certainly agree with your point about the epistemic utility of building the fastest FSM!

While the fastest FSM may use more complex logic, it can act as a reference for what semantics deem safe.

…so this has just been a tangent to say why this "fast FSM" should be considered sufficient but not necessary to implement a correct Calyx compiler.

[sampsyo]

This is a great summary, and I agree that the central problem is this lie:

This new FSM scheme exposes a crucial lie in the group isolation property of Calyx---that done signals of groups, which may come from structural elements like registers, are not isolated and in fact, must be visible outside group boundaries to enable the current style of compilation.

I am still wrapping my head around the "indexed read" idea as a fix. This is probably a better fit for synchronous discussion, but I would love to see how this fixes the example we've been toying with.

I also want to understand the difference between this approach and the sorta-strawperson (sorta not??) proposal I made above. The spirit there is to resolve the lie by making done signals private "by construction." The contract with the FSM generator would be, then, that it preserves the illusion of owning a private done register. I think this would be a change in language semantics, which would of course be bad, so I'd love to understand the difference with "indexed done," which I believe does not involve such a semantic change.

[rachitnigam]

Updated the above with an example for how indexed done signals will work in presence of par.

[rachitnigam]

@sampsyo For your proposal above, I'm having trouble convincing myself that the fsm.in = whatever & fsm.out == 0 ? 1; will actually work out. If whatever refers to a structural signal that may be shared, then we end up with FSMs that look basically the same as the ones we generate now but without the early transitions.

The broader question I'm trying to answer is if the proposal enables FSMs to operate as fast as the indexed done thing does. It may still be fine if it doesn't, but we should clear that we're imposing a different restriction on Calyx groups then to enable isolation.

[sampsyo]

Here is just a quick note to capture some of the insights that @rachitnigam revealed during a synchronous meeting earlier today, as I interpreted them:

• Here's a way to see the underlying problem in the current state of the world. If we make groups start as early as possible, then, in the first cycle of a given group's execution, its done signal should not be considered reliable. During that cycle, the signal might be high because it's actually some other group's done signal too! Fortunately, we have recently required all groups to take at least one cycle. So it suffices for the FSM logic to ignore the group's done signal for the first ("early") cycle and only pay attention to it during the group's remaining ("late") cycles, i.e., when the FSM register starts containing the state number for that group.
• To put it slightly differently, a group's done signal is only "meaningful" during the last $t-1$ cycles of a group's active span of $t$ cycles, so the FSM logic should only pay attention to it in that truncated range. That's in contrast to all the group's other signals, which are "meaningful" during the entire $t$-cycle span. (Actually, this statement is a little weird, because the done signal is also meaningful on that $t+1$th cycle, where it becomes 1 and all the other signals become meaningless.)
• To enact this policy, the FSM logic has to ensure that it only "pays attention to" a given group's done signal when the FSM's state register is currently outputting that group's state. In the presence of par, this actually means that all the various nested state registers have to be outputting the vector of state numbers that indicate the group.

[rachitnigam]

Thanks for the really nice, concise description about this!