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.
The following results assume ideal uniprocessor schedules.
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 that is consistent with the readiness model, ...
... 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.
First, we note that the priority-aware job selection policy obviously maintains work-conservation.
Second, we similarly note that schedule validity is also maintained.
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.

From the preceding facts, we conclude that uni_schedule arr_seq respects the priority policy at preemption times.