[Formal][Property Annotation] Annotate Reconvergent-paths using flow variables

[Basmet0]

Each operation has local properties on how tokens are distributed between inputs and outputs. For example, a join operation expects the same number of tokens coming from each input, and sends them to its output. By extracting all of these local equations from a circuit, and then performing Gaussian elimination, one gets equations that describe properties of paths using only the internal states of the operations, rather than having to keep track of how many tokens are sent across each channel.

[Jiahui17]

Here we should describe the model that we assume:

every unit is a cascade of: merge/join/mux -(internal_channel1)-> [slot]* -(internal_channel2)-> fork

Rename i1 -> lambda_internal_channel1

[Jiahui17]

Split this function into multiple smaller ones:

• createFlowVariables
• addEquations
• solveGaussian
• ...

[Jiahui17]

We could do a separate PR for class HandshakeOpInternalState

- <forkOp> fork1 -> { fork1.sent1, fork1.sent2, ... }
- fork1.sent2 -> { "it is a sent", "the second one" }
- parse
- print
- write smv

struct HandshakeOpInternalState {
  StringRef writeSmv() virtual = 0;
  /// This is the same as the "handshake.name" of the operation
  std::string name;
  static std::optional<HandshakeOpInternalState> parse() virtual = 0;
  Operation * getOperation(NameAnalysis& namer) {
    namer.findOepration(this->name)
  }
};


struct EagerForkSent : public HandshakeOpInternalState {
  Operation * op;
  unsigned outputId;
  StringRef writeSmv() override {

  }

  // Validate that there is an op with a matching name
  std::optional<HandshakeOpInternalState> parse(NameAnalysis& namer) override {
    

  }
};

if (auto state = EagerForkSent::parse(name)) {
  ...
} else if (auto state = BufferFull::parse(name)) {
  ...
} 

...

[Jiahui17]

@Basmet0 could you please add one CI/CD example to test this PR? we can invent a new kernel without any memory accesses

[Jiahui17]

if we do not use shared ptr here, we could just do

FlowVariable slot(cmergeOp.getInternalSlotStateNamers()[0]);

Which is much more readable IMO. I think here we should focus on more the readbility of the APIs

[Basmet0]

It needs to be a pointer as InternalStateNamer is a virtual class. I created a wrapper around it that hides the shared pointer creation, and the API now looks similar to your example.

[Jiahui17]

-> hasIndexConstraint?

Add an example of what we are talking about here

[Jiahui17]

Awesome, thanks for the nice work!