416 lines
7.0 KiB
Markdown
416 lines
7.0 KiB
Markdown
# PR-6.5 — Verifier Support for Closures (Model B)
|
|
|
|
## Briefing
|
|
|
|
The verifier must understand closure values and enforce safe invocation rules.
|
|
|
|
Under Model B:
|
|
|
|
* `CALL_CLOSURE` injects hidden `arg0`.
|
|
* User-visible arg_count excludes hidden arg.
|
|
* Captures are accessed via explicit instructions (future PR).
|
|
|
|
---
|
|
|
|
## Target
|
|
|
|
Extend verifier to:
|
|
|
|
1. Introduce stack type: `ClosureValue`.
|
|
2. Validate MAKE_CLOSURE effects.
|
|
3. Validate CALL_CLOSURE semantics:
|
|
|
|
* Ensure top of stack is ClosureValue.
|
|
* Ensure sufficient args present.
|
|
* Validate `arg_count` matches function signature expectations.
|
|
* Account for hidden arg0 when checking callee arg arity.
|
|
4. Validate ret_slots against function metadata.
|
|
|
|
---
|
|
|
|
## Work Items
|
|
|
|
1. Extend type lattice with ClosureValue.
|
|
2. Define stack transitions for MAKE_CLOSURE.
|
|
3. Define stack transitions for CALL_CLOSURE.
|
|
4. Enforce strict failure on mismatch.
|
|
|
|
---
|
|
|
|
## Acceptance Checklist
|
|
|
|
* [ ] ClosureValue type exists.
|
|
* [ ] Invalid CALL_CLOSURE rejected.
|
|
* [ ] Hidden arg0 accounted for.
|
|
* [ ] ret_slots validated.
|
|
* [ ] All verifier tests pass.
|
|
|
|
---
|
|
|
|
## Tests
|
|
|
|
1. Valid closure call passes verification.
|
|
2. CALL_CLOSURE with wrong arg_count fails.
|
|
3. CALL_CLOSURE on non-closure fails verification.
|
|
4. Nested closure calls verify correctly.
|
|
|
|
---
|
|
|
|
## Junie Instructions
|
|
|
|
You MAY:
|
|
|
|
* Extend verifier model.
|
|
* Add tests.
|
|
|
|
You MUST NOT:
|
|
|
|
* Weaken verification rules.
|
|
* Replace verifier checks with runtime-only traps.
|
|
|
|
If function metadata (arg_slots/ret_slots) is insufficient, STOP and request clarification.
|
|
|
|
---
|
|
|
|
## Definition of Done
|
|
|
|
Verifier fully supports closure creation and invocation under Model B semantics.
|
|
|
|
---
|
|
|
|
# PR-7 — Coroutines (Cooperative, Deterministic, No Mailbox)
|
|
|
|
Coroutines are the **only concurrency model** in the Prometeu VM.
|
|
|
|
This phase introduces:
|
|
|
|
* Cooperative scheduling
|
|
* Deterministic execution order
|
|
* SPAWN / YIELD / SLEEP
|
|
* Switching only at safepoints (FRAME_SYNC)
|
|
* Full GC integration
|
|
|
|
No mailbox. No message passing. No preemption.
|
|
|
|
Each PR below is self-contained and must compile independently.
|
|
|
|
---
|
|
|
|
# PR-7.1 — Coroutine Heap Object
|
|
|
|
## Briefing
|
|
|
|
A coroutine is a suspended execution context with its own stack and call frames.
|
|
|
|
No mailbox is implemented in this phase.
|
|
|
|
## Target
|
|
|
|
Define `ObjectKind::Coroutine` with:
|
|
|
|
* `state: enum { Ready, Running, Sleeping, Finished, Faulted }`
|
|
* `wake_tick: u64`
|
|
* `stack: Vec<Value>`
|
|
* `frames: Vec<CallFrame>`
|
|
|
|
Rules:
|
|
|
|
* Allocated in GC heap.
|
|
* Addressed via `HeapRef`.
|
|
* Stack and frames stored inside the coroutine object.
|
|
|
|
## Checklist
|
|
|
|
* [ ] Coroutine heap object defined.
|
|
* [ ] Stack/frames encapsulated.
|
|
* [ ] No RC/HIP remnants.
|
|
* [ ] Compiles and tests pass.
|
|
|
|
## Tests
|
|
|
|
* Allocate coroutine object.
|
|
* Validate state transitions manually.
|
|
|
|
## Junie Rules
|
|
|
|
You MAY extend heap object kinds.
|
|
You MUST NOT implement scheduling yet.
|
|
If stack representation is unclear, STOP and ask.
|
|
|
|
---
|
|
|
|
# PR-7.2 — Deterministic Scheduler Core
|
|
|
|
## Briefing
|
|
|
|
Implement a cooperative deterministic scheduler.
|
|
|
|
## Target
|
|
|
|
Scheduler structure inside VM:
|
|
|
|
* `ready_queue: VecDeque<HeapRef>`
|
|
* `sleeping: Vec<HeapRef>` (sorted or scanned by wake_tick)
|
|
* `current: Option<HeapRef>`
|
|
|
|
Policy:
|
|
|
|
* FIFO for ready coroutines.
|
|
* Sleeping coroutines move to ready when `wake_tick <= current_tick`.
|
|
|
|
No execution switching yet.
|
|
|
|
## Checklist
|
|
|
|
* [ ] Scheduler struct exists.
|
|
* [ ] Deterministic FIFO behavior.
|
|
* [ ] No randomness.
|
|
|
|
## Tests
|
|
|
|
* Enqueue 3 coroutines and ensure dequeue order stable.
|
|
|
|
## Junie Rules
|
|
|
|
You MAY add scheduler struct.
|
|
You MUST NOT implement SPAWN/YIELD/SLEEP yet.
|
|
|
|
---
|
|
|
|
# PR-7.3 — SPAWN Instruction
|
|
|
|
## Briefing
|
|
|
|
SPAWN creates a new coroutine and schedules it.
|
|
|
|
## Target
|
|
|
|
Introduce opcode:
|
|
|
|
`SPAWN fn_id, arg_count`
|
|
|
|
Semantics:
|
|
|
|
* Pop `arg_count` args.
|
|
* Create new coroutine object.
|
|
* Initialize its stack/frame with entry fn.
|
|
* Push coroutine handle onto ready queue.
|
|
|
|
Current coroutine continues execution.
|
|
|
|
## Checklist
|
|
|
|
* [ ] SPAWN opcode exists.
|
|
* [ ] Coroutine created.
|
|
* [ ] Scheduled in ready queue.
|
|
* [ ] No immediate context switch.
|
|
|
|
## Tests
|
|
|
|
* Spawn coroutine and verify it appears in ready queue.
|
|
|
|
## Junie Rules
|
|
|
|
You MAY modify interpreter dispatch.
|
|
You MUST NOT switch execution immediately.
|
|
If entry frame layout unclear, STOP and ask.
|
|
|
|
---
|
|
|
|
# PR-7.4 — YIELD Instruction
|
|
|
|
## Briefing
|
|
|
|
YIELD voluntarily gives up execution.
|
|
|
|
## Target
|
|
|
|
Opcode:
|
|
|
|
`YIELD`
|
|
|
|
Semantics:
|
|
|
|
* Current coroutine moves to end of ready queue.
|
|
* Scheduler selects next coroutine at safepoint.
|
|
|
|
Switching must occur only at FRAME_SYNC.
|
|
|
|
## Checklist
|
|
|
|
* [ ] YIELD opcode implemented.
|
|
* [ ] Current coroutine enqueued.
|
|
* [ ] No mid-instruction switching.
|
|
|
|
## Tests
|
|
|
|
* Two coroutines yielding alternate deterministically.
|
|
|
|
## Junie Rules
|
|
|
|
You MAY modify VM execution loop.
|
|
You MUST NOT allow switching outside safepoints.
|
|
|
|
---
|
|
|
|
# PR-7.5 — SLEEP Instruction
|
|
|
|
## Briefing
|
|
|
|
SLEEP suspends coroutine until a future tick.
|
|
|
|
## Target
|
|
|
|
Opcode:
|
|
|
|
`SLEEP duration_ticks`
|
|
|
|
Semantics:
|
|
|
|
* Remove coroutine from ready queue.
|
|
* Set wake_tick.
|
|
* Add to sleeping list.
|
|
|
|
At each FRAME_SYNC:
|
|
|
|
* Check sleeping coroutines.
|
|
* Move ready ones to ready_queue.
|
|
|
|
## Checklist
|
|
|
|
* [ ] SLEEP implemented.
|
|
* [ ] wake_tick respected.
|
|
* [ ] Deterministic wake behavior.
|
|
|
|
## Tests
|
|
|
|
* Sleep and verify delayed execution.
|
|
|
|
## Junie Rules
|
|
|
|
You MAY add tick tracking.
|
|
You MUST NOT rely on real wall clock time.
|
|
|
|
---
|
|
|
|
# PR-7.6 — Safepoint Integration
|
|
|
|
## Briefing
|
|
|
|
Execution switching must occur only at safepoints.
|
|
|
|
## Target
|
|
|
|
Switch coroutine only:
|
|
|
|
* After FRAME_SYNC
|
|
* After instruction completes
|
|
|
|
Never mid-instruction.
|
|
|
|
## Checklist
|
|
|
|
* [ ] Switch only at safepoints.
|
|
* [ ] No reentrancy.
|
|
|
|
## Tests
|
|
|
|
* Stress test switching under heavy loops.
|
|
|
|
## Junie Rules
|
|
|
|
You MUST enforce deterministic switching.
|
|
|
|
---
|
|
|
|
# PR-7.7 — GC Integration
|
|
|
|
## Briefing
|
|
|
|
Suspended coroutines must be GC roots.
|
|
|
|
## Target
|
|
|
|
GC mark phase must traverse:
|
|
|
|
* All coroutine stacks
|
|
* All coroutine frames
|
|
|
|
## Checklist
|
|
|
|
* [ ] GC visits all suspended coroutines.
|
|
* [ ] No leaked references.
|
|
|
|
## Tests
|
|
|
|
* Coroutine capturing heap object remains alive.
|
|
* Finished coroutine collected.
|
|
|
|
## Junie Rules
|
|
|
|
You MUST NOT change sweep policy.
|
|
|
|
---
|
|
|
|
# PR-7.8 — Verifier Rules
|
|
|
|
## Briefing
|
|
|
|
Verifier must enforce coroutine safety.
|
|
|
|
## Target
|
|
|
|
Rules:
|
|
|
|
* YIELD forbidden inside invalid contexts (define minimal safe rule).
|
|
* SPAWN argument validation.
|
|
* SLEEP argument type validation.
|
|
|
|
## Checklist
|
|
|
|
* [ ] Invalid YIELD rejected.
|
|
* [ ] SPAWN arg mismatch rejected.
|
|
|
|
## Tests
|
|
|
|
* Invalid bytecode rejected.
|
|
|
|
## Junie Rules
|
|
|
|
You MUST NOT weaken verifier.
|
|
|
|
---
|
|
|
|
# PR-7.9 — Determinism & Stress Tests
|
|
|
|
## Briefing
|
|
|
|
Validate deterministic behavior.
|
|
|
|
## Target
|
|
|
|
Tests must confirm:
|
|
|
|
* Same order across runs.
|
|
* Sleep/wake order stable.
|
|
* GC works with many coroutines.
|
|
|
|
## Checklist
|
|
|
|
* [ ] Deterministic order tests.
|
|
* [ ] Stress test 100+ coroutines.
|
|
|
|
## Junie Rules
|
|
|
|
Tests must not depend on wall clock or randomness.
|
|
|
|
---
|
|
|
|
## Final Definition of Done
|
|
|
|
* Cooperative coroutines implemented.
|
|
* Deterministic scheduling.
|
|
* No mailbox.
|
|
* GC and verifier fully integrated.
|
|
* All tests pass.
|