Library rt.restructuring.analysis.basic_facts.deadlines
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Export service completion.
In this file, we observe basic properties of the behavioral job
model w.r.t. deadlines.
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.