Library rt.model.schedule.uni.service
Require Import rt.util.all.
Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence
rt.model.priority.
Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.workload.
Module Service.
Import UniprocessorSchedule Priority Workload.
(* In this section, we define the more general notion of service received by sets of jobs. *)
Section ServiceOverSets.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
(* Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
(* ...and any uniprocessor schedule of these jobs. *)
Variable sched: schedule Job.
(* Let jobs denote any (finite) set of jobs. *)
Variable jobs: seq Job.
Section Definitions.
(* First, we define the service received by a generic set of jobs. *)
Section ServiceOfJobs.
(* Then, given any predicate over jobs, ...*)
Variable P: Job → bool.
(* ...we define the cumulative service received during [t1, t2)
by the jobs that satisfy this predicate. *)
Definition service_of_jobs (t1 t2: time) :=
\sum_(j <- jobs | P j) service_during sched j t1 t2.
End ServiceOfJobs.
(* Next, we define the service received by tasks with higher-or-equal
priority under a given FP policy. *)
Section PerTaskPriority.
Context {Task: eqType}.
Variable job_task: Job → Task.
(* Consider any FP policy. *)
Variable higher_eq_priority: FP_policy Task.
(* Let tsk be the task to be analyzed. *)
Variable tsk: Task.
(* Based on the definition of jobs of higher or equal priority (with respect to tsk), ... *)
Let of_higher_or_equal_priority j := higher_eq_priority (job_task j) tsk.
(* ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
Definition service_of_higher_or_equal_priority_tasks (t1 t2: time) :=
service_of_jobs of_higher_or_equal_priority t1 t2.
End PerTaskPriority.
(* Next, we define the service received by jobs with higher or equal priority
under JLFP policies. *)
Section PerJobPriority.
(* Consider any JLDP policy. *)
Variable higher_eq_priority: JLFP_policy Job.
(* Let j be the job to be analyzed. *)
Variable j: Job.
(* Based on the definition of jobs of higher or equal priority, ... *)
Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
(* ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
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.
(* Let P be any predicate over jobs. *)
Variable P: Job → bool.
(* In this section, we prove that the service received by any set of jobs
is upper-bounded by the corresponding workload. *)
Section ServiceBoundedByWorkload.
(* Recall the definition of workload. *)
Let workload_of := workload_of_jobs job_cost.
(* Assume that jobs do not execute after completion.*)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Then, we prove that the service received by those jobs is no larger than their workload. *)
Lemma service_of_jobs_le_workload:
∀ t1 t2,
service_of_jobs P t1 t2 ≤ workload_of jobs P.
End ServiceBoundedByWorkload.
(* In this section, we prove that the service received by any set of jobs
is upper-bounded by the corresponding interval length. *)
Section ServiceBoundedByIntervalLength.
(* Assume that jobs do not execute after completion.*)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the sequence of jobs is a set. *)
Hypothesis H_no_duplicate_jobs: uniq jobs.
(* Then, we prove that the service received by those jobs is no larger than their workload. *)
Lemma service_of_jobs_le_delta:
∀ t1 t2,
service_of_jobs P t1 t2 ≤ t2 - t1.
End ServiceBoundedByIntervalLength.
End Lemmas.
End ServiceOverSets.
End Service.
Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence
rt.model.priority.
Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.workload.
Module Service.
Import UniprocessorSchedule Priority Workload.
(* In this section, we define the more general notion of service received by sets of jobs. *)
Section ServiceOverSets.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
(* Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
(* ...and any uniprocessor schedule of these jobs. *)
Variable sched: schedule Job.
(* Let jobs denote any (finite) set of jobs. *)
Variable jobs: seq Job.
Section Definitions.
(* First, we define the service received by a generic set of jobs. *)
Section ServiceOfJobs.
(* Then, given any predicate over jobs, ...*)
Variable P: Job → bool.
(* ...we define the cumulative service received during [t1, t2)
by the jobs that satisfy this predicate. *)
Definition service_of_jobs (t1 t2: time) :=
\sum_(j <- jobs | P j) service_during sched j t1 t2.
End ServiceOfJobs.
(* Next, we define the service received by tasks with higher-or-equal
priority under a given FP policy. *)
Section PerTaskPriority.
Context {Task: eqType}.
Variable job_task: Job → Task.
(* Consider any FP policy. *)
Variable higher_eq_priority: FP_policy Task.
(* Let tsk be the task to be analyzed. *)
Variable tsk: Task.
(* Based on the definition of jobs of higher or equal priority (with respect to tsk), ... *)
Let of_higher_or_equal_priority j := higher_eq_priority (job_task j) tsk.
(* ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
Definition service_of_higher_or_equal_priority_tasks (t1 t2: time) :=
service_of_jobs of_higher_or_equal_priority t1 t2.
End PerTaskPriority.
(* Next, we define the service received by jobs with higher or equal priority
under JLFP policies. *)
Section PerJobPriority.
(* Consider any JLDP policy. *)
Variable higher_eq_priority: JLFP_policy Job.
(* Let j be the job to be analyzed. *)
Variable j: Job.
(* Based on the definition of jobs of higher or equal priority, ... *)
Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
(* ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
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.
(* Let P be any predicate over jobs. *)
Variable P: Job → bool.
(* In this section, we prove that the service received by any set of jobs
is upper-bounded by the corresponding workload. *)
Section ServiceBoundedByWorkload.
(* Recall the definition of workload. *)
Let workload_of := workload_of_jobs job_cost.
(* Assume that jobs do not execute after completion.*)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Then, we prove that the service received by those jobs is no larger than their workload. *)
Lemma service_of_jobs_le_workload:
∀ t1 t2,
service_of_jobs P t1 t2 ≤ workload_of jobs P.
End ServiceBoundedByWorkload.
(* In this section, we prove that the service received by any set of jobs
is upper-bounded by the corresponding interval length. *)
Section ServiceBoundedByIntervalLength.
(* Assume that jobs do not execute after completion.*)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the sequence of jobs is a set. *)
Hypothesis H_no_duplicate_jobs: uniq jobs.
(* Then, we prove that the service received by those jobs is no larger than their workload. *)
Lemma service_of_jobs_le_delta:
∀ t1 t2,
service_of_jobs P t1 t2 ≤ t2 - t1.
End ServiceBoundedByIntervalLength.
End Lemmas.
End ServiceOverSets.
End Service.