Library prosa.classic.model.schedule.uni.limited.schedule
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Import Job Service UniprocessorSchedule.
Section Definitions.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Variable job_lock_in_service: Job → time.
Definition job_lock_in_service_positive :=
∀ j,
arrives_in arr_seq j →
job_cost_positive job_cost j →
0 < job_lock_in_service j.
Definition job_lock_in_service_le_job_cost :=
∀ j,
arrives_in arr_seq j →
job_cost_positive job_cost j →
job_lock_in_service j ≤ job_cost j.
Definition job_nonpreemptive_after_lock_in_service :=
∀ j t t',
arrives_in arr_seq j →
t ≤ t' →
job_lock_in_service j ≤ service sched j t →
~~ completed_by job_cost sched j t' →
scheduled_at sched j t'.
Definition proper_job_lock_in_service :=
job_lock_in_service_positive ∧
job_lock_in_service_le_job_cost ∧
job_nonpreemptive_after_lock_in_service.
Variable task_lock_in_service: Task → time.
Definition task_lock_in_service_le_task_cost tsk :=
task_lock_in_service tsk ≤ task_cost tsk.
Definition task_lock_in_service_bounds_job_lock_in_service tsk :=
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_lock_in_service j ≤ task_lock_in_service tsk.
Definition proper_task_lock_in_service tsk :=
task_lock_in_service_le_task_cost tsk ∧
task_lock_in_service_bounds_job_lock_in_service tsk.
End Definitions.
Section Examples.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Section FullyPreemptiveModel.
Let job_lock_in_service (j: Job) := job_cost j.
Lemma job_nonpreemptive_after_lock_in_service_trivial:
job_nonpreemptive_after_lock_in_service job_cost arr_seq sched job_lock_in_service .
Proof.
intros j ? ? ARR LE SERV NCOMP.
move: NCOMP ⇒ /negP NCOMP; exfalso; apply: NCOMP.
move: (H_completed_jobs_dont_execute j t) ⇒ SERV2.
by apply completion_monotonic with t.
Qed.
End FullyPreemptiveModel.
Section FullyNonPreemptiveModel.
Let job_lock_in_service (j: Job) := ε.
Hypothesis H_is_nonpreemptive_schedule:
NonpreemptiveSchedule.is_nonpreemptive_schedule job_cost sched.
Lemma property_last_segment_is_nonpreemptive_holds:
job_nonpreemptive_after_lock_in_service job_cost arr_seq sched job_lock_in_service .
Proof.
unfold NonpreemptiveSchedule.is_nonpreemptive_schedule in ×.
intros j ? ? ARR LE NEQ NCOMPL; unfold job_lock_in_service in ×.
have POS: 0 < job_cost j.
{ rewrite -[0 < _]Bool.negb_involutive -eqn0Ngt; apply/negP; intros ZERO.
move: ZERO ⇒ /eqP ZERO.
rewrite /completed_by in NCOMPL.
rewrite ZERO -lt0n in NCOMPL.
move: (H_completed_jobs_dont_execute j t') ⇒ NN.
by rewrite ZERO leqNgt in NN; move: NN ⇒ /negP NN; apply: NN.
}
move: NEQ ⇒ /sum_seq_gt0P [ts [IN SCHED]].
rewrite lt0b in SCHED.
apply H_is_nonpreemptive_schedule with ts; try done.
apply ltnW, leq_trans with t; last by done.
by rewrite mem_iota add0n subn0 in IN; move: IN ⇒ /andP [_ IN].
Qed.
End FullyNonPreemptiveModel.
End Examples.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Import Job Service UniprocessorSchedule.
Section Definitions.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Variable job_lock_in_service: Job → time.
Definition job_lock_in_service_positive :=
∀ j,
arrives_in arr_seq j →
job_cost_positive job_cost j →
0 < job_lock_in_service j.
Definition job_lock_in_service_le_job_cost :=
∀ j,
arrives_in arr_seq j →
job_cost_positive job_cost j →
job_lock_in_service j ≤ job_cost j.
Definition job_nonpreemptive_after_lock_in_service :=
∀ j t t',
arrives_in arr_seq j →
t ≤ t' →
job_lock_in_service j ≤ service sched j t →
~~ completed_by job_cost sched j t' →
scheduled_at sched j t'.
Definition proper_job_lock_in_service :=
job_lock_in_service_positive ∧
job_lock_in_service_le_job_cost ∧
job_nonpreemptive_after_lock_in_service.
Variable task_lock_in_service: Task → time.
Definition task_lock_in_service_le_task_cost tsk :=
task_lock_in_service tsk ≤ task_cost tsk.
Definition task_lock_in_service_bounds_job_lock_in_service tsk :=
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_lock_in_service j ≤ task_lock_in_service tsk.
Definition proper_task_lock_in_service tsk :=
task_lock_in_service_le_task_cost tsk ∧
task_lock_in_service_bounds_job_lock_in_service tsk.
End Definitions.
Section Examples.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Section FullyPreemptiveModel.
Let job_lock_in_service (j: Job) := job_cost j.
Lemma job_nonpreemptive_after_lock_in_service_trivial:
job_nonpreemptive_after_lock_in_service job_cost arr_seq sched job_lock_in_service .
Proof.
intros j ? ? ARR LE SERV NCOMP.
move: NCOMP ⇒ /negP NCOMP; exfalso; apply: NCOMP.
move: (H_completed_jobs_dont_execute j t) ⇒ SERV2.
by apply completion_monotonic with t.
Qed.
End FullyPreemptiveModel.
Section FullyNonPreemptiveModel.
Let job_lock_in_service (j: Job) := ε.
Hypothesis H_is_nonpreemptive_schedule:
NonpreemptiveSchedule.is_nonpreemptive_schedule job_cost sched.
Lemma property_last_segment_is_nonpreemptive_holds:
job_nonpreemptive_after_lock_in_service job_cost arr_seq sched job_lock_in_service .
Proof.
unfold NonpreemptiveSchedule.is_nonpreemptive_schedule in ×.
intros j ? ? ARR LE NEQ NCOMPL; unfold job_lock_in_service in ×.
have POS: 0 < job_cost j.
{ rewrite -[0 < _]Bool.negb_involutive -eqn0Ngt; apply/negP; intros ZERO.
move: ZERO ⇒ /eqP ZERO.
rewrite /completed_by in NCOMPL.
rewrite ZERO -lt0n in NCOMPL.
move: (H_completed_jobs_dont_execute j t') ⇒ NN.
by rewrite ZERO leqNgt in NN; move: NN ⇒ /negP NN; apply: NN.
}
move: NEQ ⇒ /sum_seq_gt0P [ts [IN SCHED]].
rewrite lt0b in SCHED.
apply H_is_nonpreemptive_schedule with ts; try done.
apply ltnW, leq_trans with t; last by done.
by rewrite mem_iota add0n subn0 in IN; move: IN ⇒ /andP [_ IN].
Qed.
End FullyNonPreemptiveModel.
End Examples.