Operational semantics of the loader

Preliminaries

The loader reads instructions from a virtual object file and appends them to an instruction stream. The central operation produces a single VM instruction \(i\) and may have a side effect on a literal pool. The semantic domains in play are as follows

Semantic domains
\(V\) VM values
đ’© Names of vScheme variables (note that \(đ’© \subset V\))
ℕ Natural numbers
ℐ instructions
đ’Ș Object code (a sequence of tokens)

Here are the metavariables used to notate elements of or functions on the various semantic domains, along with their types.

Metavariables
Metavariable Type Description
\(n\), \(k\) ℕ A natural number
\(v\) \(V\) A value
\(L\) ℕ → \(V\) The literal pool
\(N\) đ’© → ℕ Sl ot numbers of global variables
\(i\) ℐ An instruction
\(I\) ℐ list A sequence of instructions
\(O\) đ’Ș list A sequence of tokens

The literal pool is meant to be a partial function: it’s defined only on a subset of natural numbers.

Loading judgment and transitions

The loader takes a sequence of tokens, consumes a prefix of that sequence, and returns an instruction. As a side effect, it may modify the literal pool or the placement of global variables. To express this action in a judgment of operational semantics, I supply an initial literal pool \(L\) and a final literal pool \(L'\), and the same for placements of global variables \(N\) and \(N'\):

\(⟹O,L,N⟩→⟚i,O',L',N'⟩\)

The grammar for virtual object code shows three forms of instruction, and there is a set of transitions for each form.

What the operational semantics buys us

The grammar tells us if a sequence of tokens constitutes valid virtual object code, but to know what to do with a valid sequence of tokens, we need the operational semantics. This situation is just like the situation we have in CS 105: a grammar tells us about syntax, but to know what happen when we run the code, we need the operational semantics. The only difference here is that the abstract machine is running at load time, to load stuff into the VM state.

This particular operational semantics has a couple of points that I like:

How to use the operational semantics

I hope you won’t need this semantics, but if you have questions about how “load function” is supposed to work, the semantics may answer them. (The nregs may remain a bit mysterious.)