While tensor types support dynamic shapes (dynamic dimensions and unranked), the interfaces defined in ControlFlowInterfaces.* (used for example by SCF) impose type equality constraints along control-flow edges.
This prevents dialects that want to allow dynamic shapes to reuse those interfaces.
There is a question here, as to the meaning of dynamic dimensions and unranked tensors. Do dynamic dimensions and unranked shapes mean âfixed but unknownâ, or can they be dynamic at runtime ? My understanding is MLIR does not want to prevent runtime dynamicism of the shapes.
So the proposal is to update the type constraints in control-flow interfaces to allow such cases.
From local work, this should be achievable with very little code. (But a significant amount of tests !)
In particular, we would define join and meet functions for builtin types (with almost all of the logic dealing with shapes). Once these are available, the constraints in ControlFlowInterfaces.* become simple checks with join and meet.
Does that sound reasonable ?
If so, Iâll clean code locally and upload things for review.
In general, the yielded types must match the declared return type of the outer if operation, and part of the process of lowering into something like SCF (which is a relatively low level dialect and has invariants amenable to code generation) must ensure this either directly or via some kind of shape refinement/casting mechanism.
In related projects that are lowering from unconstrained frontend systems, this is accomplished by adding casts which interop with type refinement. See for example the numpy.static_info_cast op. Something algorithmically needs to decide how much to refine or de-refine such decisions. Iâve also done this before by propagating special unknown types during program specification and then using a type refinement algorithm to fully type everything. For code generation, it is typically important to be precise and consistent on the data flow for how dynamic tensors are.
Itâd be good to hear from others wrt whether I am viewing this as too constrained. Also, it is completely valid to define higher level control flow operations which have whatever constraints are appropriate for your problem area.
We donât want to prevent âdynamicismâ indeed, but I see the question differently here: it is about how implicit vs explicit we should be in the IR about the type.
Right now the core dialects are leaning toward being explicit about type mismatch, for example you would need to:
Some more I should add: while the dialects upstream (including scf) are very explicit and donât prevent from lowering a higher level implicit representation by adding the explicit constructs as needed, it is true that the interface implementation could limit the implementation of more implicit conversion in the control flow implemented by external dialect, and that would be unfortunate.
Right now Iâm not sure where this assumption is baked though, but I can see transformations not being ready to handle this correctly, because of the need to potentially insert cast when performing code motion and the type would change.
Right now the perfect type equality is checked here: https://github.com/llvm/llvm-project/blob/main/mlir/lib/Interfaces/ControlFlowInterfaces.cpp#L127-L132 ; but this has to be called manually I think, there is no guarantee that every operation that implement the interface would do it (unless I missed a code path?).
Ok. Of course for a higher-level dialect the change in the constraint would look cleaner. But the cast solution does make sense if we want to preserve the type equality constraints in SCF. I am not yet sure how annoying dealing with the cast would be, but it should be ok. Iâll come back to comment here if anything interesting comes up.
Is there any interest in taking join and meet functions for the set of builtin types ?
I have found them to be useful when dealing with type inference and co.
A sample of the declarations:
/// The join function for the set of builtin types, and the partial order "less
/// specialized than or equal", noted `â¤`.
/// It returns the most specialized type (if it exists), that is less
/// specialized than both `ty1` and `ty2`.
/// The join `j` of `ty1` and `ty2` is such that:
/// * j ⤠ty1, and j ⤠ty2
/// * For any type t such that t ⤠ty1 and t ⤠ty2, t ⤠j.
/// For example:
/// ty1 | ty2 | ty1 v ty2
/// i8 | i8 | i8
/// i8 | i32 | <none> (null type)
/// tensor<1xf32> | tensor<?xf32> | tensor<?xf32>
/// tensor<1x2x?xf32> | tensor<1x?x3xf32> | tensor<1x?x?xf32>
/// tensor<4x5xf32> | tensor<6xf32> | tensor<*xf32>
/// tensor<1xi32> | i32 | <none> (null type)
/// tensor<1xi32> | tensor<i32> | tensor<*xi32>
Type join(Type ty1, Type ty2, Optional<Location> location = None);
/// More doc.
Type meet(Type ty1, Type ty2, Optional<Location> location = None);
/// Indicates whether `ty1` is compatible with `ty2`, and less specialized than
/// `ty2`.
inline bool isLessSpecialized(Type ty1, Type ty2) {
return join(ty1, ty2) == ty2;
}
/// Indicates whether `ty1` is compatible with `ty2`, and more specialized than
/// `ty2`.
inline bool isMoreSpecialized(Type ty1, Type ty2) {
return meet(ty1, ty2) == ty1;
}
Right but verifyTypes isnât called automatically by operations implementing this interface, thatâs what I referred to in my earlier post as âthis has to be called manually I thinkâ.
I donât know what the intent with this method is or why it wasnât hooked to the verifier entirely.
Changing SCF for this seems undesirable (thatâs my gut). But yeah, higher-level dialects should be able to define their own, and we should definitely think about how RegionBranchOpInterface (and possibly BranchOpInterface) can be adjusted to allow this (or add a new interface), as itâs otherwise way too tedious to have your own control flow ops/verification.
Having join/meet functions for builtin types seems useful!!! If you look at the post I linked, I describe a
âRefinableâ type interface that encodes subtyping relationships that would allow implementing join/meet functions. The other thing we need is the way to upcast/downcast through the type lattice (which the âRefinableâ interface could also provide). That would allow code to generically insert the necessary casts to make types agree at âexact type equalityâ places.
But yeah, higher-level dialects should be able to define their own, and we should definitely think about how RegionBranchOpInterface (and possibly BranchOpInterface) can be adjusted to allow this (or add a new interface), as itâs otherwise way too tedious to have your own control flow ops/verification.
That would be convenient.
Having join/meet functions for builtin types seems useful!!! If you look at the post I linked
The join/meet functions I implemented only supported the builtin types, with no way to âplug inâ support for user types. Iâll check out your thread, and see what I can contribute.
Iâd like to get to the point where we also allow:
an unknown type, that could be later inferred to a known type like âi32â or âtensor<*xi32>â This would be useful to represent both truly dynamic languages and things like c++ template instantiation.
Parameterized types, like tensor so we can typecheck things that have a compile time unknown but runtime constant size like matrix multiply of tensor * tensor . This is quite different from the current tensor<?x?xi32> that has a runtime variable size.
I think 1. can already be achieved by using a custom type. You would still need to cast from and to this type (unbox the dynamic value) if you want to actually compute on it with dialects like math. And the same cast would be used to ensure the type equality constraints that scf has.
I also find 2. appealing and maybe a custom type would be the right way to go there, as well. The main question I had was how expressive the type system should be. We have an analysis that essentially derives these parameterized types (in a side data structure) and we went with affine expressions in its âtype languageâ for now.
I also do not have a good intuition how well such a type system would compose with transformations. The advantage of an analysis is that we can just invalidate it after IR rewrites. If you put this into the type system, you have to make sure rewrites preserve the information. For higher level rewrites I can imagine this but at lower levels this seems difficult. Do you have an intuition on that?
doesnât have to be a tensor. it could turn into âintâ or âfloatâ, for instance.
The point of 2 is to be able to typecheck something like a call to matmul without specializing it. For instance, I have defined matmul(tensor<?x?xf32>, tensor<?x?xf32>) and I call it from a bunch of places in my code. I want to have one version of the matmul code that has the sizes as runtime variables. Today in MLIR, weâd cast away the size information at each call site and then presumably catch the error dynamically inside matmul at runtime. Iâd like to have richer types that would allow catching this error statically at the call site with only the type signature information:
tensor<7x4xi32> x;
matmul(x,x) // Error should have been matmul(x, transpose(x))
This isnât all about the type though, this rule can be implemented with what we have I think, but this is just not possible with the standard call operation.