Expand description
Dependency-aware parallel ready-queue scheduler (PSP-8 System 4).
The scheduler runs independent work in parallel and serializes only work that conflicts through dependencies, leases, or non-commuting durable effects. Two durable turns commute — and need no relative order — only when their semantic read and write footprints are disjoint:
writes(e) ∩ reads(e') = ∅ and writes(e') ∩ reads(e) = ∅.The conflict footprint includes durable platform state, not only workspace files: the capability table, risk budgets, fresh-identifier allocation, and the ledger root are modeled as read/write resources.
Structs§
- Execution
Lease - A held lease.
- Footprint
- The read/write footprint of a turn.
- Lease
Table - The lease table, tracking exclusive grants.
- Running
Task - A node currently executing, with the footprint it occupies.
- Scheduler
- The mutable parallel scheduler.
Enums§
- Lease
Kind - What a lease protects.
- Node
Outcome - A terminal classification for a node generation, ensuring recovery is total: every node ends accepted, certified-stopped, or escalated (PSP-8 System 4).
- Repair
Action - A repair outcome that becomes durable scheduler work (PSP-8 System 4).
- Resource
- A durable resource that turns read or write. Overlapping footprints force serialization (PSP-8 System 4 / Theorem 8).
- Scheduler
Effect - A durable scheduler command consumed by the ready-queue loop (PSP-8
SchedulerEffect).
Functions§
- recovery_
is_ total - Validate that a set of node outcomes covers every node exactly once with a terminal classification (recovery totality check).
- repair_
to_ effects - Convert a repair action into scheduler effects. A local repair that produces new executable work SHALL NOT escalate; it returns effects the ready-queue loop consumes (PSP-8 System 4).