finite-wasm icon indicating copy to clipboard operation
finite-wasm copied to clipboard

Specification of the aggregate instructions clash with the intended behaviour

Open nagisa opened this issue 1 year ago β€’ 2 comments

So today the spec for executing memory.fill and such says something along the lines of:

  1. Let 𝐹 be the current frame.
  2. Assert: due to validation, 𝐹.module.memaddrs[0] exists.
  3. Let ma be the memory address 𝐹.module.memaddrs[0].
  4. Assert: due to validation, 𝑆.mems[ma] exists.
  5. Let mem be the memory instance 𝑆.mems[ma].
  6. Assert: due to validation, a value of value type i32 is on the top of the stack.
  7. Pop the value i32.const 𝑛 from the stack.
  8. Assert: due to validation, a value of value type i32 is on the top of the stack.
  9. Pop the value val from the stack.
  10. Assert: due to validation, a value of value type i32 is on the top of the stack.
  11. Pop the value i32.const 𝑑 from the stack.
  12. If 𝑑 + 𝑛 is larger than the length of mem.data, then: a. Trap.
  13. If 𝑛 = 0, then: a. Return.
  14. Push the value i32.const 𝑑 to the stack.
  15. Push the value val to the stack.
  16. Execute the instruction i32.store8 {offset 0, align 0}.
  17. Assert: due to the earlier check against the memory size, 𝑑 + 1 < 2^32.
  18. Push the value i32.const (𝑑 + 1) to the stack.
  19. Push the value val to the stack.
  20. Push the value i32.const (𝑛 βˆ’ 1) to the stack.
  21. Execute the instruction memory.fill.

The problem is that this operation reduces to multiple other plain instructions such as i32.store8 and memory.fill. With how our specification is written, this will effectively cause memory.fill to charge at least 𝑛 times the fee(i32.store8) plus 𝑛 times the fee(memory.fill). In the implementation itself this will probably be a regular memset and therefore run at different speeds depending on the 𝑛.

The most straightforward option that came up as an idea is to, first, specify fee as pattern matching on sequence of instructions and their reductions rather than executed instruction. That is, for n=3 it would see something like

(i32.const 𝑑) val (i32.const 𝑛) memory.fill

and we would be able to β€œpattern” match this specific thing as a a memory.fill of size 𝑛 and return a corresponding fee (while all of the i32.store8s this reduces to internally would now be β€œfree” since calculating the fee for the whole aggregate does not recurse)

nagisa avatar Aug 08 '22 14:08 nagisa