Built with
Alectryon , running Coq+SerAPI v8.14.0+0.14.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.facts.behavior.service.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.facts.behavior.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]
Require Export prosa.analysis.definitions.schedule_prefix.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.definitions.job_properties.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]
(** * Completion *)
(** In this file, we establish basic facts about job completions. *)
Section CompletionFacts .
(** Consider any job type,...*)
Context {Job : JobType}.
Context `{JobCost Job}.
Context `{JobArrival Job}.
(** ...any kind of processor model,... *)
Context {PState : Type }.
Context `{ProcessorState Job PState}.
(** ...and a given schedule. *)
Variable sched : schedule PState.
(** Let [j] be any job that is to be scheduled. *)
Variable j : Job.
(** We prove that after job [j] completes, it remains completed. *)
Lemma completion_monotonic :
forall t t' ,
t <= t' ->
completed_by sched j t ->
completed_by sched j t'.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job
forall t t' : nat,
t <= t' ->
completed_by sched j t -> completed_by sched j t'
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job
forall t t' : nat,
t <= t' ->
completed_by sched j t -> completed_by sched j t'
move => t t' LE.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job t, t' : nat LE : t <= t'
completed_by sched j t -> completed_by sched j t'
rewrite /completed_by /service => COMP.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job t, t' : nat LE : t <= t' COMP : job_cost j <= service_during sched j 0 t
job_cost j <= service_during sched j 0 t'
apply leq_trans with (n := service_during sched j 0 t); auto .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job t, t' : nat LE : t <= t' COMP : job_cost j <= service_during sched j 0 t
service_during sched j 0 t <=
service_during sched j 0 t'
by apply service_monotonic.
Qed .
(** We prove that if [j] is not completed by [t'], then it's also not
completed by any earlier instant. *)
Lemma incompletion_monotonic :
forall t t' ,
t <= t' ->
~~ completed_by sched j t' ->
~~ completed_by sched j t.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job
forall t t' : nat,
t <= t' ->
~~ completed_by sched j t' ->
~~ completed_by sched j t
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job
forall t t' : nat,
t <= t' ->
~~ completed_by sched j t' ->
~~ completed_by sched j t
move => t t' LE.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job t, t' : nat LE : t <= t'
~~ completed_by sched j t' ->
~~ completed_by sched j t
apply contra.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job t, t' : nat LE : t <= t'
completed_by sched j t -> completed_by sched j t'
by apply completion_monotonic.
Qed .
(** We observe that being incomplete is the same as not having received
sufficient service yet... *)
Lemma less_service_than_cost_is_incomplete :
forall t ,
service sched j t < job_cost j
<-> ~~ completed_by sched j t.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
service sched j t < job_cost j <->
~~ completed_by sched j t
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
service sched j t < job_cost j <->
~~ completed_by sched j t
move => t.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job t : instant
service sched j t < job_cost j <->
~~ completed_by sched j t
by split ; rewrite /completed_by; [rewrite -ltnNge // | rewrite ltnNge //].
Qed .
(** ...which is also the same as having positive remaining cost. *)
Lemma incomplete_is_positive_remaining_cost :
forall t ,
~~ completed_by sched j t
<-> remaining_cost sched j t > 0 .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
~~ completed_by sched j t <->
0 < remaining_cost sched j t
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
~~ completed_by sched j t <->
0 < remaining_cost sched j t
move => t.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job t : instant
~~ completed_by sched j t <->
0 < remaining_cost sched j t
by split ; rewrite /remaining_cost -less_service_than_cost_is_incomplete subn_gt0 //.
Qed .
(** Trivially, it follows that an incomplete job has a positive cost. *)
Corollary incomplete_implies_positive_cost :
forall t ,
~~ completed_by sched j t ->
job_cost_positive j.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
~~ completed_by sched j t -> job_cost_positive j
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job
forall t : instant,
~~ completed_by sched j t -> job_cost_positive j
move => t INCOMP.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job t : instant INCOMP : ~~ completed_by sched j t
job_cost_positive j
apply : (ltn_leq_trans _);
last by apply leq_subr.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job t : instant INCOMP : ~~ completed_by sched j t
0 < job_cost j - ?m
apply incomplete_is_positive_remaining_cost.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job t : instant INCOMP : ~~ completed_by sched j t
~~ completed_by sched j ?t
exact INCOMP.
Qed .
(** In the remainder of this section, we assume that schedules are
"well-formed": jobs are scheduled neither before their arrival
nor after their completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs : completed_jobs_dont_execute sched.
(** We observe that a job that is completed at the instant of its
arrival has a cost of zero. *)
Lemma completed_on_arrival_implies_zero_cost :
completed_by sched j (job_arrival j) ->
job_cost j = 0 .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched
completed_by sched j (job_arrival j) -> job_cost j = 0
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched
completed_by sched j (job_arrival j) -> job_cost j = 0
by rewrite /completed_by no_service_before_arrival // leqn0 => /eqP.
Qed .
(** Further, we note that if a job receives service at some time t, then its
remaining cost at this time is positive. *)
Lemma serviced_implies_positive_remaining_cost :
forall t ,
service_at sched j t > 0 ->
remaining_cost sched j t > 0 .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched
forall t : instant,
0 < service_at sched j t ->
0 < remaining_cost sched j t
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched
forall t : instant,
0 < service_at sched j t ->
0 < remaining_cost sched j t
move => t SERVICE.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched t : instant SERVICE : 0 < service_at sched j t
0 < remaining_cost sched j t
rewrite -incomplete_is_positive_remaining_cost -less_service_than_cost_is_incomplete.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched t : instant SERVICE : 0 < service_at sched j t
service sched j t < job_cost j
apply H_completed_jobs.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched t : instant SERVICE : 0 < service_at sched j t
scheduled_at sched j t
by apply service_at_implies_scheduled_at.
Qed .
(** Consequently, if we have a have processor model where scheduled jobs
necessarily receive service, we can conclude that scheduled jobs have
remaining positive cost. *)
(** Assume a scheduled job always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced : ideal_progress_proc_model PState.
(** Then a scheduled job has positive remaining cost. *)
Corollary scheduled_implies_positive_remaining_cost :
forall t ,
scheduled_at sched j t ->
remaining_cost sched j t > 0 .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : instant,
scheduled_at sched j t -> 0 < remaining_cost sched j t
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : instant,
scheduled_at sched j t -> 0 < remaining_cost sched j t
rewrite /scheduled_at => t SCHEDULED.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant SCHEDULED : scheduled_in j (sched t)
0 < remaining_cost sched j t
by apply : serviced_implies_positive_remaining_cost; rewrite /service_at; apply : H_scheduled_implies_serviced.
Qed .
(** We also prove that a completed job cannot be scheduled... *)
Lemma completed_implies_not_scheduled :
forall t ,
completed_by sched j t ->
~~ scheduled_at sched j t.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : instant,
completed_by sched j t -> ~~ scheduled_at sched j t
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : instant,
completed_by sched j t -> ~~ scheduled_at sched j t
move => t COMP.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant COMP : completed_by sched j t
~~ scheduled_at sched j t
apply contra with (b := ~~ completed_by sched j t);
last by apply /negPn.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant COMP : completed_by sched j t
scheduled_at sched j t -> ~~ completed_by sched j t
move => SCHED.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant COMP : completed_by sched j t SCHED : scheduled_at sched j t
~~ completed_by sched j t
move : (H_completed_jobs j t SCHED).Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant COMP : completed_by sched j t SCHED : scheduled_at sched j t
service sched j t < job_cost j ->
~~ completed_by sched j t
by rewrite less_service_than_cost_is_incomplete.
Qed .
(** ... and that a scheduled job cannot be completed. *)
Lemma scheduled_implies_not_completed :
forall t ,
scheduled_at sched j t ->
~~ completed_by sched j t.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : instant,
scheduled_at sched j t -> ~~ completed_by sched j t
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState
forall t : instant,
scheduled_at sched j t -> ~~ completed_by sched j t
move => t SCHED.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant SCHED : scheduled_at sched j t
~~ completed_by sched j t
have REMPOS := scheduled_implies_positive_remaining_cost t SCHED.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant SCHED : scheduled_at sched j t REMPOS : 0 < remaining_cost sched j t
~~ completed_by sched j t
rewrite /remaining_cost subn_gt0 in REMPOS.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched H_completed_jobs : completed_jobs_dont_execute sched H_scheduled_implies_serviced : ideal_progress_proc_model
PState t : instant SCHED : scheduled_at sched j t REMPOS : service sched j t < job_cost j
~~ completed_by sched j t
by rewrite -less_service_than_cost_is_incomplete.
Qed .
End CompletionFacts .
(** In this section, we establish some facts that are really about service,
but are also related to completion and rely on some of the above lemmas.
Hence they are in this file rather than in the service facts file. *)
Section ServiceAndCompletionFacts .
(** Consider any job type,...*)
Context {Job : JobType}.
Context `{JobCost Job}.
(** ...any kind of processor model,... *)
Context {PState : Type }.
Context `{ProcessorState Job PState}.
(** ...and a given schedule. *)
Variable sched : schedule PState.
(** Assume that completed jobs do not execute. *)
Hypothesis H_completed_jobs :
completed_jobs_dont_execute sched.
(** Let [j] be any job that is to be scheduled. *)
Variable j : Job.
(** Assume that a scheduled job receives exactly one time unit of service. *)
Hypothesis H_unit_service : unit_service_proc_model PState.
(** To begin with, we establish that the cumulative service never exceeds a
job's total cost if service increases only by one at each step since
completed jobs don't execute. *)
Lemma service_at_most_cost :
forall t ,
service sched j t <= job_cost j.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState
forall t : instant, service sched j t <= job_cost j
Proof .Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState
forall t : instant, service sched j t <= job_cost j
move => t.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant
service sched j t <= job_cost j
elim : t => [|t]; first by rewrite service0.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : nat
service sched j t <= job_cost j ->
service sched j t.+1 <= job_cost j
rewrite -service_last_plus_before.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : nat
service sched j t <= job_cost j ->
service sched j t + service_at sched j t <= job_cost j
rewrite leq_eqVlt => /orP [/eqP EQ|LT].Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : nat EQ : service sched j t = job_cost j
service sched j t + service_at sched j t <= job_cost j
- Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : nat EQ : service sched j t = job_cost j
service sched j t + service_at sched j t <= job_cost j
rewrite not_scheduled_implies_no_service;
first by rewrite addn0 EQ.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : nat EQ : service sched j t = job_cost j
~~ scheduled_at sched j t
apply completed_implies_not_scheduled => //.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : nat EQ : service sched j t = job_cost j
completed_by sched j t
by rewrite /completed_by EQ.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : nat LT : service sched j t < job_cost j
service sched j t + service_at sched j t <= job_cost j
- Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : nat LT : service sched j t < job_cost j
service sched j t + service_at sched j t <= job_cost j
apply leq_trans with (n := service sched j t + 1 );
last by rewrite addn1.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : nat LT : service sched j t < job_cost j
service sched j t + service_at sched j t <=
service sched j t + 1
rewrite leq_add2l.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : nat LT : service sched j t < job_cost j
service_at sched j t <= 1
by apply H_unit_service.
Qed .
(** This lets us conclude that [service] and [remaining_cost] are complements
of one another. *)
Lemma service_cost_invariant :
forall t ,
(service sched j t) + (remaining_cost sched j t) = job_cost j.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState
forall t : instant,
service sched j t + remaining_cost sched j t =
job_cost j
Proof .Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState
forall t : instant,
service sched j t + remaining_cost sched j t =
job_cost j
move => t.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant
service sched j t + remaining_cost sched j t =
job_cost j
rewrite /remaining_cost subnKC //.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant
service sched j t <= job_cost j
by apply service_at_most_cost.
Qed .
(** We show that the service received by job [j] in any interval is no larger
than its cost. *)
Lemma cumulative_service_le_job_cost :
forall t t' ,
service_during sched j t t' <= job_cost j.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState
forall t t' : instant,
service_during sched j t t' <= job_cost j
Proof .Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState
forall t t' : instant,
service_during sched j t t' <= job_cost j
move => t t'.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t, t' : instant
service_during sched j t t' <= job_cost j
case /orP: (leq_total t t') => [tt'|tt']; last by rewrite service_during_geq //.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t, t' : instant tt' : t <= t'
service_during sched j t t' <= job_cost j
apply leq_trans with (n := service sched j t'); last by apply : service_at_most_cost.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t, t' : instant tt' : t <= t'
service_during sched j t t' <= service sched j t'
rewrite /service.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t, t' : instant tt' : t <= t'
service_during sched j t t' <=
service_during sched j 0 t'
rewrite -(service_during_cat sched j 0 t t') // leq_addl //.
Qed .
(** If a job isn't complete at time [t], it can't be completed at time [t +
remaining_cost j t - 1]. *)
Lemma job_doesnt_complete_before_remaining_cost :
forall t ,
~~ completed_by sched j t ->
~~ completed_by sched j (t + remaining_cost sched j t - 1 ).Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState
forall t : instant,
~~ completed_by sched j t ->
~~
completed_by sched j
(t + remaining_cost sched j t - 1 )
Proof .Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState
forall t : instant,
~~ completed_by sched j t ->
~~
completed_by sched j
(t + remaining_cost sched j t - 1 )
move => t.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant
~~ completed_by sched j t ->
~~
completed_by sched j
(t + remaining_cost sched j t - 1 )
rewrite incomplete_is_positive_remaining_cost => REMCOST.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant REMCOST : 0 < remaining_cost sched j t
~~
completed_by sched j
(t + remaining_cost sched j t - 1 )
rewrite -less_service_than_cost_is_incomplete -(service_cat sched j t);
last by rewrite -addnBA //; apply : leq_addr.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant REMCOST : 0 < remaining_cost sched j t
service sched j t +
service_during sched j t
(t + remaining_cost sched j t - 1 ) < job_cost j
apply leq_ltn_trans with (n := service sched j t + remaining_cost sched j t - 1 ).Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant REMCOST : 0 < remaining_cost sched j t
service sched j t +
service_during sched j t
(t + remaining_cost sched j t - 1 ) <=
service sched j t + remaining_cost sched j t - 1
- Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant REMCOST : 0 < remaining_cost sched j t
service sched j t +
service_during sched j t
(t + remaining_cost sched j t - 1 ) <=
service sched j t + remaining_cost sched j t - 1
by rewrite -!addnBA //; rewrite leq_add2l; apply cumulative_service_le_delta; exact .Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant REMCOST : 0 < remaining_cost sched j t
service sched j t + remaining_cost sched j t - 1 <
job_cost j
- Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant REMCOST : 0 < remaining_cost sched j t
service sched j t + remaining_cost sched j t - 1 <
job_cost j
rewrite service_cost_invariant // -subn_gt0 subKn //.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant REMCOST : 0 < remaining_cost sched j t
0 < job_cost j
move : REMCOST.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant
0 < remaining_cost sched j t -> 0 < job_cost j
rewrite /remaining_cost subn_gt0 => SERVICE.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState t : instant SERVICE : service sched j t < job_cost j
0 < job_cost j
by apply leq_ltn_trans with (n := service sched j t).
Qed .
Section GuaranteedService .
(** Assume a scheduled job always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced : ideal_progress_proc_model PState.
(** Assume that jobs are not released early. *)
Context `{JobArrival Job}.
Hypothesis H_jobs_must_arrive : jobs_must_arrive_to_execute sched.
(** We show that if job j is scheduled, then it must be pending. *)
Lemma scheduled_implies_pending :
forall t ,
scheduled_at sched j t ->
pending sched j t.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState H_scheduled_implies_serviced : ideal_progress_proc_model
PState H1 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : instant,
scheduled_at sched j t -> pending sched j t
Proof .Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState H_scheduled_implies_serviced : ideal_progress_proc_model
PState H1 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : instant,
scheduled_at sched j t -> pending sched j t
move => t SCHED.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState H_scheduled_implies_serviced : ideal_progress_proc_model
PState H1 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant SCHED : scheduled_at sched j t
pending sched j t
rewrite /pending.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState H_scheduled_implies_serviced : ideal_progress_proc_model
PState H1 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant SCHED : scheduled_at sched j t
has_arrived j t && ~~ completed_by sched j t
apply /andP; split ;
first by apply : H_jobs_must_arrive => //.Job : JobType H : JobCost Job PState : Type H0 : ProcessorState Job PState sched : schedule PState H_completed_jobs : completed_jobs_dont_execute sched j : Job H_unit_service : unit_service_proc_model PState H_scheduled_implies_serviced : ideal_progress_proc_model
PState H1 : JobArrival Job H_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant SCHED : scheduled_at sched j t
~~ completed_by sched j t
by apply : scheduled_implies_not_completed => //.
Qed .
End GuaranteedService .
End ServiceAndCompletionFacts .
(** In this section, we establish facts that on jobs with non-zero costs that
must arrive to execute. *)
Section PositiveCost .
(** Consider any type of jobs with cost and arrival-time attributes,...*)
Context {Job : JobType}.
Context `{JobCost Job}.
Context `{JobArrival Job}.
(** ...any kind of processor model,... *)
Context {PState : Type }.
Context `{ProcessorState Job PState}.
(** ...and a given schedule. *)
Variable sched : schedule PState.
(** Let [j] be any job that is to be scheduled. *)
Variable j : Job.
(** We assume that job [j] has positive cost, from which we can
infer that there always is a time in which [j] is pending, ... *)
Hypothesis H_positive_cost : job_cost j > 0 .
(** ...and that jobs must arrive to execute. *)
Hypothesis H_jobs_must_arrive :
jobs_must_arrive_to_execute sched.
(** Then, we prove that the job with a positive cost
must be scheduled to be completed. *)
Lemma completed_implies_scheduled_before :
forall t ,
completed_by sched j t ->
exists t' ,
job_arrival j <= t' < t
/\ scheduled_at sched j t'.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_positive_cost : 0 < job_cost jH_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : instant,
completed_by sched j t ->
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_positive_cost : 0 < job_cost jH_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : instant,
completed_by sched j t ->
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
rewrite /completed_by.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_positive_cost : 0 < job_cost jH_jobs_must_arrive : jobs_must_arrive_to_execute sched
forall t : instant,
job_cost j <= service sched j t ->
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
move => t COMPLETE.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_positive_cost : 0 < job_cost jH_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant COMPLETE : job_cost j <= service sched j t
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
have POSITIVE_SERVICE: 0 < service sched j t
by apply leq_trans with (n := job_cost j); auto .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_positive_cost : 0 < job_cost jH_jobs_must_arrive : jobs_must_arrive_to_execute sched t : instant COMPLETE : job_cost j <= service sched j t POSITIVE_SERVICE : 0 < service sched j t
exists t' : nat,
job_arrival j <= t' < t /\ scheduled_at sched j t'
by apply : positive_service_implies_scheduled_since_arrival; assumption .
Qed .
(** We also prove that the job is pending at the moment of its arrival. *)
Lemma job_pending_at_arrival :
pending sched j (job_arrival j).Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_positive_cost : 0 < job_cost jH_jobs_must_arrive : jobs_must_arrive_to_execute sched
pending sched j (job_arrival j)
Proof .Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_positive_cost : 0 < job_cost jH_jobs_must_arrive : jobs_must_arrive_to_execute sched
pending sched j (job_arrival j)
rewrite /pending.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_positive_cost : 0 < job_cost jH_jobs_must_arrive : jobs_must_arrive_to_execute sched
has_arrived j (job_arrival j) &&
~~ completed_by sched j (job_arrival j)
apply /andP; split ;
first by rewrite /has_arrived //.Job : JobType H : JobCost Job H0 : JobArrival Job PState : Type H1 : ProcessorState Job PState sched : schedule PState j : Job H_positive_cost : 0 < job_cost jH_jobs_must_arrive : jobs_must_arrive_to_execute sched
~~ completed_by sched j (job_arrival j)
rewrite /completed_by no_service_before_arrival // -ltnNge //.
Qed .
End PositiveCost .
Section CompletedJobs .
(** Consider any kinds of jobs and any kind of processor state. *)
Context {Job : JobType} {PState : Type }.
Context `{ProcessorState Job PState}.
(** Consider any schedule... *)
Variable sched : schedule PState.
(** ...and suppose that jobs have a cost, an arrival time, and a notion of
readiness. *)
Context `{JobCost Job}.
Context `{JobArrival Job}.
Context `{JobReady Job PState}.
(** We observe that a given job is ready only if it is also incomplete... *)
Lemma ready_implies_incomplete :
forall j t , job_ready sched j t -> ~~ completed_by sched j t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState
forall (j : Job) (t : instant),
job_ready sched j t -> ~~ completed_by sched j t
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState
forall (j : Job) (t : instant),
job_ready sched j t -> ~~ completed_by sched j t
move => j t READY.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState j : Job t : instant READY : job_ready sched j t
~~ completed_by sched j t
move : (any_ready_job_is_pending sched j t READY).Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState j : Job t : instant READY : job_ready sched j t
pending sched j t -> ~~ completed_by sched j t
by rewrite /pending => /andP [_ INCOMPLETE].
Qed .
(** ...and lift this observation also to the level of whole schedules. *)
Lemma completed_jobs_are_not_ready :
jobs_must_be_ready_to_execute sched ->
completed_jobs_dont_execute sched.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState
jobs_must_be_ready_to_execute sched ->
completed_jobs_dont_execute sched
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState
jobs_must_be_ready_to_execute sched ->
completed_jobs_dont_execute sched
rewrite /jobs_must_be_ready_to_execute /completed_jobs_dont_execute.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState
(forall (j : Job) (t : instant),
scheduled_at sched j t -> job_ready sched j t) ->
forall (j : Job) (t : instant),
scheduled_at sched j t ->
service sched j t < job_cost j
move => READY_IF_SCHED j t SCHED.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState READY_IF_SCHED : forall (j : Job) (t : instant),
scheduled_at sched j t ->
job_ready sched j tj : Job t : instant SCHED : scheduled_at sched j t
service sched j t < job_cost j
move : (READY_IF_SCHED j t SCHED) => READY.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState READY_IF_SCHED : forall (j : Job) (t : instant),
scheduled_at sched j t ->
job_ready sched j tj : Job t : instant SCHED : scheduled_at sched j t READY : job_ready sched j t
service sched j t < job_cost j
rewrite less_service_than_cost_is_incomplete.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState READY_IF_SCHED : forall (j : Job) (t : instant),
scheduled_at sched j t ->
job_ready sched j tj : Job t : instant SCHED : scheduled_at sched j t READY : job_ready sched j t
~~ completed_by sched j t
by apply ready_implies_incomplete.
Qed .
(** Furthermore, in a valid schedule, completed jobs don't execute. *)
Corollary valid_schedule_implies_completed_jobs_dont_execute :
forall arr_seq ,
valid_schedule sched arr_seq ->
completed_jobs_dont_execute sched.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
completed_jobs_dont_execute sched
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
completed_jobs_dont_execute sched
move => arr_seq [??].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState arr_seq : arrival_sequence Job _a_ : jobs_come_from_arrival_sequence sched arr_seq _b_ : jobs_must_be_ready_to_execute sched
completed_jobs_dont_execute sched
by apply completed_jobs_are_not_ready.
Qed .
(** We further observe that completed jobs don't execute if scheduled jobs
always receive non-zero service and cumulative service never exceeds job
costs. *)
Lemma ideal_progress_completed_jobs :
ideal_progress_proc_model PState ->
(forall j t , service sched j t <= job_cost j) ->
completed_jobs_dont_execute sched.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState
ideal_progress_proc_model PState ->
(forall (j : Job) (t : instant),
service sched j t <= job_cost j) ->
completed_jobs_dont_execute sched
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState
ideal_progress_proc_model PState ->
(forall (j : Job) (t : instant),
service sched j t <= job_cost j) ->
completed_jobs_dont_execute sched
move => IDEAL SERVICE_BOUND j t SCHED.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState IDEAL : ideal_progress_proc_model PState SERVICE_BOUND : forall (j : Job) (t : instant),
service sched j t <= job_cost jj : Job t : instant SCHED : scheduled_at sched j t
service sched j t < job_cost j
have UB := SERVICE_BOUND j t.+1 .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState IDEAL : ideal_progress_proc_model PState SERVICE_BOUND : forall (j : Job) (t : instant),
service sched j t <= job_cost jj : Job t : instant SCHED : scheduled_at sched j t UB : service sched j t.+1 <= job_cost j
service sched j t < job_cost j
have POS := IDEAL _ _ SCHED.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState IDEAL : ideal_progress_proc_model PState SERVICE_BOUND : forall (j : Job) (t : instant),
service sched j t <= job_cost jj : Job t : instant SCHED : scheduled_at sched j t UB : service sched j t.+1 <= job_cost j POS : 0 < service_in j (sched t)
service sched j t < job_cost j
apply ltn_leq_trans with (n := service sched j t.+1 ) => //.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState IDEAL : ideal_progress_proc_model PState SERVICE_BOUND : forall (j : Job) (t : instant),
service sched j t <= job_cost jj : Job t : instant SCHED : scheduled_at sched j t UB : service sched j t.+1 <= job_cost j POS : 0 < service_in j (sched t)
service sched j t < service sched j t.+1
rewrite -service_last_plus_before /service_at.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState IDEAL : ideal_progress_proc_model PState SERVICE_BOUND : forall (j : Job) (t : instant),
service sched j t <= job_cost jj : Job t : instant SCHED : scheduled_at sched j t UB : service sched j t.+1 <= job_cost j POS : 0 < service_in j (sched t)
service sched j t <
service sched j t + service_in j (sched t)
by rewrite -{1 }(addn0 (service sched j t)) ltn_add2l.
Qed .
End CompletedJobs .
(** We add the above lemma into a "Hint Database" basic_facts, so Coq
will be able to apply it automatically. *)
Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_facts.
(** Next, we relate the completion of jobs in schedules with identical prefixes. *)
Section CompletionInTwoSchedules .
(** Consider any processor model and any type of jobs with costs, arrival times, and a notion of readiness. *)
Context {PState : Type } {Job : JobType} `{ProcessorState Job PState} `{JobReady Job PState}.
(** If two schedules share a common prefix, then (in the prefix) jobs
complete in one schedule iff they complete in the other. *)
Lemma identical_prefix_completed_by :
forall sched1 sched2 h ,
identical_prefix sched1 sched2 h ->
forall j t ,
t <= h ->
completed_by sched1 j t = completed_by sched2 j t.PState : Type Job : JobType H, H0 : ProcessorState Job PState H1 : JobCost Job H2 : JobArrival Job H3 : JobReady Job PState
forall (sched1 sched2 : schedule PState) (h : instant),
identical_prefix sched1 sched2 h ->
forall (j : Job) (t : nat),
t <= h ->
completed_by sched1 j t = completed_by sched2 j t
Proof .PState : Type Job : JobType H, H0 : ProcessorState Job PState H1 : JobCost Job H2 : JobArrival Job H3 : JobReady Job PState
forall (sched1 sched2 : schedule PState) (h : instant),
identical_prefix sched1 sched2 h ->
forall (j : Job) (t : nat),
t <= h ->
completed_by sched1 j t = completed_by sched2 j t
move => sched1 sched2 h PREFIX j t LE_h.PState : Type Job : JobType H, H0 : ProcessorState Job PState H1 : JobCost Job H2 : JobArrival Job H3 : JobReady Job PState sched1, sched2 : schedule PState h : instant PREFIX : identical_prefix sched1 sched2 h j : Job t : nat LE_h : t <= h
completed_by sched1 j t = completed_by sched2 j t
rewrite /completed_by.PState : Type Job : JobType H, H0 : ProcessorState Job PState H1 : JobCost Job H2 : JobArrival Job H3 : JobReady Job PState sched1, sched2 : schedule PState h : instant PREFIX : identical_prefix sched1 sched2 h j : Job t : nat LE_h : t <= h
(job_cost j <= service sched1 j t) =
(job_cost j <= service sched2 j t)
rewrite (identical_prefix_service sched1 sched2) //.PState : Type Job : JobType H, H0 : ProcessorState Job PState H1 : JobCost Job H2 : JobArrival Job H3 : JobReady Job PState sched1, sched2 : schedule PState h : instant PREFIX : identical_prefix sched1 sched2 h j : Job t : nat LE_h : t <= h
identical_prefix sched1 sched2 t
now apply (identical_prefix_inclusion _ _ h).
Qed .
(** For convenience, we restate the previous lemma in terms of [pending]. *)
Corollary identical_prefix_pending :
forall sched1 sched2 h ,
identical_prefix sched1 sched2 h ->
forall j t ,
t <= h ->
pending sched1 j t = pending sched2 j t.PState : Type Job : JobType H, H0 : ProcessorState Job PState H1 : JobCost Job H2 : JobArrival Job H3 : JobReady Job PState
forall (sched1 sched2 : schedule PState) (h : instant),
identical_prefix sched1 sched2 h ->
forall (j : Job) (t : nat),
t <= h -> pending sched1 j t = pending sched2 j t
Proof .PState : Type Job : JobType H, H0 : ProcessorState Job PState H1 : JobCost Job H2 : JobArrival Job H3 : JobReady Job PState
forall (sched1 sched2 : schedule PState) (h : instant),
identical_prefix sched1 sched2 h ->
forall (j : Job) (t : nat),
t <= h -> pending sched1 j t = pending sched2 j t
move => sched1 sched2 h PREFIX j t LE_h.PState : Type Job : JobType H, H0 : ProcessorState Job PState H1 : JobCost Job H2 : JobArrival Job H3 : JobReady Job PState sched1, sched2 : schedule PState h : instant PREFIX : identical_prefix sched1 sched2 h j : Job t : nat LE_h : t <= h
pending sched1 j t = pending sched2 j t
now rewrite /pending (identical_prefix_completed_by _ sched2 h).
Qed .
End CompletionInTwoSchedules .