Library rt.restructuring.analysis.basic_facts.ideal_schedule
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From mathcomp Require Import all_ssreflect.
From rt.restructuring.model.processor Require Import ideal platform_properties.
Note: we do not re-export the basic definitions to avoid littering the global
namespace with type class instances.
In this section we estlish the classes to which an ideal schedule belongs.
Consider any job type and the ideal processor model.
We note that the ideal processor model is indeed a uniprocessor
model.
Lemma ideal_proc_model_is_a_uniprocessor_model:
uniprocessor_model (processor_state Job).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 267)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
============================
uniprocessor_model (processor_state Job)
----------------------------------------------------------------------------- *)
Proof.
move⇒ j1 j2 sched t /existsP[[]/eqP E1] /existsP[[]/eqP E2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 427)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j1, j2 : Job
sched : schedule (processor_state Job)
t : instant
E1 : sched t = Some j1
E2 : sched t = Some j2
============================
j1 = j2
----------------------------------------------------------------------------- *)
by move: E1 E2=>->[].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
uniprocessor_model (processor_state Job).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 267)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
============================
uniprocessor_model (processor_state Job)
----------------------------------------------------------------------------- *)
Proof.
move⇒ j1 j2 sched t /existsP[[]/eqP E1] /existsP[[]/eqP E2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 427)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j1, j2 : Job
sched : schedule (processor_state Job)
t : instant
E1 : sched t = Some j1
E2 : sched t = Some j2
============================
j1 = j2
----------------------------------------------------------------------------- *)
by move: E1 E2=>->[].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We observe that the ideal processor model falls into the category
of ideal-progress models, i.e., a scheduled job always receives
service.
Lemma ideal_proc_model_ensures_ideal_progress:
ideal_progress_proc_model (processor_state Job).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 270)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
============================
ideal_progress_proc_model (processor_state Job)
----------------------------------------------------------------------------- *)
Proof.
move⇒ j s /existsP[[]/eqP->]/=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 355)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : processor_state Job
============================
0 < (Some j == Some j)
----------------------------------------------------------------------------- *)
by rewrite eqxx.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
ideal_progress_proc_model (processor_state Job).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 270)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
============================
ideal_progress_proc_model (processor_state Job)
----------------------------------------------------------------------------- *)
Proof.
move⇒ j s /existsP[[]/eqP->]/=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 355)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : processor_state Job
============================
0 < (Some j == Some j)
----------------------------------------------------------------------------- *)
by rewrite eqxx.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
The ideal processor model is a unit-service model.
Lemma ideal_proc_model_provides_unit_service:
unit_service_proc_model (processor_state Job).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 273)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
============================
unit_service_proc_model (processor_state Job)
----------------------------------------------------------------------------- *)
Proof.
move⇒ j s.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 276)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : processor_state Job
============================
service_in j s <= 1
----------------------------------------------------------------------------- *)
rewrite /service_in/=/nat_of_bool.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 285)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : processor_state Job
============================
(if s == Some j then 1 else 0) <= 1
----------------------------------------------------------------------------- *)
by case:ifP.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma scheduled_in_def (j : Job) s :
scheduled_in j s = (s == Some j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 287)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : option_eqType Job
============================
scheduled_in j s = (s == Some j)
----------------------------------------------------------------------------- *)
Proof.
rewrite /scheduled_in/scheduled_on/=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 302)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : option_eqType Job
============================
[exists c, s == Some j] = (s == Some j)
----------------------------------------------------------------------------- *)
case: existsP=>[[_->]//|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 325)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : option_eqType Job
============================
~ (exists _ : unit_finType, s == Some j) -> false = (s == Some j)
----------------------------------------------------------------------------- *)
case: (s == Some j)=>//=[[]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 385)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : option_eqType Job
============================
exists _ : unit, true
----------------------------------------------------------------------------- *)
by ∃.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma scheduled_at_def sched (j : Job) t :
scheduled_at sched j t = (sched t == Some j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
sched : schedule (option_eqType Job)
j : Job
t : instant
============================
scheduled_at sched j t = (sched t == Some j)
----------------------------------------------------------------------------- *)
Proof.
by rewrite /scheduled_at scheduled_in_def.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma service_in_is_scheduled_in (j : Job) s :
service_in j s = scheduled_in j s.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 317)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : option Job
============================
service_in j s = scheduled_in j s
----------------------------------------------------------------------------- *)
Proof.
by rewrite /service_in scheduled_in_def/=.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma service_at_is_scheduled_at sched (j : Job) t :
service_at sched j t = scheduled_at sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 333)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
sched : schedule (option Job)
j : Job
t : instant
============================
service_at sched j t = scheduled_at sched j t
----------------------------------------------------------------------------- *)
Proof.
by rewrite /service_at service_in_is_scheduled_in.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
unit_service_proc_model (processor_state Job).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 273)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
============================
unit_service_proc_model (processor_state Job)
----------------------------------------------------------------------------- *)
Proof.
move⇒ j s.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 276)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : processor_state Job
============================
service_in j s <= 1
----------------------------------------------------------------------------- *)
rewrite /service_in/=/nat_of_bool.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 285)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : processor_state Job
============================
(if s == Some j then 1 else 0) <= 1
----------------------------------------------------------------------------- *)
by case:ifP.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma scheduled_in_def (j : Job) s :
scheduled_in j s = (s == Some j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 287)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : option_eqType Job
============================
scheduled_in j s = (s == Some j)
----------------------------------------------------------------------------- *)
Proof.
rewrite /scheduled_in/scheduled_on/=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 302)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : option_eqType Job
============================
[exists c, s == Some j] = (s == Some j)
----------------------------------------------------------------------------- *)
case: existsP=>[[_->]//|].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 325)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : option_eqType Job
============================
~ (exists _ : unit_finType, s == Some j) -> false = (s == Some j)
----------------------------------------------------------------------------- *)
case: (s == Some j)=>//=[[]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 385)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : option_eqType Job
============================
exists _ : unit, true
----------------------------------------------------------------------------- *)
by ∃.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma scheduled_at_def sched (j : Job) t :
scheduled_at sched j t = (sched t == Some j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
sched : schedule (option_eqType Job)
j : Job
t : instant
============================
scheduled_at sched j t = (sched t == Some j)
----------------------------------------------------------------------------- *)
Proof.
by rewrite /scheduled_at scheduled_in_def.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma service_in_is_scheduled_in (j : Job) s :
service_in j s = scheduled_in j s.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 317)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
j : Job
s : option Job
============================
service_in j s = scheduled_in j s
----------------------------------------------------------------------------- *)
Proof.
by rewrite /service_in scheduled_in_def/=.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Lemma service_at_is_scheduled_at sched (j : Job) t :
service_at sched j t = scheduled_at sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 333)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
sched : schedule (option Job)
j : Job
t : instant
============================
service_at sched j t = scheduled_at sched j t
----------------------------------------------------------------------------- *)
Proof.
by rewrite /service_at service_in_is_scheduled_in.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Next we prove a lemma which helps us to do a case analysis on
the state of an ideal schedule.
Lemma ideal_proc_model_sched_case_analysis:
∀ (sched : schedule (ideal.processor_state Job)) (t : instant),
is_idle sched t ∨ ∃ j, scheduled_at sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 341)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
============================
forall (sched : schedule (processor_state Job)) (t : instant),
is_idle sched t \/ (exists j : Job, scheduled_at sched j t)
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 343)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
sched : schedule (processor_state Job)
t : instant
============================
is_idle sched t \/ (exists j : Job, scheduled_at sched j t)
----------------------------------------------------------------------------- *)
unfold is_idle; simpl; destruct (sched t) eqn:EQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 360)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
sched : schedule (processor_state Job)
t : instant
s : Job
EQ : sched t = Some s
============================
Some s == None \/ (exists j : Job, scheduled_at sched j t)
subgoal 2 (ID 361) is:
None == None \/ (exists j : Job, scheduled_at sched j t)
----------------------------------------------------------------------------- *)
- by right; ∃ s; auto; rewrite scheduled_at_def EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 361)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
sched : schedule (processor_state Job)
t : instant
EQ : sched t = None
============================
None == None \/ (exists j : Job, scheduled_at sched j t)
----------------------------------------------------------------------------- *)
- by left; auto.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ScheduleClass.
∀ (sched : schedule (ideal.processor_state Job)) (t : instant),
is_idle sched t ∨ ∃ j, scheduled_at sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 341)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
============================
forall (sched : schedule (processor_state Job)) (t : instant),
is_idle sched t \/ (exists j : Job, scheduled_at sched j t)
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 343)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
sched : schedule (processor_state Job)
t : instant
============================
is_idle sched t \/ (exists j : Job, scheduled_at sched j t)
----------------------------------------------------------------------------- *)
unfold is_idle; simpl; destruct (sched t) eqn:EQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 360)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
sched : schedule (processor_state Job)
t : instant
s : Job
EQ : sched t = Some s
============================
Some s == None \/ (exists j : Job, scheduled_at sched j t)
subgoal 2 (ID 361) is:
None == None \/ (exists j : Job, scheduled_at sched j t)
----------------------------------------------------------------------------- *)
- by right; ∃ s; auto; rewrite scheduled_at_def EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 361)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
sched : schedule (processor_state Job)
t : instant
EQ : sched t = None
============================
None == None \/ (exists j : Job, scheduled_at sched j t)
----------------------------------------------------------------------------- *)
- by left; auto.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ScheduleClass.
Automation
We add the above lemmas into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
Hint Resolve ideal_proc_model_is_a_uniprocessor_model
ideal_proc_model_ensures_ideal_progress
ideal_proc_model_provides_unit_service : basic_facts.
ideal_proc_model_ensures_ideal_progress
ideal_proc_model_provides_unit_service : basic_facts.
We also provide tactics for case analysis on ideal processor state.
The first tactic generates two subgoals: one with idle processor and
the other with processor executing a job named JobName.
Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
let Idle := fresh "Idle" in
let Sched := fresh "Sched_" JobName in
destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].
let Idle := fresh "Idle" in
let Sched := fresh "Sched_" JobName in
destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].
The second tactic is similar to the first, but it additionally generates
two equalities: [sched t = None] and [sched t = Some j].
Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
let Idle := fresh "Idle" in
let IdleEq := fresh "Eq" Idle in
let Sched := fresh "Sched_" JobName in
let SchedEq := fresh "Eq" Sched in
destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];
[move: (Idle) ⇒ /eqP IdleEq; rewrite ?IdleEq
| move: (Sched); simpl; move ⇒ /eqP SchedEq; rewrite ?SchedEq].
let Idle := fresh "Idle" in
let IdleEq := fresh "Eq" Idle in
let Sched := fresh "Sched_" JobName in
let SchedEq := fresh "Eq" Sched in
destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];
[move: (Idle) ⇒ /eqP IdleEq; rewrite ?IdleEq
| move: (Sched); simpl; move ⇒ /eqP SchedEq; rewrite ?SchedEq].