[spec] Decoding 'align' param in text format is missing a log2 conversion step

[gasman]

Different sections of the WebAssembly spec are inconsistent about whether the 'align' parameter of load/store instructions equals the actual number of bytes to align to (i.e. 1, 2, 4, 8) or the base-2 exponent of that value (1, 2, 3, 4). Comparing against the observed behaviour of V8 and wast2wasm, and assuming these are implementing the spec as intended, the most likely interpretation seems to be:

• Within the abstract syntax, memarg.align refers to the exponent part (1, 2, 3, 4); this is backed up by the Validation section ("The alignment 2^(memarg.align) must not be larger than the width of t divided by 8").
• The binary format contains the exponent part encoded as u32: for example, an i64.load instruction with the default alignment hint of 8 bytes is encoded as 0x29 0x03 0x00, not 0x29 0x08 0x00. (This is consistent with the Binary Format section of the spec, which shows this value being transferred directly into memarg.align during decoding).
• In the text format, however, the align parameter (where specified) is given as the actual byte value: i64.load align=8, not i64.load align=3. As such, there's an implicit 'log2' conversion needed when setting memarg.align during decoding. The productions in the Text Format section don't include this detail, and just show the value being taken directly from the align= token, or from the N(=1/2/4/8) in memargN.

The most direct fix (albeit not a particularly pretty one) would be to change the outputs of the two alignN rules to log2(a) and log2(N), along with a note that a must be a power of 2.

(As an aside: the fact that this parameter exists in the spec but with no defined semantics seems like a bug to me. It implies that the people who put it there have "secret sauce" knowledge about how to use this parameter to achieve a performance optimisation, which isn't accessible to an independent developer attempting a clean-room implementation of a WebAssembly producer or consumer. Obviously, this is a Bad Thing for an open standard.)

[binji]

Yes, it looks like the text section needs a fix. I think it would be nicer to change the meaning of the memarg and align subscripts to mean the log2 value instead, then only the "align ="a:u32 rule should produce log_2(a). Either way, you're right that it should be mentioned that the alignment is required to be a power-of-two, as required by the spec tests.

Here is some information about the purpose for the alignment parameter. Agreed that it would be worthwhile to include a note about this in the spec document as well.

[rossberg]

@binji, I think what you suggest re the parsing rules is already the case, unless I'm missing something. A respective note also exists, but occurs after load's execution semantics.

See #562 for a fix for the missing log2 in the text format. I also moved the note to the beginning of the subsection to make it more visible.

[gasman]

Thanks @rossberg-chromium!

I think the subscripts do still need fixing up as @binji suggests - i.e. in the plaininstr rules, memarg_(1|2|4|8) need to become memarg_(0|1|2|3). Otherwise, following the production rules, the N in memarg_N and align_N still refers to 1/2/4/8 and so that's what ends up in the memarg.align value.

As a developer of a compiler targeting WebAssembly, who was previously unaware of the significance of aligned vs unaligned memory access, I don't think the existing note is sufficient: working purely off the information given in the spec, I would have completely disregarded alignment in my memory organisation and left the hints at their default values, resulting in the worst-case performance scenario (i.e. the code claims memory accesses are aligned, but actually they're not). The message "you don't need to worry about this, it's only an optimisation" is only true for WebAssembly consumers, and even there it's not ideal (the spec should provide enough information for the developer to decide whether or not to implement that optimisation).

Can I propose the following text (but please sanity-check, as I'm learning this on the fly...):

The alignment hint memarg.align is a non-binding assertion that the computed base address ea will always satisfy the property ea MOD 2^(memarg.align) == 0. Consumers of WebAssembly may apply optimisations for the case where this property holds, but must still produce correct results (potentially at a significant performance cost) in the case that it does not.

[rossberg]

@gasman, you are right, the log was in the wrong place. And I now understand what @binji meant :). I moved the log to the proper place and incorporated a variation of your suggested formulation (@binji, I did not apply your suggestion, since it seems nicer to have the "logification" isolated in one place.)

[binji]

@rossberg-chromium yeah, seems fine. I actually like it more since you using a = 2^n instead of log_2(a).

[rossberg]

Fixed by #562.