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.util.int.[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 ] New coercion path [GRing.subring_closedM;
GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.sdivr_closed_div;
GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.subalg_closedBM;
GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.divring_closed_div;
GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.divalg_closedBdiv;
GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,coercions,default] Notation "_ - _" was already used in scope
distn_scope. [notation-overridden,parsing,default]
Require Export prosa.model.schedule.priority_driven.[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.model.priority.gel.
Require Export prosa.model.priority.fifo.
Require Export prosa.model.priority.edf.
Require Import prosa.model.task.absolute_deadline.
Require Export prosa.analysis.facts.priority.classes.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.facts.priority.edf.
Require Export prosa.analysis.facts.priority.gel.
Require Export prosa.analysis.facts.priority.fifo.
(** * Generality of GEL *)
(** In the following, we make some formal remarks on the obvious generality of
GEL w.r.t. EDF and FIFO, and the somewhat less obvious conditional
generality w.r.t. fixed-priority scheduling. *)
(** We begin with the general setup. *)
Section GeneralityOfGEL .
(** Consider any type of tasks with relative priority points... *)
Context {Task : TaskType} `{PriorityPoint Task}.
(** ... jobs of these tasks, and ... *)
Context {Job : JobType} `{JobTask Job Task}.
(** ... any processor model. *)
Context {PState : ProcessorState Job}.
(** Suppose the jobs have arrival times and costs, and allow for any preemption
and readiness models. *)
Context {Arrival : JobArrival Job} {Cost : JobCost Job}
`{JobPreemptable Job} {JR: @JobReady Job PState Cost Arrival}.
(** ** GEL Generalizes EDF *)
(** First, let us consider EDF, the namesake of GEL, which by design it
trivially generalizes. *)
Section GELGeneralizesEDF .
(** Suppose the tasks have relative deadlines. *)
Context `{TaskDeadline Task}.
(** If each task's priority point is set to its relative deadline ... *)
Hypothesis H_priority_point :
forall tsk ,
task_priority_point tsk = task_deadline tsk.
(** ... then the GEL policy reduces to EDF. *)
Remark gel_generalizes_edf :
forall sched arr_seq ,
respects_JLFP_policy_at_preemption_point arr_seq sched (GEL Job Task)
<-> respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState H2 : TaskDeadline Task H_priority_point : forall tsk : Task,
task_priority_point tsk =
task_deadline tsk
forall (sched : schedule PState)
(arr_seq : arrival_sequence Job),
respects_JLFP_policy_at_preemption_point arr_seq sched
(GEL Job Task) <->
respects_JLFP_policy_at_preemption_point arr_seq sched
(EDF Job)
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState H2 : TaskDeadline Task H_priority_point : forall tsk : Task,
task_priority_point tsk =
task_deadline tsk
forall (sched : schedule PState)
(arr_seq : arrival_sequence Job),
respects_JLFP_policy_at_preemption_point arr_seq sched
(GEL Job Task) <->
respects_JLFP_policy_at_preemption_point arr_seq sched
(EDF Job)
by move => sched arr_seq
; split => RESPECTED j j' t ARR PT BL SCHED
; move : (RESPECTED j j' t ARR PT BL SCHED)
; rewrite !hep_job_at_jlfp
hep_job_task_deadline
hep_job_priority_point !H_priority_point
; lia .
Qed .
End GELGeneralizesEDF .
(** ** GEL Generalizes FIFO *)
(** GEL similarly generalizes FIFO in a trivial manner. *)
Section GELGeneralizesFIFO .
(** If each task's priority point is set to zero ... *)
Hypothesis H_priority_point :
forall tsk ,
task_priority_point tsk = 0 .
(** ... then the GEL policy reduces to FIFO. *)
Remark gel_generalizes_fifo :
forall sched arr_seq ,
respects_JLFP_policy_at_preemption_point arr_seq sched (GEL Job Task)
<-> respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job).Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState H_priority_point : forall tsk : Task,
task_priority_point tsk = 0 %Z
forall (sched : schedule PState)
(arr_seq : arrival_sequence Job),
respects_JLFP_policy_at_preemption_point arr_seq sched
(GEL Job Task) <->
respects_JLFP_policy_at_preemption_point arr_seq sched
(FIFO Job)
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState H_priority_point : forall tsk : Task,
task_priority_point tsk = 0 %Z
forall (sched : schedule PState)
(arr_seq : arrival_sequence Job),
respects_JLFP_policy_at_preemption_point arr_seq sched
(GEL Job Task) <->
respects_JLFP_policy_at_preemption_point arr_seq sched
(FIFO Job)
by move => sched arr_seq
; split => RESPECTED j j' t ARR PT BL SCHED
; move : (RESPECTED j j' t ARR PT BL SCHED)
; rewrite !hep_job_at_jlfp
hep_job_priority_point !H_priority_point hep_job_arrival_FIFO
; lia .
Qed .
End GELGeneralizesFIFO .
(** ** GEL Conditionally Generalizes FP *)
(** We now turn to fixed-priority scheduling. GEL does not generalize
fixed-priority scheduling in all circumstances. However, if priority
points are carefully chosen, tasks are sequential, and fixed task
priorities are unique, then GEL can be equivalent to a given arbitrary
fixed-priority policy. *)
Section GELConditionallyGeneralizesFP .
(** Consider any given fixed-priority policy that is both reflexive and
total... *)
Variable fp : FP_policy Task.
Hypothesis H_reflexive : reflexive_task_priorities fp.
Hypothesis H_total : total_task_priorities fp.
(** ... and an arbitrary valid arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** For ease of reference, we refer to the difference between the relative
priority points of two given tasks as [pp_delta]. *)
Definition pp_delta tsk tsk' :=
(task_priority_point tsk' - task_priority_point tsk)%R.
(** Before we tackle the conditional equivalence, we first establish a
helper lemma on the priority of backlogged jobs that sits at the core of
the argument. *)
Section GELPrioOfBackloggedJob .
(** Consider two arbitrary jobs [j] and [j'], ... *)
Variable j j' : Job.
(** ... their corresponding tasks [tsk] and [tsk'], ... *)
Let tsk := job_task j.
Let tsk' := job_task j'.
(** ...an arbitrary schedule, ... *)
Variable sched : schedule PState.
(** ... and an arbitrary point in time [t]. *)
Variable t : instant.
(** Suppose the relative priority point of [tsk'] is larger than that of
[tsk] ... *)
Hypothesis H_delta_pos : (pp_delta tsk tsk' >= 0 )%R.
(** ... and that the difference between the priority points of the two
tasks bounds the maximum response time of [j'] in [sched]. *)
Hypothesis H_rt_bound :
job_response_time_bound sched j' `|pp_delta tsk tsk'|.
(** For clarity, recall the definition of "higher-or-equal job priority"
under GEL and refer to it as [gel_hep_job]. *)
Let gel_hep_job := @hep_job _ (GEL Job Task).
(** We are now ready to state the auxiliary lemma: under the above
assumptions, if [j] has arrived by time [t] and [j'] is backlogged,
then [j]'s priority under GEL is higher than or equal to [j']'s
priority. *)
Lemma backlogged_job_has_lower_gel_prio :
has_arrived j t ->
backlogged sched j' t ->
gel_hep_job j j'.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j, j' : Job tsk := job_task j : Task tsk' := job_task j' : Task sched : schedule PState t : instant H_delta_pos : (0 <= pp_delta tsk tsk')%R H_rt_bound : job_response_time_bound sched j'
`|pp_delta tsk tsk'| gel_hep_job := hep_job : rel Job
has_arrived j t ->
backlogged sched j' t -> gel_hep_job j j'
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j, j' : Job tsk := job_task j : Task tsk' := job_task j' : Task sched : schedule PState t : instant H_delta_pos : (0 <= pp_delta tsk tsk')%R H_rt_bound : job_response_time_bound sched j'
`|pp_delta tsk tsk'| gel_hep_job := hep_job : rel Job
has_arrived j t ->
backlogged sched j' t -> gel_hep_job j j'
move => ARRIVED BL'.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j, j' : Job tsk := job_task j : Task tsk' := job_task j' : Task sched : schedule PState t : instant H_delta_pos : (0 <= pp_delta tsk tsk')%R H_rt_bound : job_response_time_bound sched j'
`|pp_delta tsk tsk'| gel_hep_job := hep_job : rel Job ARRIVED : has_arrived j t BL' : backlogged sched j' t
gel_hep_job j j'
rewrite /gel_hep_job/hep_job/GEL/job_priority_point.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j, j' : Job tsk := job_task j : Task tsk' := job_task j' : Task sched : schedule PState t : instant H_delta_pos : (0 <= pp_delta tsk tsk')%R H_rt_bound : job_response_time_bound sched j'
`|pp_delta tsk tsk'| gel_hep_job := hep_job : rel Job ARRIVED : has_arrived j t BL' : backlogged sched j' t
((job_arrival j)%:R + task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R
have [|ARR'] := leqP (job_arrival j)
(job_arrival j' + `|pp_delta tsk tsk'|);
first by move : H_delta_pos; rewrite /pp_delta/tsk/tsk'; lia .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j, j' : Job tsk := job_task j : Task tsk' := job_task j' : Task sched : schedule PState t : instant H_delta_pos : (0 <= pp_delta tsk tsk')%R H_rt_bound : job_response_time_bound sched j'
`|pp_delta tsk tsk'| gel_hep_job := hep_job : rel Job ARRIVED : has_arrived j t BL' : backlogged sched j' t ARR' : job_arrival j' + `|pp_delta tsk tsk'| <
job_arrival j
((job_arrival j)%:R + task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R
exfalso .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j, j' : Job tsk := job_task j : Task tsk' := job_task j' : Task sched : schedule PState t : instant H_delta_pos : (0 <= pp_delta tsk tsk')%R H_rt_bound : job_response_time_bound sched j'
`|pp_delta tsk tsk'| gel_hep_job := hep_job : rel Job ARRIVED : has_arrived j t BL' : backlogged sched j' t ARR' : job_arrival j' + `|pp_delta tsk tsk'| <
job_arrival j
False
have INCOMP : ~ completed_by sched j' t
by apply /negP; apply : backlogged_implies_incomplete.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j, j' : Job tsk := job_task j : Task tsk' := job_task j' : Task sched : schedule PState t : instant H_delta_pos : (0 <= pp_delta tsk tsk')%R H_rt_bound : job_response_time_bound sched j'
`|pp_delta tsk tsk'| gel_hep_job := hep_job : rel Job ARRIVED : has_arrived j t BL' : backlogged sched j' t ARR' : job_arrival j' + `|pp_delta tsk tsk'| <
job_arrival j INCOMP : ~ completed_by sched j' t
False
have : completed_by sched j' t => [|//].Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j, j' : Job tsk := job_task j : Task tsk' := job_task j' : Task sched : schedule PState t : instant H_delta_pos : (0 <= pp_delta tsk tsk')%R H_rt_bound : job_response_time_bound sched j'
`|pp_delta tsk tsk'| gel_hep_job := hep_job : rel Job ARRIVED : has_arrived j t BL' : backlogged sched j' t ARR' : job_arrival j' + `|pp_delta tsk tsk'| <
job_arrival j INCOMP : ~ completed_by sched j' t
completed_by sched j' t
move : H_rt_bound; rewrite /job_response_time_bound.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j, j' : Job tsk := job_task j : Task tsk' := job_task j' : Task sched : schedule PState t : instant H_delta_pos : (0 <= pp_delta tsk tsk')%R H_rt_bound : job_response_time_bound sched j'
`|pp_delta tsk tsk'| gel_hep_job := hep_job : rel Job ARRIVED : has_arrived j t BL' : backlogged sched j' t ARR' : job_arrival j' + `|pp_delta tsk tsk'| <
job_arrival j INCOMP : ~ completed_by sched j' t
completed_by sched j'
(job_arrival j' + `|pp_delta tsk tsk'|) ->
completed_by sched j' t
apply : completion_monotonic.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j, j' : Job tsk := job_task j : Task tsk' := job_task j' : Task sched : schedule PState t : instant H_delta_pos : (0 <= pp_delta tsk tsk')%R H_rt_bound : job_response_time_bound sched j'
`|pp_delta tsk tsk'| gel_hep_job := hep_job : rel Job ARRIVED : has_arrived j t BL' : backlogged sched j' t ARR' : job_arrival j' + `|pp_delta tsk tsk'| <
job_arrival j INCOMP : ~ completed_by sched j' t
job_arrival j' + `|pp_delta tsk tsk'| <= t
by move : ARRIVED; rewrite /has_arrived; lia .
Qed .
End GELPrioOfBackloggedJob .
(** With the auxiliary lemma in place, we now state the main assumptions
under which conditional generality can be shown. *)
(** Firstly, we require that the priorities of tasks that feature in the
schedule are unique. That is, no two tasks that contribute jobs to the
arrival sequence share a fixed priority. *)
Hypothesis H_unique_fixed_priorities :
forall j j' ,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j) (job_task j') ->
hp_task (job_task j) (job_task j').
(** Secondly, we require that the assigned relative priority points are
monotonic with decreasing task priority: the relative priority point
offset of a lower-priority task must not be less than that of any
higher-priority task (that features in the arrival sequence). *)
Hypothesis H_hp_delta_pos :
forall j j' ,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(pp_delta (job_task j) (job_task j') >= 0 )%R.
(** To state the third and fourth assumptions, we require an arbitrary,
valid schedule to be given. *)
Variable sched : schedule PState.
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
(** Thirdly, we require that the difference in relative priority points
between a higher- and lower-priority task exceeds the maximum response
time of the lower-priority task in the given schedule. In other words,
the priority points of lower-priority tasks must be chosen to be "large
enough" to be sufficiently far enough in the future to avoid interfering
with any concurrently pending jobs of higher-priority tasks. *)
Hypothesis H_hp_delta_rtb :
forall j j' ,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j' `|pp_delta (job_task j) (job_task j')|.
(** Fourth, we require that tasks execute sequentially. *)
Hypothesis H_sequential : sequential_tasks arr_seq sched.
(** Under the four conditions stated above, GEL generalizes the given FP
policy. *)
Theorem gel_conditionally_generalizes_fp :
respects_JLFP_policy_at_preemption_point arr_seq sched (GEL Job Task)
<-> respects_FP_policy_at_preemption_point arr_seq sched fp.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched
respects_JLFP_policy_at_preemption_point arr_seq sched
(GEL Job Task) <->
respects_FP_policy_at_preemption_point arr_seq sched
fp
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched
respects_JLFP_policy_at_preemption_point arr_seq sched
(GEL Job Task) <->
respects_FP_policy_at_preemption_point arr_seq sched
fp
split => RESPECTED j' j t ARR PT BL SCHED; last first .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
hep_job_at t j j'
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
hep_job_at t j j'
have [SAME|DIFF] := boolP (same_task j' j).Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t SAME : same_task j' j
hep_job_at t j j'
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t SAME : same_task j' j
hep_job_at t j j'
have [LT_ARR|] := ltnP (job_arrival j') (job_arrival j).Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t SAME : same_task j' j LT_ARR : job_arrival j' < job_arrival j
hep_job_at t j j'
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t SAME : same_task j' j LT_ARR : job_arrival j' < job_arrival j
hep_job_at t j j'
exfalso .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t SAME : same_task j' j LT_ARR : job_arrival j' < job_arrival j
False
have DIFF: ~ same_task j' j; last by contradiction .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t SAME : same_task j' j LT_ARR : job_arrival j' < job_arrival j
~ same_task j' j
apply /negP/sequential_tasks_different_tasks => //.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t SAME : same_task j' j LT_ARR : job_arrival j' < job_arrival j
~~ completed_by sched j' t
exact : backlogged_implies_incomplete. } Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t SAME : same_task j' j
job_arrival j <= job_arrival j' -> hep_job_at t j j'
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t SAME : same_task j' j
job_arrival j <= job_arrival j' -> hep_job_at t j j'
by rewrite hep_job_at_jlfp hep_job_arrival_gel // same_task_sym. } } Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j
hep_job_at t j j'
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j
hep_job_at t j j'
have HFP: hp_task (job_task j) (job_task j').Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j
hp_task (job_task j) (job_task j')
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j
hp_task (job_task j) (job_task j')
apply : H_unique_fixed_priorities => //.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j
~~ same_task j j'
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j
~~ same_task j j'
by rewrite same_task_sym.
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j
hep_task (job_task j) (job_task j')
by move : (RESPECTED j' j t ARR PT BL SCHED); rewrite hep_job_at_fp. } Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_FP_policy_at_preemption_point
arr_seq sched fp j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j) (job_task j')
hep_job_at t j j'
exact : (backlogged_job_has_lower_gel_prio _ _ sched t).
} } Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
hep_job_at t j j'
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
hep_job_at t j j'
rewrite hep_job_at_fp.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
hep_task (job_task j) (job_task j')
case : (boolP (same_task j' j)); first by rewrite /same_task => /eqP ->.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t
~~ same_task j' j ->
hep_task (job_task j) (job_task j')
move => DIFF; apply : contraT; rewrite not_hep_hp_task // => HFP.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j)
false
have FIN: completed_by sched j (job_arrival j + `|pp_delta (job_task j') (job_task j)|);
first by exact : H_hp_delta_rtb.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|)
false
move : (RESPECTED j' j t ARR PT BL SCHED).Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|)
hep_job_at t j j' -> false
rewrite hep_job_at_jlfp hep_job_priority_point => PRIO.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|) PRIO : ((job_arrival j)%:R +
task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R
false
have POS: (pp_delta (job_task j') (job_task j) >= 0 )%R
by exact : H_hp_delta_pos.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|) PRIO : ((job_arrival j)%:R +
task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R POS : (0 <= pp_delta (job_task j') (job_task j))%R
false
have : completed_by sched j t; last first .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|) PRIO : ((job_arrival j)%:R +
task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R POS : (0 <= pp_delta (job_task j') (job_task j))%R
completed_by sched j t -> false
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|) PRIO : ((job_arrival j)%:R +
task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R POS : (0 <= pp_delta (job_task j') (job_task j))%R
completed_by sched j t -> false
have : ~ completed_by sched j t => [|//].Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|) PRIO : ((job_arrival j)%:R +
task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R POS : (0 <= pp_delta (job_task j') (job_task j))%R
~ completed_by sched j t
by apply /negP/scheduled_implies_not_completed. } Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|) PRIO : ((job_arrival j)%:R +
task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R POS : (0 <= pp_delta (job_task j') (job_task j))%R
completed_by sched j t
{ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|) PRIO : ((job_arrival j)%:R +
task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R POS : (0 <= pp_delta (job_task j') (job_task j))%R
completed_by sched j t
apply : completion_monotonic; last exact : FIN.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|) PRIO : ((job_arrival j)%:R +
task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R POS : (0 <= pp_delta (job_task j') (job_task j))%R
job_arrival j + `|pp_delta (job_task j') (job_task j)| <=
t
move : POS; rewrite /pp_delta.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|) PRIO : ((job_arrival j)%:R +
task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R
(0 <=
task_priority_point (job_task j) -
task_priority_point (job_task j'))%R ->
job_arrival j +
`|(task_priority_point (job_task j) -
task_priority_point (job_task j'))%R| <= t
have : job_arrival j' <= t; last lia .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobTask Job Task PState : ProcessorState Job Arrival : JobArrival Job Cost : JobCost Job H1 : JobPreemptable Job JR : JobReady Job PState fp : FP_policy Task H_reflexive : reflexive_task_priorities fp H_total : total_task_priorities fp arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_unique_fixed_priorities : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
~~ same_task j j' ->
hep_task (job_task j)
(job_task j') ->
hp_task (job_task j)
(job_task j')H_hp_delta_pos : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
(0 <=
pp_delta (job_task j) (job_task j'))%Rsched : schedule PState H_sched_valid : valid_schedule sched arr_seq H_hp_delta_rtb : forall j j' : Job,
arrives_in arr_seq j ->
arrives_in arr_seq j' ->
hp_task (job_task j) (job_task j') ->
job_response_time_bound sched j'
`|pp_delta (job_task j)
(job_task j')|H_sequential : sequential_tasks arr_seq sched RESPECTED : respects_JLFP_policy_at_preemption_point
arr_seq sched (GEL Job Task) j', j : Job t : instant ARR : arrives_in arr_seq j' PT : preemption_time arr_seq sched t BL : backlogged sched j' t SCHED : scheduled_at sched j t DIFF : ~~ same_task j' j HFP : hp_task (job_task j') (job_task j) FIN : completed_by sched j
(job_arrival j +
`|pp_delta (job_task j') (job_task j)|) PRIO : ((job_arrival j)%:R +
task_priority_point (job_task j) <=
(job_arrival j')%:R +
task_priority_point (job_task j'))%R
job_arrival j' <= t
by rewrite -/(has_arrived j' t). } }
Qed .
End GELConditionallyGeneralizesFP .
End GeneralityOfGEL .