11.1. Kernel State🔗

structure

Jar.JAVM.Kernel.CodeCapData : Type
Jar.JAVM.Kernel.CodeCapData : Type

Compiled code data associated with a CODE cap.

Constructor

Jar.JAVM.Kernel.CodeCapData.mk

Fields

id : Nat

program : Jar.JAVM.ProgramBlob

jumpTable : Array Nat

structure

Jar.JAVM.Kernel.BackingStore : Type
Jar.JAVM.Kernel.BackingStore : Type

Backing store: flat byte array representing all physical pages.

Constructor

Jar.JAVM.Kernel.BackingStore.mk

Fields

data : ByteArray

totalPages : Nat

structure

Jar.JAVM.Kernel.KernelState : Type
Jar.JAVM.Kernel.KernelState : Type

Kernel state: VM pool + call stack + backing store + memory.

Constructor

Jar.JAVM.Kernel.KernelState.mk

Fields

vms : Array Jar.JAVM.Cap.VmInstance

callStack : Array Jar.JAVM.Cap.CallFrame

codeCaps : Array CodeCapData

activeVm : Nat

untyped : Jar.JAVM.Cap.UntypedCap

backing : BackingStore

memory : Jar.JAVM.Memory

Flat PVM memory shared by all VMs (simplified model).

pvmRun : PvmRunFn

PVM execution function (gas model dependent).

memCycles : Nat

The kernel maintains a pool of VM instances, a call stack for CALL/REPLY routing, compiled CODE caps, a shared backing store for physical pages, and the UNTYPED bump allocator.

def

Jar.JAVM.Kernel.KernelState.chargeGas (s : KernelState) (amount : Nat) :
  Option KernelState
Jar.JAVM.Kernel.KernelState.chargeGas
  (s : KernelState) (amount : Nat) :
  Option KernelState

Deduct gas from active VM. Returns none if insufficient.

def

Jar.JAVM.Kernel.KernelState.activeGas (state : KernelState) : Nat
Jar.JAVM.Kernel.KernelState.activeGas
  (state : KernelState) : Nat

Get remaining gas from the active VM.