Scheduler Relation

Inductive Relation specifying the Midgard scheduler.

Two main operations:

• Advance: Operator, when on their turn, take control over the scheduler
• Rewind: Round completed, and we need to rewind the scheduler.

inductive Scheduler.Relation (p : MidgardParameters) (opsDir : OperatorDirectory.State.OperatorDirectory) (t : InfoActions State.Sch_Actions) (scheduler_in : State.SchedulerDatum) : State.SchedulerDatum → Prop

• Advance {p : MidgardParameters} {opsDir : OperatorDirectory.State.OperatorDirectory} {t : InfoActions State.Sch_Actions} {scheduler_in : State.SchedulerDatum} (tid : Tokens.Elem.TId) {lnk : MUList.State.Key} {scheduler_out : State.SchedulerDatum} : t.act = State.Sch_Actions.Advance tid → ShiftTransition p scheduler_in scheduler_out = true → OperatorsConcent scheduler_out p t.info = true → MUList.State.ListST.get_key tid opsDir.active = some scheduler_out.operator_id → MUList.State.ListST.get_link tid opsDir.active = some lnk → scheduler_in.operator_id ≤ lnk → Relation p opsDir t scheduler_in scheduler_out
• Rewind {p : MidgardParameters} {opsDir : OperatorDirectory.State.OperatorDirectory} {t : InfoActions State.Sch_Actions} {scheduler_in scheduler_out : State.SchedulerDatum} {last_activation uu : PosixTime} {lnk : OperatorId} (registered_operator last_active root_active : Tokens.Elem.TId) : t.act = State.Sch_Actions.Rewind registered_operator last_active root_active → ShiftTransition p scheduler_in scheduler_out = true → OperatorsConcent scheduler_out p t.info = true → MUList.State.ListST.is_last_node last_active opsDir.active = true → MUList.State.ListST.get_key last_active opsDir.active = some scheduler_out.operator_id → MUList.State.ListST.is_root_node root_active opsDir.active = true → MUList.State.ListST.get_link root_active opsDir.active = some lnk → scheduler_in.operator_id ≤ lnk → MUList.State.ListST.is_last_node registered_operator opsDir.registered = true → MUList.State.ListST.get_data registered_operator id opsDir.registered = some last_activation → t.info.validityInternal.upper = some uu → uu < last_activation → Relation p opsDir t scheduler_in scheduler_out

def Scheduler.Notation.«term_=>SCH⟨_,_;_⟩_» : Lean.TrailingParserDescr

Equations

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