Page MenuHomePhabricator

[mlir] Tighten the verification of SameOperandsAndResultType
Needs ReviewPublic

Authored by rriddle on May 5 2022, 3:25 PM.

Details

Reviewers
mehdi_amini
Summary

We currently use and treat SameOperandsAndResultType differently than it is
actually implemented. We have many uses (both in ODS and in all of our upstream operations)
that assume that SameOperandsAndResultType means that the types are pointer-identical,
i.e. literally the "same" type. The trait implementation however, allows for shaped types to be
"compatible", meaning that they can differ in some cases (e.g. tensor<1xf32> is "compatible"
with tensor<*xf32>). This is quite problematic because it means that if used in certain ways,
an operation could: adopt invariants it doesn't expect, lose information (the assembly format
assumes that "same" means "pointer-identical"), etc. This commit rectifies this by tightening
the verification to be pointer identical. If users actually rely on this, they can get the same
behavior by using the SameOperandsAndResultShape and SameOperandsAndResultElementType
traits.

Diff Detail

Event Timeline

rriddle created this revision.May 5 2022, 3:25 PM
Herald added a project: Restricted Project. · View Herald TranscriptMay 5 2022, 3:25 PM
rriddle requested review of this revision.May 5 2022, 3:25 PM

they can get the same behavior by using the SameOperandsAndResultShape and SameOperandsAndResultElementType traits.

Should SameOperandsAndResultShape be renamed CompatibleOperandsAndResultShape?

they can get the same behavior by using the SameOperandsAndResultShape and SameOperandsAndResultElementType traits.

Should SameOperandsAndResultShape be renamed CompatibleOperandsAndResultShape?

Yeah, let me do that in a followup.

they can get the same behavior by using the SameOperandsAndResultShape and SameOperandsAndResultElementType traits.

Should SameOperandsAndResultShape be renamed CompatibleOperandsAndResultShape?

Yeah, let me do that in a followup.

But the user really wants them to be the same dynamically. E.g., if you have ?x? and ?x?, the same shape is where the four unknowns are dynamically pairwise equal. Treating ?==? as true, isn't the goal as these could be different dynamically, but statically they aren't known. And restricting shape equality to static interpretation is more lax as it doesn't require dynamic equality but merely about static type. Yes verify wise equivalent'ish, but concept captured differs. Same here represents an equality constraint, statically we don't have sufficient information to reject so we have to be permissive. But it means where you have ?x? and 7x?, the first shape's unknown can be inferred to be 7 and propagated. That's not true for compatible.

If users actually rely on this, they can get the same

behavior by using the SameOperandsAndResultShape and SameOperandsAndResultElementType
traits.

Can you add OpTraitList implementation for this? (Following InferTensorType)

they can get the same behavior by using the SameOperandsAndResultShape and SameOperandsAndResultElementType traits.

Should SameOperandsAndResultShape be renamed CompatibleOperandsAndResultShape?

Yeah, let me do that in a followup.

But the user really wants them to be the same dynamically. E.g., if you have ?x? and ?x?, the same shape is where the four unknowns are dynamically pairwise equal. Treating ?==? as true, isn't the goal as these could be different dynamically, but statically they aren't known. And restricting shape equality to static interpretation is more lax as it doesn't require dynamic equality but merely about static type. Yes verify wise equivalent'ish, but concept captured differs. Same here represents an equality constraint, statically we don't have sufficient information to reject so we have to be permissive. But it means where you have ?x? and 7x?, the first shape's unknown can be inferred to be 7 and propagated. That's not true for compatible.

Should we rename the verifyCompatibleShape method?