Mixed-shareability semantics of ref.eq

[tlively]

To preserve our principle types properties, we either have to create a new version of ref.eq for use with shared references or we have to let the existing ref.eq validate with any combination of shared and unshared operands. So far we have chosen the latter option.

This raises the question of what the semantics of ref.eq should be in interesting cases where one argument is shared and the other is unshared. Here is the behavior I assume we want, but it would be good to make sure everyone agrees.

shared	unshared	result
null	null	1
i31 c	i31 c	1
...	...	0

This would strongly encourage implementations to have the same representation for ref.null none and ref.null (shared none). It also encourages implementations to have the same representation for shared and unshared i31 values, but I don't think that should be controversial.

[conrad-watt]

This would strongly encourage implementations to have the same representation for ref.null none and ref.null (shared none).

I don't think we want to assume this in general. In particular with our decision that globals of all shared types should be allowed, it's not impossible that implementations might want to experiment with (e.g.) a "fat" unboxed representation of nonshared funcref, but a boxed representation of shared funcref. It may be more ok to assume this specifically for refs under the any hierarchy, but my feeling is that it would be most conservative (and permissive for implementations) to have a separate ref.eq instruction for shared.

[tlively]

This problem is scoped to eq types, so it would only affect none, not nofunc. I agree that the most conservative thing would be to have a new ref.eq_shared instruction, but I also don't think we need to prematurely generalize here. I ran an example program and observed that V8 currently treats shared and unshared nulls as equal, but I don't know how intentional that is.

@manoskouk or @jakobkummerow, are there any engine implementation issues we should consider here?

[conrad-watt]

I don't think introducing ref.eq_shared would be premature generalisation - the choice to unify the representations of shared eq and eq through ref.eq is a far more committal one from the point of view of engine implementations.

Having a separate instruction initially is less committal, because if we really decided in the future that engines would never use this flexibility, we could interpret both opcodes as different encodings for the same polymorphic ref.eq instruction - and potentially further smooth things over in future if instruction renumbering hasn't happened yet. We can't go in the opposite direction so easily if we prematurely unify the representations of shared eq and eq.

[rossberg]

To preserve our principle types properties, we either have to create a new version of ref.eq for use with shared references or we have to let the existing ref.eq validate with any combination of shared and unshared operands.

That shouldn't be necessary. I think the principal type is expressible just fine with a type variable ranging over 𝑠ℎ𝑎𝑟𝑒 (a.k.a., shared?), analogous to null:

𝑠ℎ𝑎𝑟𝑒𝑎𝑏𝑠ℎ𝑒𝑎𝑝𝑡𝑦𝑝𝑒 ::= 𝑠ℎ𝑎𝑟𝑒 𝑎𝑏𝑠ℎ𝑒𝑎𝑝𝑡𝑦𝑝𝑒 𝑠ℎ𝑎𝑟𝑒 ::= shared | unshared | α

Then the principal type of ref.eq is:

(ref 𝑛𝑢𝑙𝑙₁ (𝑠ℎ𝑎𝑟𝑒 eq)) (ref 𝑛𝑢𝑙𝑙₂ (𝑠ℎ𝑎𝑟𝑒 eq)) → i32

[conrad-watt]

FWIW I'd also be fine with @rossberg's solution, so long as we briefly think about whether this + any other instructions would cause issues when validating dead code (gut feeling - it's ok).

[jakobkummerow]

From an implementation perspective, it's a little early for definitive statements...

My gut feeling is that we'd probably prefer to have a single null sentinel: that's efficient whenever explicit null checks are required, and would make it difficult to implement an observable identity difference between shared and non-shared null. Then again, it's impossible to rule out that we (or another engine) might some day have some idea that requires splitting the null sentinels.

Ultimately, the implementation will be dictated by the needs of the spec. If we need shared-null and non-shared-null to be distinguishable at runtime (for ref.eq or any other feature), then we'll have no choice but to use distinct sentinels. If we need them to compare as equal in ref.eq, we'll have a very strong reason to use the same sentinel for both. If parts of the spec require the one and other parts require the other behavior, we'll complain :-)

So, if we can disallow shared/non-shared comparisons for now (and maybe forever) and thereby sidestep these pitfalls, that sounds great.

[tlively]

@rossberg, haven't we been very careful in the past to not allow type variables from one operand constrain type variables from another operand? If the share variables on both operands have to be the same, then we're setting up a nontrivial constraint that I had believed was not allowed. If they don't have to be the same, then we're allowing mixed-shareability comparisons.

[rossberg]

@tlively, problematic would be non-trivial constraints between different type variables. Multiple occurrences of the same variable are no problem. There already are cases where that is needed, e.g., with the nullability variable in the principal type of extern.convert_any (though that's occurring in operand and result).

[tlively]

Thanks, that makes sense. That seems like the best solution by far, then. I'll document in the overview that mixed-sharedness ref.eq is disallowed.