[spec review] 4 - Execution

[flagxor]

Detail oriented review of draft text:
http://webassembly.github.io/spec/core/bikeshed/index.html#execution%E2%91%A1

Try to be ready to discuss issues by the next in person WG meeting.

[eholk]

If no one's done this by the time I'm done with the Appendix, I'd be willing to take it.

[binji]

Feedback: https://gist.github.com/binji/57b6b4ff318c6dc77f6d2e1fa7b2bada

inline here:

4.2.12. Refers to the stack containing three kinds of entries "values", "labels", and "activations". Section 4.2.12.1 is called "Values", section 4.2.12.2 is called "Labels" but section 4.2.12.3 is called "Frames" instead.

4.2.12.3. The return arity is named but not labeled here. "Activation frames carry the return arity of the respective function". It should be the same as label above where n is mentioned explicitly.

4.2.13. "ultimately reducing the entire program to a single trap instruction", this isn't true when calling out to the embedder, right?

4.2.13. Note #3. The link for the label reduction rule is broken, it should go to 4.4.6.2. Also, the rule is different in the note.

4.2.13.2. What does "home" mean in "home module instance"?

4.2.13.1. Better explanation of "the hole". It's not clear (to me) what it represents and how it works.

4.2.13.3. What is the purpose of the second reduction rule? (Where a frame instruction on the stack is modified)

4.3. Mention the meta-variable "z"?

4.3. trunc is defined slightly different here than below in ftrunc_N: there q is explicitly annotated with a +.

4.3.1.3. Is this bigendian instead? It looks like it extracts the most significant bits and puts it first in the byte sequence.

4.3.2.14 - 4.3.2.17. All define the shift amount as j_2, but use k in the formula.

4.3.3.1. sp: "correspondence"

4.3.3.3 and others. it's a bit odd that the prose says nans_N{z_1, z_2} where the math says nans_N{} for the same thing.

4.3.3.4. Is there meant to be a difference between fadd and fsub here? fsub has fsub_N(\pm 0, \pm q_2) = \mp q_2 and fadd has the same thing but with z instead of q.

4.3.4.4. trunc is not defined for -0, does it need a special case?

4.3.4.6. Any "arithmetic" NaN of size N

4.4.1. It might be nice to have some examples of this mapping, e.g. add_i32(n1, n2) = iadd_32(n1, n2)

4.4.1.2. typo: unop_t1_t2

4.4.1.3. typo: binop_t1_t2

4.4.5.9. Mentioned in review for tailcall, I think -- B^k could be B^\ast here.

4.4.8. The evaluation here has a different syntax than elsewhere in this section. Is this deliberate?

4.5.3.2. typo: tableinst

4.5.3.6 (similar in 4.5.3.7). Phrasing here is ambiguous, "not empty and smaller" doesn't make it clear whether it is not(empty and smaller) or (not empty) and smaller

4.5.3.8. The (where table^* = module.tables) clause (and others) is a little confusing, since it doesn't seem to be used in the associated equation.

4.5.3.8. I don't understand the allocx definition, it seems to be a recursive definition... oh, I see, it's actually not.

4.5.3.8. What's up with whereforalli

4.5.4. Not sure if there's another way, but it is a bit unclear that val* matches val described below. It is used before definition, and also wrapped differently.

4.5.5. Discrepancy between prose and formal: formal mentions empty frame. Also, empty frame seems a little strange, maybe some explanation would help.

[binji]

@rossberg sorry, should have tagged you before!

[ericprud]

@binji, @rossberg, are these points addressed? Can this issue be closed?

[rossberg]

Hm, checking, I think I missed this. Will look into it.

[rossberg]

@binji, urgh, sorry, I somehow had missed this feedback. See #1022.

4.2.12. Refers to the stack containing three kinds of entries "values", "labels", and "activations". Section 4.2.12.1 is called "Values", section 4.2.12.2 is called "Labels" but section 4.2.12.3 is called "Frames" instead.

Renamed section title.

4.2.12.3. The return arity is named but not labeled here. "Activation frames carry the return arity of the respective function". It should be the same as label above where n is mentioned explicitly.

Added.

4.2.13. "ultimately reducing the entire program to a single trap instruction", this isn't true when calling out to the embedder, right?

It should be true even then. We axiomatically require that any such call itself reduces to either a sequence of values or a trap.

4.2.13. Note #3. The link for the label reduction rule is broken, it should go to 4.4.6.2. Also, the rule is different in the note.

Hm, this seems to be a Bikeshed issue. The link is correct in the other version of the document.

4.2.13.2. What does "home" mean in "home module instance"?

Changed to "the :ref:module instance <syntax-moduleinst> in which the computation runs, i.e., where the current function originates from."

4.2.13.1. Better explanation of "the hole". It's not clear (to me) what it represents and how it works.

Rephrased to " a hole :math:[\_] that marks the place where the next step of computation is taking place"

4.2.13.3. What is the purpose of the second reduction rule? (Where a frame instruction on the stack is modified)

This performs a reduction step inside a frame. Recursing into frames requires an explicit rule because frames are not expressible with evaluation contexts (because the recursion requires switching to frame F', and furthermore, the reduction can modify that frame).

4.3. Mention the meta-variable "z"?

That convention is already introduced in 2.2.3.1.

4.3. trunc is defined slightly different here than below in ftrunc_N: there q is explicitly annotated with a +.

Done.

4.3.1.3. Is this bigendian instead? It looks like it extracts the most significant bits and puts it first in the byte sequence.

bits() is the binary representation of the number, i.e., the list of bits in natural (big endian) order. This definition hence has to switch that order around in groups of 8.

4.3.2.14 - 4.3.2.17. All define the shift amount as j_2, but use k in the formula.

Cleaned up.

4.3.3.1. sp: "correspondence"

Fixed.

4.3.3.3 and others. it's a bit odd that the prose says nans_N{z_1, z_2} where the math says nans_N{} for the same thing.

Synchronised.

4.3.3.4. Is there meant to be a difference between fadd and fsub here? fsub has fsub_N(\pm 0, \pm q_2) = \mp q_2 and fadd has the same thing but with z instead of q.

The difference is that in the case of sub we have to toggle the sign.

4.3.4.4. trunc is not defined for -0, does it need a special case?

Hm, why is it not defined?

4.3.4.6. Any "arithmetic" NaN of size N

Refined.

4.4.1. It might be nice to have some examples of this mapping, e.g. add_i32(n1, n2) = iadd_32(n1, n2)

Added two examples.

4.4.1.2. typo: unop_t1_t2

4.4.1.3. typo: binop_t1_t2

These seem already fixed.

4.4.5.9. Mentioned in review for tailcall, I think -- B^k could be B^\ast here.

Ah, the B^n[] refers to the definition in 4.2.13.1, for which \ast is not defined.

4.4.8. The evaluation here has a different syntax than elsewhere in this section. Is this deliberate?

Changed.

4.5.3.2. typo: tableinst

Already fixed?

4.5.3.6 (similar in 4.5.3.7). Phrasing here is ambiguous, "not empty and smaller" doesn't make it clear whether it is not(empty and smaller) or (not empty) and smaller

Reworded to "is not empty and its value is smaller:

4.5.3.8. The (where table^* = module.tables) clause (and others) is a little confusing, since it doesn't seem to be used in the associated equation.

Hm, table* is used via (table.type)*.

4.5.3.8. I don't understand the allocx definition, it seems to be a recursive definition... oh, I see, it's actually not.

4.5.3.8. What's up with whereforalli

Bikeshed issue, fixed by now.

4.5.4. Not sure if there's another way, but it is a bit unclear that val* matches val described below. It is used before definition, and also wrapped differently.

Yeah, in the prose I need to spell out the (... val end)* iteration as an explicit loop.
It is used before definition because the definition is cyclic (F is required to compute val*), see the note below.

4.5.5. Discrepancy between prose and formal: formal mentions empty frame. Also, empty frame seems a little strange, maybe some explanation would help.

Yeah, technically, the formal notation always requires a current frame F, even though the external caller does not really have one in this case, so a dummy is used. In the prose I ignored this technicality. Added now for symmetry.

[binji]

4.3.1.3. Is this bigendian instead? It looks like it extracts the most significant bits and puts it first in the byte sequence.

bits() is the binary representation of the number, i.e., the list of bits in natural (big endian) order. This definition hence has to switch that order around in groups of 8.

I think this was fixed here: #968

The rest of them I agree with, seems to be just misunderstanding on my part.

[rossberg]

I think this was fixed here: #968

Ah, indeed.

[rossberg]

Closing.