Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.facts.preemption.task.nonpreemptive.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
Require Export prosa.analysis.facts.readiness.basic.
Require Export prosa.analysis.definitions.tardiness.
Require Export prosa.implementation.facts.ideal_uni.prio_aware.
Require Export prosa.implementation.definitions.task.
Require Export prosa.model.priority.edf.
(** ** Fully-Nonpreemptive Earliest-Deadline-First Schedules *)
(** In this section, we prove that the fully-nonpreemptive preemption policy
under earliest-deadline-first schedules is valid, and that the scheduling policy is
respected at each preemption point.
Some lemmas in this file are not novel facts; they are used to uniform
POET's certificates and minimize their verbosity. *)
Section Schedule .
(** In this file, we adopt the Prosa standard implementation of jobs and tasks. *)
Definition Task := concrete_task : eqType.
Definition Job := concrete_job : eqType.
(** Consider any valid arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
(** ... assume basic readiness, ... *)
Instance basic_ready_instance : JobReady Job (ideal.processor_state Job) :=
basic.basic_ready_instance.
(** ... and consider any fully-nonpreemptive, earliest-deadline-first schedule. *)
#[local] Existing Instance fully_nonpreemptive_job_model .
#[local] Existing Instance EDF .
Definition sched := uni_schedule arr_seq.
(** First, we show that only ready jobs execute. *)
Lemma sched_jobs_must_be_ready_to_execute :
jobs_must_be_ready_to_execute sched.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
jobs_must_be_ready_to_execute sched
Proof .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
jobs_must_be_ready_to_execute sched
move => j t SCHED.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t
job_ready sched j t
apply jobs_must_be_ready => //.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t
forall (t : instant) (s : seq Job) (j : Job),
choose_highest_prio_job t s = Some j -> j \in s
- arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t
forall (t : instant) (s : seq Job) (j : Job),
choose_highest_prio_job t s = Some j -> j \in s
move => tt ss jj IN.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t tt : instant ss : seq Job jj : Job IN : choose_highest_prio_job tt ss = Some jj
jj \in ss
rewrite /choose_highest_prio_job in IN.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t tt : instant ss : seq Job jj : Job IN : supremum (hep_job_at tt) ss = Some jj
jj \in ss
by apply supremum_in in IN.
- arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t
nonclairvoyant_readiness basic_ready_instance
by apply basic_readiness_nonclairvoyance.
Qed .
(** Next, we remark that such a schedule is valid. *)
Remark sched_valid :
valid_schedule sched arr_seq.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
valid_schedule sched arr_seq
Proof .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
valid_schedule sched arr_seq
split .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
jobs_come_from_arrival_sequence sched arr_seq
- arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
jobs_come_from_arrival_sequence sched arr_seq
apply np_schedule_jobs_from_arrival_sequence.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
forall (t : instant) (s : seq Job) (j : Job),
choose_highest_prio_job t s = Some j -> j \in s
by move => t ???; eapply (supremum_in (hep_job_at t)).
- arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
jobs_must_be_ready_to_execute sched
by apply sched_jobs_must_be_ready_to_execute.
Qed .
(** Next, we show that an unfinished job scheduled at time [t] is
always scheduled at time [t+1] as well. Note that the validity of
this fact also depends on which readiness model is used. *)
Lemma sched_nonpreemptive_next :
forall j t ,
scheduled_at sched j t ->
~~ completed_by sched j t.+1 ->
scheduled_at sched j t.+1 .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
forall (j : Job) (t : instant),
scheduled_at sched j t ->
~~ completed_by sched j t.+1 ->
scheduled_at sched j t.+1
Proof .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
forall (j : Job) (t : instant),
scheduled_at sched j t ->
~~ completed_by sched j t.+1 ->
scheduled_at sched j t.+1
move => j t SCHED NCOMP.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t NCOMP : ~~ completed_by sched j t.+1
scheduled_at sched j t.+1
have PENDING: job_ready sched j t by apply sched_jobs_must_be_ready_to_execute.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t NCOMP : ~~ completed_by sched j t.+1 PENDING : job_ready sched j t
scheduled_at sched j t.+1
unfold job_ready, basic_ready_instance, basic.basic_ready_instance in *.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t NCOMP : ~~ completed_by sched j t.+1 PENDING : pending sched j t
scheduled_at sched j t.+1
set chp:= choose_highest_prio_job.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t NCOMP : ~~ completed_by sched j t.+1 PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job
scheduled_at sched j t.+1
have SERV_ZERO: 0 < service sched j t.+1 .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t NCOMP : ~~ completed_by sched j t.+1 PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job
0 < service sched j t.+1
{ arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t NCOMP : ~~ completed_by sched j t.+1 PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job
0 < service sched j t.+1
exact : scheduled_implies_nonzero_service. } arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t NCOMP : ~~ completed_by sched j t.+1 PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SERV_ZERO : 0 < service sched j t.+1
scheduled_at sched j t.+1
have SERV_COST: service sched j t.+1 < job_cost j by apply less_service_than_cost_is_incomplete.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant SCHED : scheduled_at sched j t NCOMP : ~~ completed_by sched j t.+1 PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SERV_ZERO : 0 < service sched j t.+1 SERV_COST : service sched j t.+1 < job_cost j
scheduled_at sched j t.+1
move : SCHED NCOMP.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SERV_ZERO : 0 < service sched j t.+1 SERV_COST : service sched j t.+1 < job_cost j
scheduled_at sched j t ->
~~ completed_by sched j t.+1 ->
scheduled_at sched j t.+1
rewrite !scheduled_at_def /sched /uni_schedule
/pmc_uni_schedule /generic_schedule => /eqP SCHED NCOMP.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SERV_ZERO : 0 < service sched j t.+1 SERV_COST : service sched j t.+1 < job_cost j SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1
schedule_up_to
(allocation_at arr_seq choose_highest_prio_job) None
t.+1 t.+1 == Some j
rewrite schedule_up_to_def {1 }/allocation_at ifT; first by rewrite SCHED.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SERV_ZERO : 0 < service sched j t.+1 SERV_COST : service sched j t.+1 < job_cost j SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1
prev_job_nonpreemptive
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) t.+1
rewrite /prev_job_nonpreemptive SCHED /job_preemptable /fully_nonpreemptive_job_model.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SERV_ZERO : 0 < service sched j t.+1 SERV_COST : service sched j t.+1 < job_cost j SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1
job_ready
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1 &&
~~
((service
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1 == 0 )
|| (service
(schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t) j t.+1 ==
job_cost j))
move : SERV_COST SERV_ZERO; rewrite /uni_schedule /pmc_uni_schedule /generic_schedule.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1
service sched j t.+1 < job_cost j ->
0 < service sched j t.+1 ->
job_ready
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1 &&
~~
((service
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1 == 0 )
|| (service
(schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t) j t.+1 ==
job_cost j))
replace (_ (_ (_ _ _) _ t) j _) with (service sched j t.+1 ); last first .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1
service sched j t.+1 =
service
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1
{ arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1
service sched j t.+1 =
service
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1
rewrite /uni_schedule /pmc_uni_schedule /generic_schedule /service
/service_during /service_at.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1
\sum_(0 <= t < t.+1 ) service_in j (sched t) =
\sum_(0 <= t0 < t.+1 )
service_in j
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t t0)
apply eq_big_nat => i H.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 i : nat H : 0 <= i < t.+1
service_in j (sched i) =
service_in j
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t i)
replace (_ (_ _ _) _ t i) with (schedule_up_to (allocation_at arr_seq chp) None i i) => //.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 i : nat H : 0 <= i < t.+1
schedule_up_to (allocation_at arr_seq chp) None i i =
schedule_up_to
(allocation_at arr_seq choose_highest_prio_job) None
t i
by apply schedule_up_to_prefix_inclusion. } arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1
service sched j t.+1 < job_cost j ->
0 < service sched j t.+1 ->
job_ready
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1 &&
~~
((service sched j t.+1 == 0 )
|| (service sched j t.+1 == job_cost j))
move => SERV_COST SERV_ZERO; apply /andP.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 SERV_COST : service sched j t.+1 < job_cost j SERV_ZERO : 0 < service sched j t.+1
job_ready
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1 /\
~~
((service sched j t.+1 == 0 )
|| (service sched j t.+1 == job_cost j))
split ; [|by apply /norP;split ;[rewrite -lt0n|move : SERV_COST;rewrite ltn_neqAle=> /andP [??]]].arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 SERV_COST : service sched j t.+1 < job_cost j SERV_ZERO : 0 < service sched j t.+1
job_ready
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1
{ arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 SERV_COST : service sched j t.+1 < job_cost j SERV_ZERO : 0 < service sched j t.+1
job_ready
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1
unfold job_ready, basic_ready_instance, basic.basic_ready_instance.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 SERV_COST : service sched j t.+1 < job_cost j SERV_ZERO : 0 < service sched j t.+1
pending
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1
apply /andP; split ; first by move : PENDING => /andP [ARR _]; unfold has_arrived in *; lia .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : ~~
completed_by
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 SERV_COST : service sched j t.+1 < job_cost j SERV_ZERO : 0 < service sched j t.+1
~~
completed_by
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1
unfold completed_by in *; rewrite <- ltnNge in *.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : service
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 < job_cost j SERV_COST : service sched j t.+1 < job_cost j SERV_ZERO : 0 < service sched j t.+1
service
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1 < job_cost j
replace (service (_ (_ _ _) _ t) j t.+1 ) with
(service (fun t => schedule_up_to (allocation_at arr_seq chp) None t t) j t.+1 ) => //.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : service
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 < job_cost j SERV_COST : service sched j t.+1 < job_cost j SERV_ZERO : 0 < service sched j t.+1
service
(fun t : instant =>
schedule_up_to (allocation_at arr_seq chp) None t t)
j t.+1 =
service
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j t.+1
rewrite /service /service_during //=; apply eq_big_nat.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : service
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 < job_cost j SERV_COST : service sched j t.+1 < job_cost j SERV_ZERO : 0 < service sched j t.+1
forall i : nat,
0 <= i < t.+1 ->
service_at
(fun t : instant =>
schedule_up_to (allocation_at arr_seq chp) None t t)
j i =
service_at
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t) j i
move => t' /andP[GEQ0 LEQt]; rewrite /service_at.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : service
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 < job_cost j SERV_COST : service sched j t.+1 < job_cost j SERV_ZERO : 0 < service sched j t.+1 t' : nat GEQ0 : 0 <= t'LEQt : t' < t.+1
service_in j
(schedule_up_to (allocation_at arr_seq chp) None t'
t') =
service_in j
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t t')
replace (_ (_ _ _) _ t' t') with (schedule_up_to (allocation_at arr_seq chp) None t t') => //.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant PENDING : pending sched j t chp := choose_highest_prio_job : instant ->
seq concrete_job -> option concrete_job SCHED : schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t =
Some j NCOMP : service
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq
choose_highest_prio_job) None t t) j
t.+1 < job_cost j SERV_COST : service sched j t.+1 < job_cost j SERV_ZERO : 0 < service sched j t.+1 t' : nat GEQ0 : 0 <= t'LEQt : t' < t.+1
schedule_up_to (allocation_at arr_seq chp) None t t' =
schedule_up_to (allocation_at arr_seq chp) None t' t'
by symmetry ; apply schedule_up_to_prefix_inclusion; lia . }
Qed .
(** Using the lemma above, we show that the schedule is nonpreemptive. *)
Lemma sched_nonpreemptive :
nonpreemptive_schedule (uni_schedule arr_seq).arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
nonpreemptive_schedule (uni_schedule arr_seq)
Proof .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
nonpreemptive_schedule (uni_schedule arr_seq)
rewrite /nonpreemptive_schedule.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
forall (j : Job) (t t' : instant),
t <= t' ->
scheduled_at (uni_schedule arr_seq) j t ->
~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t'
move => j t; elim => [|t' IHt']; first by move => t'; have ->: t = 0 by lia .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant t' : nat IHt' : t <= t' ->
scheduled_at (uni_schedule arr_seq) j t ->
~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t'
t <= t'.+1 ->
scheduled_at (uni_schedule arr_seq) j t ->
~~ completed_by (uni_schedule arr_seq) j t'.+1 ->
scheduled_at (uni_schedule arr_seq) j t'.+1
move => LEQ SCHED NCOMP.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant t' : nat IHt' : t <= t' ->
scheduled_at (uni_schedule arr_seq) j t ->
~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t' LEQ : t <= t'.+1 SCHED : scheduled_at (uni_schedule arr_seq) j t NCOMP : ~~ completed_by (uni_schedule arr_seq) j t'.+1
scheduled_at (uni_schedule arr_seq) j t'.+1
destruct (ltngtP t t'.+1 ) as [LT | _ | EQ] => //.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant t' : nat IHt' : t <= t' ->
scheduled_at (uni_schedule arr_seq) j t ->
~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t' LEQ : true SCHED : scheduled_at (uni_schedule arr_seq) j t NCOMP : ~~ completed_by (uni_schedule arr_seq) j t'.+1 LT : t < t'.+1
scheduled_at (uni_schedule arr_seq) j t'.+1
feed_n 3 IHt'=> //. arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant t' : nat IHt' : ~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t' LEQ : true SCHED : scheduled_at (uni_schedule arr_seq) j t NCOMP : ~~ completed_by (uni_schedule arr_seq) j t'.+1 LT : t < t'.+1
~~ completed_by (uni_schedule arr_seq) j t'
{ arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant t' : nat IHt' : ~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t' LEQ : true SCHED : scheduled_at (uni_schedule arr_seq) j t NCOMP : ~~ completed_by (uni_schedule arr_seq) j t'.+1 LT : t < t'.+1
~~ completed_by (uni_schedule arr_seq) j t'
specialize (completion_monotonic sched j t' t'.+1 ) => MONO.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant t' : nat IHt' : ~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t' LEQ : true SCHED : scheduled_at (uni_schedule arr_seq) j t NCOMP : ~~ completed_by (uni_schedule arr_seq) j t'.+1 LT : t < t'.+1 MONO : t' <= t'.+1 ->
completed_by sched j t' ->
completed_by sched j t'.+1
~~ completed_by (uni_schedule arr_seq) j t'
feed MONO; first by lia . arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant t' : nat IHt' : ~~ completed_by (uni_schedule arr_seq) j t' ->
scheduled_at (uni_schedule arr_seq) j t' LEQ : true SCHED : scheduled_at (uni_schedule arr_seq) j t NCOMP : ~~ completed_by (uni_schedule arr_seq) j t'.+1 LT : t < t'.+1 MONO : completed_by sched j t' ->
completed_by sched j t'.+1
~~ completed_by (uni_schedule arr_seq) j t'
by apply contra in MONO. } arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant t' : nat IHt' : scheduled_at (uni_schedule arr_seq) j t' LEQ : true SCHED : scheduled_at (uni_schedule arr_seq) j t NCOMP : ~~ completed_by (uni_schedule arr_seq) j t'.+1 LT : t < t'.+1
scheduled_at (uni_schedule arr_seq) j t'.+1
by apply sched_nonpreemptive_next.
Qed .
(** Finally, we show that the earliest-deadline-first policy is respected
at each preemption point. *)
Lemma respects_policy_at_preemption_point_edf_np :
respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
respects_JLFP_policy_at_preemption_point arr_seq sched
(EDF Job)
Proof .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
respects_JLFP_policy_at_preemption_point arr_seq sched
(EDF Job)
apply schedule_respects_policy => //; auto with basic_rt_facts.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
nonclairvoyant_readiness basic_ready_instance
by apply basic_readiness_nonclairvoyance.
Qed .
End Schedule .