Skip to content
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] Add internal NarrowPredicateExpression utility #13041

Merged
merged 1 commit into from
Oct 27, 2022

Conversation

Lunderberg
Copy link
Contributor

Implements tvm::arith::NarrowPredicateExpression, a utility that removes free parameters from a boolean expression, such that the resulting expression being true implies that the original expression is true. For example, the predicate (0 <= i+f) && (i+f < 16), where f is a free parameter on the range 0 <= f < 2), can be narrowed to the expression (0 <= i+0) && (i+2 < 16).

In effect, NarrowPredicateExpression functions as a context-sentive tvm::tir::Substitute, where the value substituted is selected such that the resulting expression errs on the side of being false. This is an internal utility used as part of the simplifications for layout transformations (tracking issue link).

@Lunderberg
Copy link
Contributor Author

Marking as a draft PR until it passes CI. This utility could also be moved to be internal to an upcoming data-flow analysis utility.

@Lunderberg
Copy link
Contributor Author

@tvm-bot rerun

Implements `tvm::arith::NarrowPredicateExpression`, a utility that
removes free parameters from a boolean expression, such that the
resulting expression being true implies that the original expression
is true.  For example, the predicate `(0 <= i+f) && (i+f < 16)`, where
`f` is a free parameter on the range `0 <= f < 2)`, can be narrowed to
the expression `(0 <= i+0) && (i+2 < 16)`.

In effect, `NarrowPredicateExpression` functions as a context-sentive
`tvm::tir::Substitute`, where the value substituted is selected such
that the resulting expression errs on the side of being false.  This
is an internal utility used as part of the simplifications for layout
transformations ([tracking issue
link](apache#12261)).
@Lunderberg Lunderberg force-pushed the narrow_predicate_expression branch from 7652d31 to c6d78c1 Compare October 14, 2022 18:16
@Lunderberg
Copy link
Contributor Author

Rebasing onto main to get the bug fix from #13067

@Lunderberg Lunderberg marked this pull request as ready for review October 14, 2022 18:17
@tvm-bot
Copy link
Collaborator

tvm-bot commented Oct 14, 2022

Thanks for contributing to TVM! Please refer to the contributing guidelines https://tvm.apache.org/docs/contribute/ for useful information and tips. Please request code reviews from Reviewers by @-ing them in a comment.

Generated by tvm-bot

@wrongtest-intellif
Copy link
Contributor

0 <= f < 2), can be narrowed to the expression (0 <= i+0) && (i+2 < 16)

Hi~ I feel a bit confused about here: when f == 0, the i could take value in range [0, 16), thus what is the purpose to get narrowed predicate i + 2 < 16?

@Lunderberg
Copy link
Contributor Author

Hi @wrongtest-intellif ! The goal is to produce an expression that, when true, implies that the original expression is true. For this specific example, suppose we know that i + 2 < 16. Because we also know that the free parameter f satisfies 2 < f, we know that i + 2 < i + f. Therefore, since i + f < i + 2 < 16, i+f < 16.

The NarrowPredicateExpression is part of a larger data-flow analysis that I'm preparing as part of handling padded buffer transforms. When analyzing whether a specific index corresponds to padding, conditions such as pad_left <= i+f < original_width + pad_left (identifies a non-padding data value) frequently show up. By converting these into expressions that are true regardless of the value of f, or expressions that are false regardless of the value of f, we can remove reduction axes from the overall predicate expressions.

@areusch areusch added needs-triage PRs or issues that need to be investigated by maintainers to find the right assignees to address it and removed needs-triage PRs or issues that need to be investigated by maintainers to find the right assignees to address it labels Oct 19, 2022
Copy link
Contributor

@jwfromm jwfromm left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very cool idea and a nice implementation. Thanks @Lunderberg!

@jwfromm jwfromm merged commit 0c10302 into apache:main Oct 27, 2022
@Lunderberg Lunderberg deleted the narrow_predicate_expression branch October 28, 2022 14:02
xinetzone pushed a commit to daobook/tvm that referenced this pull request Nov 10, 2022
Implements `tvm::arith::NarrowPredicateExpression`, a utility that
removes free parameters from a boolean expression, such that the
resulting expression being true implies that the original expression
is true.  For example, the predicate `(0 <= i+f) && (i+f < 16)`, where
`f` is a free parameter on the range `0 <= f < 2)`, can be narrowed to
the expression `(0 <= i+0) && (i+2 < 16)`.

In effect, `NarrowPredicateExpression` functions as a context-sentive
`tvm::tir::Substitute`, where the value substituted is selected such
that the resulting expression errs on the side of being false.  This
is an internal utility used as part of the simplifications for layout
transformations ([tracking issue
link](apache#12261)).
xinetzone pushed a commit to daobook/tvm that referenced this pull request Nov 25, 2022
Implements `tvm::arith::NarrowPredicateExpression`, a utility that
removes free parameters from a boolean expression, such that the
resulting expression being true implies that the original expression
is true.  For example, the predicate `(0 <= i+f) && (i+f < 16)`, where
`f` is a free parameter on the range `0 <= f < 2)`, can be narrowed to
the expression `(0 <= i+0) && (i+2 < 16)`.

In effect, `NarrowPredicateExpression` functions as a context-sentive
`tvm::tir::Substitute`, where the value substituted is selected such
that the resulting expression errs on the side of being false.  This
is an internal utility used as part of the simplifications for layout
transformations ([tracking issue
link](apache#12261)).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants