Miri's local scheduling policy: preserve the fast path, ordered readiness/I/O/deadline effects, cyclic candidate order, fixed scheduling, and sleep/deadlock outcomes. Host effects remain explicit obligations.

inductive Miri.Concurrency.SchedulerEnvironmentAction : Type

Scheduler actions that require an interpreter or host callback before Miri can choose a local runnable thread.

• processDelayedReadiness : SchedulerEnvironmentAction
• pollHostIoNonBlocking : SchedulerEnvironmentAction
• unblockExpiredDeadlines : SchedulerEnvironmentAction

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqSchedulerEnvironmentAction : DecidableEq SchedulerEnvironmentAction

Equations

• Miri.Concurrency.instDecidableEqSchedulerEnvironmentAction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instReprSchedulerEnvironmentAction : Repr SchedulerEnvironmentAction

Equations

• Miri.Concurrency.instReprSchedulerEnvironmentAction = { reprPrec := Miri.Concurrency.instReprSchedulerEnvironmentAction.repr }

def Miri.Concurrency.instReprSchedulerEnvironmentAction.repr : SchedulerEnvironmentAction → Nat → Std.Format

Equations

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

inductive Miri.Concurrency.SchedulerPlan : Type

Result of the scheduler's first-stage dispatch.

• executeCurrent (manager : ThreadManager) : SchedulerPlan
• serviceEnvironment (manager : ThreadManager) (communicate : Bool) (actions : List SchedulerEnvironmentAction) : SchedulerPlan

def Miri.Concurrency.instReprSchedulerPlan.repr : SchedulerPlan → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprSchedulerPlan : Repr SchedulerPlan

Equations

• Miri.Concurrency.instReprSchedulerPlan = { reprPrec := Miri.Concurrency.instReprSchedulerPlan.repr }

inductive Miri.Concurrency.SchedulerError : Type

• thread (reason : ThreadError) : SchedulerError
• nondeterministicChoiceOutOfBounds (rank candidateCount : Nat) : SchedulerError

def Miri.Concurrency.instDecidableEqSchedulerError.decEq (x✝ x✝¹ : SchedulerError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Concurrency.instDecidableEqSchedulerError.decEq (Miri.Concurrency.SchedulerError.thread a) (Miri.Concurrency.SchedulerError.thread b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqSchedulerError : DecidableEq SchedulerError

Equations

• Miri.Concurrency.instDecidableEqSchedulerError = Miri.Concurrency.instDecidableEqSchedulerError.decEq

def Miri.Concurrency.instReprSchedulerError.repr : SchedulerError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprSchedulerError : Repr SchedulerError

Equations

• Miri.Concurrency.instReprSchedulerError = { reprPrec := Miri.Concurrency.instReprSchedulerError.repr }

inductive Miri.Concurrency.SchedulerAction : Type

Final action of a local scheduling decision.

• executeStep (manager : ThreadManager) (thread : ThreadId) (eligibleChoices : List ThreadId) : SchedulerAction
• sleepAndWaitForIo (manager : ThreadManager) (duration : Option Nat) : SchedulerAction
• globalDeadlock (manager : ThreadManager) : SchedulerAction
• allThreadsTerminatedInvariant (manager : ThreadManager) : SchedulerAction

@[instance_reducible]

instance Miri.Concurrency.instReprSchedulerAction : Repr SchedulerAction

Equations

• Miri.Concurrency.instReprSchedulerAction = { reprPrec := Miri.Concurrency.instReprSchedulerAction.repr }

def Miri.Concurrency.instReprSchedulerAction.repr : SchedulerAction → Nat → Std.Format

Equations

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

def Miri.Concurrency.Scheduler.terminationInfo : SchedulerAction → Option TerminationInfo

The local scheduler's terminal stop is Miri's diagnostic deadlock result, not a UB result. Local deadlocks detected by synchronization shims enter through TerminationInfo.localDeadlock directly.

Equations

• Miri.Concurrency.Scheduler.terminationInfo (Miri.Concurrency.SchedulerAction.globalDeadlock manager) = some Miri.Concurrency.TerminationInfo.globalDeadlock
• Miri.Concurrency.Scheduler.terminationInfo (Miri.Concurrency.SchedulerAction.executeStep manager thread eligibleChoices) = none
• Miri.Concurrency.Scheduler.terminationInfo (Miri.Concurrency.SchedulerAction.sleepAndWaitForIo manager duration) = none
• Miri.Concurrency.Scheduler.terminationInfo (Miri.Concurrency.SchedulerAction.allThreadsTerminatedInvariant manager) = none

def Miri.Concurrency.Scheduler.roundRobinOrder (manager : ThreadManager) : Except SchedulerError (List ThreadId)

Return Miri's exact cyclic thread visitation order: IDs after the current thread, then IDs through the current thread.

Equations

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

def Miri.Concurrency.Scheduler.eligibleThreads (manager : ThreadManager) : Except SchedulerError (List ThreadId)

Enabled IDs in the source iterator's cyclic order.

Equations

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

def Miri.Concurrency.Scheduler.plan (manager : ThreadManager) (communicate : Bool) : Except SchedulerError SchedulerPlan

Equations

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

def Miri.Concurrency.Scheduler.finishLocal (managerAfterEnvironment : ThreadManager) (potentialSleepTime : Option Nat) (anyThreadBlockedOnHost : Bool) (rank : Nat) : Except SchedulerError SchedulerAction

Finish the local scheduler policy after the listed environment callbacks have returned. rank is an explicit choice among all enabled source candidates when scheduling is nondeterministic; it is ignored under Miri's fixed-scheduling mode. The caller supplies deadline and host-I/O facts from the actual machine state.

Equations

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