-
Notifications
You must be signed in to change notification settings - Fork 3.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Arith] Provide tighter ConstIntBounds for special cases #16588
[Arith] Provide tighter ConstIntBounds for special cases #16588
Conversation
One thing that we would like to consider is the overall efficiency. ConstIntBound is one such case where we are not trying to do complicated pattern matching and relies on the independent property, as a result it can be called extensively in the inner loop of analysis. It is useful to blance the overall efficiency as well as the readability and easy to reason(it is a good thing to keep ConstIntBound simple when its behavior is predictable) , where to place those detections. I think it is helpful to support some of the more complicated patterns, usually we do that use another form of SubAnalyzer, or proves with stronger strength(https://github.com/apache/tvm/blob/main/include/tvm/arith/analyzer.h#L75). Some of our previous proves tries to introduce a different strength that is not being explicitly used in inner loops of other simplifiers. I believe this case is also similar |
Good point on checking the performance. I did a benchmark, with shown results shown in the plot below. The x-axis is the time required to run the analyzer with the Click for benchmark settings
In the majority of cases, there is effectively no performance difference. In cases where the improved bounds returned from |
I still think in this case the overall constraining the behavior of ConstIntBound is more predictable and readable. My main worry is we open a flood gate of introducing many recursive rewrite patterns to ConstIntBound itself.
|
Ah, I think I see where I may have miscommunicated. There isn't actually any recursive rewriting being performed. The pattern matching are used to extract information, and not to perform any rewrites or allocations. Stating that I absolutely agree that
I think it could be moved to the My worry with introducing arguments for the proof strength is that it adds code complexity, and requires callers to know an additional argument. For cases that have a significant computational overhead, that's worth it to avoid surprising a user. For cases that don't, and would follow the same API, I'd want to avoid having that requirement where possible. Rather than enabling it by proof strength, what if we start with it it behind an extension flag (link). Where more computationally expensive simplifications would always require a user to opt-in with a higher proof strength, individually-enabled flags could allow new simplifications to be introduced as opt-in, and only later be enabled by default.
Absolutely agreed. For this case, I compared the range of output values for several
That makes sense, and I agree that it would be good to comment on it. |
6ac8366
to
b125f5e
Compare
This PR is now updated to perform the checks for The updated behavior is sufficient to unblock #16589. |
Thank you @Lunderberg ! |
f2541cc
to
eaa2e71
Compare
Expressions of the form `(A+B)*C < (A*B)*D` can occur occur when comparing the number of operations required for two different orderings in which matrix multiplications can be performed. Proving or disproving this conditional allows an optimal order of execution to be selected, even for dynamic argument shapes. The default behavior of `ConstIntBounds` assumes that each term in an expression is independent. For example, the maximum value of `(A+B)*C - (A*B)*D` is determined by taking the maximum value of `(A+B)*C` and subtracting the minimum value of `(A*B)*D`. This algorithm can be applied in all cases, but can provide a bound that is looser than strictly required. This commit adds a check for this case in `ConstIntBounds`, to provide a tighter bound of possible values. When `A`, `B`, `C`, and `D` are all positive values, as is the case for tensor shapes, the inequality can be written as `1/A + 1/B < D/C`. If this inequality holds for the minimum values of `A`, `B`, and `D`, along with the maximum value of `C`, then it holds for all values.
eaa2e71
to
47a1fbd
Compare
This reverts commit 47a1fbd.
This is a follow-up to apache#16588. Due to an incorrect rebase, the version that was merged into `main` had the tighter `ConstIntBounds` enabled by default, rather than having them implemented in `RewriteSimplifier`, gated behind a feature flag.
This is a follow-up to apache#16588. Due to an incorrect rebase, the version that was merged into `main` had the tighter `ConstIntBounds` enabled by default, rather than having them implemented in `RewriteSimplifier`, gated behind a feature flag.
* [Arith] Provide tighter ConstIntBounds for special cases Expressions of the form `(A+B)*C < (A*B)*D` can occur occur when comparing the number of operations required for two different orderings in which matrix multiplications can be performed. Proving or disproving this conditional allows an optimal order of execution to be selected, even for dynamic argument shapes. The default behavior of `ConstIntBounds` assumes that each term in an expression is independent. For example, the maximum value of `(A+B)*C - (A*B)*D` is determined by taking the maximum value of `(A+B)*C` and subtracting the minimum value of `(A*B)*D`. This algorithm can be applied in all cases, but can provide a bound that is looser than strictly required. This commit adds a check for this case in `ConstIntBounds`, to provide a tighter bound of possible values. When `A`, `B`, `C`, and `D` are all positive values, as is the case for tensor shapes, the inequality can be written as `1/A + 1/B < D/C`. If this inequality holds for the minimum values of `A`, `B`, and `D`, along with the maximum value of `C`, then it holds for all values. * Parametrize ConstIntBound tests * Benchmark with/without the BoundUsingReciprocal function * Revert "Benchmark with/without the BoundUsingReciprocal function" This reverts commit 47a1fbd.
…ache#16735) This is a follow-up to apache#16588. Due to an incorrect rebase, the version that was merged into `main` had the tighter `ConstIntBounds` enabled by default, rather than having them implemented in `RewriteSimplifier`, gated behind a feature flag.
Expressions of the form
(A+B)*C < (A*B)*D
can occur occur when comparing the number of operations required for two different orderings in which matrix multiplications can be performed. Proving or disproving this conditional allows an optimal order of execution to be selected, even for dynamic argument shapes.The default behavior of
ConstIntBounds
assumes that each term in an expression is independent. For example, the maximum value of(A+B)*C - (A*B)*D
is determined by taking the maximum value of(A+B)*C
and subtracting the minimum value of(A*B)*D
. This algorithm can be applied in all cases, but can provide a bound that is looser than strictly required.This commit adds a check for this case in
ConstIntBounds
, to provide a tighter bound of possible values. WhenA
,B
,C
, andD
are all positive values, as is the case for tensor shapes, the inequality can be written as1/A + 1/B < D/C
. If this inequality holds for the minimum values ofA
,B
, andD
, along with the maximum value ofC
, then it holds for all values.