10.4. VM Lifecycle🔗

VMs follow a strict state machine: IDLE (can be CALLed) -> RUNNING (executing) -> WAITING_FOR_REPLY (blocked at CALL) or HALTED (terminal) or FAULTED (can be RESUMEd). Only IDLE VMs can be CALLed — this prevents reentrancy by construction. Call graphs are acyclic at all times.

CALL suspends the caller (RUNNING -> WAITING_FOR_REPLY), transfers gas to the callee, and starts the callee (IDLE -> RUNNING). REPLY pops the call frame, returns unused gas, and resumes the caller (WAITING_FOR_REPLY -> RUNNING).

RESUME restarts a FAULTED VM (FAULTED -> RUNNING), transferring fresh gas. Registers and PC are preserved — the faulting instruction is retried. This enables demand paging: the parent maps the missing page via indirection, then RESUMEs the child.

inductive type

Jar.JAVM.Cap.VmState : Type
Jar.JAVM.Cap.VmState : Type

VM lifecycle states.

FAULTED is non-terminal: RESUME can restart a faulted VM, preserving registers and PC (retries the faulting instruction).

Constructors

idle : Jar.JAVM.Cap.VmState

running : Jar.JAVM.Cap.VmState

waitingForReply : Jar.JAVM.Cap.VmState

halted : Jar.JAVM.Cap.VmState

faulted : Jar.JAVM.Cap.VmState

structure

Jar.JAVM.Cap.VmInstance : Type
Jar.JAVM.Cap.VmInstance : Type

A single VM instance.

Constructor

Jar.JAVM.Cap.VmInstance.mk

Fields

state : Jar.JAVM.Cap.VmState

codeCapId : Nat

registers : Jar.JAVM.Registers

pc : Nat

capTable : Jar.JAVM.Cap.CapTable

caller : Option Nat

entryIndex : Nat

gas : Nat

structure

Jar.JAVM.Cap.CallFrame : Type
Jar.JAVM.Cap.CallFrame : Type

Call frame saved on the kernel's call stack.

Constructor

Jar.JAVM.Cap.CallFrame.mk

Fields

callerVmId : Nat

ipcCapIdx : Option Nat

ipcWasMapped : Option (Nat × Jar.JAVM.Cap.Access)