trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> {
// Provided methods
fn run_timeout_callback(&mut self) -> InterpResult<'tcx> { ... }
fn run_on_stack_empty(&mut self) -> InterpResult<'tcx, Poll<()>> { ... }
fn schedule(&mut self) -> InterpResult<'tcx, SchedulingAction> { ... }
}
Provided Methods§
Sourcefn run_timeout_callback(&mut self) -> InterpResult<'tcx>
fn run_timeout_callback(&mut self) -> InterpResult<'tcx>
Execute a timeout callback on the callback’s thread.
fn run_on_stack_empty(&mut self) -> InterpResult<'tcx, Poll<()>>
Sourcefn schedule(&mut self) -> InterpResult<'tcx, SchedulingAction>
fn schedule(&mut self) -> InterpResult<'tcx, SchedulingAction>
Decide which action to take next and on which thread.
The currently implemented scheduling policy is the one that is commonly used in stateless model checkers such as Loom: run the active thread as long as we can and switch only when we have to (the active thread was blocked, terminated, or has explicitly asked to be preempted).
If GenMC mode is active, the scheduling is instead handled by GenMC.