# 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 valid arrival sequence of such jobs, ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence 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 JLDP.
Hypothesis H_total : total_priorities JLDP.
Hypothesis H_transitive : transitive_priorities JLDP.
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.
Proof.
apply np_schedule_work_conserving ⇒ //.
move⇒ t 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 ⇒ //.
move⇒ t 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.
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 arr_seq schedule t →
supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j.
Proof.
move⇒ j t SCHED PREEMPT.
have NOT_NP: ~~ prev_job_nonpreemptive (prefix t) t.
{ apply /(contraL _ PREEMPT)/np_consistent ⇒ // t' s j'.
exact: supremum_in. }
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 //.
by 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.
move⇒ j1 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 /prefix ⇒ t' LT.
elim: t PREEMPT SCHED_j2 NOT_SCHED_j1 LT ⇒ [//|t IHt] PREEMPT SCHED_j2 NOT_SCHED_j1 LT.
rewrite /pmc_uni_schedule/generic_schedule (schedule_up_to_prefix_inclusion _ _ t' t) //.
- rewrite /prefix scheduled_at_def.
induction t ⇒ //.
by rewrite schedule_up_to_empty. }
move⇒ BACK_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) ⇒ //.
exact: mem_backlogged_jobs. }
Qed.
End PrioAwareUniprocessorScheduler.