mem.init and mem.drop appear to break single-pass validation

[julian-seward1]

Per my understanding, the new insns mem.init and mem.drop have an immediate (literal) operand, which is an index indicating the data segment from which the initialising data is to be copied. I ran into a problem implementing validation for them, in that it's not possible to check that the literal value is in range at the time when validation passes over the code, because at that point the number of data segments isn't known -- the data segments appear in the binary format only after the code.

But I might misunderstand. Can someone please clarify?

[binji]

Yes, I see what you mean. Though you still can do it in one pass, you'd just have to remember the maximum data segment index and defer the validation error until you know how many data segments there are. I don't know of a good way around this, unfortunately.

[AndrewScheidecker]

The init/drop ops are also verified to only use passive segments, so deferring the validation requires keeping track of all expected passive segment indices.

IMO it's better to just make an out-of-range or active segment a runtime trap instead of a validation error.

[conrad-watt]

What was the original reason that init/drop cannot be used with active segments? Is there an expectation that implementations might want to optimise the representation of the module/instantiation process? Or just general silliness of dropping an active segment? I could imagine legitimate reasons for wanting init.

Our decision on this issue/PR (WebAssembly/threads#94) / (WebAssembly/spec#820) moves active segments towards being passive segments + an init-esque syntactic sugar for the start function. So maybe this could be revisited, and then a single index really would be sufficient for deferred validation.

[binji]

The original reason came from @lars-t-hansen in this comment which I've inlined here:

Just to reflect a conversation going on in #85: In my opinion, mem.init and mem.drop should only be usable with what's called "inactive" segments in that PR, ie, segments that are not copied into memory at instantiation time. If not, then mem.init will be sensitive to GC timing (an "active" segment referenced by mem.init might or might not have been removed by GC already because the module object was reaped) and instantiation will be sensitive to the timing of program execution, possibly in another thread (a concurrent mem.drop might have removed the segment). Either way we would need to spec failure semantics that we don't need if we simply say that "inactive" segments are for run-time use and "active" segments are for instantiation-time use. It should therefore be a verification failure for mem.init and mem.drop to reference segments that are not marked as "inactive".

[conrad-watt]

Thanks! Since this part of instantiation is now going to precisely share runtime semantics with mem.init, and therefore gets mem.init's failure semantics in the drop case for free, the spec point seems less forceful now.

One of the motivations I originally gave for the decision I linked above was that this alignment of instantiation and mem.init would reduce the overhead of spec'ing failure cases in a future-proof way (a hypothetical mem.protect in my original example).

I might not fully understand the point about GC though. From my perspective, even with purely passive data segments, if mem.drop is a hint to the GC to collect a segment, correctly handling a concurrent mem.init is a concern.

[AndrewScheidecker]

I might not fully understand the point about GC though. From my perspective, even with purely passive data segments, if mem.drop is a hint to the GC to collect a segment, correctly handling a concurrent mem.init is a concern.

I think the references to GC are superfluous. The goal is to be able to free the memory used by active segments after instantiation. If implementations are allowed to free that memory, then mem.init may fail for active segments. In the interest of avoiding non-determinism, it's reasonable to just prohibit mem.init for active segments.

The concurrent semantics of mem.drop and mem.init should also not depend on non-determinism in in when a GC actually frees the segment memory after a mem.drop. If a mem.drop x event occurs before the mem.init x event, the mem.init should trap.

Since the mem.init instruction can trap at runtime if the segment has already been dropped, I propose that the instruction is changed so the segment index immediate is promoted to an operand, and that all validation of the segment index is done at runtime: that the index is in range, that it identifies a passive segment, and that the segment has not yet been dropped. The same change would be made to the segment index immediates on mem.drop, table.init, and table.drop. That works around the streaming validation issue raised by this issue.

[rossberg]

I propose that the instruction is changed so the segment index immediate is promoted to an operand

Index spaces are static and all references to indices must be static. Otherwise we'd break the ability to renumber indices (a.k.a. alpha renaming) in code transformations. Consider e.g. tools like module mergers. (Mapping dynamic to static indices is what Wasm has tables for.)

To be clear, that is a separate question from making the validity check for the index static. But it would be a very odd disconnect from the rest of the language to not validate the use of a static index statically in this one case. I don't think that is sufficiently justified by minor implementation inconvenience.

[AndrewScheidecker]

I will concede your point about static indices.

But it would be a very odd disconnect from the rest of the language to not validate the use of a static index statically in this one case. I don't think that is sufficiently justified by minor implementation inconvenience.

It would stand out, but so does adding a validation dependency on a later section.

Another option would be to add a section that must occur before the code section to forward declare passive data segments.

I don't think that is sufficiently justified by minor implementation inconvenience.

My proposal isn't motivated by convenience. Implementing this stuff is far less effort than to try to effect change in the spec.

[conrad-watt]

I think the references to GC are superfluous. The goal is to be able to free the memory used by active segments after instantiation. If implementations are allowed to free that memory, then mem.init may fail for active segments. In the interest of avoiding non-determinism, it's reasonable to just prohibit mem.init for active segments.

The concurrent semantics of mem.drop and mem.init should also not depend on non-determinism in in when a GC actually frees the segment memory after a mem.drop. If a mem.drop x event occurs before the mem.init x event, the mem.init should trap.

If mem.init were to be allowed for active segments, then obviously any segment used this way couldn't be GC'd after instantiation, and would have to be explicitly dropped to enable GC. I don't think non-determinism is the concern.

However, this might make my interpretation of active segments a bad idea, because it might affect expectations existing code could have about GC behaviour of data segments. Since the target of mem.init is known statically though, maybe this isn't a major concern, as it shouldn't be that hard during compilation to detect that a data segment (active or passive) is never referenced.

EDIT: Ah, actually, JIT and so on maybe makes this more non-trivial. And doing it during validation means you have to keep track of indices anyway. Ok - I think my idea doesn't help this issue, unless it's not a big deal that active data segments wouldn't be GC'd as eagerly as they are now.

[rossberg]

@conrad-watt, I thought the idea for explaining active segments and their memory usage behaviour accurately would be that they correspond to a start function doing mem.init directly followed by mem.drop for each of them. Is there any problem with that?

[conrad-watt]

It corresponds to doing (equivalent to) mem.init on its own. No mem.drop, since a module may be instantiated multiple times. The point is that, currently, when a module falls out of scope, all active data segments can be GC'd, even if its instantiations are still in scope. This is still the case with the new semantics. My suggestion here was to also allow mem.init for active segments, which would invalidate this, since a module could fall out of scope while an instance of it (containing a mem.init) could still be in scope.

EDIT: After some discussion over email, I've realised this isn't correct, see below.

[rossberg]

I think there is some confusion in this (and perhaps previous) discussion regarding concurrency and dropping segments. To be precise, what's being dropped are the segment instances, which are internal to a single module instance (see @binji's spec draft). Since module instances cannot be shared across threads, neither can segment instances. So memory/table.drop do not have any concurrent behaviour.

GC is involved in so far that an implementation may choose (and is intended) to share the representation of a module's memory segments with their instances. In such an implementation, some concurrent synchronisation is necessary for memory.drop, in order to delete the segment with the last live reference. However, any concurrency on this level is an implementation detail and not observable in the language or its memory model.

Note that an implementation can only share memory segments. Table segments contain unsharable references that are generally fresh per instance.

So I see no issue with explaining active segments as passive ones with an implicit init+drop.

[conrad-watt]

A consequence of this would be that mem.init on an active segment could become a runtime trap (same as a passive segment that's dropped), as @AndrewScheidecker floated at one point. This would solve the individual index-tracking issue.

I was nurturing some pretty severe misconceptions about how segments are shared and GC'd between instances.

[binji]

Looping back to the original point on single-pass validation:

Another option would be to add a section that must occur before the code section to forward declare passive data segments.

It seems a bit heavyweight to add a new section for this, IMO.

As an alternative we could require that all passive segments are defined after all active segments. That way you could just remember the range of referenced segment indexes and make sure it is fully contained within the range of passive segment indexes that is defined later.