Stateful connection of scheduler.rs::schedule to local thread policy. Host readiness/deadline processing remains explicit; choices cover scheduling alternatives.

structure Miri.Interpreter.SchedulingHooks (S C : Type) : Type

• manager : S → Concurrency.ThreadManager
• setManager : Concurrency.ThreadManager → S → S
• communicate : S → Bool
• processDelayedReadiness : C → S → StepResult S Unit
• pollNonBlocking : C → S → StepResult S Unit
• unblockExpiredDeadlines : C → S → StepResult S (Option Nat)
• anyThreadBlockedOnHost : S → Bool
• threadRank : C → List Concurrency.ThreadId → Nat

def Miri.Interpreter.Scheduling.localSchedule {S C : Type} (hooks : SchedulingHooks S C) (choice : C) (state : S) : StepResult S RunSchedulingAction

Source local scheduling, with environment effects run in source order. The communicate setting and thread manager are re-read after callbacks.

Equations

• One or more equations did not get rendered due to their size.