This change gives explicit order of verifier execution and adds `hasRegionVerifier` and `verifyWithRegions` to increase the granularity of verifier classification. The orders are as below, 1. InternalOpTrait will be verified first, they can be run independently. 2. `verifyInvariants` which is constructed by ODS, it verifies the type, attributes, .etc. 3. Other Traits/Interfaces that have marked their verifier as `verifyTrait` or `verifyWithRegions=0`. 4. Custom verifier which is defined in the op and has marked `hasVerifier=1` If an operation has regions, then it may have the second phase, 5. Traits/Interfaces that have marked their verifier as `verifyRegionTrait` or `verifyWithRegions=1`. This implies the verifier needs to access the operations in its regions. 6. Custom verifier which is defined in the op and has marked `hasRegionVerifier=1` Note that the second phase will be run after the operations in the region are verified. Based on the verification order, you will be able to avoid verifying duplicate things.
Details
Diff Detail
- Repository
- rG LLVM Github Monorepo
Event Timeline
LG but my main gripe is with the naming.
mlir/docs/OpDefinitions.md | ||
---|---|---|
573 | You should clarify that these are actually "core" traits vs "early" traits. | |
575 | Can you add the verification of nested operations and then traits/interfaces/verifiers that are run after that to the verification order list? | |
mlir/include/mlir/IR/OpBase.td | ||
2203 | I'm not crazy about the names earlyVerify and lateVerify. If the behaviour of the current verify function is the same as earlyVerify, then why not just keep it and rename lateVerify to something like verifyAfterNestedOps? (Which is also a less ambiguous name). @jpienaar any thoughts? | |
mlir/include/mlir/IR/OpDefinition.h | ||
1623 | So in theory a single trait can define all of the verifyCoreTrait, verifyEarlyTrait, and verifyLateTrait functions? Is this a useful capability or maybe something that should be avoided? I.e. instead traits define a template parameter VerificationOrder::First or Early or AfterNestedOps. | |
mlir/include/mlir/IR/SymbolTable.h | ||
340 ↗ | (On Diff #398041) | nice |
mlir/include/mlir/IR/OpBase.td | ||
---|---|---|
2203 | Agreed on names (I'm also not fan of core - to some extent everything we verify is core to the op or trait). Could you clarify the existing behavior vs the new ones here? (Jeff's question). This reminds me of a ternary tree traversal in-order (with two leave nodes). Perhaps explicit is better, instead of early and late. preNestedRegionVerification, postNestedRegionVerification. What if we had PostNestedRegionVerify<"too"> ODS traits and then just generated the verification order in the op? That could also help with reuse ODS, make it easier to attach and avoid making this blocks of code on the op. |
mlir/include/mlir/IR/OpBase.td | ||
---|---|---|
2203 | Yes, the existing verify is at the same order as earlyVerify. The reason I add it is to let people be aware this verification behavior. When they define the verifier for an op, they can also be aware that there's an ordering thing need to take care About the core thing, I was thinking the name like verifyStructureTrait or verifyInvariantTrait. I want to say that they are the MLIR core traits and they are supposed to be the first group of verifiers to be run (because they can be run independently). Any suggestions for the name? I agree that the name is not good, I wanted it to be short but couldn't have a better idea. preNestedRegionVerification and postNestedRegionVerification I think is way better. about PostNestedRegionVerify, I think this is a good idea. I prefer not to have many code blocks in the ODS. Will use this approach in the next revision. |
mlir/include/mlir/IR/OpBase.td | ||
---|---|---|
2203 | postNestedRegionVerification is a little bit too long: let postNestedRegionVerifier = [{...}]; Seems a little bit excessive. I would personally petition that the verifier with the same behaviour as the old verifier keep its name (i.e. verifier) whereas the new hooks get the longer names. |
mlir/include/mlir/IR/OpBase.td | ||
---|---|---|
2203 | Also agreed on the naming. IMO the common thing should be the easiest to spell. Do we know how many operations would need something other than late verification? It feels not great to have to say postRegionVerification(or anything with Region) on an operation that doesn't have regions (the overwhelming majority). What if we just left the name verify as-is and made that correspond to late verification, with anything other than "after everything else" having a special name? |
mlir/include/mlir/IR/OpBase.td | ||
---|---|---|
2203 | Sorry, currently I only know few of them like the SymbolTable. Some verifiers may be the late verification category but they just make it work with either duplicated verification or replying on implementation defined behavior. About the region, you gave a good point. Not all the operations have regions. I agree with the idea that give the verify the late semantic and having a name for early category. What do you think if we replace the way we define a verifier with having a trait to do that? (The idea mentioned by Jacques from above) |
Also, can you update the patch description (and documentation) to clearly lay out the verification order? I.e.
- core traits
- early traits (?)
- early interfaces
- early op
- nested region verifiers
- late traits
- late interfaces
- late op
mlir/include/mlir/IR/OpBase.td | ||
---|---|---|
2203 | I'm kind of "eh" on the ODS traits idea. I think that we can keep verifier (or hasVerifier) as is, with its current behaviour. The "early" verifier can be preNestedVerifier (or hasPreNestedVerifier). I think this name is descriptive enough but not too long, given that not many ops have pre-nested verifiers. And those that do probably have regions. As for traits: I think the verification order should be specified by a template argument or something template <typename ConcreteType> class MyTrait : public TraitBase<ConcreteType, MyTrait, TraitBase::VerifyPostNested> {...}; Where the default is VerifyPostNested, as it currently (and only) is. The three places would be called VerifyFirst, VerifyPreNested, and VerifyPostNested. With the current implementation of trait verification ordering, it's possible for a trait to (by defining one of each function) verify itself at three different locations. This capability is probably not necessary. Interfaces should have the same naming as op verifiers (i.e. verifier and preNestedVerifier) |
mlir/include/mlir/IR/OpBase.td | ||
---|---|---|
2203 | Now we just have an updated on defining the verifier, I may not change the way we use it. So the trait proposal was faded out. I would like to make the current hasVerifier as VerifyPostNested and have a better name for the other. Yes, I prefer not to give the capability of defining both pre/post in a trait/interface(maybe op needs it). In the next revision, I'm considering something like dependsOnRegionVerification to indicate the pre/post behavior. Hopefully, things will be easier and clear. |
Abandon the early-/late- label which are too complicated.
Add hasRegionVerifier and verifyWithRegions for op and interface respectively
and keep the order of verifier defined by hasVerifier so that we have reduced
the number of new labels.
mlir/docs/OpDefinitions.md | ||
---|---|---|
578 | ||
579 | ? "Position" as in according to the verification order? | |
601–602 | I would say something like "Verifiers further down the order can rely on certain invariants being verified by a previous verifier and do not need to re-verify them" | |
mlir/docs/Traits.md | ||
39–44 | ||
59–61 | ||
mlir/include/mlir/Dialect/Affine/IR/AffineOps.h | ||
231 | Why not just delete the verifyInvariants function? To avoid having two names for the same function. | |
mlir/include/mlir/IR/OpBase.td | ||
2027 | ||
2061 | I see that the purpose of this is so that these traits are placed first. Why is this needed? I thought that the traits would be verified in the order they are declared on the op (including in ODS). |
Overall LGTM. I'm "eh" on the InternalOpTrait approach. Probably should also wait for river
mlir/include/mlir/Dialect/Affine/IR/AffineOps.h | ||
---|---|---|
231 | Some places they use the verifyInvariants to do verification which I think that may not the correct way to do that. At here, I just make the calling of verifyInvariants has the same behavior as before. Once I confirm that's incorrect, I'll remove this verifyInvariantsImpl. PS. I left a TODO in OpDefinitionsGen.cpp which addresses this | |
mlir/include/mlir/IR/OpBase.td | ||
2061 | The main reason is the execution of verifyInvariantsImpl(which verify the types/attrs/regions, .etc, and is wrapped with OpInvariants trait). verifyInvariantsImpl depends on some core traits(for example, verifying the type of variadic operands may need AttrSizedOperandSegments to be verified) so that it needs to be run after these core traits and before other user defined trait/interface. Some of the core traits we are able to ensure the order, like ZeroOperands, because they are inserted by tblgen. Other core traits are added by the user. In order to distinguish the core traits and user defined traits, InternalOpTrait was added. It's similar to GenInternalTrait In case I didn't explain it clear, here's an example, this is the traits declared, OpInvariants trait needs to be inserted after AttrSizedOperandSegments and before FooTrait. |
mlir/include/mlir/IR/OpBase.td | ||
---|---|---|
2028 | I'm not sure we want the doc here to refer to "core MLIR framework". I think what you are getting at here is that some traits we want to be treated as "first" in the list? the invariants for those traits are a bit more constrained than "defined in core MLIR framework". We have a lot of traits defined in IR/ just because (for legacy reasons or some other weird reason), but that doesn't give them any special significance over other traits. We should really nail down here a fundamental characteristic that separates these classes of traits from the rest (e.g. you mention that some traits are used to do important structural verification that is relied upon to be done first). | |
2058–2062 | Not all of these are things I would define as "core traits". A lot of these are essentially "user traits", but just happen to be defined here. Are any of these really necessary to be treated as "core" traits? The only ones I can really think of are maybe things related to operand segment sizes (like AttrSizedOperandSegments). | |
2482 | ||
mlir/tools/mlir-tblgen/OpDefinitionsGen.cpp | ||
2243 | Realistically, I think users should not be calling anything related to verification directly on the op class. Some people have been calling op.verify()(now op.verifyInvariants()) thinking that it does the same thing as mlir::verify(it doesn't). If we want users to be able to verify just a specific operation (and not nested operation), we should add an explicit API to Verifier.h alongside mlir::verify. |
mlir/docs/OpDefinitions.md | ||
---|---|---|
570–602 | Why do these need to be separate? Is there a problem with having both? I assume the constraints on the two methods are different right? |
mlir/docs/OpDefinitions.md | ||
---|---|---|
570–602 | Yes, we can have both but I wasn't sure if we really need it. The user defined verifier is supposed to verify the thing which is not scoped by the trait, interface or certain invariants and no one is able to have the dependency with user defined verifier. Then It implies that the logic in hasVerifier can be moved into hasRegionVerifier. And now I only allow one verifier for trait/interface, so I make them consistent. What do you think? |
Because there's no major concern in the verification order, I would like to merge this first so that we can have the new test cases written in a way that meet the new verification request.
You hadn't updated the documentation, and our discussion hadn't been resolved. Please refrain from submitting patches that have open discussion.
Sorry, my bad. will update the doc and we can address the hasVerifier and hasRegionVerifier discussion there.
You should clarify that these are actually "core" traits vs "early" traits.