[Bug][TIR] Split Error in Schedule Verification

[zxybazh]

Hi, I noticed a split error when schedule verification is enabled with debug_mask="all", where I think the split is actually valid.
Script to reproduce the issue is here: https://gist.github.com/zxybazh/0759810aa841508c68abbdf7a00c4ab2

The error says:

- Wrong region_cover:  (output, expected=0, actual=1)
- Wrong stage_pipeline:  (root, expected=0, actual=1)

With the help from @spectrometerHBH I noticed this might be related to the region analysis part here:

tvm/src/tir/schedule/state.cc

Line 105 in fefc27f

arith::IntSet::Interval(analyzer->canonical_simplify(produced_region[i].min()),

May I ask if there's any specifical reason that we use canonical_simplify here instead of Simplify?

CC: @wrongtest-intellif @junrushao1994

cc @Hzfengsy @junrushao

[wrongtest-intellif]

use canonical_simplify here instead of Simplify

Hi, the last modification to canonical_simplify is in #9941. Where use canonical first help prove certain patterns. Maybe we could enrich rewrite rules.

For the case, unfortunately, current system can not prove
floormod(((i0_i1_i2_0_i3_0_fused_fused_0*512) + i0_i1_i2_0_i3_0_fused_fused_1), 3136) >= ((floordiv(floormod(((i0_i1_i2_0_i3_0_fused_fused_0*512) + i0_i1_i2_0_i3_0_fused_fused_1), 3136), 56)*56) + floormod(((i0_i1_i2_0_i3_0_fused_fused_0*8) + i0_i1_i2_0_i3_0_fused_fused_1), 56))

if we do not canonical, this is provable:
((floordiv(floormod(((i0_i1_i2_0_i3_0_fused_fused_0*512) + i0_i1_i2_0_i3_0_fused_fused_1), 3136), 56)*56) + floormod(((i0_i1_i2_0_i3_0_fused_fused_0*512) + i0_i1_i2_0_i3_0_fused_fused_1), 56)) >= ((floordiv(floormod(((i0_i1_i2_0_i3_0_fused_fused_0*512) + i0_i1_i2_0_i3_0_fused_fused_1), 3136), 56)*56) + floormod(((i0_i1_i2_0_i3_0_fused_fused_0*8) + i0_i1_i2_0_i3_0_fused_fused_1), 56))

[vinx13]

any updates @wrongtest-intellif ? I also encountered some similar issues, I was not able to prove ((min(0, ((ax0_0_0_ax1_0_0_fused*64) - 63)) + 126) - ((ax0_0_0_ax1_0_0_fused*64) + 63)) <= 0, ax0_0_0_ax1_0_0_fused \in [0, 2). I think overall the analyzer cannot guarantee the final result is simplified, by default analyzer->Simplify will iterate two times (https://github.com/apache/tvm/blob/main/src/arith/analyzer.cc#L129) which is not always sufficient. Shall we just call Simplify since canonical_simplify is part of Simplify?

[wrongtest-intellif]

@vinx13 I agree here the invocation to standalone canonical_simplify is quite strange. However actually I try to increase the steps but could not fix the issue. The order of rewrite_simplify and canonical_simplify matters such that if we first rewrite_simplify (the first step of Simplify), we will never be able to proof some cases, no matter how many times of iters, and vice versa according to current issue.

Whether could I add two code path here as a middle term solution?

• Step 1. Try directly use Simplify here, the most cases should be covered.
• Step 2. If it fails unfortunately, try canonical_simplify first.

For a long term solution to be more robust, I notice that there do exist rules to handle patterns like in your mentioned cases. But unfortunately, for example, if we have a cancel pattern R(a - b) -> simplified, current system could not ensure for a + c - b the pattern could be matched with associative rule, unless the term order is luckily changed (canonical_simplify sometimes achieve this). It seems that a O(n^2) summation term matching is required to solve this issue.

[wrongtest-intellif]

cc @zxybazh Hi~ could you reproduce the https://gist.github.com/zxybazh/0759810aa841508c68abbdf7a00c4ab2 on current HEAD? I failed to reproduce the split verification error..., maybe some improvements happen? (though I think the original issue still exists)

[wrongtest-intellif]

((min(0, ((ax0_0_0_ax1_0_0_fused64) - 63)) + 126) - ((ax0_0_0_ax1_0_0_fused64) + 63)) <= 0, ax0_0_0_ax1_0_0_fused \in [0, 2)

Hi~ Could you kindly provide some associated bad case for it? cc @vinx13

[vinx13]

@wrongtest-intellif this is the case I found https://gist.github.com/vinx13/011a2578eb82509512ac7e896372b410 I think your solution makes sense. In the long term we might want to improve the rewriting rule and ensure that after a certain of iterations the expression should reach a stable form that can be used for region cover analysis

[zxybazh]

cc @zxybazh Hi~ could you reproduce the https://gist.github.com/zxybazh/0759810aa841508c68abbdf7a00c4ab2 on current HEAD? I failed to reproduce the split verification error..., maybe some improvements happen? (though I think the original issue still exists)

Hi I cannot reproduce it either, I did a bit bisect and found this PR #12527 resolved that.

[zxybazh]

Won't fix for now. Please feel free to reopen if this reproduces.