Library prosa.implementation.facts.ideal_uni.prio_aware

Ideal Uniprocessor Scheduler Properties

This file establishes facts about the reference model of a priority- and preemption-model-aware ideal uniprocessor scheduler.
Consider any type of jobs with costs and arrival times, ...
  Context {Job : JobType} {JC : JobCost Job} {JA : JobArrival Job}.

... in the context of an ideal uniprocessor model.
Suppose we are given a consistent arrival sequence of such jobs, ...
... a non-clairvoyant readiness model, ...
... a preemption model, ...
  Context `{JobPreemptable Job}.

... and reflexive, total, and transitive JLDP priority policy.
  Context `{JLDP : JLDP_policy Job}.
  Hypothesis H_reflexive_priorities: reflexive_priorities.
  Hypothesis H_total: total_priorities.
  Hypothesis H_transitive: transitive_priorities.

Consider the schedule generated by the preemption-policy- and priority-aware ideal uniprocessor scheduler...
...and assume that the preemption model is consistent with the readiness model.
First, we note that the priority-aware job selection policy obviously maintains work-conservation.
  Corollary uni_schedule_work_conserving:
    work_conserving arr_seq schedule.
  Proof.
    apply np_schedule_work_conserving ⇒ //.
    movet jobs.
    rewrite /choose_highest_prio_job; split.
    - by apply supremum_none.
    - by move⇒ →.
  Qed.

Second, we similarly note that schedule validity is also maintained.
  Corollary uni_schedule_valid:
    valid_schedule schedule arr_seq.
  Proof.
    apply np_schedule_valid ⇒ //.
    movet jobs j.
    by apply supremum_in.
  Qed.

Third, the schedule respects also the preemption model semantics.
  Section PreemptionCompliance.

Suppose that every job in arr_seq adheres to the basic validity requirement that jobs must start execution to become nonpreemptive.
    Hypothesis H_valid_preemption_function :
       j,
        arrives_in arr_seq j
        job_cannot_become_nonpreemptive_before_execution j.

Since uni_schedule arr_seq is an instance of np_uni_schedule, the compliance of schedule with the preemption model follows trivially from the compliance of np_uni_schedule.
    Corollary schedule_respects_preemption_model :
      schedule_respects_preemption_model arr_seq schedule.
    Proof.
      by apply np_respects_preemption_model.
    Qed.

  End PreemptionCompliance.

Now we proceed to the main property of the priority-aware scheduler: in the following section we establish that uni_schedule arr_seq is compliant with the given priority policy whenever jobs are preemptable.
  Section Priority.

For notational convenience, recall the definitions of the job-selection policy and a prefix of the schedule based on which the next decision is made.
To start, we observe that, at preemption times, the scheduled job is a supremum w.r.t. to the priority order and the set of backlogged jobs.
    Lemma scheduled_job_is_supremum:
       j t,
        scheduled_at schedule j t
        preemption_time schedule t
        supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j.
    Proof.
      movej t SCHED PREEMPT.
      have NOT_NP: ~~ prev_job_nonpreemptive (prefix t) t.
      { apply contraL with (b := preemption_time (uni_schedule arr_seq) t) ⇒ //.
        now apply np_consistent. }
      move: SCHED.
      rewrite scheduled_at_def ⇒ /eqP.
      rewrite {1}/schedule/uni_schedule/pmc_uni_schedule/generic_schedule schedule_up_to_def /allocation_at -/(prefix t).
      rewrite ifF //.
      now apply negbTE.
    Qed.

From the preceding facts, we conclude that uni_schedule arr_seq respects the priority policy at preemption times.
    Theorem schedule_respects_policy :
      respects_JLDP_policy_at_preemption_point arr_seq schedule JLDP.
    Proof.
      movej1 j2 t ARRIVES PREEMPT BACK_j1 SCHED_j2.
      case: (boolP (scheduled_at (uni_schedule arr_seq) j1 t)) ⇒ [SCHED_j1|NOT_SCHED_j1].
      { have <-: j1 = j2 by apply (ideal_proc_model_is_a_uniprocessor_model j1 j2 (uni_schedule arr_seq) t).
        by apply H_reflexive_priorities. }
      { move: BACK_j1.
        have ->: backlogged (uni_schedule arr_seq) j1 t = backlogged (prefix t) j1 t.
        { apply backlogged_prefix_invariance' with (h := t) ⇒ //.
          rewrite /identical_prefix /uni_schedule /prefixt' LT.
          induction t ⇒ //.
          rewrite /pmc_uni_schedule/generic_schedule (schedule_up_to_prefix_inclusion _ _ t' t) //.
          rewrite /prefix scheduled_at_def.
          induction t ⇒ //.
          now rewrite schedule_up_to_empty. }
        moveBACK_j1.
        move: (scheduled_job_is_supremum j2 t SCHED_j2 PREEMPT) ⇒ SUPREMUM.
        apply supremum_spec with (s := jobs_backlogged_at arr_seq (prefix t) t) ⇒ //.
        now apply mem_backlogged_jobs. }
    Qed.

  End Priority.

End PrioAwareUniprocessorScheduler.