Intrepid/prometeu-studio
Intrepid/prometeu-studio
3
0
Fork 0
Code Pull Requests 1 Activity
prometeu-studio/docs/specs/random/pbs_old/Prometeu VM Memory model.md
bQUARKz aa1e0860d2
add spec docs
2026-03-24 13:42:16 +00:00

7.1 KiB
Raw Blame History

Prometeu VM Memory Model v0

Status: v0 (normative, implementer-facing)

Purpose: define the runtime memory model required to execute PBS programs with stable bytecode.

This specification describes the four memory regions and their interactions:

  1. Constant Pool (read-only)
  2. Stack (SAFE)
  3. Heap (HIP storage bytes/slots)
  4. Gate Pool (HIP handles, RC, metadata)

1. Design Goals

  1. Bytecode stability: instruction meanings and data formats must remain stable across versions.
  2. Deterministic behavior: no tracing GC; reclamation is defined by reference counts and safe points.
  3. Explicit costs: HIP allocation and aliasing are explicit via gates.
  4. PBS alignment: SAFE vs HIP semantics match PBS model.

2. Memory Regions Overview

2.1 Constant Pool (RO)

A program-wide immutable pool containing:

  • integers, floats, bounded ints
  • strings
  • (optional in future) constant composite literals

Properties:

  • read-only during execution
  • indexed by ConstId
  • VM bytecode uses PUSH_CONST(ConstId)

2.2 Stack (SAFE)

The stack contains:

  • local variables (by slot)
  • operand stack values for instruction evaluation

SAFE properties:

  • values are copied by value
  • no aliasing across variables unless the value is a gate handle
  • stack values are reclaimed automatically when frames unwind

2.3 Heap (HIP storage)

The heap is a contiguous array of machine slots (e.g., Value slots), used only as storage backing for HIP objects.

Heap properties:

  • heap cells are not directly addressable by bytecode
  • heap is accessed only via Gate Pool resolution

The heap may implement:

  • bump allocation (v0)
  • free list (optional)
  • compaction is not required in v0

2.4 Gate Pool (HIP handles)

The gate pool is the authoritative table mapping a small integer handle (GateId) to a storage object.

Gate Pool entry (conceptual):

GateEntry {
  alive: bool,
  base: HeapIndex,
  slots: u32,

  strong_rc: u32,
  weak_rc: u32,          // optional in v0; may be reserved

  type_id: TypeId,       // required for layout + debug
  flags: GateFlags,
}

Properties:

  • GateId is stable during the lifetime of an entry
  • GateId values may be reused only after an entry is fully reclaimed (v0 may choose to never reuse)
  • any invalid GateId access is a runtime trap (deterministic)

3. SAFE vs HIP

3.1 SAFE

SAFE is stack-only execution:

  • primitives
  • structs / arrays as value copies
  • temporaries

SAFE values are always reclaimed by frame unwinding.

3.2 HIP

HIP is heap-backed storage:

  • storage objects allocated with alloc
  • accessed through gates
  • aliasing occurs by copying a gate handle

HIP values are reclaimed by reference counting.

4. Value Representation

4.1 Stack Values

A VM Value type must minimally support:

  • Int(i64)
  • Float(f64)
  • Bounded(u32)
  • Bool(bool)
  • String(ConstId) or StringRef(ConstId) (strings live in const pool)
  • Gate(GateId) ← this is the only HIP pointer form in v0
  • Unit

Rule: any former Ref pointer type must be reinterpreted as GateId.

5. Allocation (alloc) and Gate Creation

5.1 Concept

PBS alloc creates:

  1. heap backing storage (N slots)
  2. a gate pool entry
  3. returns a gate handle onto the stack

5.2 Required inputs

Allocation must be shape-explicit:

  • TypeId describing the allocated storage type
  • slots describing the storage size

5.3 Runtime steps (normative)

On ALLOC(type_id, slots):

  1. allocate slots contiguous heap cells

  2. create gate entry:

    • base = heap_index
    • slots = slots
    • strong_rc = 1
    • type_id = type_id

  3. push Gate(gate_id) to stack

5.4 Example

PBS:

let v: Box<Vector> = box(Vector.ZERO);

Lowering conceptually:

  • compute value Vector.ZERO (SAFE)
  • ALLOC(TypeId(Vector), slots=2) → returns Gate(g0)
  • store the two fields into heap via STORE_GATE_FIELD

6. Gate Access (Read/Write)

6.1 Access Principle

Heap is never accessed directly. All reads/writes go through:

  1. gate validation
  2. gate → (base, slots)
  3. bounds check
  4. heap read/write

6.2 Read / Peek

peek copies from HIP storage to SAFE value.

  • no RC changes
  • no aliasing is created

6.3 Borrow (read-only view)

Borrow provides temporary read-only access.

  • runtime may enforce with a borrow stack (debug)
  • v0 may treat borrow as a checked read scope

6.4 Mutate (mutable view)

Mutate provides temporary mutable access.

  • v0 may treat mutate as:

    • read into scratch (SAFE)
    • write back on EndMutate

Or (preferred later):

  • direct heap writes within a guarded scope

7. Reference Counting (RC)

7.1 Strong RC

Strong RC counts how many live gate handles exist.

A GateId is considered live if it exists in:

  • a stack slot
  • a global slot
  • a heap storage cell (HIP) (future refinement)

7.2 RC operations

When copying a gate handle into a new location:

  • increment strong_rc

When a gate handle is removed/overwritten:

  • decrement strong_rc

Rule: RC updates are required for any VM instruction that:

  • assigns locals/globals
  • stores into heap cells
  • pops stack values

7.3 Release and Reclamation

When strong_rc reaches 0:

  • gate entry becomes eligible for reclamation
  • actual reclamation occurs at a safe point

Safe points (v0):

  • end of frame
  • explicit FRAME_SYNC (if present)

Reclamation:

  1. mark gate entry alive = false
  2. optionally add heap region to a free list
  3. gate id may be recycled (optional)

No tracing GC is performed.

8. Weak Gates (Reserved / Optional)

v0 may reserve the field weak_rc but does not require full weak semantics.

If implemented:

  • weak handles do not keep storage alive
  • upgrading weak → strong requires a runtime check

9. Runtime Traps (Deterministic)

The VM must trap deterministically on:

  • invalid GateId
  • accessing a dead gate
  • out-of-bounds offset
  • type mismatch in a typed store/load (if enforced)

Traps must include:

  • opcode
  • span (if debug info present)
  • message

10. Examples

10.1 Aliasing via gates

let a: Box<Vector> = box(Vector.ZERO);
let b: Box<Vector> = a; // copy handle, RC++

mutate b {
  it.x += 10;
}

let v: Vector = unbox(a); // observes mutation

Explanation:

  • a and b are GateId copies
  • mutation writes to the same heap storage
  • unbox(a) peeks/copies storage into SAFE value

10.2 No HIP for strings

let s: string = "hello";
  • string literal lives in constant pool
  • s is a SAFE value referencing ConstId

11. Conformance Checklist

A VM is conformant with this spec if:

  • it implements the four memory regions
  • GateId is the only HIP pointer form
  • ALLOC(type_id, slots) returns GateId
  • heap access is only via gate resolution
  • RC increments/decrements occur on gate copies/drops
  • reclamation happens only at safe points

Appendix A — Implementation Notes (Non-normative)

  • Start with bump-alloc heap + never-reuse GateIds (simplest v0)
  • Add free list later
  • Add borrow/mutate enforcement later as debug-only checks