Library probsa.util.prosa.prio_aware

Require Export prosa.implementation.facts.ideal_uni.preemption_aware.

Ideal Uniprocessor Scheduler Properties

This file establishes facts about the reference model of a priority- and preemption-model-aware ideal uniprocessor scheduler.

The following results assume ideal uniprocessor schedules.

Require Import prosa.model.processor.ideal.

Section PrioAwareUniprocessorScheduler.

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.

Let PState := ideal.processor_state Job.
Let idle_state : PState := None.

Suppose we are given a consistent arrival sequence of such jobs, ...

Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.

... a non-clairvoyant readiness model, ...

Context {RM: JobReady Job (ideal.processor_state Job)}.
Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.

... a preemption model that is consistent with the readiness model, ...

Context `{JobPreemptable Job}.
Hypothesis H_valid_preemption_behavior: valid_nonpreemptive_readiness RM.

... and reflexive, total, and transitive JLDP priority policy.

  Context `{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.

Let schedule := uni_schedule arr_seq.

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.

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.

  Let policy := allocation_at arr_seq choose_highest_prio_job.
  Let prefix t := if t is t'.+1
                  then schedule_up_to policy idle_state t'
                  else empty_schedule idle_state.

  Lemma scheduled_job_is_supremum_new :
    ∀ j t,
      supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j →
      preemption_time schedule t →
      scheduled_at schedule j t.
  Proof.
    move⇒ j t SUP 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: SUP.
    rewrite scheduled_at_def ⇒ /eqP.
    rewrite {1}/schedule/uni_schedule/np_uni_schedule/generic_schedule schedule_up_to_def /allocation_at -/(prefix t).
    rewrite ifF //.
    now apply negbTE.
  Qed.

End PrioAwareUniprocessorScheduler.