Documentation

FMMidgard.Scheduler.Properties

Scheduler Properties #

Here we focus on properties about the scheduler in isolation. In particular, we want to write propeties about who can and cannot take control of the scheduler.

We want to guarantee that active operators do not lose their right to operate.

The scheduler measures time, and thus, we can prove that time advances by shifts.

source
theorem Scheduler.Properties.ShiftStepShiftInterval (p : MidgardParameters) (opsDir : OperatorDirectory.State.OperatorDirectory) (i : InfoActions State.Sch_Actions) (sch_in sch_out : State.SchedulerDatum) (step : Relation p opsDir i sch_in sch_out) :
sch_out.shift_start = sch_in.shift_end p.shift_duration

After step, new scheduler shift starts when the previous one finishes.

source
theorem Scheduler.Properties.CurrentOperatorIsChoosenFromActive (p : MidgardParameters) (opsDir : OperatorDirectory.State.OperatorDirectory) {i : InfoActions State.Sch_Actions} {sch_in sch_out : State.SchedulerDatum} (Step : Relation p opsDir i sch_in sch_out) :
∃ (tkn_id : Tokens.Elem.TId), MUList.State.ListST.is_member sch_out.operator_id tkn_id opsDir.active = true

Current operators are chosen from the active queue.

source
theorem Scheduler.Properties.CurrentIsActive (p : MidgardParameters) (opsDir : OperatorDirectory.State.OperatorDirectory) (sch : State.SchedulerDatum) (HSch : Computational.SchedulerMachine.AfterInit { parameters := p, operatorsDir := opsDir } sch) :
∃ (tkn : Tokens.Elem.TId), MUList.State.ListST.is_member sch.operator_id tkn opsDir.active = true

The current scheduler operator was in the active queue upon activation.

Operators can retire while operating. However, there is no way of proving that here, operators directory operates outside of the scheduler scope. See PoC.Blaster, I tried make the model checker detect this case.

The property that the current operator operating is active is a property of the composition of the OperatorDirectory and Scheduler modules.

source
@[reducible, inline]
abbrev Scheduler.Properties.ActiveCondition (opsDir : OperatorDirectory.State.OperatorDirectory) (root : Tokens.Elem.TId) :
Prop
Equations
Instances For
    source
    def Scheduler.Properties.ShiftDuration (p : MidgardParameters) :
    Prop
    Equations
    Instances For
      source
      theorem Scheduler.Properties.NotEmpty (p : MidgardParameters) :
      (∃ (lower : ℕ) (upper : ℕ), lower < upper ∧ p.shift_duration ≤ lower ∧ upper < 2 * p.shift_duration) ↔ 1 < p.shift_duration
      source
      theorem Scheduler.Properties.ClaimSchedulerNotRewind (p : MidgardParameters) (opsDir : OperatorDirectory.State.OperatorDirectory) (sch : State.SchedulerDatum) (me : OperatorId) (tkn : Tokens.Elem.TId) (lnk : MUList.State.Key) (me_active : MUList.State.ListST.is_member me tkn opsDir.active = true) (me_not_last : MUList.State.ListST.get_link tkn opsDir.active = some lnk) (me_next : sch.operator_id ≤ lnk) (lower upper : PosixTime) (HSchTimeLower : sch.shift_start + p.shift_duration ≤ lower) (HSchTimeUpper : upper < sch.shift_start + 2 * p.shift_duration) :
      ∃ (a : State.Sch_Actions) (s' : State.SchedulerDatum), StateMachine.next p opsDir { act := a, info := have __src := InputInfo.empty; { validityInternal := { lower := some lower, upper := some upper }, value := __src.value, fee := __src.fee, validator := me, txId := __src.txId } } sch = ComputationResult.Success s' ∧ s'.operator_id = me

      Property: The next operator can claim the scheduler if times are alright.

      source
      theorem Scheduler.Properties.ClaimSchedulerRewind (p : MidgardParameters) (opsDir : OperatorDirectory.State.OperatorDirectory) {sch : State.SchedulerDatum} {me : OperatorId} {tkn : Tokens.Elem.TId} (me_active : MUList.State.ListST.is_member me tkn opsDir.active = true) (me_last : MUList.State.ListST.is_last_node tkn opsDir.active = true) {root_id : Tokens.Elem.TId} (root : MUList.State.ListST.is_root_node root_id opsDir.active = true) (me_next : MUList.State.ListST.is_anchor sch.operator_id root_id opsDir.active = true) {lower upper : PosixTime} (HSchTimeLower : sch.shift_start + p.shift_duration ≤ lower) (HSchTimeUpper : upper < sch.shift_start + 2 * p.shift_duration) {last_reg : Tokens.Elem.TId} (last_registered : MUList.State.ListST.is_last_node last_reg opsDir.registered = true) {last_act_time : PosixTime} (act_time : MUList.State.ListST.get_data last_reg id opsDir.registered = some last_act_time) (not_activable : upper < last_act_time) :
      ∃ (a : State.Sch_Actions) (s' : State.SchedulerDatum), StateMachine.next p opsDir { act := a, info := have __src := InputInfo.empty; { validityInternal := { lower := some lower, upper := some upper }, value := __src.value, fee := __src.fee, validator := me, txId := __src.txId } } sch = ComputationResult.Success s' ∧ s'.operator_id = me

      Claiming the scheduler after rewind.

      source
      def Scheduler.Properties.EligibleForAct (time : PosixTime) (last_tid : Tokens.Elem.TId) :
      Option OperatorId
      Equations
      Instances For
        source
        def Scheduler.Properties.OpsEligibleForAct (time : PosixTime) :
        List OperatorId
        Equations
        Instances For