Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.definitions.readiness.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.definitions.work_bearing_readiness.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.behavior.completion.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.model.task_arrivals.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** Throughout this file, we assume the sequential task readiness model, which
means that a job is ready to execute only if all prior jobs of the same task
have completed. *)
Require Export prosa.model.readiness.sequential.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** In this section, we show some useful properties of the sequential
task readiness model. *)
Section SequentialTasksReadiness .
(** Consider any type of job associated with any type of tasks ... *)
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** ... and any kind of processor state. *)
Context {PState : ProcessorState Job}.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** Recall that we assume sequential tasks. *)
#[local] Instance sequential_readiness : JobReady Job PState :=
sequential_ready_instance arr_seq.
(** Consider any valid schedule of [arr_seq]. *)
Variable sched : schedule PState.
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
(** Consider an FP policy that indicates a reflexive
higher-or-equal priority relation. *)
Context `{FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
(** First, we show that the sequential readiness model is non-clairvoyant. *)
Fact sequential_readiness_nonclairvoyance :
nonclairvoyant_readiness sequential_readiness.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities
nonclairvoyant_readiness sequential_readiness
Proof .Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities
nonclairvoyant_readiness sequential_readiness
intros sched1 sched2 ? ? ID ? LE; rewrite //=.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities sched1, sched2 : schedule PState j : Job h : instant ID : identical_prefix sched1 sched2 h t : nat LE : t <= h
pending sched1 j t &&
prior_jobs_complete arr_seq sched1 j t =
pending sched2 j t &&
prior_jobs_complete arr_seq sched2 j t
erewrite identical_prefix_pending; eauto 2 .Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities sched1, sched2 : schedule PState j : Job h : instant ID : identical_prefix sched1 sched2 h t : nat LE : t <= h
pending sched2 j t &&
prior_jobs_complete arr_seq sched1 j t =
pending sched2 j t &&
prior_jobs_complete arr_seq sched2 j t
destruct (boolP (pending sched2 j t)) as [_ | _] => //=.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities sched1, sched2 : schedule PState j : Job h : instant ID : identical_prefix sched1 sched2 h t : nat LE : t <= h
prior_jobs_complete arr_seq sched1 j t =
prior_jobs_complete arr_seq sched2 j t
destruct (boolP (prior_jobs_complete arr_seq sched2 j t)) as [ALL | NOT_ALL]; apply /eqP.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities sched1, sched2 : schedule PState j : Job h : instant ID : identical_prefix sched1 sched2 h t : nat LE : t <= h ALL : prior_jobs_complete arr_seq sched2 j t
prior_jobs_complete arr_seq sched1 j t == true
- Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities sched1, sched2 : schedule PState j : Job h : instant ID : identical_prefix sched1 sched2 h t : nat LE : t <= h ALL : prior_jobs_complete arr_seq sched2 j t
prior_jobs_complete arr_seq sched1 j t == true
rewrite eqb_id; apply /allP; intros ? IN.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities sched1, sched2 : schedule PState j : Job h : instant ID : identical_prefix sched1 sched2 h t : nat LE : t <= h ALL : prior_jobs_complete arr_seq sched2 j t x : Job IN : x
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j)
completed_by sched1 x t
move : ALL => /allP ALL; specialize (ALL x IN).Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities sched1, sched2 : schedule PState j : Job h : instant ID : identical_prefix sched1 sched2 h t : nat LE : t <= h x : Job IN : x
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) ALL : (fun x : Job =>
is_true (completed_by sched2 x t)) x
completed_by sched1 x t
by erewrite identical_prefix_completed_by; eauto 2 .Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities sched1, sched2 : schedule PState j : Job h : instant ID : identical_prefix sched1 sched2 h t : nat LE : t <= h NOT_ALL : ~~ prior_jobs_complete arr_seq sched2 j t
prior_jobs_complete arr_seq sched1 j t == false
- Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities sched1, sched2 : schedule PState j : Job h : instant ID : identical_prefix sched1 sched2 h t : nat LE : t <= h NOT_ALL : ~~ prior_jobs_complete arr_seq sched2 j t
prior_jobs_complete arr_seq sched1 j t == false
move : NOT_ALL => /allPn [x IN NCOMP].Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities sched1, sched2 : schedule PState j : Job h : instant ID : identical_prefix sched1 sched2 h t : nat LE : t <= h x : Job IN : x
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched2 x t
prior_jobs_complete arr_seq sched1 j t == false
rewrite eqbF_neg; apply /allPn; exists x => //.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities sched1, sched2 : schedule PState j : Job h : instant ID : identical_prefix sched1 sched2 h t : nat LE : t <= h x : Job IN : x
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched2 x t
~~ completed_by sched1 x t
by erewrite identical_prefix_completed_by; eauto 2 .
Qed .
(** Next, we show that the sequential readiness model ensures that
tasks are sequential. That is, that jobs of the same task
execute in order of their arrival. *)
Lemma sequential_readiness_implies_sequential_tasks :
sequential_tasks arr_seq sched.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities
sequential_tasks arr_seq sched
Proof .Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities
sequential_tasks arr_seq sched
intros j1 j2 t ARR1 ARR2 SAME LT SCHED.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2 SCHED : scheduled_at sched j2 t
completed_by sched j1 t
destruct (boolP (job_ready sched j2 t)) as [READY | NREADY].Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2 SCHED : scheduled_at sched j2 t READY : job_ready sched j2 t
completed_by sched j1 t
- Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2 SCHED : scheduled_at sched j2 t READY : job_ready sched j2 t
completed_by sched j1 t
move : READY => /andP [PEND /allP ALL]; apply : ALL.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2 SCHED : scheduled_at sched j2 t PEND : pending sched j2 t
j1
\in task_arrivals_before arr_seq (job_task j2)
(job_arrival j2)
rewrite mem_filter; apply /andP; split ; first by done .Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2 SCHED : scheduled_at sched j2 t PEND : pending sched j2 t
j1 \in arrivals_between arr_seq 0 (job_arrival j2)
by apply arrived_between_implies_in_arrivals => //.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2 SCHED : scheduled_at sched j2 t NREADY : ~~ job_ready sched j2 t
completed_by sched j1 t
- Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2 SCHED : scheduled_at sched j2 t NREADY : ~~ job_ready sched j2 t
completed_by sched j1 t
exfalso ; apply /(negP NREADY)/job_scheduled_implies_ready => //.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j1, j2 : Job t : instant ARR1 : arrives_in arr_seq j1 ARR2 : arrives_in arr_seq j2 SAME : same_task j1 j2 LT : job_arrival j1 < job_arrival j2 SCHED : scheduled_at sched j2 t NREADY : ~~ job_ready sched j2 t
jobs_must_be_ready_to_execute sched
exact : (valid_schedule_jobs_must_be_ready_to_execute sched arr_seq).
Qed .
(** Finally, we show that the sequential readiness model is a
work-bearing readiness model. That is, if a job [j] is pending
but not ready at a time instant [t], then there exists another
(earlier) job of the same task that is pending and ready at time
[t]. *)
Lemma sequential_readiness_implies_work_bearing_readiness :
work_bearing_readiness arr_seq sched.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities
work_bearing_readiness arr_seq sched
Proof .Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities
work_bearing_readiness arr_seq sched
intros j.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j : Job
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
have EX: exists k , job_arrival j <= k by (exists (job_arrival j )).Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j : Job EX : exists k : nat, job_arrival j <= k
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
destruct EX as [k LE]; move : j LE.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat
forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
induction k; intros ? ? ? ARR PEND.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j : Job LE : job_arrival j <= 0 t : instant ARR : arrives_in arr_seq j PEND : pending sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
{ Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j : Job LE : job_arrival j <= 0 t : instant ARR : arrives_in arr_seq j PEND : pending sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
destruct (boolP (job_ready sched j t)) as [READY | NREADY].Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j : Job LE : job_arrival j <= 0 t : instant ARR : arrives_in arr_seq j PEND : pending sched j t READY : job_ready sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
{ Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j : Job LE : job_arrival j <= 0 t : instant ARR : arrives_in arr_seq j PEND : pending sched j t READY : job_ready sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
by exists j ; repeat split ; eauto using (H_priority_is_reflexive 0 ). } Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j : Job LE : job_arrival j <= 0 t : instant ARR : arrives_in arr_seq j PEND : pending sched j t NREADY : ~~ job_ready sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
{ Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j : Job LE : job_arrival j <= 0 t : instant ARR : arrives_in arr_seq j PEND : pending sched j t NREADY : ~~ job_ready sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
move : NREADY; rewrite //= PEND Bool.andb_true_l => /allPn [jhp IN NCOMP].Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j : Job LE : job_arrival j <= 0 t : instant ARR : arrives_in arr_seq j PEND : pending sched j t jhp : Job IN : jhp
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched jhp t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
pending sched j_hp t &&
prior_jobs_complete arr_seq sched j_hp t /\
hep_job j_hp j
apply arrives_in_task_arrivals_before_implies_arrives_before in IN; last by done .Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities j : Job LE : job_arrival j <= 0 t : instant ARR : arrives_in arr_seq j PEND : pending sched j t jhp : Job IN : job_arrival jhp < job_arrival j NCOMP : ~~ completed_by sched jhp t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
pending sched j_hp t &&
prior_jobs_complete arr_seq sched j_hp t /\
hep_job j_hp j
by exfalso ; move : LE; rewrite leqn0 => /eqP EQ; rewrite EQ in IN.
}
} Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job LE : job_arrival j <= k.+1 t : instant ARR : arrives_in arr_seq j PEND : pending sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
{ Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job LE : job_arrival j <= k.+1 t : instant ARR : arrives_in arr_seq j PEND : pending sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
move : LE; rewrite leq_eqVlt ltnS => /orP [/eqP EQ | LE]; last by apply IHk.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
destruct (boolP (job_ready sched j t)) as [READY | NREADY].Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 READY : job_ready sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
{ Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 READY : job_ready sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
by exists j ; repeat split ; eauto using (H_priority_is_reflexive 0 ). } Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 NREADY : ~~ job_ready sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
{ Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 NREADY : ~~ job_ready sched j t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j
move : NREADY; rewrite //= PEND Bool.andb_true_l => /allPn [j' IN NCOMP].Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
pending sched j_hp t &&
prior_jobs_complete arr_seq sched j_hp t /\
hep_job j_hp j
have LE' : job_arrival j' <= k.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t
job_arrival j' <= k
{ Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t
job_arrival j' <= k
by apply arrives_in_task_arrivals_before_implies_arrives_before in IN; rewrite // -ltnS -EQ. } Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k
exists j_hp : Job,
arrives_in arr_seq j_hp /\
pending sched j_hp t &&
prior_jobs_complete arr_seq sched j_hp t /\
hep_job j_hp j
have ARR' : arrives_in arr_seq j'.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k
arrives_in arr_seq j'
{ Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k
arrives_in arr_seq j'
by eapply arrives_in_task_arrivals_implies_arrived; eauto 2 . } Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k ARR' : arrives_in arr_seq j'
exists j_hp : Job,
arrives_in arr_seq j_hp /\
pending sched j_hp t &&
prior_jobs_complete arr_seq sched j_hp t /\
hep_job j_hp j
have PEND' : pending sched j' t.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k ARR' : arrives_in arr_seq j'
pending sched j' t
{ Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k ARR' : arrives_in arr_seq j'
pending sched j' t
apply /andP; split ; last by done .Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k ARR' : arrives_in arr_seq j'
has_arrived j' t
move : PEND => /andP [LE _].Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k ARR' : arrives_in arr_seq j' LE : has_arrived j t
has_arrived j' t
by unfold has_arrived in *; lia .
} Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat IHk : forall j : Job,
job_arrival j <= k ->
forall t : instant,
arrives_in arr_seq j ->
pending sched j t ->
exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp jj : Job t : instant ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 j' : Job IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k ARR' : arrives_in arr_seq j' PEND' : pending sched j' t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
pending sched j_hp t &&
prior_jobs_complete arr_seq sched j_hp t /\
hep_job j_hp j
specialize (IHk j' LE' t ARR' PEND').Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat t : instant j' : Job IHk : exists j_hp : Job,
arrives_in arr_seq j_hp /\
job_ready sched j_hp t /\ hep_job j_hp j'j : Job ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k ARR' : arrives_in arr_seq j' PEND' : pending sched j' t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
pending sched j_hp t &&
prior_jobs_complete arr_seq sched j_hp t /\
hep_job j_hp j
destruct IHk as [j'' [ARR'' [READY'' HEP'']]].Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat t : instant j', j'' : Job ARR'' : arrives_in arr_seq j'' READY'' : job_ready sched j'' t HEP'' : hep_job j'' j' j : Job ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k ARR' : arrives_in arr_seq j' PEND' : pending sched j' t
exists j_hp : Job,
arrives_in arr_seq j_hp /\
pending sched j_hp t &&
prior_jobs_complete arr_seq sched j_hp t /\
hep_job j_hp j
exists j'' ; repeat split ; auto .Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat t : instant j', j'' : Job ARR'' : arrives_in arr_seq j'' READY'' : job_ready sched j'' t HEP'' : hep_job j'' j' j : Job ARR : arrives_in arr_seq j PEND : pending sched j t EQ : job_arrival j = k.+1 IN : j'
\in task_arrivals_before arr_seq
(job_task j)
(job_arrival j) NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k ARR' : arrives_in arr_seq j' PEND' : pending sched j' t
hep_job j'' j
clear EQ; apply arrives_in_task_arrivals_implies_job_task in IN; move : IN => /eqP EQ.Job : JobType Task : TaskType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq H2 : FP_policy Task H_priority_is_reflexive : reflexive_priorities k : nat t : instant j', j'' : Job ARR'' : arrives_in arr_seq j'' READY'' : job_ready sched j'' t HEP'' : hep_job j'' j' j : Job ARR : arrives_in arr_seq j PEND : pending sched j t NCOMP : ~~ completed_by sched j' t LE' : job_arrival j' <= k ARR' : arrives_in arr_seq j' PEND' : pending sched j' t EQ : job_task j' = job_task j
hep_job j'' j
by rewrite /hep_job /FP_to_JLFP -EQ.
}
}
Qed .
End SequentialTasksReadiness .