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.sequential.
Require Export prosa.analysis.definitions.tardiness.
Require Export prosa.implementation.facts.ideal_uni.prio_aware.
Require Export prosa.implementation.definitions.task.
(** ** Fully-Nonpreemptive Fixed-Priority Schedules *)
(** In this section, we prove some facts about the fully-nonpreemptive
preemption policy under fixed-priority schedules.
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 sequential readiness, ... *)
Instance sequential_ready_instance : JobReady Job (ideal.processor_state Job) :=
sequential_ready_instance arr_seq.
(** ... and consider any fully-nonpreemptive, fixed-priority schedule. *)
#[local] Existing Instance fully_nonpreemptive_job_model .
#[local] Existing Instance NumericFPAscending .
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 sequential_ready_instance
by apply sequential_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 READY: 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 READY : job_ready sched j t
scheduled_at sched j t.+1
move : READY => /andP[/andP[ARR NC] /allP PRIOR].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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t}
scheduled_at sched j t.+1
have SZ: 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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t}
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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t}
0 < service sched j t.+1
apply scheduled_implies_nonzero_service; last by simpl ; exists t ; split .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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t}
ideal_progress_proc_model (processor_state Job)
by apply ideal_proc_model_ensures_ideal_progress. } 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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} SZ : 0 < service sched j t.+1
scheduled_at sched j t.+1
have SC: 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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} SZ : 0 < service sched j t.+1 SC : service sched j t.+1 < job_cost j
scheduled_at sched j t.+1
move : SCHED NCOMP; 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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} SZ : 0 < service sched j t.+1 SC : 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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} SZ : 0 < service sched j t.+1 SC : 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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} SZ : 0 < service sched j t.+1 SC : 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.job_cost j))
move : SC SZ; 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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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.job_cost j))
set chp:= choose_highest_prio_job; set sut:= schedule_up_to.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
service sched j t.+1 < job_cost j ->
0 < service sched j t.+1 ->
job_ready (sut (allocation_at arr_seq chp) None t) j
t.+1 &&
~~
((service (sut (allocation_at arr_seq chp) None t) j
t.+1 == 0 )
|| (service (sut (allocation_at arr_seq chp) None t)
j t.+1 == job.job_cost j))
replace (_ (_ (_ _ _) _ t) j t.+1 ) 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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
service sched j t.+1 =
service (sut (allocation_at arr_seq chp) None t) j
t.+1
{ arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
service sched j t.+1 =
service (sut (allocation_at arr_seq chp) None t) j
t.+1
rewrite /uni_schedule /pmc_uni_schedule /generic_schedule /service
/service_during /service_at; apply eq_big_nat => i H.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) i : nat H : 0 <= i < t.+1
service_in j (sched i) =
service_in j
(sut (allocation_at arr_seq chp) None t i)
replace (_ (_ _ _) _ t i) with (sut (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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) i : nat H : 0 <= i < t.+1
sut (allocation_at arr_seq chp) None i i =
sut (allocation_at arr_seq chp) 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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job)
service sched j t.+1 < job_cost j ->
0 < service sched j t.+1 ->
job_ready (sut (allocation_at arr_seq chp) None t) j
t.+1 &&
~~
((service sched j t.+1 == 0 )
|| (service sched j t.+1 == job.job_cost j))
move => SC SZ; apply /andP.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1
job_ready (sut (allocation_at arr_seq chp) None t) j
t.+1 /\
~~
((service sched j t.+1 == 0 )
|| (service sched j t.+1 == job.job_cost j))
split ; last by apply /norP; split ; [rewrite -lt0n|move :SC; rewrite ltn_neqAle=> /andP[??]].arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1
job_ready (sut (allocation_at arr_seq chp) None t) j
t.+1
apply /andP; split ; [apply /andP; split ; [by unfold has_arrived in *; lia |]|].arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1
~~
completed_by (sut (allocation_at arr_seq chp) None t)
j t.+1
{ arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1
~~
completed_by (sut (allocation_at arr_seq chp) 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 ARR : has_arrived j t NC : service sched j t < job.job_cost j PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job,
job.job_cost x <= service sched x t} 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.job_cost j chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1
service (sut (allocation_at arr_seq chp) None t) j
t.+1 < job.job_cost j
replace (_ _ j _) with (service (fun t => sut (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 ARR : has_arrived j t NC : service sched j t < job.job_cost j PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job,
job.job_cost x <= service sched x t} 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.job_cost j chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1
service
(fun t : instant =>
sut (allocation_at arr_seq chp) None t t) j t.+1 =
service (sut (allocation_at arr_seq chp) 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 ARR : has_arrived j t NC : service sched j t < job.job_cost j PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job,
job.job_cost x <= service sched x t} 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.job_cost j chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1
forall i : nat,
0 <= i < t.+1 ->
service_at
(fun t : instant =>
sut (allocation_at arr_seq chp) None t t) j i =
service_at (sut (allocation_at arr_seq chp) 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 ARR : has_arrived j t NC : service sched j t < job.job_cost j PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job,
job.job_cost x <= service sched x t} 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.job_cost j chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1 t' : nat GEQ0 : 0 <= t'LEQt : t' < t.+1
service_in j
(sut (allocation_at arr_seq chp) None t' t') =
service_in j
(sut (allocation_at arr_seq chp) None t t')
replace (_ _ _ _ _) with (sut (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 ARR : has_arrived j t NC : service sched j t < job.job_cost j PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job,
job.job_cost x <= service sched x t} 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.job_cost j chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1 t' : nat GEQ0 : 0 <= t'LEQt : t' < t.+1
sut (allocation_at arr_seq chp) None t t' =
sut (allocation_at arr_seq chp) None t' t'
by symmetry ; apply schedule_up_to_prefix_inclusion; lia . } arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1
prior_jobs_complete arr_seq
(sut (allocation_at arr_seq chp) None t) j t.+1
{ arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1
prior_jobs_complete arr_seq
(sut (allocation_at arr_seq chp) None t) j t.+1
apply /allP => j' IN; apply (leq_trans (PRIOR j' IN)).arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j)
service sched j' t <=
service (sut (allocation_at arr_seq chp) None t) j'
t.+1
rewrite /service /service_during big_nat_recr //= -(addn0 (\sum_(0 <= _ < t) _)).arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j)
\sum_(0 <= H < t) service_at sched j' H + 0 <=
\sum_(0 <= i < t)
service_at (sut (allocation_at arr_seq chp) None t)
j' i +
service_at (sut (allocation_at arr_seq chp) None t) j'
t
apply leq_add => //; apply eq_leq, eq_big_nat.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j)
forall i : nat,
0 <= i < t ->
service_at sched j' i =
service_at (sut (allocation_at arr_seq chp) None t) j'
i
move => t' /andP[GEQ0 LEQt].arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j) t' : nat GEQ0 : 0 <= t'LEQt : t' < t
service_at sched j' t' =
service_at (sut (allocation_at arr_seq chp) None t) j'
t'
rewrite /service_at /sched /uni_schedule /pmc_uni_schedule /generic_schedule.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq j : Job t : instant ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j) t' : nat GEQ0 : 0 <= t'LEQt : t' < t
service_in j'
(schedule_up_to
(allocation_at arr_seq choose_highest_prio_job)
None t' t') =
service_in j'
(sut (allocation_at arr_seq chp) None t t')
replace (_ (_ _ _) _ t' t') with (sut (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 ARR : has_arrived j t NC : ~~ completed_by sched j t PRIOR : {in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j),
forall x : Job, completed_by sched x t} 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 chp := choose_highest_prio_job : instant -> seq Job -> option Job sut := schedule_up_to : PointwisePolicy (processor_state Job) ->
processor_state Job ->
instant -> schedule (processor_state Job) SC : service sched j t.+1 < job_cost j SZ : 0 < service sched j t.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(concept.job_task j)
(job.job_arrival j) t' : nat GEQ0 : 0 <= t'LEQt : t' < t
sut (allocation_at arr_seq chp) None t t' =
schedule_up_to
(allocation_at arr_seq choose_highest_prio_job) 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 fixed-priority policy is respected at each preemption point. *)
Lemma respects_policy_at_preemption_point_np :
respects_FP_policy_at_preemption_point arr_seq sched (NumericFPAscending Task).arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
respects_FP_policy_at_preemption_point arr_seq sched
(NumericFPAscending Task)
Proof .arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
respects_FP_policy_at_preemption_point arr_seq sched
(NumericFPAscending Task)
apply schedule_respects_policy => //.arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq
nonclairvoyant_readiness sequential_ready_instance
by apply sequential_readiness_nonclairvoyance.
Qed .
End Schedule .