130 lines
4.7 KiB
Markdown
130 lines
4.7 KiB
Markdown
# Prometeu Virtual Machine (PVM)
|
|
|
|
Domain: VM subsystem overview
|
|
Function: normative
|
|
|
|
This chapter defines the VM as an execution subsystem inside the PROMETEU machine.
|
|
|
|
It is intentionally narrower than the broader machine specs:
|
|
|
|
- execution model;
|
|
- opcode families;
|
|
- verifier boundary;
|
|
- relationship between the VM and adjacent specs.
|
|
|
|
For the bytecode-level instruction contract, see [`../virtual-machine/ISA_CORE.md`](../vm-arch/ISA_CORE.md).
|
|
|
|
## 1 Scope
|
|
|
|
The PVM is a **deterministic, stack-based VM** designed for a fantasy console environment with fixed frame timing and explicit hardware-facing services.
|
|
|
|
This chapter does not fully restate:
|
|
|
|
- detailed value and calling semantics;
|
|
- heap/gate/GC internals;
|
|
- coroutine scheduling internals;
|
|
- host ABI policy.
|
|
|
|
Those now live in focused companion specs:
|
|
|
|
- [`02a-vm-values-and-calling-convention.md`](02a-vm-values-and-calling-convention.md)
|
|
- [`02b-vm-function-values-and-closures.md`](02b-vm-function-values-and-closures.md)
|
|
- [`03-memory-stack-heap-and-allocation.md`](03-memory-stack-heap-and-allocation.md)
|
|
- [`09a-coroutines-and-cooperative-scheduling.md`](09a-coroutines-and-cooperative-scheduling.md)
|
|
- [`16-host-abi-and-syscalls.md`](16-host-abi-and-syscalls.md)
|
|
- [`16a-syscall-policies.md`](16a-syscall-policies.md)
|
|
|
|
## 2 Core Design Principles
|
|
|
|
The PVM is designed around the following constraints:
|
|
|
|
1. **Deterministic execution**: no hidden threads or asynchronous callbacks.
|
|
2. **Frame-based timing**: execution is bounded by frame time and explicit safepoints.
|
|
3. **Safe memory model**: heap access is mediated by validated handles.
|
|
4. **Simple compilation target**: stack-based bytecode with verified control flow.
|
|
5. **Stable ABI**: calls and syscalls follow fixed slot-based contracts.
|
|
6. **First-class functions**: user function values are represented through closures.
|
|
|
|
## 3 Execution Model
|
|
|
|
The PVM executes bytecode inside the PROMETEU frame loop.
|
|
|
|
Each frame:
|
|
|
|
1. firmware enters the VM;
|
|
2. the VM runs until:
|
|
- the frame budget is consumed; or
|
|
- a `FRAME_SYNC` instruction is reached;
|
|
3. at `FRAME_SYNC`, the VM reaches the primary safepoint for GC and cooperative scheduling;
|
|
4. control returns to firmware/runtime orchestration.
|
|
|
|
`FRAME_SYNC` is the primary VM synchronization point. It is the boundary where the machine can safely account for:
|
|
|
|
- GC opportunity;
|
|
- coroutine handoff;
|
|
- frame-completion semantics;
|
|
- deterministic return to firmware.
|
|
|
|
## 4 Instruction Families
|
|
|
|
The public VM instruction surface is documented at the bytecode level in [`../virtual-machine/ISA_CORE.md`](../vm-arch/ISA_CORE.md). At the machine/spec level, the instruction families are:
|
|
|
|
- execution control:
|
|
- `NOP`, `HALT`, `JMP`, `JMP_IF_FALSE`, `JMP_IF_TRUE`, `TRAP`, `FRAME_SYNC`
|
|
- stack manipulation:
|
|
- `PUSH_CONST`, literal pushes, `POP`, `POP_N`, `DUP`, `SWAP`
|
|
- arithmetic and logic:
|
|
- numeric, comparison, boolean, and bitwise operations
|
|
- variable access:
|
|
- globals and locals
|
|
- function calls:
|
|
- `CALL`, `RET`
|
|
- function values:
|
|
- `MAKE_CLOSURE`, `CALL_CLOSURE`
|
|
- cooperative concurrency:
|
|
- `SPAWN`, `YIELD`, `SLEEP`
|
|
- VM/host boundary:
|
|
- `HOSTCALL`, `SYSCALL`, `INTRINSIC`
|
|
|
|
The machine-level rule is simple:
|
|
|
|
- opcodes define explicit behavior;
|
|
- there are no hidden execution paths;
|
|
- timing-sensitive behavior is exposed through frame and safepoint semantics.
|
|
|
|
## 5 Verifier Boundary
|
|
|
|
Before execution, bytecode must pass the verifier.
|
|
|
|
The verifier ensures, at minimum:
|
|
|
|
1. valid instruction decoding;
|
|
2. valid jump targets;
|
|
3. consistent stack depth across control-flow joins;
|
|
4. valid call/return shape;
|
|
5. closure call safety rules;
|
|
6. patched syscall and intrinsic validity.
|
|
|
|
The verifier is structural. It does not replace runtime validation of dynamic values.
|
|
|
|
## 6 Relationship to Adjacent Specs
|
|
|
|
- [`02a-vm-values-and-calling-convention.md`](02a-vm-values-and-calling-convention.md) defines slot values, tuples, frames, and return-slot semantics.
|
|
- [`02b-vm-function-values-and-closures.md`](02b-vm-function-values-and-closures.md) defines closure representation and function-value behavior.
|
|
- [`03-memory-stack-heap-and-allocation.md`](03-memory-stack-heap-and-allocation.md) defines stack/heap, handles, object layout, and GC.
|
|
- [`09-events-and-concurrency.md`](09-events-and-concurrency.md) defines events, timers, and the frame boundary model.
|
|
- [`09a-coroutines-and-cooperative-scheduling.md`](09a-coroutines-and-cooperative-scheduling.md) defines coroutine lifecycle and scheduling.
|
|
- [`16-host-abi-and-syscalls.md`](16-host-abi-and-syscalls.md) defines the syscall ABI boundary.
|
|
|
|
## 7 Summary
|
|
|
|
The PVM is:
|
|
|
|
- stack-based;
|
|
- deterministic;
|
|
- frame-synchronized;
|
|
- verifier-gated;
|
|
- closure-capable;
|
|
- coroutine-capable;
|
|
- embedded inside the larger PROMETEU console model, not equal to it.
|