Library prosa.classic.model.schedule.uni.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 prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module UniprocessorSchedule.
Import SporadicTaskset.
Export Time ArrivalSequence.
Section Schedule.
Section ScheduleDef.
Variable Job: eqType.
Definition schedule := time → option Job.
End ScheduleDef.
Section ScheduleProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable sched: schedule Job.
Section JobProperties.
Variable j: Job.
Definition scheduled_at (t: time) := sched t == Some j.
Definition service_at (t: time) : time := scheduled_at t.
Definition service_during (t1 t2: time) :=
\sum_(t1 ≤ t < t2) service_at t.
Definition service (t: time) := service_during 0 t.
Definition completed_by (t: time) := job_cost j ≤ service t.
Definition pending (t: time) := has_arrived job_arrival j t && ~~ completed_by t.
Definition pending_earlier_and_at (t: time) :=
arrived_before job_arrival j t && ~~ completed_by t.
Definition backlogged (t: time) := pending t && ~~ scheduled_at t.
End JobProperties.
Section ProcessorProperties.
Definition is_idle (t: time) := sched t == None.
Definition total_service_during (t1 t2: time) :=
\sum_(t1 ≤ t < t2) ~~ is_idle t.
Definition total_service (t2: time) := total_service_during 0 t2.
End ProcessorProperties.
Section PropertyOfSequentiality.
Context {Task: eqType}.
Variable job_task: Job → Task.
Let same_task j1 j2 := job_task j1 == job_task j2.
Definition sequential_jobs :=
∀ j1 j2 t,
same_task j1 j2 →
job_arrival j1 < job_arrival j2 →
scheduled_at j2 t →
completed_by j1 t.
Hypothesis H_sequential_jobs: sequential_jobs.
Corollary scheduler_executes_job_with_earliest_arrival:
∀ j1 j2 t,
same_task j1 j2 →
~~ completed_by j2 t →
scheduled_at j1 t →
job_arrival j1 ≤ job_arrival j2.
End PropertyOfSequentiality.
End ScheduleProperties.
Section ValidSchedules.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable sched: schedule Job.
Definition jobs_come_from_arrival_sequence (arr_seq: arrival_sequence Job) :=
∀ j t, scheduled_at sched j t → arrives_in arr_seq j.
Definition jobs_must_arrive_to_execute :=
∀ j t, scheduled_at sched j t → has_arrived job_arrival j t.
Definition completed_jobs_dont_execute :=
∀ j t, service sched j t ≤ job_cost j.
End ValidSchedules.
Section Lemmas.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable sched: schedule Job.
Definition remaining_cost j t :=
job_cost j - service sched j t.
Section Service.
Variable j: Job.
Lemma service_at_most_one:
∀ t, service_at sched j t ≤ 1.
Lemma cumulative_service_le_delta:
∀ t delta,
service_during sched j t (t + delta) ≤ delta.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Lemma scheduled_implies_positive_remaining_cost:
∀ t,
scheduled_at sched j t →
remaining_cost j t > 0.
End Service.
Section Completion.
Variable j: Job.
Lemma completion_monotonic:
∀ t t',
t ≤ t' →
completed_by job_cost sched j t →
completed_by job_cost sched j t'.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Lemma completed_implies_not_scheduled :
∀ t,
completed_by job_cost sched j t →
~~ scheduled_at sched j t.
Lemma scheduled_implies_not_completed:
∀ t,
scheduled_at sched j t →
~~ completed_by job_cost sched j t.
Lemma cumulative_service_le_job_cost :
∀ t t',
service_during sched j t t' ≤ job_cost j.
Lemma job_doesnt_complete_before_remaining_cost:
∀ t,
~~ completed_by job_cost sched j t →
~~ completed_by job_cost sched j (t + remaining_cost j t - 1).
Section JobMustBeScheduled.
Hypothesis H_positive_cost: job_cost j > 0.
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute job_arrival sched.
Lemma completed_implies_scheduled_before:
∀ t,
completed_by job_cost sched j t →
∃ t',
job_arrival j ≤ t' < t
∧ scheduled_at sched j t'.
End JobMustBeScheduled.
End Completion.
Section Arrival.
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute job_arrival sched.
Variable j: Job.
Lemma service_before_job_arrival_zero :
∀ t,
t < job_arrival j →
service_at sched j t = 0.
Lemma cumulative_service_before_job_arrival_zero :
∀ t1 t2,
t2 ≤ job_arrival j →
\sum_(t1 ≤ i < t2) service_at sched j i = 0.
Lemma ignore_service_before_arrival:
∀ t1 t2,
t1 ≤ job_arrival j →
t2 ≥ job_arrival j →
\sum_(t1 ≤ t < t2) service_at sched j t =
\sum_(job_arrival j ≤ t < t2) service_at sched j t.
End Arrival.
Section Pending.
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute job_arrival sched.
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 job_arrival job_cost sched j t.
Variable arr_seq: arrival_sequence Job.
Lemma job_pending_at_arrival:
arrives_in arr_seq j →
job_cost j > 0 →
pending job_arrival job_cost sched j (job_arrival j).
End Pending.
Section OnlyOneJobScheduled.
Variable j1 j2: Job.
Lemma only_one_job_scheduled:
∀ t,
scheduled_at sched j1 t →
scheduled_at sched j2 t →
j1 = j2.
End OnlyOneJobScheduled.
Section ServiceIsUnitGrowthFunction.
Lemma service_is_unit_growth_function:
∀ j,
unit_growth_function (service sched j).
Variable j: Job.
Variable t: time.
Variable s0: time.
Hypothesis H_less_than_s: s0 < service sched j t.
Corollary exists_intermediate_service:
∃ t0,
t0 < t ∧
service sched j t0 = s0.
End ServiceIsUnitGrowthFunction.
Section ScheduledAtEarlierTime.
Lemma scheduled_at_earlier_time:
∀ j t,
service sched j t > 0 →
∃ t0,
t0 < t ∧
scheduled_at sched j t0.
End ScheduledAtEarlierTime.
Section ServiceNotZero.
Variable j: Job.
Variable t1 t2: time.
Hypothesis H_service_not_zero: service_during sched j t1 t2 > 0.
Lemma cumulative_service_implies_scheduled :
∃ t,
t1 ≤ t < t2 ∧
scheduled_at sched j t.
End ServiceNotZero.
Section TimesWithSameService.
Variable j: Job.
Variable t1 t2: time.
Hypothesis H_same_service: service sched j t1 = service sched j t2.
Lemma same_service_implies_scheduled_at_earlier_times:
[∃ t: 'I_t1, scheduled_at sched j t] =
[∃ t': 'I_t2, scheduled_at sched j t'].
End TimesWithSameService.
End Lemmas.
End Schedule.
End UniprocessorSchedule.
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.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module UniprocessorSchedule.
Import SporadicTaskset.
Export Time ArrivalSequence.
Section Schedule.
Section ScheduleDef.
Variable Job: eqType.
Definition schedule := time → option Job.
End ScheduleDef.
Section ScheduleProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable sched: schedule Job.
Section JobProperties.
Variable j: Job.
Definition scheduled_at (t: time) := sched t == Some j.
Definition service_at (t: time) : time := scheduled_at t.
Definition service_during (t1 t2: time) :=
\sum_(t1 ≤ t < t2) service_at t.
Definition service (t: time) := service_during 0 t.
Definition completed_by (t: time) := job_cost j ≤ service t.
Definition pending (t: time) := has_arrived job_arrival j t && ~~ completed_by t.
Definition pending_earlier_and_at (t: time) :=
arrived_before job_arrival j t && ~~ completed_by t.
Definition backlogged (t: time) := pending t && ~~ scheduled_at t.
End JobProperties.
Section ProcessorProperties.
Definition is_idle (t: time) := sched t == None.
Definition total_service_during (t1 t2: time) :=
\sum_(t1 ≤ t < t2) ~~ is_idle t.
Definition total_service (t2: time) := total_service_during 0 t2.
End ProcessorProperties.
Section PropertyOfSequentiality.
Context {Task: eqType}.
Variable job_task: Job → Task.
Let same_task j1 j2 := job_task j1 == job_task j2.
Definition sequential_jobs :=
∀ j1 j2 t,
same_task j1 j2 →
job_arrival j1 < job_arrival j2 →
scheduled_at j2 t →
completed_by j1 t.
Hypothesis H_sequential_jobs: sequential_jobs.
Corollary scheduler_executes_job_with_earliest_arrival:
∀ j1 j2 t,
same_task j1 j2 →
~~ completed_by j2 t →
scheduled_at j1 t →
job_arrival j1 ≤ job_arrival j2.
End PropertyOfSequentiality.
End ScheduleProperties.
Section ValidSchedules.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable sched: schedule Job.
Definition jobs_come_from_arrival_sequence (arr_seq: arrival_sequence Job) :=
∀ j t, scheduled_at sched j t → arrives_in arr_seq j.
Definition jobs_must_arrive_to_execute :=
∀ j t, scheduled_at sched j t → has_arrived job_arrival j t.
Definition completed_jobs_dont_execute :=
∀ j t, service sched j t ≤ job_cost j.
End ValidSchedules.
Section Lemmas.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable sched: schedule Job.
Definition remaining_cost j t :=
job_cost j - service sched j t.
Section Service.
Variable j: Job.
Lemma service_at_most_one:
∀ t, service_at sched j t ≤ 1.
Lemma cumulative_service_le_delta:
∀ t delta,
service_during sched j t (t + delta) ≤ delta.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Lemma scheduled_implies_positive_remaining_cost:
∀ t,
scheduled_at sched j t →
remaining_cost j t > 0.
End Service.
Section Completion.
Variable j: Job.
Lemma completion_monotonic:
∀ t t',
t ≤ t' →
completed_by job_cost sched j t →
completed_by job_cost sched j t'.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute job_cost sched.
Lemma completed_implies_not_scheduled :
∀ t,
completed_by job_cost sched j t →
~~ scheduled_at sched j t.
Lemma scheduled_implies_not_completed:
∀ t,
scheduled_at sched j t →
~~ completed_by job_cost sched j t.
Lemma cumulative_service_le_job_cost :
∀ t t',
service_during sched j t t' ≤ job_cost j.
Lemma job_doesnt_complete_before_remaining_cost:
∀ t,
~~ completed_by job_cost sched j t →
~~ completed_by job_cost sched j (t + remaining_cost j t - 1).
Section JobMustBeScheduled.
Hypothesis H_positive_cost: job_cost j > 0.
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute job_arrival sched.
Lemma completed_implies_scheduled_before:
∀ t,
completed_by job_cost sched j t →
∃ t',
job_arrival j ≤ t' < t
∧ scheduled_at sched j t'.
End JobMustBeScheduled.
End Completion.
Section Arrival.
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute job_arrival sched.
Variable j: Job.
Lemma service_before_job_arrival_zero :
∀ t,
t < job_arrival j →
service_at sched j t = 0.
Lemma cumulative_service_before_job_arrival_zero :
∀ t1 t2,
t2 ≤ job_arrival j →
\sum_(t1 ≤ i < t2) service_at sched j i = 0.
Lemma ignore_service_before_arrival:
∀ t1 t2,
t1 ≤ job_arrival j →
t2 ≥ job_arrival j →
\sum_(t1 ≤ t < t2) service_at sched j t =
\sum_(job_arrival j ≤ t < t2) service_at sched j t.
End Arrival.
Section Pending.
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute job_arrival sched.
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 job_arrival job_cost sched j t.
Variable arr_seq: arrival_sequence Job.
Lemma job_pending_at_arrival:
arrives_in arr_seq j →
job_cost j > 0 →
pending job_arrival job_cost sched j (job_arrival j).
End Pending.
Section OnlyOneJobScheduled.
Variable j1 j2: Job.
Lemma only_one_job_scheduled:
∀ t,
scheduled_at sched j1 t →
scheduled_at sched j2 t →
j1 = j2.
End OnlyOneJobScheduled.
Section ServiceIsUnitGrowthFunction.
Lemma service_is_unit_growth_function:
∀ j,
unit_growth_function (service sched j).
Variable j: Job.
Variable t: time.
Variable s0: time.
Hypothesis H_less_than_s: s0 < service sched j t.
Corollary exists_intermediate_service:
∃ t0,
t0 < t ∧
service sched j t0 = s0.
End ServiceIsUnitGrowthFunction.
Section ScheduledAtEarlierTime.
Lemma scheduled_at_earlier_time:
∀ j t,
service sched j t > 0 →
∃ t0,
t0 < t ∧
scheduled_at sched j t0.
End ScheduledAtEarlierTime.
Section ServiceNotZero.
Variable j: Job.
Variable t1 t2: time.
Hypothesis H_service_not_zero: service_during sched j t1 t2 > 0.
Lemma cumulative_service_implies_scheduled :
∃ t,
t1 ≤ t < t2 ∧
scheduled_at sched j t.
End ServiceNotZero.
Section TimesWithSameService.
Variable j: Job.
Variable t1 t2: time.
Hypothesis H_same_service: service sched j t1 = service sched j t2.
Lemma same_service_implies_scheduled_at_earlier_times:
[∃ t: 'I_t1, scheduled_at sched j t] =
[∃ t': 'I_t2, scheduled_at sched j t'].
End TimesWithSameService.
End Lemmas.
End Schedule.
End UniprocessorSchedule.