Library prosa.classic.model.schedule.uni.service
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.workload.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Service.
Import UniprocessorSchedule Priority Workload.
Section ServiceOverSets.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Variable jobs: seq Job.
Section Definitions.
Section ServiceOfJobs.
Variable P: Job → bool.
Definition service_of_jobs (t1 t2: time) :=
\sum_(j <- jobs | P j) service_during sched j t1 t2.
End ServiceOfJobs.
Section PerTaskPriority.
Context {Task: eqType}.
Variable job_task: Job → Task.
Variable higher_eq_priority: FP_policy Task.
Variable tsk: Task.
Let of_higher_or_equal_priority j := higher_eq_priority (job_task j) tsk.
Definition service_of_higher_or_equal_priority_tasks (t1 t2: time) :=
service_of_jobs of_higher_or_equal_priority t1 t2.
End PerTaskPriority.
Section PerJobPriority.
Variable higher_eq_priority: JLFP_policy Job.
Variable j: Job.
Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
Definition service_of_higher_or_equal_priority_jobs (t1 t2: time) :=
service_of_jobs of_higher_or_equal_priority t1 t2.
End PerJobPriority.
End Definitions.
Section Lemmas.
Variable P: Job → bool.
Section ServiceBoundedByWorkload.
Let workload_of := workload_of_jobs job_cost.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Lemma service_of_jobs_le_workload:
∀ t1 t2,
service_of_jobs P t1 t2 ≤ workload_of jobs P.
End ServiceBoundedByWorkload.
Section ServiceBoundedByIntervalLength.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_no_duplicate_jobs: uniq jobs.
Lemma service_of_jobs_le_delta:
∀ t1 t2,
service_of_jobs P t1 t2 ≤ t2 - t1.
End ServiceBoundedByIntervalLength.
End Lemmas.
End ServiceOverSets.
Section ExtraDefinitions.
Context {Task: eqType}.
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 tsk: Task.
Let of_task_tsk j := job_task j == tsk.
Definition task_service_of_jobs_received_in ta1 ta2 t1 t2 :=
service_of_jobs sched (jobs_arrived_between arr_seq ta1 ta2) of_task_tsk t1 t2.
Definition task_service_between t1 t2 := task_service_of_jobs_received_in t1 t2 t1 t2.
End ExtraDefinitions.
Section ExtraLemmas.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
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_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
Let job_completed_by := completed_by job_cost sched.
Let arrivals_between := jobs_arrived_between arr_seq.
Lemma service_monotonic:
∀ j t1 t2,
t1 ≤ t2 →
service sched j t1 ≤ service sched j t2.
Lemma service_during_cat:
∀ j t t1 t2,
t1 ≤ t ≤ t2 →
service_during sched j t1 t2 =
service_during sched j t1 t + service_during sched j t t2.
Lemma incremental_service_during:
∀ j t1 t2 k,
service_during sched j t1 t2 > k →
∃ t, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = k.
Lemma service_of_jobs_le_1:
∀ (t1 t2 t: time) (P: Job → bool),
\sum_(j <- arrivals_between t1 t2 | P j) service_at sched j t ≤ 1.
Lemma total_service_of_jobs_le_delta:
∀ (t Δ: time) (P: Job → bool),
\sum_(j <- arrivals_between t (t + Δ) | P j)
service_during sched j t (t + Δ) ≤ Δ.
Lemma low_service_implies_existence_of_idle_time :
∀ t1 t2,
t1 ≤ t2 →
service_of_jobs sched (arrivals_between 0 t2) predT t1 t2 < t2 - t1 →
∃ t, t1 ≤ t < t2 ∧ is_idle sched t.
Section ServiceCat.
Lemma service_of_jobs_cat_scheduling_interval :
∀ P t1 t2 t,
t1 ≤ t ≤ t2 →
service_of_jobs sched (arrivals_between t1 t2) P t1 t2
= service_of_jobs sched (arrivals_between t1 t) P t1 t
+ service_of_jobs sched (arrivals_between t1 t) P t t2
+ service_of_jobs sched (arrivals_between t t2) P t t2.
Lemma service_of_jobs_cat_arrival_interval :
∀ P t1 t2 t,
t1 ≤ t ≤ t2 →
service_of_jobs sched (arrivals_between t1 t2) P t t2 =
service_of_jobs sched (arrivals_between t1 t) P t t2 +
service_of_jobs sched (arrivals_between t t2) P t t2.
End ServiceCat.
Section WorkloadServiceAndCompletion.
Variable P: Job → bool.
Variables t1 t2: time.
Let jobs := arrivals_between t1 t2.
Variable t_compl: time.
Lemma workload_eq_service_impl_all_jobs_have_completed:
workload_of_jobs job_cost jobs P =
service_of_jobs sched jobs P t1 t_compl →
(∀ j, j \in jobs → P j → job_completed_by j t_compl).
Lemma all_jobs_have_completed_impl_workload_eq_service:
(∀ j, j \in jobs → P j → job_completed_by j t_compl) →
workload_of_jobs job_cost jobs P =
service_of_jobs sched jobs P t1 t_compl.
Lemma all_jobs_have_completed_equiv_workload_eq_service:
(∀ j, j \in jobs → P j → job_completed_by j t_compl) ↔
workload_of_jobs job_cost jobs P =
service_of_jobs sched jobs P t1 t_compl.
End WorkloadServiceAndCompletion.
End ExtraLemmas.
End Service.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.workload.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Service.
Import UniprocessorSchedule Priority Workload.
Section ServiceOverSets.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Variable jobs: seq Job.
Section Definitions.
Section ServiceOfJobs.
Variable P: Job → bool.
Definition service_of_jobs (t1 t2: time) :=
\sum_(j <- jobs | P j) service_during sched j t1 t2.
End ServiceOfJobs.
Section PerTaskPriority.
Context {Task: eqType}.
Variable job_task: Job → Task.
Variable higher_eq_priority: FP_policy Task.
Variable tsk: Task.
Let of_higher_or_equal_priority j := higher_eq_priority (job_task j) tsk.
Definition service_of_higher_or_equal_priority_tasks (t1 t2: time) :=
service_of_jobs of_higher_or_equal_priority t1 t2.
End PerTaskPriority.
Section PerJobPriority.
Variable higher_eq_priority: JLFP_policy Job.
Variable j: Job.
Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
Definition service_of_higher_or_equal_priority_jobs (t1 t2: time) :=
service_of_jobs of_higher_or_equal_priority t1 t2.
End PerJobPriority.
End Definitions.
Section Lemmas.
Variable P: Job → bool.
Section ServiceBoundedByWorkload.
Let workload_of := workload_of_jobs job_cost.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Lemma service_of_jobs_le_workload:
∀ t1 t2,
service_of_jobs P t1 t2 ≤ workload_of jobs P.
End ServiceBoundedByWorkload.
Section ServiceBoundedByIntervalLength.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_no_duplicate_jobs: uniq jobs.
Lemma service_of_jobs_le_delta:
∀ t1 t2,
service_of_jobs P t1 t2 ≤ t2 - t1.
End ServiceBoundedByIntervalLength.
End Lemmas.
End ServiceOverSets.
Section ExtraDefinitions.
Context {Task: eqType}.
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 tsk: Task.
Let of_task_tsk j := job_task j == tsk.
Definition task_service_of_jobs_received_in ta1 ta2 t1 t2 :=
service_of_jobs sched (jobs_arrived_between arr_seq ta1 ta2) of_task_tsk t1 t2.
Definition task_service_between t1 t2 := task_service_of_jobs_received_in t1 t2 t1 t2.
End ExtraDefinitions.
Section ExtraLemmas.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
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_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
Let job_completed_by := completed_by job_cost sched.
Let arrivals_between := jobs_arrived_between arr_seq.
Lemma service_monotonic:
∀ j t1 t2,
t1 ≤ t2 →
service sched j t1 ≤ service sched j t2.
Lemma service_during_cat:
∀ j t t1 t2,
t1 ≤ t ≤ t2 →
service_during sched j t1 t2 =
service_during sched j t1 t + service_during sched j t t2.
Lemma incremental_service_during:
∀ j t1 t2 k,
service_during sched j t1 t2 > k →
∃ t, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = k.
Lemma service_of_jobs_le_1:
∀ (t1 t2 t: time) (P: Job → bool),
\sum_(j <- arrivals_between t1 t2 | P j) service_at sched j t ≤ 1.
Lemma total_service_of_jobs_le_delta:
∀ (t Δ: time) (P: Job → bool),
\sum_(j <- arrivals_between t (t + Δ) | P j)
service_during sched j t (t + Δ) ≤ Δ.
Lemma low_service_implies_existence_of_idle_time :
∀ t1 t2,
t1 ≤ t2 →
service_of_jobs sched (arrivals_between 0 t2) predT t1 t2 < t2 - t1 →
∃ t, t1 ≤ t < t2 ∧ is_idle sched t.
Section ServiceCat.
Lemma service_of_jobs_cat_scheduling_interval :
∀ P t1 t2 t,
t1 ≤ t ≤ t2 →
service_of_jobs sched (arrivals_between t1 t2) P t1 t2
= service_of_jobs sched (arrivals_between t1 t) P t1 t
+ service_of_jobs sched (arrivals_between t1 t) P t t2
+ service_of_jobs sched (arrivals_between t t2) P t t2.
Lemma service_of_jobs_cat_arrival_interval :
∀ P t1 t2 t,
t1 ≤ t ≤ t2 →
service_of_jobs sched (arrivals_between t1 t2) P t t2 =
service_of_jobs sched (arrivals_between t1 t) P t t2 +
service_of_jobs sched (arrivals_between t t2) P t t2.
End ServiceCat.
Section WorkloadServiceAndCompletion.
Variable P: Job → bool.
Variables t1 t2: time.
Let jobs := arrivals_between t1 t2.
Variable t_compl: time.
Lemma workload_eq_service_impl_all_jobs_have_completed:
workload_of_jobs job_cost jobs P =
service_of_jobs sched jobs P t1 t_compl →
(∀ j, j \in jobs → P j → job_completed_by j t_compl).
Lemma all_jobs_have_completed_impl_workload_eq_service:
(∀ j, j \in jobs → P j → job_completed_by j t_compl) →
workload_of_jobs job_cost jobs P =
service_of_jobs sched jobs P t1 t_compl.
Lemma all_jobs_have_completed_equiv_workload_eq_service:
(∀ j, j \in jobs → P j → job_completed_by j t_compl) ↔
workload_of_jobs job_cost jobs P =
service_of_jobs sched jobs P t1 t_compl.
End WorkloadServiceAndCompletion.
End ExtraLemmas.
End Service.