Skip to main content

SWITCH_IN_CHARGE_FORMAT

Constant SWITCH_IN_CHARGE_FORMAT 

Source
pub const SWITCH_IN_CHARGE_FORMAT: u32 = 3;
Expand description

The format from which a schedule replay charges a scheduler turn for every replayed switch to a thread that then runs guest code (Scheduler::bump_global_time), as the run that wrote the record charged the yield turn the switch stands for. A run charges every such stretch when it follows no record, or follows one of this format. A replay of an older record charges as before: its writer cannot say whether its own run followed a schedule, and so left those stretches uncharged.

This restores the switch-in charge when guest events retire. A bare TraceReplay turn does not become previous_turn_tid: main’s ordinary turn rule continues to decide subsequent signal charges. This format alone does not claim equality of every record/replay clock observation.