Library prosa.classic.model.schedule.uni.end_time
Require Import Arith Nat.
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.job
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.response_time.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Set Bullet Behavior "Strict Subproofs".
Module end_time.
Import UniprocessorSchedule Job ResponseTime.
Section Task.
Context {task: eqType}.
Variable task_cost: task → time.
Variable task_period: task → time.
Variable task_deadline: task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → task.
Inductive diagnosis_option : Set :=
| OK : instant → diagnosis_option
| Failure : instant → diagnosis_option.
Section Job_end_time_Def.
Variable sched: schedule Job.
Variable job:Job.
Let job_scheduled_at t:= scheduled_at sched job t = true.
Fixpoint end_time_option (t:instant) (c:duration) (wf:nat):=
match c with
| 0 ⇒ OK t
| S c'⇒ match wf with
| 0 ⇒ Failure t
| S wf'⇒ if scheduled_at sched job t then end_time_option (S t) c' wf'
else end_time_option (S t) c wf'
end
end.
Inductive end_time_predicate : instant→ duration→instant→Prop:=
|C0_: ∀ t, end_time_predicate t 0 t
|S_C_not_sched: ∀ t c e,
¬job_scheduled_at t→
end_time_predicate (S t) (S c) e→
end_time_predicate t (S c) e
|S_C_sched: ∀ t c e,
job_scheduled_at t→
end_time_predicate (S t) c e→
end_time_predicate t (S c) e.
Definition completes_at (t:instant):=
end_time_predicate (job_arrival job) (job_cost job) t.
End Job_end_time_Def.
Section Lemmas.
Variable job:Job.
Variable sched: schedule Job.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_valid_job:
valid_realtime_job job_cost job_deadline job.
Let job_end_time_function:= end_time_option sched job.
Let job_end_time_p:= end_time_predicate sched job.
Let job_completes_at := completes_at sched job.
Let job_scheduled_at t:= scheduled_at sched job t = true.
Theorem end_time_function_predicat_equivalence:
∀ e wf t c,
job_end_time_function t c wf = OK e →
job_end_time_p t c e.
Proof.
induction wf as [| wf' IHwf']; intros t c; simpl.
- destruct c; intros H; inversion H .
apply C0_.
- intros IHSwf. case Hcases:(scheduled_at sched job t); destruct c.
+ inversion IHSwf. apply C0_.
+ rewrite Hcases in IHSwf. apply IHwf' in IHSwf. apply S_C_sched with (c:=c)(e:=e).
apply Hcases. apply IHSwf.
+ inversion IHSwf. apply C0_.
+ rewrite Hcases in IHSwf. apply IHwf' in IHSwf. apply S_C_not_sched with (c:=c)(e:=e).
× rewrite Hcases. done.
× apply IHSwf.
Qed.
Theorem end_time_predicat_function_equivalence:
∀ t c e ,
job_end_time_p t c e →
∃ wf, job_end_time_function t c wf = OK e.
Proof.
intros.
induction H as [t|t c e Hcase1 Hpre [wf Hwf] |t c e Hcase2 Hpre [wf Hwf]].
- ∃ 1. done.
- ∃ (1+wf).
case Csa:(scheduled_at sched job t).
+ done.
+ simpl. rewrite Csa. apply Hwf.
- ∃ (1+wf). simpl.
rewrite Hcase2. apply Hwf.
Qed.
Lemma end_time_predicate_not_sched:
∀ t c e,
~(job_scheduled_at t) →
end_time_predicate sched job t c.+1 e →
end_time_predicate sched job t.+1 c.+1 e.
Proof.
intros× Hcase1 Hpre.
induction t as [| t' IHt'];
inversion Hpre; try apply H2; done.
Qed.
Lemma end_time_predicate_sched:
∀ t c e,
job_scheduled_at t →
end_time_predicate sched job t c.+1 e →
end_time_predicate sched job t.+1 c e.
Proof.
intros× Hcase2 Hpre.
induction t as [| t' IHt'];
inversion Hpre; try apply H2; done.
Qed.
Variable job_end: instant.
Let job_completed_by:=
completed_by job_cost sched.
Let job_service_during:=
service_during sched job.
Lemma arrival_le_end:
∀ t c e, job_end_time_p t c e → t ≤ e.
Proof.
intros× G.
induction G as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; ssrlia.
Qed.
Lemma arrival_add_cost_le_end:
∀ t c e,
job_end_time_p t c e →
t+c≤e.
Proof.
intros× h1.
induction h1 as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; ssrlia.
Qed.
Lemma service_eq_cost_at_end_time:
job_completes_at job_end →
job_service_during (job_arrival job) job_end = job_cost job.
Proof.
intros job_cmplted.
induction job_cmplted as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre];
unfold job_service_during, service_during in ×.
- by rewrite big_geq.
- apply arrival_le_end in Hpre.
rewrite big_ltn // IHHpre /service_at.
case cases:(scheduled_at sched job t); try easy; done.
- apply arrival_le_end in Hpre.
rewrite big_ltn // IHHpre /service_at.
rewrite Hcase2 //.
Qed.
Lemma completed_by_end_time:
job_completes_at job_end →
job_completed_by job job_end.
Proof.
intro job_cmplted.
unfold job_completed_by, completed_by, service, service_during.
rewrite (ignore_service_before_arrival job_arrival sched ) //.
- apply service_eq_cost_at_end_time in job_cmplted.
by rewrite -job_cmplted.
- by apply arrival_le_end in job_cmplted.
Qed.
Corollary end_time_positive:
job_completes_at job_end → job_end > 0.
Proof.
intro h1.
assert (H_slot: job_cost job > 0) by (apply H_valid_job).
apply completed_by_end_time in h1.
unfold job_completed_by, completed_by, service, service_during in h1.
destruct job_end; trivial.
rewrite big_geq // in h1.
ssrlia.
Qed.
Lemma job_uncompletes_at_end_time_sub_1:
job_completes_at job_end →
job_service_during (job_arrival job) (job_end .-1) = (job_cost job) .-1.
Proof.
intros job_cmplted.
induction job_cmplted as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre];
unfold job_service_during, service_during in×.
- apply big_geq, leq_pred.
- apply arrival_add_cost_le_end, leq_sub2r with (p:=1) in Hpre.
rewrite subn1 addnS //= addSn subn1 in Hpre.
apply leq_ltn_trans with (m:=t) in Hpre; try (apply leq_addr).
rewrite big_ltn // IHHpre /service_at /service_during.
case C:(scheduled_at sched job t);done.
- destruct c.
+ inversion Hpre. apply big_geq. ssrlia.
+ apply arrival_add_cost_le_end, leq_sub2r with (p:=1) in Hpre.
rewrite subn1 addnS //= addSn subn1 in Hpre.
apply leq_ltn_trans with (m:=t) in Hpre; try (apply leq_addr).
rewrite big_ltn // /service_at / service_during IHHpre Hcase2 //.
Qed.
Lemma job_uncompleted_before_end_time:
job_completes_at job_end →
∀ t', job_arrival job ≤ t' ∧ t'≤ job_end.-1 →
job_service_during (job_arrival job) t' < job_cost job.
Proof.
intros job_cmplted t' [ht1 ht2].
assert (H_slot: job_cost job > 0) by (apply H_valid_job).
apply leq_ltn_trans with (n:= (job_cost job).-1); last ssrlia.
rewrite -job_uncompletes_at_end_time_sub_1 // /job_service_during /service_during.
assert (H_lt: ∃ delta, t' + delta = job_end.-1).
- move/leP:ht2 ⇒ ht2.
apply Nat.le_exists_sub in ht2.
destruct ht2 as [p [ht21 ht22]]. ∃ p. ssrlia.
- destruct H_lt as [delta ht']. rewrite -ht'.
replace (\sum_(job_arrival job ≤ t < t' + delta) service_at sched job t)
with (addn_monoid(\big[addn_monoid/0]_(job_arrival job ≤ i < t') service_at sched job i)
(\big[addn_monoid/0]_(t' ≤ i < t'+delta) service_at sched job i)); simpl; try ssrlia.
symmetry. apply big_cat_nat; ssrlia.
Qed.
End Lemmas.
End Task.
End end_time.
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.job
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.response_time.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Set Bullet Behavior "Strict Subproofs".
Module end_time.
Import UniprocessorSchedule Job ResponseTime.
Section Task.
Context {task: eqType}.
Variable task_cost: task → time.
Variable task_period: task → time.
Variable task_deadline: task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → task.
Inductive diagnosis_option : Set :=
| OK : instant → diagnosis_option
| Failure : instant → diagnosis_option.
Section Job_end_time_Def.
Variable sched: schedule Job.
Variable job:Job.
Let job_scheduled_at t:= scheduled_at sched job t = true.
Fixpoint end_time_option (t:instant) (c:duration) (wf:nat):=
match c with
| 0 ⇒ OK t
| S c'⇒ match wf with
| 0 ⇒ Failure t
| S wf'⇒ if scheduled_at sched job t then end_time_option (S t) c' wf'
else end_time_option (S t) c wf'
end
end.
Inductive end_time_predicate : instant→ duration→instant→Prop:=
|C0_: ∀ t, end_time_predicate t 0 t
|S_C_not_sched: ∀ t c e,
¬job_scheduled_at t→
end_time_predicate (S t) (S c) e→
end_time_predicate t (S c) e
|S_C_sched: ∀ t c e,
job_scheduled_at t→
end_time_predicate (S t) c e→
end_time_predicate t (S c) e.
Definition completes_at (t:instant):=
end_time_predicate (job_arrival job) (job_cost job) t.
End Job_end_time_Def.
Section Lemmas.
Variable job:Job.
Variable sched: schedule Job.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_valid_job:
valid_realtime_job job_cost job_deadline job.
Let job_end_time_function:= end_time_option sched job.
Let job_end_time_p:= end_time_predicate sched job.
Let job_completes_at := completes_at sched job.
Let job_scheduled_at t:= scheduled_at sched job t = true.
Theorem end_time_function_predicat_equivalence:
∀ e wf t c,
job_end_time_function t c wf = OK e →
job_end_time_p t c e.
Proof.
induction wf as [| wf' IHwf']; intros t c; simpl.
- destruct c; intros H; inversion H .
apply C0_.
- intros IHSwf. case Hcases:(scheduled_at sched job t); destruct c.
+ inversion IHSwf. apply C0_.
+ rewrite Hcases in IHSwf. apply IHwf' in IHSwf. apply S_C_sched with (c:=c)(e:=e).
apply Hcases. apply IHSwf.
+ inversion IHSwf. apply C0_.
+ rewrite Hcases in IHSwf. apply IHwf' in IHSwf. apply S_C_not_sched with (c:=c)(e:=e).
× rewrite Hcases. done.
× apply IHSwf.
Qed.
Theorem end_time_predicat_function_equivalence:
∀ t c e ,
job_end_time_p t c e →
∃ wf, job_end_time_function t c wf = OK e.
Proof.
intros.
induction H as [t|t c e Hcase1 Hpre [wf Hwf] |t c e Hcase2 Hpre [wf Hwf]].
- ∃ 1. done.
- ∃ (1+wf).
case Csa:(scheduled_at sched job t).
+ done.
+ simpl. rewrite Csa. apply Hwf.
- ∃ (1+wf). simpl.
rewrite Hcase2. apply Hwf.
Qed.
Lemma end_time_predicate_not_sched:
∀ t c e,
~(job_scheduled_at t) →
end_time_predicate sched job t c.+1 e →
end_time_predicate sched job t.+1 c.+1 e.
Proof.
intros× Hcase1 Hpre.
induction t as [| t' IHt'];
inversion Hpre; try apply H2; done.
Qed.
Lemma end_time_predicate_sched:
∀ t c e,
job_scheduled_at t →
end_time_predicate sched job t c.+1 e →
end_time_predicate sched job t.+1 c e.
Proof.
intros× Hcase2 Hpre.
induction t as [| t' IHt'];
inversion Hpre; try apply H2; done.
Qed.
Variable job_end: instant.
Let job_completed_by:=
completed_by job_cost sched.
Let job_service_during:=
service_during sched job.
Lemma arrival_le_end:
∀ t c e, job_end_time_p t c e → t ≤ e.
Proof.
intros× G.
induction G as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; ssrlia.
Qed.
Lemma arrival_add_cost_le_end:
∀ t c e,
job_end_time_p t c e →
t+c≤e.
Proof.
intros× h1.
induction h1 as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; ssrlia.
Qed.
Lemma service_eq_cost_at_end_time:
job_completes_at job_end →
job_service_during (job_arrival job) job_end = job_cost job.
Proof.
intros job_cmplted.
induction job_cmplted as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre];
unfold job_service_during, service_during in ×.
- by rewrite big_geq.
- apply arrival_le_end in Hpre.
rewrite big_ltn // IHHpre /service_at.
case cases:(scheduled_at sched job t); try easy; done.
- apply arrival_le_end in Hpre.
rewrite big_ltn // IHHpre /service_at.
rewrite Hcase2 //.
Qed.
Lemma completed_by_end_time:
job_completes_at job_end →
job_completed_by job job_end.
Proof.
intro job_cmplted.
unfold job_completed_by, completed_by, service, service_during.
rewrite (ignore_service_before_arrival job_arrival sched ) //.
- apply service_eq_cost_at_end_time in job_cmplted.
by rewrite -job_cmplted.
- by apply arrival_le_end in job_cmplted.
Qed.
Corollary end_time_positive:
job_completes_at job_end → job_end > 0.
Proof.
intro h1.
assert (H_slot: job_cost job > 0) by (apply H_valid_job).
apply completed_by_end_time in h1.
unfold job_completed_by, completed_by, service, service_during in h1.
destruct job_end; trivial.
rewrite big_geq // in h1.
ssrlia.
Qed.
Lemma job_uncompletes_at_end_time_sub_1:
job_completes_at job_end →
job_service_during (job_arrival job) (job_end .-1) = (job_cost job) .-1.
Proof.
intros job_cmplted.
induction job_cmplted as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre];
unfold job_service_during, service_during in×.
- apply big_geq, leq_pred.
- apply arrival_add_cost_le_end, leq_sub2r with (p:=1) in Hpre.
rewrite subn1 addnS //= addSn subn1 in Hpre.
apply leq_ltn_trans with (m:=t) in Hpre; try (apply leq_addr).
rewrite big_ltn // IHHpre /service_at /service_during.
case C:(scheduled_at sched job t);done.
- destruct c.
+ inversion Hpre. apply big_geq. ssrlia.
+ apply arrival_add_cost_le_end, leq_sub2r with (p:=1) in Hpre.
rewrite subn1 addnS //= addSn subn1 in Hpre.
apply leq_ltn_trans with (m:=t) in Hpre; try (apply leq_addr).
rewrite big_ltn // /service_at / service_during IHHpre Hcase2 //.
Qed.
Lemma job_uncompleted_before_end_time:
job_completes_at job_end →
∀ t', job_arrival job ≤ t' ∧ t'≤ job_end.-1 →
job_service_during (job_arrival job) t' < job_cost job.
Proof.
intros job_cmplted t' [ht1 ht2].
assert (H_slot: job_cost job > 0) by (apply H_valid_job).
apply leq_ltn_trans with (n:= (job_cost job).-1); last ssrlia.
rewrite -job_uncompletes_at_end_time_sub_1 // /job_service_during /service_during.
assert (H_lt: ∃ delta, t' + delta = job_end.-1).
- move/leP:ht2 ⇒ ht2.
apply Nat.le_exists_sub in ht2.
destruct ht2 as [p [ht21 ht22]]. ∃ p. ssrlia.
- destruct H_lt as [delta ht']. rewrite -ht'.
replace (\sum_(job_arrival job ≤ t < t' + delta) service_at sched job t)
with (addn_monoid(\big[addn_monoid/0]_(job_arrival job ≤ i < t') service_at sched job i)
(\big[addn_monoid/0]_(t' ≤ i < t'+delta) service_at sched job i)); simpl; try ssrlia.
symmetry. apply big_cat_nat; ssrlia.
Qed.
End Lemmas.
End Task.
End end_time.