Library prosa.implementation.facts.ideal_uni.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.

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, ...

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...

Let schedule := uni_schedule arr_seq.

...and assume that the preemption model is consistent with the readiness model.

Hypothesis H_valid_preemption_behavior:
valid_nonpreemptive_readiness RM schedule.

First, we note that the priority-aware job selection policy obviously maintains work-conservation.

Corollary uni_schedule_work_conserving:
work_conserving arr_seq schedule.

Second, we similarly note that schedule validity is also maintained.

Corollary uni_schedule_valid:
valid_schedule schedule arr_seq.

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.

  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.

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.

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.

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.
  End Priority.

End PrioAwareUniprocessorScheduler.