Invalid pipeline with resource sharing passes type checking

[rachitnigam]

The following program defines an unsafe pipeline:

import "primitives/core.fil";

component Main<G>(
  @interface[G, G+3] go_G: 1,
  @[G, G+1] l0: 32,
  @[G, G+1] r0: 32,
  @[G+9, G+10] l1: 32,
  @[G+9, G+10] r1: 32,
) -> () {
  M := new Mult;

  m0 := M<G>(l0, r0);
  m1 := M<G+9>(l1, r1);
}

It runs the same multiplier on the first and the ninth cycles of its execution.
However, this pipeline is unsafe; here is a sequence of events that will cause conflicting use of G:

1. Cycle 0: Main triggered (invocation 1), m0 starts executing
2. Cycle 3: M completes execution
3. Cycle 9: Main triggered again (invocation 2). However, invocation 1 of Main attempts to execute m1 which now conflicts with execution of m0 in invocation 1.

The @interface port should be constrained so that it does not attempt to restart the module until all executions of a instance have had a chance to run.

Initiation Intervals for Pipelines

Definition: For a pipeline $P$, let $P(t)$ be the invocation of $P$ at time $t$. The initiation interval is the smallest value $i$ such that for all cycles $t$, $P(t)$ and $P(t+i)$ do not conflict. In order words, $i$ is the minimum number of cycles before which $P$ can be safely executed anytime in the future.

Definition (safe execution of a pipeline): A pipeline execution is safe if no resource used in the pipeline conflicts with any other usages of the pipeline. In other words, all active invocations of the pipeline use disjoint sets of resources.

Note: The use of "anytime" in the definition of an initiation interval is important because there might exist other values $l$ such that $l < i$ and $P(t)$ and $P(t+l)$ do not conflict however, there exists some time $n$ such that $P(t)$ and $P(t+l+n)$ do conflict. The existence of such $n$ makes $l$ an invalid initiation interval. Filament could infer this if there was a way to force the calling context to invoke the pipeline exactly $l$ cycles later.

The current restriction on @interface are:

1. Its delay, computed as the difference between the end and start time, is longer than the delay of any input or output port that uses the interface's corresponding event.
2. Its delay is longer than the delay required by any invocation that uses the corresponding event for scheduling.
3. Its delay is sufficient to ensure that reuse of an instance does not conflict with any other use.

We can divide the requirements into safety conditions for one invocation and safety conditions for pipelined use.
(3), along with the availability checking of signals within the body of the component, ensures that one use of a pipeline is correct; all signals are valid when they are read and resource usage is non-conflicting.

(1) & (2) attempt to ensure that pipelined usages of the component are safe.
(1) ensures that subsequent pipelined invocations do not break the requirements or guarantees of a previous invocation.
(2) ensures that all components used inside the module are only invoked when they can be safely pipelined.

The missing piece is this: the @interface signal needs to ensure that a pipelined invocation of a resource does not conflict with the current use of the components.
A high-level, we can imagine "ghost" version of all components floating around that represent the execution of the pipeline at time interval $i$. We need to ensure that none of them conflict with the current execution.

My current thought on how to do it is by ensure that the end time of @interface is greater than or equal to the max of the end times of all usages of an instance. I have to convince myself that this is necessary and sufficient.

[rachitnigam]

@sampsyo Do the constraint feel consistent with my explanation from our meeting?

[rachitnigam]

Just updating this to say that the bounds are probably min(...) of the start times of all invocations and max(...) of the end times of all invocations.

[sampsyo]

This all sounds right! (Sorry for the delay in this affirmation.) The one thing I'd be curious about nailing down is categorizing criteria (i.e., (1), (2), and (3) above) into "goal criteria" and "sufficient conditions" for those criteria. Namely, it seems like (3) is clearly a goal, in that avoiding conflicts is the property we're trying to enforce. (1) sounds a bit more like a sufficient condition that implies a goal, which may be (3) or something else. I'm not 100% sure about (2). But does the desire for that distinction make sense?

[rachitnigam]

Yeah, it makes a lot of sense! (3) really is a goal criteria while the other two are sufficient conditions to enforce the real type safety properties of the system. Another way to view this is that we haven't yet turned (3) into a sufficient condition, its just stating the desired property