11.6. VM Creation (RETYPE + CREATE)🔗

RETYPE allocates physical pages from the UNTYPED bump allocator, producing an unmapped DATA cap.

def

Jar.JAVM.Kernel.handleRetype (state : KernelState) :
  KernelState × DispatchResult
Jar.JAVM.Kernel.handleRetype
  (state : KernelState) :
  KernelState × DispatchResult

CALL UNTYPED: φ[7]=n_pages, φ[12]=dst_slot (with indirection). Bumps untyped allocator, creates DATA cap at dst_slot.

CREATE instantiates a new VM from a CODE cap with a bitmask-selected subset of capabilities from the CODE cap's CNode.

def

Jar.JAVM.Kernel.handleCreate (state : KernelState)
  (codeCapId codeCnodeVm : Nat) : KernelState × DispatchResult
Jar.JAVM.Kernel.handleCreate
  (state : KernelState)
  (codeCapId codeCnodeVm : Nat) :
  KernelState × DispatchResult

CALL CODE: φ[7]=bitmask (u64), φ[12]=dst_slot for HANDLE. Bitmask copies caps from CODE's CNode. Creates new VM + HANDLE.