COMP3161/COMP9164 Supplementary Lecture Notes
Abstract Machines
Gabriele Keller, Liam O’Connor, Johannes ̊ ∗ October 10, 2021
1 Abstract Machines
Abstract machines are a theoretical model of a calculator, typically consisting of a set of states, including initial and final states, and a set of machine operations, which manipulate the state of the machine. They are an important concept in theoretical computer science, for example to specify the operational semantics of a programming language (as we did we MinHs and TinyImp), or computational and complexity theory. Probably one of the best known examples of an abstract machine is the Turing machine, which was designed by in 1936 as a means to tackle the Entscheidungsproblem (Decision Problem).
Abstract Machines are closely related to Virtual Machines, which are basically Abstract Ma- chines with an implementation. Such virtual machines can be used to achieve portability of high- level programming languages (like the Java Virtual Machine, or the Common Language Framework for the .NET framework) or complete operating systems.
In this course, we use abstract machines as a means to study the operational semantics of programming languages. We started with two simple machines, which have a very small set of operations and states. We will gradually add more details to the machine and bring it closer to a machine we could actually use as a basis for an implementation. We do this in order to make languages easier to reason about – we use the higher level specification (for example, big step semantics) for reasoning about higher level properties such as safety, and use the lower level specification for reasoning about machine characteristics such as performance.
Technically, you have already seen two examples of abstract machines – in the structural oper- ational semantics of a language (the “small step” semantics), and in the evaluation (“big step”) semantics. While these technically constitute abstract machines, they are perhaps too abstract for our needs.
We seek to specify the evaluation of a language in a more “low-level” way. Should we start from the evaluation semantics, or the small-step semantics? Notice that the evaluation semantics do not even specify the order in which terms should be evaluated. Seeing as nondeterminism doesn’t exist in real computers, we must specify such an order. Hence we could say that the small-step semantics are “lower-level” than the big-step. Therefore, it makes sense for us to start with the small-step semantics. We call the small-step semantics of MinHS the M Machine.
2 The C Machine
One thing still left rather abstract in the M Machine is control flow, specifically, the notion of a runtime stack. When we want to evaluate a term, say Plus (Plus (Num 2) (Num 3)) (Num 4), the M Machine rules tell us that we must first evaluate the inner Plus (Num 2) (Num 3) and then return it to the original expression. This is akin to pushing the greater expression context onto a stack,
∗Just minor edits
evaluating the inner expression and then popping the context off the stack again, returning the evaluated expression to it.
We will introduce a new machine, the C Machine, that makes this stack explicit. In order to do this, we will need to formalise it, but we will get an informal intuition for it first.
2.1 C Machine States
In the M Machine, the state of the machine merely consists of the current expression to be evaluated – the notion of the stack is hidden in the deduction tree of the inference rules. In our C Machine, however, our state consists of three parts:
• The current expression to be evaluated
• A stack of expression frames
• A single binary flag that denotes whether the machine is currently evaluating an expression, or returning a value after evaluating.
To start with, we will introduce some new symbols to represent the stack. Formally:
s Stack x Frame ◦ Stack x ◃ s Stack
So, ◦ represents the empty stack, and x ◃ s is a stack with a frame x on the top. But what is a frame? We define a frame as an expression with a hole in it, denoted by . For example:
Plus (Num 3)
Is a Plus expression awaiting evaluation of its first argument. In this way, our frames are suspended
computations, which are awaiting further information in order to be evaluated. 2.1.1 A sketch of a C Machine
Now that we have the stack, we can have a shot at representing the machine states. Suppose we want to evaluate our earlier example with the C Machine:
Plus (Plus (Num 2) (Num 3)) Num 4
To begin, we need to come up with an initial state for our expression. So, when we start, we have the empty stack (◦), and the machine starts with the flag set to evaluate the expression (denoted by ≻).
◦ ≻ Plus (Plus (Num 2) (Num 3)) (Num 4)
The rules in the M Machine state that in order to evaluate a Plus expression, first the first subexpression should be evaluated, then the second. Hence, in this case, our C Machine will mirror the behaviour of the M Machine; that is, it should evaluate Plus (Num 2) (Num 3) first. To achieve this, a stack frame is pushed for Plus, with a in place of the first subexpression, and the machine is set to evaluate the expression we just replaced:
Plus (Num 4)◃◦ ≻ Plus (Num 2) (Num 3)
Now the machine has to evaluate another plus, so another stack frame is pushed:
Plus (Num 3)◃Plus (Num 4)◃◦ ≻ Num 2
Now the machine simply has to evaluate a numeric literal. Seeing as no further evaluation need take place (the value associated with the expression can be inferred without further work), the machine switches to return (denoted by ≺) the value back into the awaiting stack frame:
Plus (Num 3)◃Plus (Num 4)◃◦ ≺ 2 2
Having evaluated the first argument, the machine again suspends computation of the plus expres- sion in order to evaluate the second subexpression, which proceeds similarly:
Plus 2 ◃Plus (Num 4)◃◦ ≻ Num 3 Plus 2 ◃Plus (Num 4)◃◦ ≺ 3
As the machine is returning the last value necessary for the plus frame, it pops the frame off the stack, performs a primitive addition operation, and returns the result 5:
Plus Num4◃◦ ≺ 5 The rest of the evaluation proceeds predictably:
Plus5◃◦ ≻ Num4 Plus5◃◦ ≺ 4 ◦≺9
2.2 Formalising the C Machine
Now that we have an informal idea of what our C Machine looks like, we can begin to formalise
the machine. An abstract machine in general consists of: • A set of states Σ.
• A set of initial states I ⊆ Σ.
• AsetoffinalstatesF ⊆Σ.
• A state transition function, → : Σ → Σ.
You’ve seen these before—they’re also called small-step semantics.
We can specify formally each of these components. The set of states Σ is specified as follows:
s Stack e Expr s Stack v Value s≻e∈Σ s≺v∈Σ
That is, Σ is comprised of all evaluating states and all returning states.
The set of initial states I is defined as the set of all evaluating states with an empty stack:
e Expr ◦≻e∈I
The final states F are defined as all returning states with an empty stack: v Value
Now we must define the state transition relation for our C Machine, →c.
2.2.1 Literals
To begin, we will start on the easy part – Evaluating numeric and boolean literals:
s≻Numv→c s≺v s≻Boolv→c s≺v
So, the machine simply returns the corresponding values unchanged – no further computation is necessary. For function values, we must introduce some new notation, but the principle is the same as for numbers and booleans:
s ≻ Fun (f.x.···) →c s ≺ ⟨⟨f.x···⟩⟩ 3
2.2.2 Primitive Operations
Now we can specify more complicated rules, such as that for Plus. When faced with an unevaluated Plus expression, the machine first evaluates the first subexpression, and pushes the rest on the stack:
s≻Pluse1 e2 →c Plus e2◃s≻e1
Once that subexpression is evaluated, the machine will begin evaluating the second subexpression:
Plus e2◃s≺v→c Plusv◃s≻e2
Finally, when both subexpressions are evaluated, the machine returns the resultant sum, computed
via a primitive operation, +:
Plusv1 ◃s≺v2 →c s≺(v1+v2)
The definitions for Times, Greater, Equal, Not, And etc. are very similar, just making use of
different primitive machine operations.
2.2.3 Conditionals
Now, what about if? Recall that in the M Machine, the machine first evaluates the condition to some result, and, depending on the result, would evaluate just one branch of the conditional.
Similarly, when faced with an unevaluated If expression, the C Machine evalutes the condition first:
s≻Ifcte→c If te◃s≻c
If the result is True, the first branch is evaluated, otherwise the second:
If te◃s≺True→c s≻t If te◃s≺False→c s≻e 2.2.4 Function Application
Finally, we must deal with function application. Recall that in the M Machine, first the function expression was evaluated, then the argument to the function, then finally the body of the function, substituting in the value of the argument. We employ a similar strategy here.
First evaluate the function value:
s≻Applyf a→c Apply a◃s≻f Then, evaluate the argument:
Apply a◃s≺⟨⟨f.x.e⟩⟩→c Apply⟨⟨f.x.e⟩⟩◃s≻a
Then finally evaluate the function body, substituting the value for the argument, and the function
name in case the function is recursive:
Apply⟨⟨f.x.e⟩⟩◃s≺va →c s≻e[f:=(Funf.x.e),x=va]
2.3 Example
Here we have a simple function that determines if the provided argument is even, applied to the argument 3. To make things shorter, we rename the Num abstract syntax expression to simply N, Minus to Sub, and Apply to Ap.
→c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c →c
◦ Ap (N3)◃◦ Ap (N3)◃◦ Ap ⟨⟨···⟩⟩ ◃◦ Ap ⟨⟨···⟩⟩ ◃◦ ◦ If ···◃◦ (N0)◃If···◃◦ (N0)◃If···◃◦ LEq 3 ◃If ···◃◦ LEq 3 ◃If ···◃◦ If ··· (Ap ···)◃◦ ◦ Ap (Sub ···)◃◦ Ap (Sub ···)◃◦ Ap ⟨⟨···⟩⟩ ◃◦ (N2)◃Ap···◃◦ (N2)◃Ap···◃◦ Sub 3 ◃Ap ···◃◦ Sub 3 ◃Ap ···◃◦ Ap ⟨⟨···⟩⟩ ◃◦ ◦ If ···◃◦ (N0)◃If···◃◦ (N0)◃If···◃◦ LEq 1 ◃If ···◃◦ LEq 1 ◃If ···◃◦ If ··· (Ap ···)◃◦ ◦ Ap (Sub ···)◃◦ Ap (Sub ···)◃◦ Ap ⟨⟨···⟩⟩ ◃◦ (N2)◃Ap···◃◦ (N2)◃Ap···◃◦ Sub 1 ◃Ap ···◃◦ Sub 1 ◃Ap ···◃◦ Ap ⟨⟨···⟩⟩ ◃◦ ◦ If ···◃◦ (N0)◃If···◃◦ (N0)◃If···◃◦ LEq -1 ◃If ···◃◦ LEq -1 ◃If ···◃◦ If(Eq(N-1)(N0))···◃◦ ◦ Eq (N0)◃◦ Eq (N0)◃◦ Eq -1 ◃◦ Eq -1 ◃◦ ◦
≻ Ap(Funf.x.(If(LEqx(N0))(Eqx(N0))(Apf (Subx(N2)))))(N3) ≻ Funf.x.(If(LEqx(N0))(Eqx(N0))(Apf (Subx(N2))))
≺ ⟨⟨f.x.(If (LEq x (N 0)) (Eq x (N 0)) (Ap f (Sub x (N 2))))⟩⟩
≻ If(LEq(N3)(N0))(Eq(N3)(N0))(Ap(Fun ···)(Sub(N3)(N2))) ≻ LEq(N3)(N0)
≻ (Ap (Fun ···) (Sub (N 3) (N 2)))
≻ (Fun ···)
≺ ⟨⟨· · ·⟩⟩
≻ Sub(N3)(N2)
≻ If(LEq(N1)(N0))(Eq(N1)(N0))(Ap(Fun ···)(Sub(N1)(N2))) ≻ LEq(N1)(N0)
≻ (Ap (Fun ···) (Sub (N 1) (N 2)))
≻ (Fun ···)
≺ ⟨⟨· · ·⟩⟩
≻ Sub(N1)(N2)
≻ If (LEq (N -1) (N 0)) (Eq (N -1) (N 0)) (Ap (Fun ···) (Sub (N -1) (N 2))) ≻ LEq(N-1)(N0)
≻ Eq(N-1)(N0)
Wow, that long just to compute if three is even! No wonder we prefer evaluation semantics! Computers, however, certainly would prefer the C Machine – note that every state transition for the C Machine is an axiom. This means we can implement it as a single tight while loop that moves from state to state until it reaches a state in F .
Note: In an exam situation, you may be asked to present a derivation like the above. It is not necessary to write out every single step, just those steps you believe to be most important.
3 The E Machine
Now that we’ve made control flow more explicit, it becomes easier to see how we would implement the language efficiently on a real computer.
Let’s take a look at our primitive machine operations so far: • The Numeric Operators – +, * etc.
• Comparison Operators – ==, < etc.
• Logical Operators - &&, ||, !
• Substitution - e[x := y]
The great thing about most of these is that they are often native machine instructions in most computers, so they can be implemented very efficiently.
The one operation that cannot be implemented very efficiently is substitution. Substitution is of complexity O(n) in the size of the expression—it would be very difficult to implement it as an efficient machine instruction!
So, we are going to extend our machine once more, to include environments in the machine state. We will call our new machine the E Machine. This way, we make the machine look up variables in the environment rather than rely on substitution.
We extend our states as follows:
sStack ΓEnv eExpr sStack ΓEnv eExpr
s|Γ≻e∈Σ s|Γ≺e∈Σ
Note this is exactly the same as the C Machine, except with environments added. How do we
denote environments?
Γ Env x Ident v Value x = v; Γ Env
So, • is the empty environment, and we add new bindings to the environment with the notation x = v.
Now we need to add some rules for dealing with variables. In the C Machine, a variable occurring by itself was a stuck state - the only way for such a situation to arise is if the variable is free, which makes it an invalid expression. In the M Machine, variables are to be expected - if they occur in the environment:
s|x=v;Γ≻x→E s|x=v;Γ≺v
Now, what happens when we call a function? Naturally, we’d want to introduce new bindings to our environment, for the argument and the recursive name. When the function returns, however, we want to remove these bindings, as they are no longer in scope. The way we achieve this is somewhat unusual. We extend our stack to be able to include environments as well as frames:
s Stack x Frame s Stack Γ Env ◦ Stack x ◃ s Stack Γ ◃ s Stack
Then, when we apply a function, we add the bindings, and push the old environment to the stack: Apply⟨⟨f.x.e⟩⟩◃s|Γ≺v→E Γ◃s|x=v;f=⟨⟨f.x.e⟩⟩;Γ≻e
When the function returns, we restore the environment from the stack, which has the effect of removing the unwanted bindings:
Γ◃s|∆≺v→E s|Γ≺v 6
All other state transition rules are identical to the C Machine, preserving the environment across the transition.
The initial and final states are also unchanged, except that they now include the empty envi- ronment:
e Expr v Value ◦|•≻e∈I ◦|•≺v∈F
3.1 Closures
3.1.1 The Problem
Suppose we had a function that depended on variables that are free inside the function body, but in scope where the function is defined. A common example is partial application, or nested functions - like in the following (slightly abridged) example:
→E →E →E →E
◦|• App 4◃◦|• App 3◃App 4◃◦|•
App ⟨⟨f.x.(Fun g.y.x)⟩⟩ ◃App 4◃◦|• •◃App 4◃◦|x=3;f =⟨⟨···⟩⟩;• •◃App 4◃◦|x=3;f =⟨⟨···⟩⟩;•
App 4◃◦|• App⟨⟨g.y.x⟩⟩◃◦|•
•◃◦|y=4;g=⟨⟨g.y.x⟩⟩;•
≻ App (App (Fun f.x.(Fun g.y.x)) 3) 4 ≻ App (Fun f.x.(Fun g.y.x)) 3
≻ Fun f.x.(Fun g.y.x)
≻ Fun g.y.x ≺ ⟨⟨g.y.x⟩⟩ ≺ ⟨⟨g.y.x⟩⟩
The problem with these situations is now apparent - we can’t evaluate x here, as x is not in our environment! But, where the function g is defined, x is most certainly in scope. The problem here is that the function value for g escaped the scope in which it was defined.
3.1.2 The Solution
To fix this problem, we must revise our definition of a function value. Instead of essentially being an expression with some bound variables, we will instead make it a pair of the expression for the body of the function, and the environment in which it is defined, i.e:
s|Γ ≻ Fun (f.x.e) →E s|Γ ≺ ⟨⟨Γ,f.x.e⟩⟩
This pairing of a function body and an environment is called a closure.
When we apply a closure with an argument, it’s very similar to our rules before, except instead
of simply augmenting the current environment with the argument values and recursive name, we first set the current environment to be contents of the closure:
App⟨⟨∆,f.x.e⟩⟩◃s|Γ ≺ v →E Γ◃s|x=v;f=⟨⟨∆,f.x.e⟩⟩;∆ ≻ e
With this environment capture in place, we can now evaluate the example above successfully:
→E →E →E →E
→E →E →E →E
◦|• App 4◃◦|• App 3◃App 4◃◦|•
App ⟨⟨•,f.x.(Fun g.y.x)⟩⟩ ◃App 4◃◦|• •◃App 4◃◦|x=3;f =⟨⟨···⟩⟩;• •◃App 4◃◦|x=3;f =⟨⟨···⟩⟩;•
App 4◃◦|• App⟨⟨x=3;f;•g.y.x⟩⟩◃◦|•
•◃◦|y=4;g=⟨⟨···⟩⟩;x=3;f =⟨⟨···⟩⟩;• •◃◦|y=4;g=⟨⟨···⟩⟩;x=3;f =⟨⟨···⟩⟩;• ◦|•
≻ App (App (Fun f.x.(Fun g.y.x)) 3) 4 ≻ App (Fun f.x.(Fun g.y.x)) 3
≻ Fun f.x.(Fun g.y.x)
≻ Fun g.y.x
≺ ⟨⟨x=3;f;•,g.y.x⟩⟩ ≺ ⟨⟨x=3;f;•,g.y.x⟩⟩
≻ x ≺ 3 ≺ 3