Library rt.model.schedule.uni.jitter.schedule
Require Import rt.util.all.
Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job.
Require Import rt.model.schedule.uni.schedule.
Require Import rt.model.arrival.jitter.arrival_sequence.
(* In this file, we prove additional definitions and lemmas about jitter-aware schedules. *)
Module UniprocessorScheduleWithJitter.
(* To formalize jitter, we import the original uniprocessor schedule and
redefine some of the properties. *)
Export ArrivalSequenceWithJitter UniprocessorSchedule.
(* In this section we redefine properties that depend on the arrival time. *)
Section RedefiningProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
(* Consider any uniprocessor schedule. *)
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
(* First, we redefine some job properties. *)
Section JobProperties.
(* Let j be any job in the arrival sequence. *)
Variable j: Job.
(* Then, we say that job j is pending at time t iff the jitter has passed but
j has not completed by time t. *)
Definition pending (t: time) :=
jitter_has_passed job_arrival job_jitter j t && ~~ completed_by job_cost sched j t.
(* Finally, we say that job j is backlogged at time t iff it is pending and not scheduled. *)
Definition backlogged (t: time) :=
pending t && ~~ scheduled_at sched j t.
End JobProperties.
(* Next, we define properties of a valid jitter-aware schedule. *)
Section ValidSchedules.
(* In any jitter-aware schedule, a job can only be scheduled after
the jitter has passed. *)
Definition jobs_execute_after_jitter :=
∀ j t,
scheduled_at sched j t → jitter_has_passed job_arrival job_jitter j t.
End ValidSchedules.
(* In this section, we prove some basic lemmas about jitter-aware schedules. *)
Section Lemmas.
(* For simplicity, let's define some local names. *)
Let has_actually_arrived := jitter_has_passed job_arrival job_jitter.
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
(* We begin by proving properties related to job arrivals. *)
Section Arrival.
(* Assume that jobs only execute after the jitter has passed. *)
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
(* First, we show that every job in the schedule only executes after its arrival time. *)
Lemma jobs_with_jitter_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* Now, let j be any job. *)
Variable j: Job.
(* First, we show that if the jitter has passed, then the job must have arrived. *)
Lemma jitter_has_passed_implies_arrived:
∀ t,
has_actually_arrived j t →
has_arrived job_arrival j t.
(* Now we prove that job j does not receive service at any time t before
its actual arrival time. *)
Lemma service_before_jitter_is_zero :
∀ t,
t < actual_job_arrival j →
service_at sched j t = 0.
(* Note that the same property applies to the cumulative service. *)
Lemma cumulative_service_before_jitter_is_zero :
∀ t1 t2,
t2 ≤ actual_job_arrival j →
\sum_(t1 ≤ i < t2) service_at sched j i = 0.
(* Hence, one can ignore the service received by a job before the jitter. *)
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.
End Arrival.
(* In this section, we prove properties about pending jobs. *)
Section Pending.
(* Assume that jobs only execute after the jitter has passed... *)
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
(* ...and that completed jobs do not execute. *)
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
(* Let j be any job. *)
Variable j: Job.
(* First, we show that if job j is scheduled, then it must be pending. *)
Lemma scheduled_implies_pending:
∀ t,
scheduled_at sched j t → pending j t.
End Pending.
End Lemmas.
End RedefiningProperties.
End UniprocessorScheduleWithJitter.
Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job.
Require Import rt.model.schedule.uni.schedule.
Require Import rt.model.arrival.jitter.arrival_sequence.
(* In this file, we prove additional definitions and lemmas about jitter-aware schedules. *)
Module UniprocessorScheduleWithJitter.
(* To formalize jitter, we import the original uniprocessor schedule and
redefine some of the properties. *)
Export ArrivalSequenceWithJitter UniprocessorSchedule.
(* In this section we redefine properties that depend on the arrival time. *)
Section RedefiningProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
(* Consider any uniprocessor schedule. *)
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
(* First, we redefine some job properties. *)
Section JobProperties.
(* Let j be any job in the arrival sequence. *)
Variable j: Job.
(* Then, we say that job j is pending at time t iff the jitter has passed but
j has not completed by time t. *)
Definition pending (t: time) :=
jitter_has_passed job_arrival job_jitter j t && ~~ completed_by job_cost sched j t.
(* Finally, we say that job j is backlogged at time t iff it is pending and not scheduled. *)
Definition backlogged (t: time) :=
pending t && ~~ scheduled_at sched j t.
End JobProperties.
(* Next, we define properties of a valid jitter-aware schedule. *)
Section ValidSchedules.
(* In any jitter-aware schedule, a job can only be scheduled after
the jitter has passed. *)
Definition jobs_execute_after_jitter :=
∀ j t,
scheduled_at sched j t → jitter_has_passed job_arrival job_jitter j t.
End ValidSchedules.
(* In this section, we prove some basic lemmas about jitter-aware schedules. *)
Section Lemmas.
(* For simplicity, let's define some local names. *)
Let has_actually_arrived := jitter_has_passed job_arrival job_jitter.
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
(* We begin by proving properties related to job arrivals. *)
Section Arrival.
(* Assume that jobs only execute after the jitter has passed. *)
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
(* First, we show that every job in the schedule only executes after its arrival time. *)
Lemma jobs_with_jitter_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* Now, let j be any job. *)
Variable j: Job.
(* First, we show that if the jitter has passed, then the job must have arrived. *)
Lemma jitter_has_passed_implies_arrived:
∀ t,
has_actually_arrived j t →
has_arrived job_arrival j t.
(* Now we prove that job j does not receive service at any time t before
its actual arrival time. *)
Lemma service_before_jitter_is_zero :
∀ t,
t < actual_job_arrival j →
service_at sched j t = 0.
(* Note that the same property applies to the cumulative service. *)
Lemma cumulative_service_before_jitter_is_zero :
∀ t1 t2,
t2 ≤ actual_job_arrival j →
\sum_(t1 ≤ i < t2) service_at sched j i = 0.
(* Hence, one can ignore the service received by a job before the jitter. *)
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.
End Arrival.
(* In this section, we prove properties about pending jobs. *)
Section Pending.
(* Assume that jobs only execute after the jitter has passed... *)
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
(* ...and that completed jobs do not execute. *)
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
(* Let j be any job. *)
Variable j: Job.
(* First, we show that if job j is scheduled, then it must be pending. *)
Lemma scheduled_implies_pending:
∀ t,
scheduled_at sched j t → pending j t.
End Pending.
End Lemmas.
End RedefiningProperties.
End UniprocessorScheduleWithJitter.