Library prosa.classic.model.schedule.uni.jitter.schedule
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.arrival.jitter.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module UniprocessorScheduleWithJitter.
Export ArrivalSequenceWithJitter UniprocessorSchedule.
Section RedefiningProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Section JobProperties.
Variable j: Job.
Definition pending (t: time) :=
jitter_has_passed job_arrival job_jitter j t && ~~ completed_by job_cost sched j t.
Definition backlogged (t: time) :=
pending t && ~~ scheduled_at sched j t.
End JobProperties.
Section ValidSchedules.
Definition jobs_execute_after_jitter :=
∀ j t,
scheduled_at sched j t → jitter_has_passed job_arrival job_jitter j t.
End ValidSchedules.
Section Lemmas.
Let has_actually_arrived := jitter_has_passed job_arrival job_jitter.
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
Section Arrival.
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
Lemma jobs_with_jitter_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Proof.
intros j t SCHED.
apply leq_trans with (n := actual_arrival job_arrival job_jitter j);
first by apply leq_addr.
by apply H_jobs_execute_after_jitter.
Qed.
Variable j: Job.
Lemma jitter_has_passed_implies_arrived:
∀ t,
has_actually_arrived j t →
has_arrived job_arrival j t.
Proof.
by intros t PASS; apply: leq_trans PASS; apply leq_addr.
Qed.
Lemma service_before_jitter_is_zero :
∀ t,
t < actual_job_arrival j →
service_at sched j t = 0.
Proof.
rename H_jobs_execute_after_jitter into ARR; red in ARR; intros t LT.
specialize (ARR j t).
apply contra with (c := scheduled_at sched j t)
(b := jitter_has_passed job_arrival job_jitter j t) in ARR;
last by rewrite -ltnNge.
by apply/eqP; rewrite eqb0.
Qed.
Lemma cumulative_service_before_jitter_is_zero :
∀ t1 t2,
t2 ≤ actual_job_arrival j →
\sum_(t1 ≤ i < t2) service_at sched j i = 0.
Proof.
intros t1 t2 LE; apply/eqP; rewrite -leqn0.
apply leq_trans with (n := \sum_(t1 ≤ i < t2) 0);
last by rewrite big_const_nat iter_addn mul0n addn0.
rewrite big_nat_cond [\sum_(_ ≤ _ < _) 0]big_nat_cond.
apply leq_sum; intro i; rewrite andbT; move ⇒ /andP LTi; des.
rewrite service_before_jitter_is_zero; first by ins.
by apply leq_trans with (n := t2); ins.
Qed.
Lemma ignore_service_before_jitter:
∀ t1 t2,
t1 ≤ actual_job_arrival j ≤ t2 →
\sum_(t1 ≤ t < t2) service_at sched j t =
\sum_(actual_job_arrival j ≤ t < t2) service_at sched j t.
Proof.
move ⇒ t1 t2 /andP [LE1 GE2].
rewrite → big_cat_nat with (n := actual_job_arrival j); try (by done).
by rewrite /= cumulative_service_before_jitter_is_zero; [rewrite add0n | apply leqnn].
Qed.
End Arrival.
Section Pending.
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Variable j: Job.
Lemma scheduled_implies_pending:
∀ t,
scheduled_at sched j t → pending j t.
Proof.
rename H_jobs_execute_after_jitter into ARR,
H_completed_jobs into COMP.
unfold jobs_must_arrive_to_execute, completed_jobs_dont_execute in ×.
intros t SCHED.
unfold pending; apply/andP; split; first by apply ARR.
apply/negP; unfold not; intro COMPLETED.
have BUG := COMP j t.+1.
rewrite leqNgt in BUG; move: BUG ⇒ /negP BUG; apply BUG.
unfold service, service_during; rewrite -addn1 big_nat_recr // /=.
by apply leq_add; last rewrite /service_at SCHED.
Qed.
End Pending.
End Lemmas.
End RedefiningProperties.
End UniprocessorScheduleWithJitter.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.arrival.jitter.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module UniprocessorScheduleWithJitter.
Export ArrivalSequenceWithJitter UniprocessorSchedule.
Section RedefiningProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Section JobProperties.
Variable j: Job.
Definition pending (t: time) :=
jitter_has_passed job_arrival job_jitter j t && ~~ completed_by job_cost sched j t.
Definition backlogged (t: time) :=
pending t && ~~ scheduled_at sched j t.
End JobProperties.
Section ValidSchedules.
Definition jobs_execute_after_jitter :=
∀ j t,
scheduled_at sched j t → jitter_has_passed job_arrival job_jitter j t.
End ValidSchedules.
Section Lemmas.
Let has_actually_arrived := jitter_has_passed job_arrival job_jitter.
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
Section Arrival.
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
Lemma jobs_with_jitter_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Proof.
intros j t SCHED.
apply leq_trans with (n := actual_arrival job_arrival job_jitter j);
first by apply leq_addr.
by apply H_jobs_execute_after_jitter.
Qed.
Variable j: Job.
Lemma jitter_has_passed_implies_arrived:
∀ t,
has_actually_arrived j t →
has_arrived job_arrival j t.
Proof.
by intros t PASS; apply: leq_trans PASS; apply leq_addr.
Qed.
Lemma service_before_jitter_is_zero :
∀ t,
t < actual_job_arrival j →
service_at sched j t = 0.
Proof.
rename H_jobs_execute_after_jitter into ARR; red in ARR; intros t LT.
specialize (ARR j t).
apply contra with (c := scheduled_at sched j t)
(b := jitter_has_passed job_arrival job_jitter j t) in ARR;
last by rewrite -ltnNge.
by apply/eqP; rewrite eqb0.
Qed.
Lemma cumulative_service_before_jitter_is_zero :
∀ t1 t2,
t2 ≤ actual_job_arrival j →
\sum_(t1 ≤ i < t2) service_at sched j i = 0.
Proof.
intros t1 t2 LE; apply/eqP; rewrite -leqn0.
apply leq_trans with (n := \sum_(t1 ≤ i < t2) 0);
last by rewrite big_const_nat iter_addn mul0n addn0.
rewrite big_nat_cond [\sum_(_ ≤ _ < _) 0]big_nat_cond.
apply leq_sum; intro i; rewrite andbT; move ⇒ /andP LTi; des.
rewrite service_before_jitter_is_zero; first by ins.
by apply leq_trans with (n := t2); ins.
Qed.
Lemma ignore_service_before_jitter:
∀ t1 t2,
t1 ≤ actual_job_arrival j ≤ t2 →
\sum_(t1 ≤ t < t2) service_at sched j t =
\sum_(actual_job_arrival j ≤ t < t2) service_at sched j t.
Proof.
move ⇒ t1 t2 /andP [LE1 GE2].
rewrite → big_cat_nat with (n := actual_job_arrival j); try (by done).
by rewrite /= cumulative_service_before_jitter_is_zero; [rewrite add0n | apply leqnn].
Qed.
End Arrival.
Section Pending.
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Variable j: Job.
Lemma scheduled_implies_pending:
∀ t,
scheduled_at sched j t → pending j t.
Proof.
rename H_jobs_execute_after_jitter into ARR,
H_completed_jobs into COMP.
unfold jobs_must_arrive_to_execute, completed_jobs_dont_execute in ×.
intros t SCHED.
unfold pending; apply/andP; split; first by apply ARR.
apply/negP; unfold not; intro COMPLETED.
have BUG := COMP j t.+1.
rewrite leqNgt in BUG; move: BUG ⇒ /negP BUG; apply BUG.
unfold service, service_during; rewrite -addn1 big_nat_recr // /=.
by apply leq_add; last rewrite /service_at SCHED.
Qed.
End Pending.
End Lemmas.
End RedefiningProperties.
End UniprocessorScheduleWithJitter.