Precise semantics of memory.copy

[lars-t-hansen]

The overview currently says:

Copy data from a source memory region to destination region; these regions may overlap: the copy is performed as if the source region was first copied to a temporary buffer, then the temporary buffer is copied to the destination region.

There's also some agreement about effectively having to copy low->high, and thus to write data up to the bounds limit for the target, see #10, so assume that. This agreement seems to have been justified by the possible presence of an mprotect-like function that may make pages in the middle of a memory unavailable for reading and/or writing.

In unshared memory memory.copy is efficiently implementable without a buffer as follows, even in the presence of mprotect:

• if any source address is OOB or is unmapped then
  • trap
• if the tail of the target memory is OOB then
  • shrink the target memory down to the in-bounds range
  • set a flag that we must trap, the trap address is the first OOB address
• if any remaining target address is unmapped then
  • shrink the target memory down to the range that does not include the lowest unmapped address
  • set a flag that we must trap when we're done, the trap address will be the lowest unmapped address
• now copy src->target for the remaining target range, overlaps can be handled by copying high->low because that's not observable - there will be no faults
• if the trap flag was set then
  • trap

For shared memory it's different. As some other agent can protect/unprotect pages of both source and target while the copying is happening, the copy may in fact have to use a temp buffer for all copies that can't be proven not to straddle any page boundaries. (Suppose we don't, and just copy source->target, and a source page becomes unmapped and we must fault. Now the target is partially changed, contrary to semantics.) Clearly such a proof is possible at runtime, but even so. Large copies that span pages will be forced to allocate a temp buffer equal to the size of the copy, I think, as the implementation may write no target addresses until all source addresses have been read.

Yet it's desirable to avoid such a temp buffer. Though the requirement of a temp buffer won't affect the copy performance in unshared memories, it will put shared memory at a disadvantage, performance-wise.

Would it not be better to bow to reality here and say that if the copy is overlapping and src < dest, then copying is as-if high->low, and otherwise as-if low->high? This is no less implementation-invariant and it allows a straightforward optimization to be used by implementations, and implementations that were going to do something else anyway ought not be worse off. Implementations must still be a little careful around page boundaries but the buffer allocation is avoidable.

(I'll be happy to learn it if I've overlooked something here, and I expect none of us like to argue with reference to what an un(der)specified mprotect function does or does not do, but since we've already waded in with both feet on this one we might as well see where it leads.)

[conrad-watt]

The high->low/low->high switch on src < dest sounds completely reasonable to me. One immediate consequence, even for the sequential semantics, would be that if src < dest, and the tail of the target memory is OOB, a trap would occur without anything being written. So we would want to decide this now, because it's observable.

[binji]

Yes, I think I originally thought to write it this way and it was suggested that I write it more vague. Seems unlikely that this additional constraint will put any burden on implementers (famous last words).

[lars-t-hansen]

I'll produce a PR to update the language.

[lars-t-hansen]

PR merged.