Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.implementation.facts.ideal_uni.preemption_aware.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
(** * 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.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule
work_conserving arr_seq schedule
Proof .Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule
work_conserving arr_seq schedule
apply np_schedule_work_conserving => //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule
forall (t : instant) (s : seq Job),
choose_highest_prio_job t s = None <-> s = [::]
move => t jobs.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule t : instant jobs : seq Job
choose_highest_prio_job t jobs = None <-> jobs = [::]
rewrite /choose_highest_prio_job; split .Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule t : instant jobs : seq Job
supremum (hep_job_at t) jobs = None -> jobs = [::]
- Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule t : instant jobs : seq Job
supremum (hep_job_at t) jobs = None -> jobs = [::]
by apply supremum_none.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule t : instant jobs : seq Job
jobs = [::] -> supremum (hep_job_at t) jobs = None
- Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule t : instant jobs : seq Job
jobs = [::] -> supremum (hep_job_at t) jobs = None
by move => ->.
Qed .
(** Second, we similarly note that schedule validity is also maintained. *)
Corollary uni_schedule_valid :
valid_schedule schedule arr_seq.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule
valid_schedule schedule arr_seq
Proof .Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule
valid_schedule schedule arr_seq
apply np_schedule_valid => //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule
forall (t : instant) (s : seq Job) (j : Job),
choose_highest_prio_job t s = Some j -> j \in s
move => t jobs j.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule t : instant jobs : seq Job j : Job
choose_highest_prio_job t jobs = Some j -> j \in jobs
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 :
forall 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.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule H_valid_preemption_function : forall j : Job,
arrives_in arr_seq j ->
job_cannot_become_nonpreemptive_before_execution
j
schedule_respects_preemption_model arr_seq schedule
Proof .Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule H_valid_preemption_function : forall j : Job,
arrives_in arr_seq j ->
job_cannot_become_nonpreemptive_before_execution
j
schedule_respects_preemption_model arr_seq schedule
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. *)
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 :
forall 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.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState
forall (j : Job) (t : instant),
scheduled_at schedule j t ->
preemption_time schedule t ->
supremum (hep_job_at t)
(jobs_backlogged_at arr_seq (prefix t) t) = Some j
Proof .Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState
forall (j : Job) (t : instant),
scheduled_at schedule j t ->
preemption_time schedule t ->
supremum (hep_job_at t)
(jobs_backlogged_at arr_seq (prefix t) t) = Some j
move => j t SCHED PREEMPT.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j : Job t : instant SCHED : scheduled_at schedule j t PREEMPT : preemption_time schedule t
supremum (hep_job_at t)
(jobs_backlogged_at arr_seq (prefix t) t) = Some j
have NOT_NP: ~~ prev_job_nonpreemptive (prefix t) t.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j : Job t : instant SCHED : scheduled_at schedule j t PREEMPT : preemption_time schedule t
~~ prev_job_nonpreemptive (prefix t) t
{ Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j : Job t : instant SCHED : scheduled_at schedule j t PREEMPT : preemption_time schedule t
~~ prev_job_nonpreemptive (prefix t) t
apply contraL with (b := preemption_time (uni_schedule arr_seq) t) => //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j : Job t : instant SCHED : scheduled_at schedule j t PREEMPT : preemption_time schedule t
prev_job_nonpreemptive (prefix t) t ->
~~ preemption_time (uni_schedule arr_seq) t
now apply np_consistent. } Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j : Job t : instant SCHED : scheduled_at schedule j t PREEMPT : preemption_time schedule t NOT_NP : ~~ prev_job_nonpreemptive (prefix t) t
supremum (hep_job_at t)
(jobs_backlogged_at arr_seq (prefix t) t) = Some j
move : SCHED.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j : Job t : instant PREEMPT : preemption_time schedule t NOT_NP : ~~ prev_job_nonpreemptive (prefix t) t
scheduled_at schedule j t ->
supremum (hep_job_at t)
(jobs_backlogged_at arr_seq (prefix t) t) = Some j
rewrite scheduled_at_def => /eqP.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j : Job t : instant PREEMPT : preemption_time schedule t NOT_NP : ~~ prev_job_nonpreemptive (prefix t) t
schedule t = Some j ->
supremum (hep_job_at t)
(jobs_backlogged_at arr_seq (prefix t) t) = Some j
rewrite {1 }/schedule/uni_schedule/pmc_uni_schedule/generic_schedule schedule_up_to_def /allocation_at -/(prefix t).Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j : Job t : instant PREEMPT : preemption_time schedule t NOT_NP : ~~ prev_job_nonpreemptive (prefix t) t
(if prev_job_nonpreemptive (prefix t) t
then prefix t t.-1
else
choose_highest_prio_job t
(jobs_backlogged_at arr_seq (prefix t) t)) =
Some j ->
supremum (hep_job_at t)
(jobs_backlogged_at arr_seq (prefix t) t) = Some j
rewrite ifF //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j : Job t : instant PREEMPT : preemption_time schedule t NOT_NP : ~~ prev_job_nonpreemptive (prefix t) t
prev_job_nonpreemptive (prefix t) t = false
now 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.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState
respects_JLDP_policy_at_preemption_point arr_seq
schedule JLDP
Proof .Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState
respects_JLDP_policy_at_preemption_point arr_seq
schedule JLDP
move => j1 j2 t ARRIVES PREEMPT BACK_j1 SCHED_j2.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t BACK_j1 : backlogged schedule j1 t SCHED_j2 : scheduled_at schedule j2 t
hep_job_at t j2 j1
case : (boolP (scheduled_at (uni_schedule arr_seq) j1 t)) => [SCHED_j1|NOT_SCHED_j1].Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t BACK_j1 : backlogged schedule j1 t SCHED_j2 : scheduled_at schedule j2 t SCHED_j1 : scheduled_at (uni_schedule arr_seq) j1 t
hep_job_at t j2 j1
{ Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t BACK_j1 : backlogged schedule j1 t SCHED_j2 : scheduled_at schedule j2 t SCHED_j1 : scheduled_at (uni_schedule arr_seq) j1 t
hep_job_at t j2 j1
have <-: j1 = j2 by apply (ideal_proc_model_is_a_uniprocessor_model j1 j2 (uni_schedule arr_seq) t).Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t BACK_j1 : backlogged schedule j1 t SCHED_j2 : scheduled_at schedule j2 t SCHED_j1 : scheduled_at (uni_schedule arr_seq) j1 t
hep_job_at t j1 j1
by apply H_reflexive_priorities. } Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t BACK_j1 : backlogged schedule j1 t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t
hep_job_at t j2 j1
{ Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t BACK_j1 : backlogged schedule j1 t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t
hep_job_at t j2 j1
move : BACK_j1.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t
backlogged schedule j1 t -> hep_job_at t j2 j1
have ->: backlogged (uni_schedule arr_seq) j1 t = backlogged (prefix t) j1 t.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t
backlogged (uni_schedule arr_seq) j1 t =
backlogged (prefix t) j1 t
{ Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t
backlogged (uni_schedule arr_seq) j1 t =
backlogged (prefix t) j1 t
apply backlogged_prefix_invariance' with (h := t) => //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t
identical_prefix (uni_schedule arr_seq) (prefix t) t
rewrite /identical_prefix /uni_schedule /prefix => t' LT.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t t' : nat LT : t' < t
pmc_uni_schedule arr_seq choose_highest_prio_job t' =
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end t'
induction t => //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : nat ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t.+1 SCHED_j2 : scheduled_at schedule j2 t.+1 NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t.+1 t' : nat LT : t' < t.+1 IHt : preemption_time schedule t ->
scheduled_at schedule j2 t ->
~~ scheduled_at (uni_schedule arr_seq) j1 t ->
t' < t ->
pmc_uni_schedule arr_seq choose_highest_prio_job
t' =
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end t'
pmc_uni_schedule arr_seq choose_highest_prio_job t' =
schedule_up_to policy idle_state t t'
rewrite /pmc_uni_schedule/generic_schedule (schedule_up_to_prefix_inclusion _ _ t' t) //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t
~~ scheduled_at (prefix t) j1 t
rewrite /prefix scheduled_at_def.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end t != Some j1
induction t => //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : nat ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t.+1 SCHED_j2 : scheduled_at schedule j2 t.+1 NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t.+1 IHt : preemption_time schedule t ->
scheduled_at schedule j2 t ->
~~ scheduled_at (uni_schedule arr_seq) j1 t ->
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end t != Some j1
schedule_up_to policy idle_state t t.+1 != Some j1
now rewrite schedule_up_to_empty. } Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t
backlogged (prefix t) j1 t -> hep_job_at t j2 j1
move => BACK_j1.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t BACK_j1 : backlogged (prefix t) j1 t
hep_job_at t j2 j1
move : (scheduled_job_is_supremum j2 t SCHED_j2 PREEMPT) => SUPREMUM.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t BACK_j1 : backlogged (prefix t) j1 t SUPREMUM : supremum (hep_job_at t)
(jobs_backlogged_at arr_seq (prefix t) t) =
Some j2
hep_job_at t j2 j1
apply supremum_spec with (s := jobs_backlogged_at arr_seq (prefix t) t) => //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := ideal.processor_state Job : ProcessorState Job idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (ideal.processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job JLDP : JLDP_policy Job H_reflexive_priorities : reflexive_priorities H_total : total_priorities H_transitive : transitive_priorities schedule := uni_schedule arr_seq : schedule.schedule
(ideal.processor_state Job) H_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule policy := allocation_at arr_seq choose_highest_prio_job : schedule.schedule (ideal.processor_state Job) ->
instant -> option Job prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState j1, j2 : Job t : instant ARRIVES : arrives_in arr_seq j1 PREEMPT : preemption_time schedule t SCHED_j2 : scheduled_at schedule j2 t NOT_SCHED_j1 : ~~
scheduled_at
(uni_schedule arr_seq) j1 t BACK_j1 : backlogged (prefix t) j1 t SUPREMUM : supremum (hep_job_at t)
(jobs_backlogged_at arr_seq (prefix t) t) =
Some j2
j1 \in jobs_backlogged_at arr_seq (prefix t) t
now apply mem_backlogged_jobs. }
Qed .
End Priority .
End PrioAwareUniprocessorScheduler .