Library prosa.implementation.facts.ideal_uni.prio_aware
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.implementation.facts.ideal_uni.preemption_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 that is consistent with the readiness model, ...
Context `{JobPreemptable Job}.
Hypothesis H_valid_preemption_behavior:
valid_nonpreemptive_readiness RM.
Hypothesis H_valid_preemption_behavior:
valid_nonpreemptive_readiness RM.
... 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.
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.
Corollary uni_schedule_work_conserving:
work_conserving arr_seq schedule.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 363)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
============================
work_conserving arr_seq schedule
----------------------------------------------------------------------------- *)
Proof.
apply np_schedule_work_conserving ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 369)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
============================
forall (t : instant) (s : seq Job),
choose_highest_prio_job t s = None <-> s = [::]
----------------------------------------------------------------------------- *)
move⇒ t jobs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 460)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
t : instant
jobs : seq Job
============================
choose_highest_prio_job t jobs = None <-> jobs = [::]
----------------------------------------------------------------------------- *)
rewrite /choose_highest_prio_job; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 467)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
t : instant
jobs : seq Job
============================
supremum (hep_job_at t) jobs = None -> jobs = [::]
subgoal 2 (ID 468) is:
jobs = [::] -> supremum (hep_job_at t) jobs = None
----------------------------------------------------------------------------- *)
- by apply supremum_none.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 468)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
t : instant
jobs : seq Job
============================
jobs = [::] -> supremum (hep_job_at t) jobs = None
----------------------------------------------------------------------------- *)
- by move⇒ →.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
work_conserving arr_seq schedule.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 363)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
============================
work_conserving arr_seq schedule
----------------------------------------------------------------------------- *)
Proof.
apply np_schedule_work_conserving ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 369)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
============================
forall (t : instant) (s : seq Job),
choose_highest_prio_job t s = None <-> s = [::]
----------------------------------------------------------------------------- *)
move⇒ t jobs.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 460)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
t : instant
jobs : seq Job
============================
choose_highest_prio_job t jobs = None <-> jobs = [::]
----------------------------------------------------------------------------- *)
rewrite /choose_highest_prio_job; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 467)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
t : instant
jobs : seq Job
============================
supremum (hep_job_at t) jobs = None -> jobs = [::]
subgoal 2 (ID 468) is:
jobs = [::] -> supremum (hep_job_at t) jobs = None
----------------------------------------------------------------------------- *)
- by apply supremum_none.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 468)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
t : instant
jobs : seq Job
============================
jobs = [::] -> supremum (hep_job_at t) jobs = None
----------------------------------------------------------------------------- *)
- by move⇒ →.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Second, we similarly note that schedule validity is also maintained.
Corollary uni_schedule_valid:
valid_schedule schedule arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 371)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
============================
valid_schedule schedule arr_seq
----------------------------------------------------------------------------- *)
Proof.
apply np_schedule_valid ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
============================
forall (t : instant) (s : seq Job) (j : Job),
choose_highest_prio_job t s = Some j -> j \in s
----------------------------------------------------------------------------- *)
move⇒ t jobs j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 410)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
t : instant
jobs : seq Job
j : Job
============================
choose_highest_prio_job t jobs = Some j -> j \in jobs
----------------------------------------------------------------------------- *)
now apply supremum_in.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
valid_schedule schedule arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 371)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
============================
valid_schedule schedule arr_seq
----------------------------------------------------------------------------- *)
Proof.
apply np_schedule_valid ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
============================
forall (t : instant) (s : seq Job) (j : Job),
choose_highest_prio_job t s = Some j -> j \in s
----------------------------------------------------------------------------- *)
move⇒ t jobs j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 410)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
t : instant
jobs : seq Job
j : Job
============================
choose_highest_prio_job t jobs = Some j -> j \in jobs
----------------------------------------------------------------------------- *)
now apply supremum_in.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 405)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
move⇒ j t SCHED PREEMPT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 409)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 412)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
subgoal 2 (ID 414) is:
supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 412)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 423)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 414)
subgoal 1 (ID 414) is:
supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 414)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 453)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 493)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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/np_uni_schedule/generic_schedule schedule_up_to_def /allocation_at -/(prefix t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 526)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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 (predn t)
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 534)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 405)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
move⇒ j t SCHED PREEMPT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 409)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 412)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
subgoal 2 (ID 414) is:
supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 412)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 423)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 414)
subgoal 1 (ID 414) is:
supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 414)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 453)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 493)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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/np_uni_schedule/generic_schedule schedule_up_to_def /allocation_at -/(prefix t).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 526)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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 (predn t)
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 534)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
From the preceding facts, we conclude that [uni_schedule arr_seq]
respects the priority policy at preemption times.
Theorem schedule_respects_policy :
respects_policy_at_preemption_point arr_seq schedule.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 413)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState
============================
respects_policy_at_preemption_point arr_seq schedule
----------------------------------------------------------------------------- *)
Proof.
move⇒ j1 j2 t ARRIVES PREEMPT BACK_j1 SCHED_j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 421)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 483)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
subgoal 2 (ID 484) is:
hep_job_at t j2 j1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 483)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 501)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
----------------------------------------------------------------------------- *)
now apply H_reflexive_priorities.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 484)
subgoal 1 (ID 484) is:
hep_job_at t j2 j1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 484)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 484)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 503)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 524)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
subgoal 2 (ID 529) is:
backlogged (prefix t) j1 t -> hep_job_at t j2 j1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 524)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 537)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
subgoal 2 (ID 539) is:
~~ scheduled_at (prefix t) j1 t
----------------------------------------------------------------------------- *)
rewrite /identical_prefix /uni_schedule /prefix ⇒ t' LT.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 599)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
============================
np_uni_schedule arr_seq choose_highest_prio_job t' =
match t with
| 0 => empty_schedule idle_state
| succn t'0 => schedule_up_to policy idle_state t'0
end t'
subgoal 2 (ID 539) is:
~~ scheduled_at (prefix t) j1 t
----------------------------------------------------------------------------- *)
induction t ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 631)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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 (succn t)
SCHED_j2 : scheduled_at schedule j2 (succn t)
NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 (succn t)
t' : nat
LT : t' < succn t
IHt : preemption_time schedule t ->
scheduled_at schedule j2 t ->
~~ scheduled_at (uni_schedule arr_seq) j1 t ->
t' < t ->
np_uni_schedule arr_seq choose_highest_prio_job t' =
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end t'
============================
np_uni_schedule arr_seq choose_highest_prio_job t' =
schedule_up_to policy idle_state t t'
subgoal 2 (ID 539) is:
~~ scheduled_at (prefix t) j1 t
----------------------------------------------------------------------------- *)
rewrite /np_uni_schedule /generic_schedule (schedule_up_to_prefix_inclusion _ _ t' t) //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 539)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 710)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
| succn t' => schedule_up_to policy idle_state t'
end t != Some j1
----------------------------------------------------------------------------- *)
induction t ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 734)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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 (succn t)
SCHED_j2 : scheduled_at schedule j2 (succn t)
NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 (succn t)
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
| succn t' => schedule_up_to policy idle_state t'
end t != Some j1
============================
schedule_up_to policy idle_state t (succn t) != Some j1
----------------------------------------------------------------------------- *)
now rewrite schedule_up_to_empty.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 529)
subgoal 1 (ID 529) is:
backlogged (prefix t) j1 t -> hep_job_at t j2 j1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 529)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 767)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 769)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 781)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Priority.
End PrioAwareUniprocessorScheduler.
respects_policy_at_preemption_point arr_seq schedule.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 413)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState
============================
respects_policy_at_preemption_point arr_seq schedule
----------------------------------------------------------------------------- *)
Proof.
move⇒ j1 j2 t ARRIVES PREEMPT BACK_j1 SCHED_j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 421)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 483)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
subgoal 2 (ID 484) is:
hep_job_at t j2 j1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 483)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 501)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
----------------------------------------------------------------------------- *)
now apply H_reflexive_priorities.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 484)
subgoal 1 (ID 484) is:
hep_job_at t j2 j1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 484)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 484)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 503)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 524)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
subgoal 2 (ID 529) is:
backlogged (prefix t) j1 t -> hep_job_at t j2 j1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 524)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 537)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
subgoal 2 (ID 539) is:
~~ scheduled_at (prefix t) j1 t
----------------------------------------------------------------------------- *)
rewrite /identical_prefix /uni_schedule /prefix ⇒ t' LT.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 599)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
============================
np_uni_schedule arr_seq choose_highest_prio_job t' =
match t with
| 0 => empty_schedule idle_state
| succn t'0 => schedule_up_to policy idle_state t'0
end t'
subgoal 2 (ID 539) is:
~~ scheduled_at (prefix t) j1 t
----------------------------------------------------------------------------- *)
induction t ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 631)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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 (succn t)
SCHED_j2 : scheduled_at schedule j2 (succn t)
NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 (succn t)
t' : nat
LT : t' < succn t
IHt : preemption_time schedule t ->
scheduled_at schedule j2 t ->
~~ scheduled_at (uni_schedule arr_seq) j1 t ->
t' < t ->
np_uni_schedule arr_seq choose_highest_prio_job t' =
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end t'
============================
np_uni_schedule arr_seq choose_highest_prio_job t' =
schedule_up_to policy idle_state t t'
subgoal 2 (ID 539) is:
~~ scheduled_at (prefix t) j1 t
----------------------------------------------------------------------------- *)
rewrite /np_uni_schedule /generic_schedule (schedule_up_to_prefix_inclusion _ _ t' t) //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 539)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 710)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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
| succn t' => schedule_up_to policy idle_state t'
end t != Some j1
----------------------------------------------------------------------------- *)
induction t ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 734)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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 (succn t)
SCHED_j2 : scheduled_at schedule j2 (succn t)
NOT_SCHED_j1 : ~~ scheduled_at (uni_schedule arr_seq) j1 (succn t)
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
| succn t' => schedule_up_to policy idle_state t'
end t != Some j1
============================
schedule_up_to policy idle_state t (succn t) != Some j1
----------------------------------------------------------------------------- *)
now rewrite schedule_up_to_empty.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 529)
subgoal 1 (ID 529) is:
backlogged (prefix t) j1 t -> hep_job_at t j2 j1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 529)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 767)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 769)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 781)
Job : JobType
JC : JobCost Job
JA : JobArrival Job
PState := processor_state Job : Type
idle_state := None : PState
arr_seq : arrival_sequence Job
H_consistent_arrival_times : consistent_arrival_times arr_seq
RM : JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM
H : JobPreemptable Job
H_valid_preemption_behavior : valid_nonpreemptive_readiness RM
H0 : JLDP_policy Job
H_reflexive_priorities : reflexive_priorities
H_total : total_priorities
H_transitive : transitive_priorities
schedule := uni_schedule arr_seq : schedule.schedule (processor_state Job)
policy := allocation_at arr_seq choose_highest_prio_job
: schedule.schedule (processor_state Job) -> instant -> option Job
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Priority.
End PrioAwareUniprocessorScheduler.