gc icon indicating copy to clipboard operation
gc copied to clipboard

`ref.i31` is both an administrative instruction and an instruction

Open redianthus opened this issue 2 years ago • 10 comments

Since the renaming of i31.new to ref.i31, ref.i31 appears twice in the set of instructions (when including administrative instructions) with each having a different syntax (one made of an integer in the case of the administrative one).

Then, the reduction rule for ref.i31 is quite confusing:

(i32.const n) ref.i31 -> ref.i31 (n mod 2^31)

On the left side you have the ref.i31 syntax and on the other side the ref.i31 int syntax.

Is there any plan to change one of them again to try to clarifies things ?

redianthus avatar Nov 06 '23 15:11 redianthus

Yeah, this is analogous to ref.func, where we go from ref.func $x to ref.func 𝑎𝑑𝑑𝑟, essentially overloading the mnemonic. We should probably have a better naming scheme for administrative instructions that are reducts of regular ones.

rossberg avatar Nov 06 '23 18:11 rossberg

We should probably have a better naming scheme for administrative instructions that are reducts of regular ones.

Indeed, that would help in some cases. I'm writing a proof and I either have to explain that there are two instruction with the same name (which I'd like to avoid because it's disturbing the reader) or use another name (likely i31.new) otherwise it will be too much confusing for potential reviewers that are not familiar with the Wasm semantics.

redianthus avatar Nov 08 '23 13:11 redianthus

The only convention I could think of so far is to add a prime to the administrative versions, which we e.g. used in the OOPSLA'19 memory model paper. How about going with that for your paper as well?

rossberg avatar Nov 08 '23 14:11 rossberg

That could be a solution. I'm going to think about it and see if I can think of something else.

I believe it would be good to also harmonize the script format. For instance, here:

(assert_return (invoke "f") (ref.i31))

The ref.i31 should probably match what we have as the administrative instruction, what do you think ?

redianthus avatar Nov 08 '23 14:11 redianthus

Hm, yeah, but then all ref patterns should still follow a consistent naming scheme as well.

rossberg avatar Nov 08 '23 14:11 rossberg

Here are a few possibilities:

Name i31 instr i31 admin i31 result struct instr struct admin struct result func instr func admin func result
Current ref.i31 ref.i31 u31 ref.i31 struct.new ref.struct structaddr ref.struct ref.func ref.func funcaddr ref.func
Old i31.new ref.i31 u31 ref.i31 struct.new ref.struct structaddr ref.struct ref.func ref.func funcaddr ref.func
Prime ref.i31 ref.i31' u31 ref.i31' struct.new ref.struct' structaddr ref.struct' ref.func ref.func' funcaddr ref.func'
Ptr ref.i31 ptr.i31 u31 ptr.i31 struct.new ptr.struct structaddr ptr.struct ref.func ptr.func funcaddr ptr.func
New i31.new ref.i31 u31 ref.i31 struct.new ref.struct structaddr ref.struct func.new ref.func funcaddr ref.func
Ptr+Const ref.i31 i31.const u31 i31.const u31? struct.new ptr.struct structaddr ptr.struct ref.func ptr.func funcaddr ptr.func
New+Const i31.new i31.const u31 i31.const u31? struct.new ref.struct structaddr ref.struct func.new ref.func funcaddr ref.func

The one I like the most is probably the New one.

redianthus avatar Nov 08 '23 17:11 redianthus

Well, we should find a convention that works uniformly for more than just references. For example, we have invoke which is just call', threads have wait', and possibly others. And of course I dropped i31.new for a reason: to distinguish allocations from just referencing.

rossberg avatar Nov 10 '23 15:11 rossberg

I can't find the call' you're referring to, where is it defined ?

redianthus avatar Nov 10 '23 16:11 redianthus

It's currently called invoke (on main repo), but relates to call in exactly the same way as ref.func relates to ref.func with addr. Ideally, they should use the same convention.

rossberg avatar Nov 10 '23 16:11 rossberg

Ideally, they should use the same convention.

Ideally yes, but I'm not sure we can find a convention that is not confusing. To me, adding a prime is confusing because these are not variables but instruction literals. I believe it would make everything simpler if we were to find a proper name for each of them - of course, that may not always be easy.

If we want to distinguish allocating instructions, we could have i31.of_i32 instead of i31.new. For func.new, I don't have a good name right now, I'll try to think about it.

I knew the invoke one (I thought you were saying it was reducing to call' and I was getting worried that I missed something in my formalization). I believe this one is a perfectly fine name.

For wait', I don't know. I'm not familiar yet with the threads proposal semantics.

EDIT:

Quoting your answer in #478:

See my reply on the other issue. Also, ref.null is already standardised as part of Wasm 2.0 (as is ref.func, btw), so we cannot change it anymore.

OK, so we probably won't be able to fix the issue in the way I propose by having proper name for each instructions. Still, I believe we could fix those that are not yet fully part of a released standard such as i31.ref being renamed to i31.of_i32 or whatever.

redianthus avatar Nov 10 '23 16:11 redianthus