Miri scheduler.rs run_on_stack_empty, step_current_thread and one run_threads iteration. Empty MIR stack is not program termination: callbacks, TLS destructors and termination hooks still run. Environment effects and thread storage are required operations, not assumed successes.

inductive Miri.Interpreter.StackEmptyPoll : Type

• pending : StackEmptyPoll
• ready : StackEmptyPoll

def Miri.Interpreter.instReprStackEmptyPoll.repr : StackEmptyPoll → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprStackEmptyPoll : Repr StackEmptyPoll

Equations

• Miri.Interpreter.instReprStackEmptyPoll = { reprPrec := Miri.Interpreter.instReprStackEmptyPoll.repr }

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqStackEmptyPoll : DecidableEq StackEmptyPoll

Equations

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

inductive Miri.Interpreter.RunSchedulingAction : Type

• executeStep : RunSchedulingAction
• sleepAndWaitForIo (duration : Option Nat) : RunSchedulingAction

def Miri.Interpreter.instReprRunSchedulingAction.repr : RunSchedulingAction → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprRunSchedulingAction : Repr RunSchedulingAction

Equations

• Miri.Interpreter.instReprRunSchedulingAction = { reprPrec := Miri.Interpreter.instReprRunSchedulingAction.repr }

def Miri.Interpreter.instDecidableEqRunSchedulingAction.decEq (x✝ x✝¹ : RunSchedulingAction) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqRunSchedulingAction.decEq Miri.Interpreter.RunSchedulingAction.executeStep Miri.Interpreter.RunSchedulingAction.executeStep = isTrue ⋯
• Miri.Interpreter.instDecidableEqRunSchedulingAction.decEq Miri.Interpreter.RunSchedulingAction.executeStep (Miri.Interpreter.RunSchedulingAction.sleepAndWaitForIo duration) = isFalse ⋯
• Miri.Interpreter.instDecidableEqRunSchedulingAction.decEq (Miri.Interpreter.RunSchedulingAction.sleepAndWaitForIo duration) Miri.Interpreter.RunSchedulingAction.executeStep = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqRunSchedulingAction : DecidableEq RunSchedulingAction

Equations

• Miri.Interpreter.instDecidableEqRunSchedulingAction = Miri.Interpreter.instDecidableEqRunSchedulingAction.decEq

structure Miri.Interpreter.RunLoopHooks (S C Callback : Type) : Type

• coreStep : C → S → StepResult S Bool
• takeStackEmptyCallback : S → StepResult S Callback

  Reset the diagnostic origin and take the active thread's callback; recursive invocation must observe it as absent until restoration.

• invokeStackEmptyCallback : C → Callback → S → StepResult S StackEmptyPoll
• restoreStackEmptyCallback : Callback → S → StepResult S Unit

  Restore on the thread active after the callback, matching Miri's getter.

• terminateActiveThread : C → Bool → S → StepResult S Unit
• interrupted : S → Bool
• handleAbnormalTermination : S → S
• schedule : C → S → StepResult S RunSchedulingAction
• communicate : S → Bool
• pollAndUnblock : C → Option Nat → S → StepResult S Unit
• sleep : C → Nat → S → StepResult S Unit

def Miri.Interpreter.RunLoop.runOnStackEmpty {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (choice : C) (state : S) : StepResult S StackEmptyPoll

Equations

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

def Miri.Interpreter.RunLoop.stepCurrentThread {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (choice : C) (state : S) : StepResult S Unit

Equations

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

def Miri.Interpreter.RunLoop.iteration {S C Callback : Type} (hooks : RunLoopHooks S C Callback) (choice : C) (state : S) : StepResult S Unit

One outer-loop iteration; success means another iteration is required. A fuel-bound runner must report fuel exhaustion as unknown, never as a return.

Equations

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

def Miri.Interpreter.RunLoop.reportsUB : StepError → Bool

These observers classify results; they do not prove completeness of any supplied hooks or establish a Rust safety theorem.

Equations

• Miri.Interpreter.RunLoop.reportsUB (Miri.Interpreter.StepError.undefinedBehavior reason) = true
• Miri.Interpreter.RunLoop.reportsUB Miri.Interpreter.StepError.retagWriteToReadOnly = true
• Miri.Interpreter.RunLoop.reportsUB (Miri.Interpreter.StepError.termination info) = info.isUbReport
• Miri.Interpreter.RunLoop.reportsUB x✝ = false