Erratic stack overflow in infer.rs 'live_vars'

[acl-cqc]

• See branch tests/infer_stack_overflow for the test (not very minimal, sorry - I haven't tried to reduce)
• Commit 6d4b446 precisely identifies the place where the HashSet's iteration order determines the outcome, and makes the test panic every time (without affecting any other test - obviously this hasn't come up before)
• The problem seems to be that merge_equal_metas has found a set of equal variables where one also has a Plus constraint on another. This results in the merged variable effectively having a plus constraint on itself!
• I also tried the fix of fix(Inference): Work harder in variable instantiation #591 (see branch tests/infer_stack_overflow2) , but although that PR adds code to deal with cycles, it doesn't fix the bug. I think the problem is that live_var (where the infinite-recursion happens) is called from results before we get to instantiating variables. This suggests that we may need to deal with cycles of Plus nodes (as fix(Inference): Work harder in variable instantiation #591 does) earlier, i.e. in main_loop rather than instantiate_variables ??

[croyzor]

😱

[acl-cqc]

Ok, so a sufficient condition for creating a Meta that has a Plus on itself (the source of the infinite loop) appears to be to have nodes A,B,C; and edges A->B, A->C, B->C.

• Clearly if B's extension_reqs are not already in A's output-extensions set, then a lift node will be needed on the edge A -> C
• However, if B's extension_reqs are present in A's output-extensions set, no lift node is really required: you wouldn't need one if you specified all the input_extensions yourself. But if you don't do this, this might hang the algorithm. (I've not established what conditions there might be beyond a Plus constraint from a meta to itself)....

In this case the node A was a Const used in two places. "Fixes" to the test include:

• Adding a Lift on the second use makes the test pass, see 09c07b6.
• Adding a Lift on the first use lead to a similar infinite-loop but more difficult to spot (a cycle of Plus nodes of length > 1) :-( :-(
• Adding a Lift node on both uses solved the above problem but meant we couldn't infer a set of input extensions to the Const node (!), so the test still fails.
  • Also specifying the input-extensions of the Const to pure, the test passed. Note PR refactor: NodeType constructors, adding new_auto #635 would do that by default, which seems like a good step, although we still need both Lift nodes.
• An alternative fix (39e8740) was to fix the input-extensions of the Const (a unary-unit-sum!) to include the extension id (collections)! Which says that a solution does exist but that the inference algorithm is hanging rather than finding it.

[acl-cqc]

So, some easy steps for this particular case where node A is a Const:

• For Const nodes: default to no input-extensions, as per refactor: NodeType constructors, adding new_auto #635
• Remove the Equals constraint for Static edges. (A single line deletion.) Whilst this is not removing the need for lift nodes, it solves a needlessly-painful common case (i.e. using constants and calling functions).

For the general case, we'll need to work on the algorithm...

• I note live_vars are only used in fn results. So rather than a live_var function that recurses (perhaps infinitely :-( ), we could calculate the set of live_vars (by a scan through all Plus constraints, using a queue and a "seen" hashset) at the beginning of fn results. This would avoid all such infinite loops :-).
  • This could be tricky if we really need to know which "variable" makes a particular meta live. However AFAICS there is only one variable (the input-extensions to the whole hugr)??? So we could make that clear by changing variables: HashSet to variables: Option....
• But I have to ask how much this two-stage algorithm with variables is helping us; it adds a lot of complication. Could we not require the Hugr input extensions to be fixed (or constrain them to empty-set if open)?

[acl-cqc]

EDIT: Remainder moved to #639
This relates quite strongly to how we deal with cycles of Plus constraints, so I'll dump some thoughts here.

• I suspect we should deal with cycles much earlier, i.e. in main_loop - either in merge_equal_metas or in parallel with it, rather than in instantiate_variables as in PR fix(Inference): Work harder in variable instantiation #591. That is, a cycle of Plus constraints, means all nodes on the cycle must be equal, so can be merged.
  • However, we must record the ExtensionId's added by the Plus constraints somehow....
  • How about not (just?) solutions but lower_bounds - a cycle of Plus constraints sets a lower bound, the merged meta must include the lower-bound extensions. (Maybe in addition to solutions? or maybe we also have upper_bounds when known - if there is a single concrete solution, then lower=upper. Or maybe we have another variant Constraint::IncludesSet - note we could remove Constraint::Plus if we then also had Constraint::IncludesMeta).
  • Note that when all Meta's connected by Equals constraints are merged, and all cycles of Plus constraints are merged, we have a tree of plus constraints. The leaves can therefore only be Metas with concrete solutions, or "variables". Every node will have a solution (if it doesn't depend upon a variable) or a lower-bound (if it does - the lower-bound is the union of Plus(ExtensionId,...) on any path to a variable). If there is only one variable (the input-extensions to the whole Hugr), then the solutions are just calculated by taking union of each lower-bound with the value of said variable....

I think the big advantage of this is it avoids the need for the lift node? In some cases? I.e. it'll fix a lower-bound for the outputs of A just because they must be equal to themselves union B.extension_reqs ?

[acl-cqc]

EDIT: Remainder moved to #639

I think the big advantage of this is it avoids the need for the lift node? In some cases? I.e. it'll fix a lower-bound for the outputs of A just because they must be equal to themselves union B.extension_reqs ?

Of course no - if we require that input extensions at the target of every (static/value/control) edge equal output extensions at the source, we would still need lift nodes. But validation is different from inference, and it would be easy to change validation to check merely that extensions at the source of each edge were a subset of extensions at the target; perhaps the above then gives a procedure for inference?