Library prosa.classic.model.schedule.uni.jitter.schedule
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.arrival.jitter.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module UniprocessorScheduleWithJitter.
Export ArrivalSequenceWithJitter UniprocessorSchedule.
Section RedefiningProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Section JobProperties.
Variable j: Job.
Definition pending (t: time) :=
jitter_has_passed job_arrival job_jitter j t && ~~ completed_by job_cost sched j t.
Definition backlogged (t: time) :=
pending t && ~~ scheduled_at sched j t.
End JobProperties.
Section ValidSchedules.
Definition jobs_execute_after_jitter :=
∀ j t,
scheduled_at sched j t → jitter_has_passed job_arrival job_jitter j t.
End ValidSchedules.
Section Lemmas.
Let has_actually_arrived := jitter_has_passed job_arrival job_jitter.
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
Section Arrival.
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
Lemma jobs_with_jitter_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Variable j: Job.
Lemma jitter_has_passed_implies_arrived:
∀ t,
has_actually_arrived j t →
has_arrived job_arrival j t.
Lemma service_before_jitter_is_zero :
∀ t,
t < actual_job_arrival j →
service_at sched j t = 0.
Lemma cumulative_service_before_jitter_is_zero :
∀ t1 t2,
t2 ≤ actual_job_arrival j →
\sum_(t1 ≤ i < t2) service_at sched j i = 0.
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.
Section Pending.
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Variable j: Job.
Lemma scheduled_implies_pending:
∀ t,
scheduled_at sched j t → pending j t.
End Pending.
End Lemmas.
End RedefiningProperties.
End UniprocessorScheduleWithJitter.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.arrival.jitter.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module UniprocessorScheduleWithJitter.
Export ArrivalSequenceWithJitter UniprocessorSchedule.
Section RedefiningProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Section JobProperties.
Variable j: Job.
Definition pending (t: time) :=
jitter_has_passed job_arrival job_jitter j t && ~~ completed_by job_cost sched j t.
Definition backlogged (t: time) :=
pending t && ~~ scheduled_at sched j t.
End JobProperties.
Section ValidSchedules.
Definition jobs_execute_after_jitter :=
∀ j t,
scheduled_at sched j t → jitter_has_passed job_arrival job_jitter j t.
End ValidSchedules.
Section Lemmas.
Let has_actually_arrived := jitter_has_passed job_arrival job_jitter.
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
Section Arrival.
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
Lemma jobs_with_jitter_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Variable j: Job.
Lemma jitter_has_passed_implies_arrived:
∀ t,
has_actually_arrived j t →
has_arrived job_arrival j t.
Lemma service_before_jitter_is_zero :
∀ t,
t < actual_job_arrival j →
service_at sched j t = 0.
Lemma cumulative_service_before_jitter_is_zero :
∀ t1 t2,
t2 ≤ actual_job_arrival j →
\sum_(t1 ≤ i < t2) service_at sched j i = 0.
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.
Section Pending.
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Variable j: Job.
Lemma scheduled_implies_pending:
∀ t,
scheduled_at sched j t → pending j t.
End Pending.
End Lemmas.
End RedefiningProperties.
End UniprocessorScheduleWithJitter.