JAR: Join-Accumulate Refine

11.8. Data Transfer🔗

CALL on a DATA cap copies pages between two DATA caps' backing store regions. This is the kernel's memcpy primitive for inter-VM data transfer.

🔗def
Jar.JAVM.Kernel.handleCallData (state : KernelState)
  (srcVm srcSlot : Nat) : KernelState × DispatchResult
Jar.JAVM.Kernel.handleCallData
  (state : KernelState)
  (srcVm srcSlot : Nat) :
  KernelState × DispatchResult

CALL(DATA) = memcpy between two DATA caps via backing store. φ[7]=src_offset, φ[8]=len, φ[9]=dst_offset, φ[12]=dst DATA cap ref.