9.12. Gas Cost Model🔗

Per-basic-block gas metering simulates a pipelined processor with 4-wide decode, out-of-order execution, and 5 execution units (4 ALU, 4 LOAD, 4 STORE, 1 MUL, 1 DIV). Each instruction has a cycle latency, decode slot cost, and execution unit requirements.

structure

Jar.JAVM.ExecUnits : Type
Jar.JAVM.ExecUnits : Type

Execution unit requirements for an instruction.

Constructor

Jar.JAVM.ExecUnits.mk

Fields

alu : Nat

load : Nat

store : Nat

mul : Nat

div : Nat

structure

Jar.JAVM.InstrCost : Type
Jar.JAVM.InstrCost : Type

Result of instruction cost analysis.

Constructor

Jar.JAVM.InstrCost.mk

Fields

cycles : Nat

decodeSlots : Nat

execUnits : Jar.JAVM.ExecUnits

destRegs : Array Nat

srcRegs : Array Nat

isTerminator : Bool

isMoveReg : Bool

def

Jar.JAVM.branchCost (code bitmask : ByteArray) (targetPC : Nat) : Nat
Jar.JAVM.branchCost
  (code bitmask : ByteArray)
  (targetPC : Nat) : Nat

Branch cost 𝔟: 1 if target is unlikely(2) or trap(0), else 20.

def

Jar.JAVM.instructionCost (code bitmask : ByteArray) (pc : Nat)
  (memCycles : Nat := 25) : Jar.JAVM.InstrCost
Jar.JAVM.instructionCost
  (code bitmask : ByteArray) (pc : Nat)
  (memCycles : Nat := 25) :
  Jar.JAVM.InstrCost

Instruction cost lookup. Returns cost info based on opcode. Uses code/bitmask for branch target lookup.

9.12.1. Full Pipeline Gas Model🔗

The full pipeline gas model simulates an out-of-order processor with a reorder buffer (ROB), tracking instruction decode, dispatch, execution, and retirement. This is the reference model — it produces the same results as single-pass for the rv64em ISA but at higher computational cost.

structure

Jar.JAVM.RobEntry : Type
Jar.JAVM.RobEntry : Type

Reorder buffer entry.

Constructor

Jar.JAVM.RobEntry.mk

Fields

state : Jar.JAVM.RobState

cyclesLeft : Nat

deps : Array Nat

destRegs : Array Nat

execUnits : Jar.JAVM.ExecUnits

inductive type

Jar.JAVM.RobState : Type
Jar.JAVM.RobState : Type

ROB entry state.

Constructors

dec : Jar.JAVM.RobState

wait : Jar.JAVM.RobState

exe : Jar.JAVM.RobState

fin : Jar.JAVM.RobState

structure

Jar.JAVM.GasSimState : Type
Jar.JAVM.GasSimState : Type

Pipeline simulation state.

Constructor

Jar.JAVM.GasSimState.mk

Fields

ι : Option Nat

cycles : Nat

remainingDecodeSlots : Nat

remainingStartSlots : Nat

remainingExecUnits : Jar.JAVM.ExecUnits

rob : Array Jar.JAVM.RobEntry

def

Jar.JAVM.canDecode (s : Jar.JAVM.GasSimState) : Bool
Jar.JAVM.canDecode
  (s : Jar.JAVM.GasSimState) : Bool

Can we decode the next instruction?

def

Jar.JAVM.decodeInstr (code bitmask : ByteArray)
  (s : Jar.JAVM.GasSimState) : Jar.JAVM.GasSimState
Jar.JAVM.decodeInstr
  (code bitmask : ByteArray)
  (s : Jar.JAVM.GasSimState) :
  Jar.JAVM.GasSimState

Decode the next instruction and update state.

def

Jar.JAVM.canDispatch (s : Jar.JAVM.GasSimState) : Bool
Jar.JAVM.canDispatch
  (s : Jar.JAVM.GasSimState) : Bool

Can we dispatch an instruction?

def

Jar.JAVM.dispatch (s : Jar.JAVM.GasSimState) : Jar.JAVM.GasSimState
Jar.JAVM.dispatch
  (s : Jar.JAVM.GasSimState) :
  Jar.JAVM.GasSimState

Dispatch the oldest ready instruction.

def

Jar.JAVM.findReadyEntry (s : Jar.JAVM.GasSimState) : Option Nat
Jar.JAVM.findReadyEntry
  (s : Jar.JAVM.GasSimState) : Option Nat

Find index of oldest WAIT entry that is ready to dispatch.

def

Jar.JAVM.allDepsFinished (rob : Array Jar.JAVM.RobEntry)
  (entry : Jar.JAVM.RobEntry) : Bool
Jar.JAVM.allDepsFinished
  (rob : Array Jar.JAVM.RobEntry)
  (entry : Jar.JAVM.RobEntry) : Bool

Check if all dependencies of a ROB entry are finished.

def

Jar.JAVM.advanceCycle (s : Jar.JAVM.GasSimState) : Jar.JAVM.GasSimState
Jar.JAVM.advanceCycle
  (s : Jar.JAVM.GasSimState) :
  Jar.JAVM.GasSimState

Advance one cycle: increment counter, reset slots, tick EXE entries.

def

Jar.JAVM.robAllFinished (s : Jar.JAVM.GasSimState) : Bool
Jar.JAVM.robAllFinished
  (s : Jar.JAVM.GasSimState) : Bool

Check if ROB is all finished (or empty).

def

Jar.JAVM.gasCostForBlockFull (code bitmask : ByteArray)
  (startPC : Nat) : Nat
Jar.JAVM.gasCostForBlockFull
  (code bitmask : ByteArray)
  (startPC : Nat) : Nat

Compute gas cost for a basic block using full pipeline simulation. Returns max(cycles - 3, 1).

9.12.2. Single-Pass Gas Model🔗

In jar1, gas costs are computed by the single-pass model — an O(n) pipeline simulation that tracks per-register readiness cycles. This omits execution unit contention (subsumed by decode throughput for the rv64em ISA) and dispatch width limits, yielding equivalent results with significantly less computation.

structure

Jar.JAVM.GasSimStateSP : Type
Jar.JAVM.GasSimStateSP : Type

Single-pass simulation state.

Constructor

Jar.JAVM.GasSimStateSP.mk

Fields

ι : Option Nat

cycle : Nat

decodeUsed : Nat

regDone : Array Nat

maxDone : Nat

def

Jar.JAVM.gasCostForBlockSinglePass (code bitmask : ByteArray)
  (startPC : Nat) (memCycles : Nat := 25) : Nat
Jar.JAVM.gasCostForBlockSinglePass
  (code bitmask : ByteArray)
  (startPC : Nat)
  (memCycles : Nat := 25) : Nat

Compute gas cost for a basic block using the single-pass model. Returns max(maxDone - 3, 1).