Correctness of Guard Synthesis

[rachitnigam]

Compilation of high-level Filament programs need to turn all invocation into guarded assignments that forward the source values into the instance's ports as specified by the schedule.

In short, it must turn this high-level program:

M := new Mult; m0 := M<G>(a.out);

into:

M := new Mult; m0 := invoke M<G>; m0.left = guard ? a.out;

The core problem during lowering is synthesizing guard expressions for each invocation. Here, we'll show that for a well-typed high-level Filament program, we can always generate correct guards.

Restrictions: We only address compilation of programs without max expressions and adhering to restrictions from #27 which disallows relating events using ordering constraints.

Ports on Pipelined FSMs

Generating FSMs: We assume that for each event G for the current component, there is an FSM called Gf that is triggered by the interface port for G:

component main<G>(@interface[G, G+d] go_G: 1) -> (...) {
    fsm Gf[n](go_G);
}

The FSMs for each event can be thought of as a series of shift registers of length n. The port Gf._i is active when the $i^{th}$ register has a token in it. The interval type for a port is:

Gf._i : @[G+i-d, G+i+d] + @exact[G+i, G+i+1]

where d is the delay for the port that triggers the FSM.

First, we look at the active part of the specification: @exact[G+i, G+i+1]. This means that the guard has a non-zero value $i$ cycles after a token enters the FSM.

The availability of the guard is more complex: [G+i-d, G+i+d]. It states that the guard is guaranteed to have a known value in the given duration. Next, it says that the guard does not observe a new token for d cycles after it gets a token or d cycles before it observes a new token.

The intuition for this is that if an FSM is triggered at most once every d cycles, each token is separated by d cycles in both the past and the future. The first token is a special case but we assume that resetting the circuit instantiates everything to $0$.

Constraints on Low-level Assignments

In the high-level program

m0 := M<G>(a.out);

We have the restriction that a.out is available for at least as long as m0.left requires. Thus, if we have the availabilities $[G+m_s, G+n_s]$ and $[G+m_d, G+n_d]$ for a.out and m0.left respectively, we have $[G+m_s, G+n_s] \supseteq [G+m_d, G+n_d]$.

When generating the assignment:

m0.left = guard ? a.out;

We need to synthesize a guard that is available for $[G+m_s, G+n_s]$ and active for $[G+m_d, G+n_d]$, i.e. it has a non-zero value in the interval that the destination requires and long enough to guard the source port.

Lemma: The delay for the event $G$ is greater than or equal to $n_s - m_s$.
Proof. Since a.out is an output from some instance related to invocation a, we know that G must obey the delay constraints (as specified in #20). Specifically, the delay must be longer than the length of the interval of any input or output port. Similar reasoning applies to any input port of the component that can be used in this position.

We also know that $n_s - m_s \geq n_d - m_d$ due to the subset relationship between the source and destination port.

Synthesizability of Guards

Here is the rule we use to generate guards: If the requirement of a destination port is $[G+m_d, G+n_d]$, generate the expression:

Gf._md | Gf._m{d+1} | ... | Gf._n{d-1}

So, if we have the interval $[G+3, G+5]$, we'll generate the expression:

Gf._3 | Gf._4

To show that this is correct, we need to show that:

1. The guard is active for as long as the destination requires
2. The guard is available for as long as the source is

We have (1) by construction since we use the destination to construct the guard expression.

For (2), we have $n_s - m_s \leq d$ and $m_s \leq m_d$, thus we have:

$$ m_s + d \leq m_d + d $$

$$ n_s \leq m_d + d $$

This shows that the guard is active at least until the end of the interval for the source port.

Next, we can use similar reasoning to show that the guard is active at least before the start of the source port:

$$ n_d \leq n_s $$

$$ n_d - d \leq n_s - d $$

$$ n_d - d \leq m_s $$

Thus, we have that the guard is available for at least as long as the source port and active as long as the destination requires.

Implementation

The implementation in the compiler currently does not have a way to talk about terms like G+i-d since negation of events is not supported. If we want the lowered programs to type check, we need some way of doing this. If not, we can skip implementing this and rely on the pen-and-paper proof.