# Library prosa.implementation.facts.ideal_uni.prio_aware

# Ideal Uniprocessor Scheduler Properties

Consider any type of jobs with costs and arrival times, ...

... in the context of an ideal uniprocessor model.

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.

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.

Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.

... a preemption model, ...

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

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.

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

Third, the schedule respects also the preemption model semantics.

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.

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

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.

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.

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.

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