Library prosa.analysis.facts.behavior.deadlines
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.behavior.completion.
Consider any given type of jobs with costs and deadlines...
... any given type of processor states.
We begin with schedules / processor models in which scheduled jobs
always receive service.
Consider a given reference schedule...
...in which complete jobs don't execute...
...and scheduled jobs always receive service.
We observe that, if a job is known to meet its deadline, then
its deadline must be later than any point at which it is
scheduled. That is, if a job that meets its deadline is
scheduled at time t, we may conclude that its deadline is at a
time later than t.
Lemma scheduled_at_implies_later_deadline:
∀ j t,
job_meets_deadline sched j →
scheduled_at sched j t →
t < job_deadline j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 53)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
============================
forall (j : Job) (t : instant),
job_meets_deadline sched j -> scheduled_at sched j t -> t < job_deadline j
----------------------------------------------------------------------------- *)
Proof.
move⇒ j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 55)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
============================
job_meets_deadline sched j -> scheduled_at sched j t -> t < job_deadline j
----------------------------------------------------------------------------- *)
rewrite /job_meets_deadline ⇒ COMP SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j (job_deadline j)
SCHED : scheduled_at sched j t
============================
t < job_deadline j
----------------------------------------------------------------------------- *)
case: (boolP (t < job_deadline j)) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 82)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j (job_deadline j)
SCHED : scheduled_at sched j t
============================
~~ (t < job_deadline j) -> false
----------------------------------------------------------------------------- *)
rewrite -leqNgt ⇒ AFTER_DL.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 112)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j (job_deadline j)
SCHED : scheduled_at sched j t
AFTER_DL : job_deadline j <= t
============================
false
----------------------------------------------------------------------------- *)
apply completion_monotonic with (t' := t) in COMP ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 117)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j t
SCHED : scheduled_at sched j t
AFTER_DL : job_deadline j <= t
============================
false
----------------------------------------------------------------------------- *)
apply scheduled_implies_not_completed in SCHED ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 146)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j t
SCHED : ~~ completed_by sched j t
AFTER_DL : job_deadline j <= t
============================
false
----------------------------------------------------------------------------- *)
move/negP in SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 217)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j t
AFTER_DL : job_deadline j <= t
SCHED : ~ completed_by sched j t
============================
false
----------------------------------------------------------------------------- *)
contradiction.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End IdealProgressSchedules.
∀ j t,
job_meets_deadline sched j →
scheduled_at sched j t →
t < job_deadline j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 53)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
============================
forall (j : Job) (t : instant),
job_meets_deadline sched j -> scheduled_at sched j t -> t < job_deadline j
----------------------------------------------------------------------------- *)
Proof.
move⇒ j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 55)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
============================
job_meets_deadline sched j -> scheduled_at sched j t -> t < job_deadline j
----------------------------------------------------------------------------- *)
rewrite /job_meets_deadline ⇒ COMP SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j (job_deadline j)
SCHED : scheduled_at sched j t
============================
t < job_deadline j
----------------------------------------------------------------------------- *)
case: (boolP (t < job_deadline j)) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 82)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j (job_deadline j)
SCHED : scheduled_at sched j t
============================
~~ (t < job_deadline j) -> false
----------------------------------------------------------------------------- *)
rewrite -leqNgt ⇒ AFTER_DL.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 112)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j (job_deadline j)
SCHED : scheduled_at sched j t
AFTER_DL : job_deadline j <= t
============================
false
----------------------------------------------------------------------------- *)
apply completion_monotonic with (t' := t) in COMP ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 117)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j t
SCHED : scheduled_at sched j t
AFTER_DL : job_deadline j <= t
============================
false
----------------------------------------------------------------------------- *)
apply scheduled_implies_not_completed in SCHED ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 146)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j t
SCHED : ~~ completed_by sched j t
AFTER_DL : job_deadline j <= t
============================
false
----------------------------------------------------------------------------- *)
move/negP in SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 217)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched : schedule PState
H_completed_jobs : completed_jobs_dont_execute sched
H_scheduled_implies_serviced : ideal_progress_proc_model PState
j : Job
t : instant
COMP : completed_by sched j t
AFTER_DL : job_deadline j <= t
SCHED : ~ completed_by sched j t
============================
false
----------------------------------------------------------------------------- *)
contradiction.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End IdealProgressSchedules.
In the following section, we observe that it is sufficient to
establish that service is invariant across two schedules at a
job's deadline to establish that it either meets its deadline in
both schedules or none.
Consider any two schedules [sched] and [sched'].
We observe that, if the service is invariant at the time of a
job's absolute deadline, and if the job meets its deadline in one of the schedules,
then it meets its deadline also in the other schedule.
Lemma service_invariant_implies_deadline_met:
∀ j,
service sched j (job_deadline j) = service sched' j (job_deadline j) →
(job_meets_deadline sched j ↔ job_meets_deadline sched' j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched, sched' : schedule PState
============================
forall j : Job,
service sched j (job_deadline j) = service sched' j (job_deadline j) ->
job_meets_deadline sched j <-> job_meets_deadline sched' j
----------------------------------------------------------------------------- *)
Proof.
move⇒ j SERVICE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched, sched' : schedule PState
j : Job
SERVICE : service sched j (job_deadline j) =
service sched' j (job_deadline j)
============================
job_meets_deadline sched j <-> job_meets_deadline sched' j
----------------------------------------------------------------------------- *)
split;
by rewrite /job_meets_deadline /completed_by -SERVICE.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End EqualProgress.
End DeadlineFacts.
∀ j,
service sched j (job_deadline j) = service sched' j (job_deadline j) →
(job_meets_deadline sched j ↔ job_meets_deadline sched' j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched, sched' : schedule PState
============================
forall j : Job,
service sched j (job_deadline j) = service sched' j (job_deadline j) ->
job_meets_deadline sched j <-> job_meets_deadline sched' j
----------------------------------------------------------------------------- *)
Proof.
move⇒ j SERVICE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
PState : eqType
H1 : ProcessorState Job PState
sched, sched' : schedule PState
j : Job
SERVICE : service sched j (job_deadline j) =
service sched' j (job_deadline j)
============================
job_meets_deadline sched j <-> job_meets_deadline sched' j
----------------------------------------------------------------------------- *)
split;
by rewrite /job_meets_deadline /completed_by -SERVICE.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End EqualProgress.
End DeadlineFacts.