abstract-machine

name	abstract-machine
description	Implement abstract machines for defining and executing operational semantics of programming languages.
version	1.0.0
tags	["semantics","interpreters","popl","theory"]
difficulty	intermediate
languages	["haskell","ocaml","python"]
dependencies	["lambda-calculus-interpreter","operational-semantics-definer"]

Abstract Machine

Abstract machines define operational semantics by specifying computation as transitions between configurations. They bridge formal semantics and practical interpreters, enabling both reasoning about programs and efficient implementation.

When to Use This Skill

• Defining operational semantics for languages
• Building efficient interpreters
• Reasoning about program evaluation
• Implementing virtual machines
• Teaching programming language theory

What This Skill Does

1. Configuration Definition: Define machine state (code, environment, continuation)
2. Transition Rules: Specify how configurations evolve
3. Stack Management: Handle control flow with continuations
4. Environment Handling: Manage variable bindings
5. Termination Detection: Identify final states

Key Concepts

Concept	Description
Configuration	Complete machine state at a point
Control	Expression or value being processed
Environment	Variable bindings
Continuation	What to do next (stack)
Transition	Rule for moving between configurations

Tips

• Use de Bruijn indices to avoid variable capture
• CEK is good for call-by-value
• Krivine is elegant for call-by-name
• SECD was designed for functional languages
• Defunctionalize continuations for compilers

Common Use Cases

• Formalizing language semantics
• Building interpreters
• Proving type safety
• Implementing virtual machines
• Teaching PL concepts

Related Skills

• lambda-calculus-interpreter - Direct style interpretation
• operational-semantics-definer - Small-step/big-step semantics
• denotational-semantics-builder - Mathematical semantics
• cps-transformer - Continuation-passing style

Canonical References

Reference	Why It Matters
Felleisen & Friedman, "Control Operators, the SECD-Machine, and the λ-Calculus" (1986)	CEK machine
Landin, "The Mechanical Evaluation of Expressions" (1964)	SECD machine
Krivine, "A Call-by-Name Lambda-Calculus Machine" (published 2007, developed earlier)	Krivine machine

Tradeoffs and Limitations

Approach Tradeoffs

Approach	Pros	Cons
CEK	Simple, CBN/CBV variants	Explicit environments
SECD	Stack-based, familiar	More complex state
Krivine	Elegant for CBN	Not for CBV

When NOT to Use This Skill

• When denotational semantics is more appropriate
• For simple expression evaluation
• When efficiency is the only concern

Limitations

• May be less intuitive than big-step
• Need to handle errors explicitly
• Control flow can be spread across rules

Assessment Criteria

A high-quality implementation should have:

Criterion	What to Look For
Completeness	Handles all language constructs
Determinism	Each configuration has unique successor
Termination	Reaches final state for terminating programs
Correctness	Matches expected semantics

Quality Indicators

✅ Good: Complete transition rules, handles all cases, matches expected semantics ⚠️ Warning: Missing some constructs, stuck states ❌ Bad: Non-deterministic, doesn't terminate correctly

Research Tools & Artifacts

Real-world abstract machine implementations to study:

Artifact	Why It Matters
GHC's STG machine	Production call-by-need machine with sparks, blackholes, info tables
Lua 5.3 VM	Simple, efficient register-based VM with upvalues and coroutines
JavaScript V8 Ignition	Register-based bytecode interpreter with turbofan integration
OCaml bytecode interpreter	Direct-style VM with closures and effect handlers
JVM HotSpot interpreter	Stack-based with JIT compilation hints
WebAssembly reference interpreter	Formal specification machine

Key Implementations to Study

• PyPy interpreter (RPython): How meta-tracing works with the VM
• LuaJIT: Efficient closure representation and JIT compilation
• GHCi interpreter: Bytecode-based REPL for Haskell

Research Frontiers

Current active research in abstract machines:

Direction	Key Papers	Challenge
Effect handlers	"Handlers of Algebraic Effects" (Plotkin & Pretnar, 2009)	Encoding algebraic effects in CEK/Krivine
Delimited continuations	"Control Delimiters and their Hierarchies" (Felleisen, 1988)	Multiple prompts, composable snapshots
Multi-stage	"MetaOCaml" (2003)	Staging the machine itself
WebAssembly	"A Formal Specification" (2020)	Verification of the reference interpreter
Zero-cost exceptions	"Zero-cost Exception Handling" (2018)	Efficient error paths without overhead

Hot Topics

1. Compacting collectors for VM heaps: GCs designed for short-lived bytecode
2. Speculative optimization: Profile-guided specialization at runtime
3. Hardware-enforced isolation: CHERI capabilities in VM design

Implementation Pitfalls

Common bugs in production abstract machine implementations:

Pitfall	Real Example	Prevention
Stack overflow	Early OCaml bytecode had limited stack	Grow stacks dynamically, detect overflow
Space leaks	GHC's CAF retention issues	Analyze closure usage, prune unused
Wrong tail recursion	Early JavaScript engines	Verify tail call optimization (TCO)
Closure escape	Lua's upvalue capture bugs	Track closure lifetimes precisely
Wrong environment capture	Python's late binding closures	Capture by value vs reference
Improper frame pointers	Debug builds vs optimized	Preserve stack frame invariants

The "Space Leak" Story

GHC once had a famous space leak where CAFs (Constant Applicative Forms) retained heap:

-- This creates a CAF that retains xs
result = map expensiveFunction veryLargeList
-- Forces entire list despite laziness

Solution: Selective CAF elimination, scrutinize, and blackholes for synchronization.

Tail Call Optimization Pitfalls

Wrong TCO can cause crashes:

• Must check accumulator patterns correctly
• Must handle mutual recursion
• Must preserve tail position across branches
• Debugging: stack traces differ in tail-recursive code