Library prosa.analysis.facts.behavior.completion
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.behavior.service.
Require Export prosa.analysis.facts.behavior.arrivals.
Consider any job type,...
...any kind of processor model,...
...and a given schedule.
Let j be any job that is to be scheduled.
We prove that after job j completes, it remains completed.
Lemma completion_monotonic:
∀ t t',
t ≤ t' →
completed_by sched j t →
completed_by sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 342)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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.
move ⇒ t t' LE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 345)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 360)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t t',
t ≤ t' →
completed_by sched j t →
completed_by sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 342)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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.
move ⇒ t t' LE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 345)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 360)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We observe that being incomplete is the same as not having received
sufficient service yet...
Lemma less_service_than_cost_is_incomplete:
∀ t,
service sched j t < job_cost j
↔ ~~ completed_by sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 353)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
============================
forall t : instant,
service sched j t < job_cost j <-> ~~ completed_by sched j t
----------------------------------------------------------------------------- *)
Proof.
move⇒ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 354)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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 //].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
service sched j t < job_cost j
↔ ~~ completed_by sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 353)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
============================
forall t : instant,
service sched j t < job_cost j <-> ~~ completed_by sched j t
----------------------------------------------------------------------------- *)
Proof.
move⇒ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 354)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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 //].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
...which is also the same as having positive remaining cost.
Lemma incomplete_is_positive_remaining_cost:
∀ t,
~~ completed_by sched j t
↔ remaining_cost sched j t > 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 363)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
============================
forall t : instant,
~~ completed_by sched j t <-> 0 < remaining_cost sched j t
----------------------------------------------------------------------------- *)
Proof.
move⇒ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 364)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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 //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
~~ completed_by sched j t
↔ remaining_cost sched j t > 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 363)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
============================
forall t : instant,
~~ completed_by sched j t <-> 0 < remaining_cost sched j t
----------------------------------------------------------------------------- *)
Proof.
move⇒ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 364)
Job : JobType
H : JobCost Job
PState : Type
H0 : 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 //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Assume that completed jobs do not execute.
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:
∀ t,
service_at sched j t > 0 →
remaining_cost sched j t > 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
H_completed_jobs : completed_jobs_dont_execute sched
============================
forall t : instant,
0 < service_at sched j t -> 0 < remaining_cost sched j t
----------------------------------------------------------------------------- *)
Proof.
move⇒ t SERVICE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 378)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 400)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 401)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
service_at sched j t > 0 →
remaining_cost sched j t > 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
H_completed_jobs : completed_jobs_dont_execute sched
============================
forall t : instant,
0 < service_at sched j t -> 0 < remaining_cost sched j t
----------------------------------------------------------------------------- *)
Proof.
move⇒ t SERVICE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 378)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 400)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 401)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
Then a scheduled job has positive remaining cost.
Corollary scheduled_implies_positive_remaining_cost:
∀ t,
scheduled_at sched j t →
remaining_cost sched j t > 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 387)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
rewrite /scheduled_at ⇒ t SCHEDULED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
scheduled_at sched j t →
remaining_cost sched j t > 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 387)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
rewrite /scheduled_at ⇒ t SCHEDULED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We also prove that a completed job cannot be scheduled...
Lemma completed_implies_not_scheduled:
∀ t,
completed_by sched j t →
~~ scheduled_at sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
move⇒ t COMP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 398)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 403)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 425)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 426)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
completed_by sched j t →
~~ scheduled_at sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
move⇒ t COMP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 398)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 403)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 425)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 426)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
... and that a scheduled job cannot be completed.
Lemma scheduled_implies_not_completed:
∀ t,
scheduled_at sched j t →
~~ completed_by sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 405)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
move⇒ t SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 407)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 412)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 441)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End CompletionFacts.
∀ t,
scheduled_at sched j t →
~~ completed_by sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 405)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
move⇒ t SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 407)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 412)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 441)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
Consider any job type,...
...any kind of processor model,...
...and a given schedule.
Assume that completed jobs do not execute.
Let [j] be any job that is to be scheduled.
Assume that a scheduled job receives exactly one time unit of service.
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:
∀ t,
service sched j t ≤ job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 344)
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.
move⇒ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 345)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 355)
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 (succn t) <= job_cost j
----------------------------------------------------------------------------- *)
rewrite -service_last_plus_before.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
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].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 455)
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
subgoal 2 (ID 456) is:
service sched j t + service_at sched j t <= job_cost j
----------------------------------------------------------------------------- *)
- rewrite not_scheduled_implies_no_service;
first by rewrite addn0 EQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 469)
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
subgoal 2 (ID 456) is:
service sched j t + service_at sched j t <= job_cost j
----------------------------------------------------------------------------- *)
apply completed_implies_not_scheduled ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 482)
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
subgoal 2 (ID 456) is:
service sched j t + service_at sched j t <= job_cost j
----------------------------------------------------------------------------- *)
by rewrite /completed_by EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 456)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 517)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 526)
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
service sched j t ≤ job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 344)
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.
move⇒ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 345)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 355)
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 (succn t) <= job_cost j
----------------------------------------------------------------------------- *)
rewrite -service_last_plus_before.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
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].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 455)
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
subgoal 2 (ID 456) is:
service sched j t + service_at sched j t <= job_cost j
----------------------------------------------------------------------------- *)
- rewrite not_scheduled_implies_no_service;
first by rewrite addn0 EQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 469)
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
subgoal 2 (ID 456) is:
service sched j t + service_at sched j t <= job_cost j
----------------------------------------------------------------------------- *)
apply completed_implies_not_scheduled ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 482)
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
subgoal 2 (ID 456) is:
service sched j t + service_at sched j t <= job_cost j
----------------------------------------------------------------------------- *)
by rewrite /completed_by EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 456)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 517)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 526)
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
This lets us conclude that [service] and [remaining_cost] are complements
of one another.
Lemma service_cost_invariant:
∀ t,
(service sched j t) + (remaining_cost sched j t) = job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 357)
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.
move⇒ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 358)
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 371)
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
(service sched j t) + (remaining_cost sched j t) = job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 357)
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.
move⇒ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 358)
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 371)
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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:
∀ t t',
service_during sched j t t' ≤ job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
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.
move⇒ t t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 367)
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 399)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 418)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 430)
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t t',
service_during sched j t t' ≤ job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
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.
move⇒ t t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 367)
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 399)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 418)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 430)
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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:
∀ t,
~~ completed_by sched j t →
~~ completed_by sched j (t + remaining_cost sched j t - 1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 379)
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.
move⇒ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 380)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 421)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 452)
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).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 497)
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
subgoal 2 (ID 498) is:
service sched j t + remaining_cost sched j t - 1 < job_cost j
----------------------------------------------------------------------------- *)
- by rewrite -!addnBA //; rewrite leq_add2l; apply cumulative_service_le_delta; exact.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 498)
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 590)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 614)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 626)
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).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Section GuaranteedService.
∀ t,
~~ completed_by sched j t →
~~ completed_by sched j (t + remaining_cost sched j t - 1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 379)
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.
move⇒ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 380)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 421)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 452)
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).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 497)
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
subgoal 2 (ID 498) is:
service sched j t + remaining_cost sched j t - 1 < job_cost j
----------------------------------------------------------------------------- *)
- by rewrite -!addnBA //; rewrite leq_add2l; apply cumulative_service_le_delta; exact.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 498)
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 590)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 614)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 626)
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).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Section GuaranteedService.
Assume a scheduled job always receives some positive service.
Assume that jobs are not released early.
We show that if job j is scheduled, then it must be pending.
Lemma scheduled_implies_pending:
∀ t,
scheduled_at sched j t →
pending sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 395)
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.
move⇒ t SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 397)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 404)
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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 431)
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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End GuaranteedService.
End ServiceAndCompletionFacts.
∀ t,
scheduled_at sched j t →
pending sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 395)
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.
move⇒ t SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 397)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 404)
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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 431)
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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End GuaranteedService.
End ServiceAndCompletionFacts.
In this section, we establish facts that on jobs with non-zero costs that
must arrive to execute.
Consider any type of jobs with cost and arrival-time attributes,...
...any kind of processor model,...
...and a given schedule.
Let [j] be any job that is to be scheduled.
We assume that job [j] has positive cost, from which we can
infer that there always is a time in which [j] is pending, ...
...and that jobs must arrive to execute.
Then, we prove that the job with a positive cost
must be scheduled to be completed.
Lemma completed_implies_scheduled_before:
∀ t,
completed_by sched j t →
∃ t',
job_arrival j ≤ t' < t
∧ scheduled_at sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 350)
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 j
H_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.
rewrite /completed_by.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 357)
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 j
H_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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 359)
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 j
H_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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 369)
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 j
H_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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
completed_by sched j t →
∃ t',
job_arrival j ≤ t' < t
∧ scheduled_at sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 350)
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 j
H_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.
rewrite /completed_by.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 357)
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 j
H_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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 359)
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 j
H_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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 369)
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 j
H_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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 358)
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 j
H_jobs_must_arrive : jobs_must_arrive_to_execute sched
============================
pending sched j (job_arrival j)
----------------------------------------------------------------------------- *)
Proof.
rewrite /pending.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
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 j
H_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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 392)
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 j
H_jobs_must_arrive : jobs_must_arrive_to_execute sched
============================
~~ completed_by sched j (job_arrival j)
----------------------------------------------------------------------------- *)
rewrite /completed_by no_service_before_arrival // -ltnNge //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PositiveCost.
Section CompletedJobs.
pending sched j (job_arrival j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 358)
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 j
H_jobs_must_arrive : jobs_must_arrive_to_execute sched
============================
pending sched j (job_arrival j)
----------------------------------------------------------------------------- *)
Proof.
rewrite /pending.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
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 j
H_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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 392)
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 j
H_jobs_must_arrive : jobs_must_arrive_to_execute sched
============================
~~ completed_by sched j (job_arrival j)
----------------------------------------------------------------------------- *)
rewrite /completed_by no_service_before_arrival // -ltnNge //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PositiveCost.
Section CompletedJobs.
Consider any kinds of jobs and any kind of processor state.
Consider any schedule...
...and suppose that jobs have a cost, an arrival time, and a notion of
readiness.
We observe that a given job is ready only if it is also incomplete...
Lemma ready_implies_incomplete:
∀ j t, job_ready sched j t → ~~ completed_by sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 349)
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.
move⇒ j t READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 352)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 359)
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].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ j t, job_ready sched j t → ~~ completed_by sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 349)
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.
move⇒ j t READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 352)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 359)
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].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 360)
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.
rewrite /jobs_must_be_ready_to_execute /completed_jobs_dont_execute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 370)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 374)
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 t
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
move: (READY_IF_SCHED j t SCHED) ⇒ READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
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 t
j : 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
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 t
j : 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
jobs_must_be_ready_to_execute sched →
completed_jobs_dont_execute sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 360)
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.
rewrite /jobs_must_be_ready_to_execute /completed_jobs_dont_execute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 370)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 374)
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 t
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
move: (READY_IF_SCHED j t SCHED) ⇒ READY.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
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 t
j : 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
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 t
j : 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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 →
(∀ j t, service sched j t ≤ job_cost j) →
completed_jobs_dont_execute sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
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.
move⇒ IDEAL SERVICE_BOUND j t SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 382)
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 j
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
have UB := SERVICE_BOUND j t.+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 387)
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 j
j : Job
t : instant
SCHED : scheduled_at sched j t
UB : service sched j (succn t) <= job_cost j
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
have POS := IDEAL _ _ SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
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 j
j : Job
t : instant
SCHED : scheduled_at sched j t
UB : service sched j (succn t) <= 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 400)
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 j
j : Job
t : instant
SCHED : scheduled_at sched j t
UB : service sched j (succn t) <= job_cost j
POS : 0 < service_in j (sched t)
============================
service sched j t < service sched j (succn t)
----------------------------------------------------------------------------- *)
rewrite -service_last_plus_before /service_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 441)
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 j
j : Job
t : instant
SCHED : scheduled_at sched j t
UB : service sched j (succn t) <= 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End CompletedJobs.
ideal_progress_proc_model PState →
(∀ j t, service sched j t ≤ job_cost j) →
completed_jobs_dont_execute sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 376)
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.
move⇒ IDEAL SERVICE_BOUND j t SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 382)
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 j
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
have UB := SERVICE_BOUND j t.+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 387)
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 j
j : Job
t : instant
SCHED : scheduled_at sched j t
UB : service sched j (succn t) <= job_cost j
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
have POS := IDEAL _ _ SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
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 j
j : Job
t : instant
SCHED : scheduled_at sched j t
UB : service sched j (succn t) <= 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 400)
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 j
j : Job
t : instant
SCHED : scheduled_at sched j t
UB : service sched j (succn t) <= job_cost j
POS : 0 < service_in j (sched t)
============================
service sched j t < service sched j (succn t)
----------------------------------------------------------------------------- *)
rewrite -service_last_plus_before /service_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 441)
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 j
j : Job
t : instant
SCHED : scheduled_at sched j t
UB : service sched j (succn t) <= 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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End CompletedJobs.