Library prosa.classic.model.schedule.global.basic.schedule
Require Import prosa.classic.util.all
prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Schedule.
Export ArrivalSequence.
Definition processor (num_cpus: nat) := 'I_num_cpus.
Section ScheduleDef.
Variable Job: eqType.
Variable num_cpus: nat.
Definition schedule :=
processor num_cpus → time → option Job.
End ScheduleDef.
Section ScheduledJobs.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Context {arr_seq: arrival_sequence Job}.
Variable job_cost: Job → time.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Variable j: Job.
Definition scheduled_on (cpu: processor num_cpus) (t: time) :=
sched cpu t == Some j.
Definition scheduled (t: time) :=
[∃ cpu, scheduled_on cpu t].
Definition is_idle (cpu: processor num_cpus) (t: time) :=
sched cpu t = None.
Definition service_at (t: time) :=
\sum_(cpu < num_cpus | scheduled_on cpu t) 1.
Definition service (t': time) := \sum_(0 ≤ t < t') service_at t.
Definition service_during (t1 t2: time) := \sum_(t1 ≤ t < t2) service_at t.
Definition completed (t: time) := service t ≥ job_cost j.
Definition pending (t: time) := has_arrived job_arrival j t && ~~completed t.
Definition backlogged (t: time) := pending t && ~~scheduled t.
Definition carried_in (t1: time) := arrived_before job_arrival j t1 && ~~ completed t1.
Definition carried_out (t1 t2: time) := arrived_before job_arrival j t2 && ~~ completed t2.
Definition jobs_scheduled_at (t: time) :=
\cat_(cpu < num_cpus) make_sequence (sched cpu t).
Definition jobs_scheduled_between (t1 t2: time) :=
undup (\cat_(t1 ≤ t < t2) jobs_scheduled_at t).
End ScheduledJobs.
Section ValidSchedules.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Definition sequential_jobs :=
∀ j t cpu1 cpu2,
sched cpu1 t = Some j → sched cpu2 t = Some j → cpu1 = cpu2.
Definition jobs_must_arrive_to_execute :=
∀ j t,
scheduled sched j t →
has_arrived job_arrival j t.
Definition completed_jobs_dont_execute :=
∀ j t, service sched j t ≤ job_cost j.
Definition jobs_come_from_arrival_sequence (arr_seq: arrival_sequence Job) :=
∀ j t, scheduled sched j t → arrives_in arr_seq j.
End ValidSchedules.
Section JobLemmas.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Variable j: Job.
Section Basic.
Lemma not_scheduled_no_service :
∀ t,
~~ scheduled sched j t = (service_at sched j t == 0).
Proof.
unfold scheduled, service_at, scheduled_on; intros t; apply/idP/idP.
{
intros NOTSCHED.
rewrite negb_exists in NOTSCHED.
move: NOTSCHED ⇒ /forallP NOTSCHED.
rewrite big_seq_cond.
rewrite → eq_bigr with (F2 := fun i ⇒ 0);
first by rewrite big_const_seq iter_addn mul0n addn0.
move ⇒ cpu /andP [_ /eqP SCHED].
by specialize (NOTSCHED cpu); rewrite SCHED eq_refl in NOTSCHED.
}
{
intros NOSERV; rewrite big_mkcond -sum_nat_eq0_nat in NOSERV.
move: NOSERV ⇒ /allP ALL.
rewrite negb_exists; apply/forallP; intros cpu.
exploit (ALL cpu); [by apply mem_index_enum | by desf].
}
Qed.
Lemma cumulative_service_implies_service :
∀ t1 t2,
service_during sched j t1 t2 != 0 →
∃ t,
t1 ≤ t < t2 ∧
service_at sched j t != 0.
Proof.
intros t1 t2 NONZERO.
destruct ([∃ t: 'I_t2, (t ≥ t1) && (service_at sched j t != 0)]) eqn:EX.
{
move: EX ⇒ /existsP EX; destruct EX as [x EX]. move: EX ⇒ /andP [GE SERV].
∃ x; split; last by done.
by apply/andP; split; [by done | apply ltn_ord].
}
{
apply negbT in EX; rewrite negb_exists in EX; move: EX ⇒ /forallP EX.
unfold service_during in NONZERO; rewrite big_nat_cond in NONZERO.
rewrite (eq_bigr (fun x ⇒ 0)) in NONZERO;
first by rewrite -big_nat_cond big_const_nat iter_addn mul0n addn0 in NONZERO.
intros i; rewrite andbT; move ⇒ /andP [GT LT].
specialize (EX (Ordinal LT)); simpl in EX.
by rewrite GT andTb negbK in EX; apply/eqP.
}
Qed.
Lemma service_implies_cumulative_service:
∀ t t1 t2,
t1 ≤ t < t2 →
service_at sched j t != 0 →
service_during sched j t1 t2 != 0.
Proof.
intros t t1 t2 LE NONZERO.
unfold service_during.
rewrite (bigD1_seq t) /=;
[| by rewrite mem_index_iota | by apply iota_uniq].
rewrite -lt0n -addn1 addnC.
by apply leq_add; first by rewrite lt0n.
Qed.
End Basic.
Section SequentialJobs.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Lemma service_at_most_one :
∀ t, service_at sched j t ≤ 1.
Proof.
unfold service_at, sequential_jobs in *; ins.
destruct (scheduled sched j t) eqn:SCHED; unfold scheduled in SCHED.
{
move: SCHED ⇒ /existsP [cpu SCHED]; des.
rewrite -big_filter (bigD1_seq cpu);
[simpl | | by have [e _ [UNIQ _ ] _] := big_enumP];
last by rewrite mem_filter; apply/andP; split.
rewrite -big_filter -filter_predI big_filter.
rewrite → eq_bigr with (F2 := fun cpu ⇒ 0);
first by rewrite /= big_const_seq iter_addn mul0n 2!addn0.
intro cpu'; move ⇒ /andP [/eqP NEQ /eqP SCHED'].
exfalso; apply NEQ.
by apply H_sequential_jobs with (j := j) (t := t); last by apply/eqP.
}
{
apply negbT in SCHED; rewrite negb_exists in SCHED.
move: SCHED ⇒ /forallP SCHED.
rewrite big_pred0; red; ins; apply negbTE, SCHED.
}
Qed.
Lemma cumulative_service_le_delta :
∀ t delta, service_during sched j t (t + delta) ≤ delta.
Proof.
unfold service_at, sequential_jobs in *; ins.
generalize dependent t.
induction delta.
{
ins; unfold service_during; rewrite addn0.
by rewrite big_geq.
}
{
unfold service_during; intro t.
rewrite -addn1 addnA addn1 big_nat_recr; last by apply leq_addr.
apply leq_add; first by apply IHdelta.
by apply service_at_most_one.
}
Qed.
End SequentialJobs.
Section Completion.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Lemma completion_monotonic :
∀ t t',
t ≤ t' →
completed job_cost sched j t →
completed job_cost sched j t'.
Proof.
unfold completed; move ⇒ t t' LE COMPt.
apply leq_trans with (service sched j t); first by done.
by rewrite /service /service_during [in X in _ ≤ X](@big_cat_nat _ _ _ t) //= leq_addr.
Qed.
Lemma completed_implies_not_scheduled :
∀ t,
completed job_cost sched j t →
~~ scheduled sched j t.
Proof.
rename H_completed_jobs into COMP.
unfold completed_jobs_dont_execute in ×.
intros t COMPLETED.
apply/negP; red; intro SCHED.
have BUG := COMP j t.+1.
rewrite leqNgt in BUG; move: BUG ⇒ /negP BUG; apply: BUG.
unfold service, service_during; rewrite big_nat_recr // /= -addn1.
apply leq_add; first by done.
by rewrite lt0n -not_scheduled_no_service negbK.
Qed.
Lemma cumulative_service_le_job_cost :
∀ t t',
service_during sched j t t' ≤ job_cost j.
Proof.
unfold service_during; rename H_completed_jobs into COMP; red in COMP; ins.
destruct (t > t') eqn:GT.
by rewrite big_geq // -ltnS; apply ltn_trans with (n := t); ins.
apply leq_trans with
(n := \sum_(0 ≤ t0 < t') service_at sched j t0);
last by apply COMP.
rewrite → big_cat_nat with (m := 0) (n := t);
[by apply leq_addl | by ins | by rewrite leqNgt negbT //].
Qed.
End Completion.
Section Arrival.
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute job_arrival sched.
Lemma service_before_job_arrival_zero :
∀ t,
t < job_arrival j →
service_at sched j t = 0.
Proof.
rename H_jobs_must_arrive into ARR; red in ARR; intros t LT.
specialize (ARR j t).
apply contra with (c := scheduled sched j t)
(b := has_arrived job_arrival j t) in ARR;
last by rewrite -ltnNge.
apply/eqP; rewrite -leqn0; unfold service_at.
rewrite big_pred0 //; red.
intros cpu; apply negbTE.
by move: ARR; rewrite negb_exists; move ⇒ /forallP ARR; apply ARR.
Qed.
Lemma cumulative_service_before_job_arrival_zero :
∀ t1 t2,
t2 ≤ 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_job_arrival_zero; first by ins.
by apply leq_trans with (n := t2); ins.
Qed.
Lemma service_before_arrival_eq_service_during :
∀ t0 t,
t0 ≤ job_arrival j →
\sum_(t0 ≤ t < job_arrival j + t) service_at sched j t =
\sum_(job_arrival j ≤ t < job_arrival j + t) service_at sched j t.
Proof.
intros t0 t LE; rewrite → big_cat_nat with (n := job_arrival j);
[| by ins | by apply leq_addr].
by rewrite /= cumulative_service_before_job_arrival_zero; [rewrite add0n | apply leqnn].
Qed.
End Arrival.
Section Pending.
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Lemma scheduled_implies_pending:
∀ t,
scheduled sched j t →
pending job_arrival job_cost sched j t.
Proof.
rename H_jobs_must_arrive into ARRIVE,
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 ARRIVE.
apply/negP; unfold not; intro COMPLETED.
have BUG := COMP j t.+1.
rewrite leqNgt in BUG; move: BUG ⇒ /negP BUG; apply BUG.
unfold service; rewrite -addn1 big_nat_recr // /=.
apply leq_add; first by done.
rewrite lt0n; apply/eqP; red; move ⇒ /eqP NOSERV.
rewrite -not_scheduled_no_service in NOSERV.
by rewrite SCHED in NOSERV.
Qed.
End Pending.
End JobLemmas.
Section ScheduledJobsLemmas.
Context {Job: eqType}.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Section Membership.
Lemma mem_scheduled_jobs_eq_scheduled :
∀ j t,
j \in jobs_scheduled_at sched t = scheduled sched j t.
Proof.
unfold jobs_scheduled_at, scheduled, scheduled_on.
intros j t; apply/idP/idP.
{
intros IN.
apply mem_bigcat_ord_exists in IN; des.
apply/existsP; ∃ i.
destruct (sched i t); last by done.
by rewrite mem_seq1 in IN; move: IN ⇒ /eqP IN; subst.
}
{
move ⇒ /existsP EX; destruct EX as [i SCHED].
apply mem_bigcat_ord with (j := i); first by apply ltn_ord.
by move: SCHED ⇒ /eqP SCHED; rewrite SCHED /= mem_seq1 eq_refl.
}
Qed.
End Membership.
Section Uniqueness.
Hypothesis H_sequential_jobs : sequential_jobs sched.
Lemma scheduled_jobs_uniq :
∀ t,
uniq (jobs_scheduled_at sched t).
Proof.
intros t; rename H_sequential_jobs into SEQUENTIAL.
unfold sequential_jobs in SEQUENTIAL.
clear -SEQUENTIAL.
unfold jobs_scheduled_at.
induction num_cpus; first by rewrite big_ord0.
{
rewrite big_ord_recr cat_uniq; apply/andP; split.
{
apply bigcat_ord_uniq;
first by intro i; unfold make_sequence; desf.
intros x i1 i2 IN1 IN2; unfold make_sequence in ×.
desf; move: Heq0 Heq ⇒ SOME1 SOME2.
rewrite mem_seq1 in IN1; rewrite mem_seq1 in IN2.
move: IN1 IN2 ⇒ /eqP IN1 /eqP IN2; subst x s0.
specialize (SEQUENTIAL s t (widen_ord (leqnSn n) i1)
(widen_ord (leqnSn n) i2) SOME1 SOME2).
by inversion SEQUENTIAL; apply ord_inj.
}
apply/andP; split; last by unfold make_sequence; destruct (sched ord_max).
{
rewrite -all_predC; apply/allP; unfold predC; simpl.
intros x INx.
unfold make_sequence in INx.
destruct (sched ord_max t) eqn:SCHED;
last by rewrite in_nil in INx.
apply/negP; unfold not; intro IN'.
have EX := mem_bigcat_ord_exists _ x n.
apply EX in IN'; des; clear EX.
unfold make_sequence in IN'.
desf; rename Heq into SCHEDi.
rewrite mem_seq1 in INx; rewrite mem_seq1 in IN'.
move: INx IN' ⇒ /eqP INx /eqP IN'; subst x s0.
specialize (SEQUENTIAL s t ord_max (widen_ord (leqnSn n) i) SCHED SCHEDi).
inversion SEQUENTIAL; destruct i as [i EQ]; simpl in ×.
clear SEQUENTIAL SCHEDi.
by rewrite H0 ltnn in EQ.
}
}
Qed.
End Uniqueness.
Section NumberOfJobs.
Lemma num_scheduled_jobs_le_num_cpus :
∀ t,
size (jobs_scheduled_at sched t) ≤ num_cpus.
Proof.
intros t.
unfold jobs_scheduled_at.
destruct num_cpus; first by rewrite big_ord0.
apply leq_trans with (1×n.+1); last by rewrite mul1n.
apply size_bigcat_ord_max.
by ins; unfold make_sequence; desf.
Qed.
End NumberOfJobs.
End ScheduledJobsLemmas.
End Schedule.
Module ScheduleOfSporadicTask.
Import SporadicTask Job.
Export Schedule.
Section ScheduledJobs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → sporadic_task.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Variable tsk: sporadic_task.
Definition task_scheduled_on (cpu: processor num_cpus) (t: time) :=
if (sched cpu t) is Some j then
(job_task j == tsk)
else false.
Definition task_is_scheduled (t: time) :=
[∃ cpu, task_scheduled_on cpu t].
Definition jobs_of_task_scheduled_between (t1 t2: time) :=
filter (fun j ⇒ job_task j == tsk)
(jobs_scheduled_between sched t1 t2).
End ScheduledJobs.
Section ScheduleProperties.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Definition jobs_of_same_task_dont_execute_in_parallel :=
∀ j j' t,
job_task j = job_task j' →
scheduled sched j t →
scheduled sched j' t →
j = j'.
End ScheduleProperties.
Section BasicLemmas.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis jobs_dont_execute_after_completion :
completed_jobs_dont_execute job_cost sched.
Variable tsk: sporadic_task.
Variable j: Job.
Hypothesis H_job_of_task: job_task j = tsk.
Hypothesis valid_job:
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Lemma cumulative_service_le_task_cost :
∀ t t',
service_during sched j t t' ≤ task_cost tsk.
Proof.
rename valid_job into VALID; unfold valid_sporadic_job in *; ins; des.
apply leq_trans with (n := job_cost j);
last by rewrite -H_job_of_task; apply VALID0.
by apply cumulative_service_le_job_cost.
Qed.
End BasicLemmas.
End ScheduleOfSporadicTask.
prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Schedule.
Export ArrivalSequence.
Definition processor (num_cpus: nat) := 'I_num_cpus.
Section ScheduleDef.
Variable Job: eqType.
Variable num_cpus: nat.
Definition schedule :=
processor num_cpus → time → option Job.
End ScheduleDef.
Section ScheduledJobs.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Context {arr_seq: arrival_sequence Job}.
Variable job_cost: Job → time.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Variable j: Job.
Definition scheduled_on (cpu: processor num_cpus) (t: time) :=
sched cpu t == Some j.
Definition scheduled (t: time) :=
[∃ cpu, scheduled_on cpu t].
Definition is_idle (cpu: processor num_cpus) (t: time) :=
sched cpu t = None.
Definition service_at (t: time) :=
\sum_(cpu < num_cpus | scheduled_on cpu t) 1.
Definition service (t': time) := \sum_(0 ≤ t < t') service_at t.
Definition service_during (t1 t2: time) := \sum_(t1 ≤ t < t2) service_at t.
Definition completed (t: time) := service t ≥ job_cost j.
Definition pending (t: time) := has_arrived job_arrival j t && ~~completed t.
Definition backlogged (t: time) := pending t && ~~scheduled t.
Definition carried_in (t1: time) := arrived_before job_arrival j t1 && ~~ completed t1.
Definition carried_out (t1 t2: time) := arrived_before job_arrival j t2 && ~~ completed t2.
Definition jobs_scheduled_at (t: time) :=
\cat_(cpu < num_cpus) make_sequence (sched cpu t).
Definition jobs_scheduled_between (t1 t2: time) :=
undup (\cat_(t1 ≤ t < t2) jobs_scheduled_at t).
End ScheduledJobs.
Section ValidSchedules.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Definition sequential_jobs :=
∀ j t cpu1 cpu2,
sched cpu1 t = Some j → sched cpu2 t = Some j → cpu1 = cpu2.
Definition jobs_must_arrive_to_execute :=
∀ j t,
scheduled sched j t →
has_arrived job_arrival j t.
Definition completed_jobs_dont_execute :=
∀ j t, service sched j t ≤ job_cost j.
Definition jobs_come_from_arrival_sequence (arr_seq: arrival_sequence Job) :=
∀ j t, scheduled sched j t → arrives_in arr_seq j.
End ValidSchedules.
Section JobLemmas.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Variable j: Job.
Section Basic.
Lemma not_scheduled_no_service :
∀ t,
~~ scheduled sched j t = (service_at sched j t == 0).
Proof.
unfold scheduled, service_at, scheduled_on; intros t; apply/idP/idP.
{
intros NOTSCHED.
rewrite negb_exists in NOTSCHED.
move: NOTSCHED ⇒ /forallP NOTSCHED.
rewrite big_seq_cond.
rewrite → eq_bigr with (F2 := fun i ⇒ 0);
first by rewrite big_const_seq iter_addn mul0n addn0.
move ⇒ cpu /andP [_ /eqP SCHED].
by specialize (NOTSCHED cpu); rewrite SCHED eq_refl in NOTSCHED.
}
{
intros NOSERV; rewrite big_mkcond -sum_nat_eq0_nat in NOSERV.
move: NOSERV ⇒ /allP ALL.
rewrite negb_exists; apply/forallP; intros cpu.
exploit (ALL cpu); [by apply mem_index_enum | by desf].
}
Qed.
Lemma cumulative_service_implies_service :
∀ t1 t2,
service_during sched j t1 t2 != 0 →
∃ t,
t1 ≤ t < t2 ∧
service_at sched j t != 0.
Proof.
intros t1 t2 NONZERO.
destruct ([∃ t: 'I_t2, (t ≥ t1) && (service_at sched j t != 0)]) eqn:EX.
{
move: EX ⇒ /existsP EX; destruct EX as [x EX]. move: EX ⇒ /andP [GE SERV].
∃ x; split; last by done.
by apply/andP; split; [by done | apply ltn_ord].
}
{
apply negbT in EX; rewrite negb_exists in EX; move: EX ⇒ /forallP EX.
unfold service_during in NONZERO; rewrite big_nat_cond in NONZERO.
rewrite (eq_bigr (fun x ⇒ 0)) in NONZERO;
first by rewrite -big_nat_cond big_const_nat iter_addn mul0n addn0 in NONZERO.
intros i; rewrite andbT; move ⇒ /andP [GT LT].
specialize (EX (Ordinal LT)); simpl in EX.
by rewrite GT andTb negbK in EX; apply/eqP.
}
Qed.
Lemma service_implies_cumulative_service:
∀ t t1 t2,
t1 ≤ t < t2 →
service_at sched j t != 0 →
service_during sched j t1 t2 != 0.
Proof.
intros t t1 t2 LE NONZERO.
unfold service_during.
rewrite (bigD1_seq t) /=;
[| by rewrite mem_index_iota | by apply iota_uniq].
rewrite -lt0n -addn1 addnC.
by apply leq_add; first by rewrite lt0n.
Qed.
End Basic.
Section SequentialJobs.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Lemma service_at_most_one :
∀ t, service_at sched j t ≤ 1.
Proof.
unfold service_at, sequential_jobs in *; ins.
destruct (scheduled sched j t) eqn:SCHED; unfold scheduled in SCHED.
{
move: SCHED ⇒ /existsP [cpu SCHED]; des.
rewrite -big_filter (bigD1_seq cpu);
[simpl | | by have [e _ [UNIQ _ ] _] := big_enumP];
last by rewrite mem_filter; apply/andP; split.
rewrite -big_filter -filter_predI big_filter.
rewrite → eq_bigr with (F2 := fun cpu ⇒ 0);
first by rewrite /= big_const_seq iter_addn mul0n 2!addn0.
intro cpu'; move ⇒ /andP [/eqP NEQ /eqP SCHED'].
exfalso; apply NEQ.
by apply H_sequential_jobs with (j := j) (t := t); last by apply/eqP.
}
{
apply negbT in SCHED; rewrite negb_exists in SCHED.
move: SCHED ⇒ /forallP SCHED.
rewrite big_pred0; red; ins; apply negbTE, SCHED.
}
Qed.
Lemma cumulative_service_le_delta :
∀ t delta, service_during sched j t (t + delta) ≤ delta.
Proof.
unfold service_at, sequential_jobs in *; ins.
generalize dependent t.
induction delta.
{
ins; unfold service_during; rewrite addn0.
by rewrite big_geq.
}
{
unfold service_during; intro t.
rewrite -addn1 addnA addn1 big_nat_recr; last by apply leq_addr.
apply leq_add; first by apply IHdelta.
by apply service_at_most_one.
}
Qed.
End SequentialJobs.
Section Completion.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Lemma completion_monotonic :
∀ t t',
t ≤ t' →
completed job_cost sched j t →
completed job_cost sched j t'.
Proof.
unfold completed; move ⇒ t t' LE COMPt.
apply leq_trans with (service sched j t); first by done.
by rewrite /service /service_during [in X in _ ≤ X](@big_cat_nat _ _ _ t) //= leq_addr.
Qed.
Lemma completed_implies_not_scheduled :
∀ t,
completed job_cost sched j t →
~~ scheduled sched j t.
Proof.
rename H_completed_jobs into COMP.
unfold completed_jobs_dont_execute in ×.
intros t COMPLETED.
apply/negP; red; intro SCHED.
have BUG := COMP j t.+1.
rewrite leqNgt in BUG; move: BUG ⇒ /negP BUG; apply: BUG.
unfold service, service_during; rewrite big_nat_recr // /= -addn1.
apply leq_add; first by done.
by rewrite lt0n -not_scheduled_no_service negbK.
Qed.
Lemma cumulative_service_le_job_cost :
∀ t t',
service_during sched j t t' ≤ job_cost j.
Proof.
unfold service_during; rename H_completed_jobs into COMP; red in COMP; ins.
destruct (t > t') eqn:GT.
by rewrite big_geq // -ltnS; apply ltn_trans with (n := t); ins.
apply leq_trans with
(n := \sum_(0 ≤ t0 < t') service_at sched j t0);
last by apply COMP.
rewrite → big_cat_nat with (m := 0) (n := t);
[by apply leq_addl | by ins | by rewrite leqNgt negbT //].
Qed.
End Completion.
Section Arrival.
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute job_arrival sched.
Lemma service_before_job_arrival_zero :
∀ t,
t < job_arrival j →
service_at sched j t = 0.
Proof.
rename H_jobs_must_arrive into ARR; red in ARR; intros t LT.
specialize (ARR j t).
apply contra with (c := scheduled sched j t)
(b := has_arrived job_arrival j t) in ARR;
last by rewrite -ltnNge.
apply/eqP; rewrite -leqn0; unfold service_at.
rewrite big_pred0 //; red.
intros cpu; apply negbTE.
by move: ARR; rewrite negb_exists; move ⇒ /forallP ARR; apply ARR.
Qed.
Lemma cumulative_service_before_job_arrival_zero :
∀ t1 t2,
t2 ≤ 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_job_arrival_zero; first by ins.
by apply leq_trans with (n := t2); ins.
Qed.
Lemma service_before_arrival_eq_service_during :
∀ t0 t,
t0 ≤ job_arrival j →
\sum_(t0 ≤ t < job_arrival j + t) service_at sched j t =
\sum_(job_arrival j ≤ t < job_arrival j + t) service_at sched j t.
Proof.
intros t0 t LE; rewrite → big_cat_nat with (n := job_arrival j);
[| by ins | by apply leq_addr].
by rewrite /= cumulative_service_before_job_arrival_zero; [rewrite add0n | apply leqnn].
Qed.
End Arrival.
Section Pending.
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Lemma scheduled_implies_pending:
∀ t,
scheduled sched j t →
pending job_arrival job_cost sched j t.
Proof.
rename H_jobs_must_arrive into ARRIVE,
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 ARRIVE.
apply/negP; unfold not; intro COMPLETED.
have BUG := COMP j t.+1.
rewrite leqNgt in BUG; move: BUG ⇒ /negP BUG; apply BUG.
unfold service; rewrite -addn1 big_nat_recr // /=.
apply leq_add; first by done.
rewrite lt0n; apply/eqP; red; move ⇒ /eqP NOSERV.
rewrite -not_scheduled_no_service in NOSERV.
by rewrite SCHED in NOSERV.
Qed.
End Pending.
End JobLemmas.
Section ScheduledJobsLemmas.
Context {Job: eqType}.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Section Membership.
Lemma mem_scheduled_jobs_eq_scheduled :
∀ j t,
j \in jobs_scheduled_at sched t = scheduled sched j t.
Proof.
unfold jobs_scheduled_at, scheduled, scheduled_on.
intros j t; apply/idP/idP.
{
intros IN.
apply mem_bigcat_ord_exists in IN; des.
apply/existsP; ∃ i.
destruct (sched i t); last by done.
by rewrite mem_seq1 in IN; move: IN ⇒ /eqP IN; subst.
}
{
move ⇒ /existsP EX; destruct EX as [i SCHED].
apply mem_bigcat_ord with (j := i); first by apply ltn_ord.
by move: SCHED ⇒ /eqP SCHED; rewrite SCHED /= mem_seq1 eq_refl.
}
Qed.
End Membership.
Section Uniqueness.
Hypothesis H_sequential_jobs : sequential_jobs sched.
Lemma scheduled_jobs_uniq :
∀ t,
uniq (jobs_scheduled_at sched t).
Proof.
intros t; rename H_sequential_jobs into SEQUENTIAL.
unfold sequential_jobs in SEQUENTIAL.
clear -SEQUENTIAL.
unfold jobs_scheduled_at.
induction num_cpus; first by rewrite big_ord0.
{
rewrite big_ord_recr cat_uniq; apply/andP; split.
{
apply bigcat_ord_uniq;
first by intro i; unfold make_sequence; desf.
intros x i1 i2 IN1 IN2; unfold make_sequence in ×.
desf; move: Heq0 Heq ⇒ SOME1 SOME2.
rewrite mem_seq1 in IN1; rewrite mem_seq1 in IN2.
move: IN1 IN2 ⇒ /eqP IN1 /eqP IN2; subst x s0.
specialize (SEQUENTIAL s t (widen_ord (leqnSn n) i1)
(widen_ord (leqnSn n) i2) SOME1 SOME2).
by inversion SEQUENTIAL; apply ord_inj.
}
apply/andP; split; last by unfold make_sequence; destruct (sched ord_max).
{
rewrite -all_predC; apply/allP; unfold predC; simpl.
intros x INx.
unfold make_sequence in INx.
destruct (sched ord_max t) eqn:SCHED;
last by rewrite in_nil in INx.
apply/negP; unfold not; intro IN'.
have EX := mem_bigcat_ord_exists _ x n.
apply EX in IN'; des; clear EX.
unfold make_sequence in IN'.
desf; rename Heq into SCHEDi.
rewrite mem_seq1 in INx; rewrite mem_seq1 in IN'.
move: INx IN' ⇒ /eqP INx /eqP IN'; subst x s0.
specialize (SEQUENTIAL s t ord_max (widen_ord (leqnSn n) i) SCHED SCHEDi).
inversion SEQUENTIAL; destruct i as [i EQ]; simpl in ×.
clear SEQUENTIAL SCHEDi.
by rewrite H0 ltnn in EQ.
}
}
Qed.
End Uniqueness.
Section NumberOfJobs.
Lemma num_scheduled_jobs_le_num_cpus :
∀ t,
size (jobs_scheduled_at sched t) ≤ num_cpus.
Proof.
intros t.
unfold jobs_scheduled_at.
destruct num_cpus; first by rewrite big_ord0.
apply leq_trans with (1×n.+1); last by rewrite mul1n.
apply size_bigcat_ord_max.
by ins; unfold make_sequence; desf.
Qed.
End NumberOfJobs.
End ScheduledJobsLemmas.
End Schedule.
Module ScheduleOfSporadicTask.
Import SporadicTask Job.
Export Schedule.
Section ScheduledJobs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → sporadic_task.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Variable tsk: sporadic_task.
Definition task_scheduled_on (cpu: processor num_cpus) (t: time) :=
if (sched cpu t) is Some j then
(job_task j == tsk)
else false.
Definition task_is_scheduled (t: time) :=
[∃ cpu, task_scheduled_on cpu t].
Definition jobs_of_task_scheduled_between (t1 t2: time) :=
filter (fun j ⇒ job_task j == tsk)
(jobs_scheduled_between sched t1 t2).
End ScheduledJobs.
Section ScheduleProperties.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Definition jobs_of_same_task_dont_execute_in_parallel :=
∀ j j' t,
job_task j = job_task j' →
scheduled sched j t →
scheduled sched j' t →
j = j'.
End ScheduleProperties.
Section BasicLemmas.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis jobs_dont_execute_after_completion :
completed_jobs_dont_execute job_cost sched.
Variable tsk: sporadic_task.
Variable j: Job.
Hypothesis H_job_of_task: job_task j = tsk.
Hypothesis valid_job:
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Lemma cumulative_service_le_task_cost :
∀ t t',
service_during sched j t t' ≤ task_cost tsk.
Proof.
rename valid_job into VALID; unfold valid_sporadic_job in *; ins; des.
apply leq_trans with (n := job_cost j);
last by rewrite -H_job_of_task; apply VALID0.
by apply cumulative_service_le_job_cost.
Qed.
End BasicLemmas.
End ScheduleOfSporadicTask.