Library prosa.classic.analysis.uni.susp.dynamic.oblivious.reduction
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.schedulability.
Require Import prosa.classic.model.schedule.uni.basic.platform.
Require Import prosa.classic.model.schedule.uni.susp.suspension_intervals
prosa.classic.model.schedule.uni.susp.schedule prosa.classic.model.schedule.uni.susp.platform.
Require Import prosa.classic.model.schedule.uni.transformation.construction.
Require Import prosa.classic.implementation.uni.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
Module ReductionToBasicSchedule.
Import Job SporadicTaskset Suspension Priority SuspensionIntervals
Schedulability ScheduleConstruction.
Module susp := ScheduleWithSuspensions.
Module susp_oblivious := Platform.
Module susp_aware := PlatformWithSuspensions.
Section Reduction.
Context {Task: eqType}.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → Task.
Variable ts: seq Task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_priority_is_reflexive: JLDP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: JLDP_is_transitive higher_eq_priority.
Hypothesis H_priority_is_total: JLDP_is_total arr_seq higher_eq_priority.
Variable original_job_cost: Job → time.
Variable original_task_cost: Task → time.
Variable next_suspension: job_suspension Job.
Variable task_suspension_bound: Task → time.
Hypothesis H_dynamic_suspensions:
dynamic_suspension_model original_job_cost job_task next_suspension task_suspension_bound.
Variable sched_susp: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched_susp arr_seq.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched_susp.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute original_job_cost sched_susp.
Hypothesis H_work_conserving:
susp_aware.work_conserving job_arrival original_job_cost next_suspension arr_seq sched_susp.
Hypothesis H_respects_priority:
susp_aware.respects_JLDP_policy job_arrival original_job_cost next_suspension
arr_seq sched_susp higher_eq_priority.
Hypothesis H_respects_self_suspensions:
respects_self_suspensions job_arrival original_job_cost next_suspension sched_susp.
Section CostInflation.
Let job_total_suspension :=
total_suspension original_job_cost next_suspension.
Definition inflated_job_cost (j: Job) :=
original_job_cost j + job_total_suspension j.
Definition inflated_task_cost (tsk: Task) :=
original_task_cost tsk + task_suspension_bound tsk.
Section NewParametersAreValid.
Let jobs_are_valid job_cost task_cost :=
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Let tasks_are_valid task_cost :=
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_inflated_cost_le_deadline_and_period:
∀ tsk,
tsk \in ts →
inflated_task_cost tsk ≤ task_deadline tsk ∧
inflated_task_cost tsk ≤ task_period tsk.
Lemma suspension_oblivious_job_parameters_remain_valid:
jobs_are_valid original_job_cost original_task_cost →
jobs_are_valid inflated_job_cost inflated_task_cost.
Lemma suspension_oblivious_task_parameters_remain_valid:
tasks_are_valid original_task_cost → tasks_are_valid inflated_task_cost.
End NewParametersAreValid.
End CostInflation.
Section ScheduleConstruction.
Section ConstructionStep.
Variable sched_prefix: schedule Job.
Variable t: time.
Let job_is_pending := pending job_arrival inflated_job_cost sched_prefix.
Definition pending_jobs :=
[seq j <- jobs_arrived_up_to arr_seq t | job_is_pending j t].
Definition highest_priority_job := seq_min (higher_eq_priority t) pending_jobs.
Definition build_schedule : option Job :=
if highest_priority_job is Some j_hp then
if (sched_susp t) is Some j_sched then
if job_is_pending j_sched t && higher_eq_priority t j_sched j_hp then
Some j_sched
else
highest_priority_job
else highest_priority_job
else highest_priority_job.
End ConstructionStep.
Let empty_schedule : schedule Job := fun t ⇒ None.
Definition sched_new := build_schedule_from_prefixes build_schedule empty_schedule.
Lemma sched_new_depends_only_on_service:
∀ sched1 sched2 t,
(∀ j, service sched1 j t = service sched2 j t) →
build_schedule sched1 t = build_schedule sched2 t.
Corollary sched_new_uses_construction_function:
∀ t,
sched_new t = build_schedule sched_new t.
End ScheduleConstruction.
Section GeneratedScheduleIsValid.
Lemma sched_newjobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched_new arr_seq.
Lemma sched_new_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched_new.
Lemma sched_new_completed_jobs_dont_execute:
completed_jobs_dont_execute inflated_job_cost sched_new.
Lemma sched_new_work_conserving:
susp_oblivious.work_conserving job_arrival inflated_job_cost arr_seq sched_new.
Lemma sched_new_respects_policy:
susp_oblivious.respects_JLDP_policy job_arrival inflated_job_cost
arr_seq sched_new higher_eq_priority.
Lemma sched_new_breaks_ties:
∀ j1 j2 t,
higher_eq_priority t j1 j2 →
higher_eq_priority t j2 j1 →
scheduled_at sched_susp j1 t →
pending job_arrival inflated_job_cost sched_new j1 t →
scheduled_at sched_new j2 t →
j1 = j2.
Section Service.
Let job_suspended_at (sched: schedule Job) :=
suspended_at job_arrival original_job_cost next_suspension sched.
Let job_cumulative_suspension :=
cumulative_suspension job_arrival original_job_cost next_suspension sched_susp.
Let job_service_with_suspensions := service sched_susp.
Let job_service_without_suspensions := service sched_new.
Section InductiveStep.
Variable t: time.
Hypothesis H_induction_hypothesis:
∀ j,
arrives_in arr_seq j →
job_service_without_suspensions j t ≤
job_service_with_suspensions j t + job_cumulative_suspension j t.
Variable j: Job.
Hypothesis H_comes_from_arrival_sequence: arrives_in arr_seq j.
Lemma reduction_inductive_step_not_arrived:
~~ has_arrived job_arrival j t →
job_service_without_suspensions j t.+1 ≤
job_service_with_suspensions j t.+1 + job_cumulative_suspension j t.+1.
Hypothesis H_j_has_arrived: has_arrived job_arrival j t.
Section CompletedInSuspensionAwareSchedule.
Hypothesis H_j_has_completed:
completed_by original_job_cost sched_susp j t.
Lemma reduction_inductive_step_case1_completed:
job_service_without_suspensions j t.+1 ≤
job_service_with_suspensions j t.+1 + job_cumulative_suspension j t.+1.
End CompletedInSuspensionAwareSchedule.
Section PendingInSuspensionAwareSchedule.
Hypothesis H_j_is_pending:
~~ completed_by original_job_cost sched_susp j t.
Lemma reduction_inductive_step_not_scheduled_in_new:
~~ scheduled_at sched_new j t →
scheduled_at sched_new j t ≤
job_suspended_at sched_susp j t + scheduled_at sched_susp j t.
Lemma reduction_inductive_step_scheduled_in_susp:
scheduled_at sched_susp j t →
scheduled_at sched_new j t ≤
job_suspended_at sched_susp j t + scheduled_at sched_susp j t.
Section NotScheduledInSuspensionAware.
Hypothesis H_j_scheduled_in_new: scheduled_at sched_new j t.
Hypothesis H_j_not_scheduled_in_susp: ~~ scheduled_at sched_susp j t.
Section ProofByContradiction.
Hypothesis H_j_is_not_suspended: ~~ job_suspended_at sched_susp j t.
Lemma reduction_inductive_step_j_is_backlogged:
susp.backlogged job_arrival original_job_cost next_suspension sched_susp j t.
Lemma reduction_inductive_step_exists_hep_job:
∃ j_hp, arrives_in arr_seq j_hp ∧
scheduled_at sched_susp j_hp t ∧
higher_eq_priority t j_hp j.
Variable j_hp: Job.
Hypothesis H_j_hp_comes_from_sequence: arrives_in arr_seq j_hp.
Hypothesis H_j_hp_is_scheduled: scheduled_at sched_susp j_hp t.
Hypothesis H_higher_or_equal_priority: higher_eq_priority t j_hp j.
Lemma reduction_inductive_step_j_hp_completed_in_new:
completed_by inflated_job_cost sched_new j_hp t.
Lemma reduction_inductive_step_j_hp_completed_in_susp:
completed_by original_job_cost sched_susp j_hp t.
Lemma reduction_inductive_step_contradiction: False.
End ProofByContradiction.
End NotScheduledInSuspensionAware.
Lemma reduction_inductive_step_case2_pending:
job_service_without_suspensions j t.+1 ≤
job_service_with_suspensions j t.+1 + job_cumulative_suspension j t.+1.
End PendingInSuspensionAwareSchedule.
End InductiveStep.
Theorem suspension_oblivious_preserves_service:
∀ j t,
arrives_in arr_seq j →
job_service_without_suspensions j t ≤ job_service_with_suspensions j t
+ job_cumulative_suspension j t.
Corollary suspension_oblivious_preserves_completion:
∀ j t,
arrives_in arr_seq j →
completed_by inflated_job_cost sched_new j t →
completed_by original_job_cost sched_susp j t.
End Service.
End GeneratedScheduleIsValid.
Let schedulable_without_suspensions :=
job_misses_no_deadline job_arrival inflated_job_cost job_deadline sched_new.
Let schedulable_with_suspensions :=
job_misses_no_deadline job_arrival original_job_cost job_deadline sched_susp.
Hypothesis H_schedulable_without_suspensions:
∀ j,
arrives_in arr_seq j →
schedulable_without_suspensions j.
Corollary suspension_oblivious_preserves_schedulability:
∀ j,
arrives_in arr_seq j →
schedulable_with_suspensions j.
End Reduction.
End ReductionToBasicSchedule.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.schedulability.
Require Import prosa.classic.model.schedule.uni.basic.platform.
Require Import prosa.classic.model.schedule.uni.susp.suspension_intervals
prosa.classic.model.schedule.uni.susp.schedule prosa.classic.model.schedule.uni.susp.platform.
Require Import prosa.classic.model.schedule.uni.transformation.construction.
Require Import prosa.classic.implementation.uni.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
Module ReductionToBasicSchedule.
Import Job SporadicTaskset Suspension Priority SuspensionIntervals
Schedulability ScheduleConstruction.
Module susp := ScheduleWithSuspensions.
Module susp_oblivious := Platform.
Module susp_aware := PlatformWithSuspensions.
Section Reduction.
Context {Task: eqType}.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → Task.
Variable ts: seq Task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_priority_is_reflexive: JLDP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: JLDP_is_transitive higher_eq_priority.
Hypothesis H_priority_is_total: JLDP_is_total arr_seq higher_eq_priority.
Variable original_job_cost: Job → time.
Variable original_task_cost: Task → time.
Variable next_suspension: job_suspension Job.
Variable task_suspension_bound: Task → time.
Hypothesis H_dynamic_suspensions:
dynamic_suspension_model original_job_cost job_task next_suspension task_suspension_bound.
Variable sched_susp: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched_susp arr_seq.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched_susp.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute original_job_cost sched_susp.
Hypothesis H_work_conserving:
susp_aware.work_conserving job_arrival original_job_cost next_suspension arr_seq sched_susp.
Hypothesis H_respects_priority:
susp_aware.respects_JLDP_policy job_arrival original_job_cost next_suspension
arr_seq sched_susp higher_eq_priority.
Hypothesis H_respects_self_suspensions:
respects_self_suspensions job_arrival original_job_cost next_suspension sched_susp.
Section CostInflation.
Let job_total_suspension :=
total_suspension original_job_cost next_suspension.
Definition inflated_job_cost (j: Job) :=
original_job_cost j + job_total_suspension j.
Definition inflated_task_cost (tsk: Task) :=
original_task_cost tsk + task_suspension_bound tsk.
Section NewParametersAreValid.
Let jobs_are_valid job_cost task_cost :=
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Let tasks_are_valid task_cost :=
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_inflated_cost_le_deadline_and_period:
∀ tsk,
tsk \in ts →
inflated_task_cost tsk ≤ task_deadline tsk ∧
inflated_task_cost tsk ≤ task_period tsk.
Lemma suspension_oblivious_job_parameters_remain_valid:
jobs_are_valid original_job_cost original_task_cost →
jobs_are_valid inflated_job_cost inflated_task_cost.
Lemma suspension_oblivious_task_parameters_remain_valid:
tasks_are_valid original_task_cost → tasks_are_valid inflated_task_cost.
End NewParametersAreValid.
End CostInflation.
Section ScheduleConstruction.
Section ConstructionStep.
Variable sched_prefix: schedule Job.
Variable t: time.
Let job_is_pending := pending job_arrival inflated_job_cost sched_prefix.
Definition pending_jobs :=
[seq j <- jobs_arrived_up_to arr_seq t | job_is_pending j t].
Definition highest_priority_job := seq_min (higher_eq_priority t) pending_jobs.
Definition build_schedule : option Job :=
if highest_priority_job is Some j_hp then
if (sched_susp t) is Some j_sched then
if job_is_pending j_sched t && higher_eq_priority t j_sched j_hp then
Some j_sched
else
highest_priority_job
else highest_priority_job
else highest_priority_job.
End ConstructionStep.
Let empty_schedule : schedule Job := fun t ⇒ None.
Definition sched_new := build_schedule_from_prefixes build_schedule empty_schedule.
Lemma sched_new_depends_only_on_service:
∀ sched1 sched2 t,
(∀ j, service sched1 j t = service sched2 j t) →
build_schedule sched1 t = build_schedule sched2 t.
Corollary sched_new_uses_construction_function:
∀ t,
sched_new t = build_schedule sched_new t.
End ScheduleConstruction.
Section GeneratedScheduleIsValid.
Lemma sched_newjobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched_new arr_seq.
Lemma sched_new_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched_new.
Lemma sched_new_completed_jobs_dont_execute:
completed_jobs_dont_execute inflated_job_cost sched_new.
Lemma sched_new_work_conserving:
susp_oblivious.work_conserving job_arrival inflated_job_cost arr_seq sched_new.
Lemma sched_new_respects_policy:
susp_oblivious.respects_JLDP_policy job_arrival inflated_job_cost
arr_seq sched_new higher_eq_priority.
Lemma sched_new_breaks_ties:
∀ j1 j2 t,
higher_eq_priority t j1 j2 →
higher_eq_priority t j2 j1 →
scheduled_at sched_susp j1 t →
pending job_arrival inflated_job_cost sched_new j1 t →
scheduled_at sched_new j2 t →
j1 = j2.
Section Service.
Let job_suspended_at (sched: schedule Job) :=
suspended_at job_arrival original_job_cost next_suspension sched.
Let job_cumulative_suspension :=
cumulative_suspension job_arrival original_job_cost next_suspension sched_susp.
Let job_service_with_suspensions := service sched_susp.
Let job_service_without_suspensions := service sched_new.
Section InductiveStep.
Variable t: time.
Hypothesis H_induction_hypothesis:
∀ j,
arrives_in arr_seq j →
job_service_without_suspensions j t ≤
job_service_with_suspensions j t + job_cumulative_suspension j t.
Variable j: Job.
Hypothesis H_comes_from_arrival_sequence: arrives_in arr_seq j.
Lemma reduction_inductive_step_not_arrived:
~~ has_arrived job_arrival j t →
job_service_without_suspensions j t.+1 ≤
job_service_with_suspensions j t.+1 + job_cumulative_suspension j t.+1.
Hypothesis H_j_has_arrived: has_arrived job_arrival j t.
Section CompletedInSuspensionAwareSchedule.
Hypothesis H_j_has_completed:
completed_by original_job_cost sched_susp j t.
Lemma reduction_inductive_step_case1_completed:
job_service_without_suspensions j t.+1 ≤
job_service_with_suspensions j t.+1 + job_cumulative_suspension j t.+1.
End CompletedInSuspensionAwareSchedule.
Section PendingInSuspensionAwareSchedule.
Hypothesis H_j_is_pending:
~~ completed_by original_job_cost sched_susp j t.
Lemma reduction_inductive_step_not_scheduled_in_new:
~~ scheduled_at sched_new j t →
scheduled_at sched_new j t ≤
job_suspended_at sched_susp j t + scheduled_at sched_susp j t.
Lemma reduction_inductive_step_scheduled_in_susp:
scheduled_at sched_susp j t →
scheduled_at sched_new j t ≤
job_suspended_at sched_susp j t + scheduled_at sched_susp j t.
Section NotScheduledInSuspensionAware.
Hypothesis H_j_scheduled_in_new: scheduled_at sched_new j t.
Hypothesis H_j_not_scheduled_in_susp: ~~ scheduled_at sched_susp j t.
Section ProofByContradiction.
Hypothesis H_j_is_not_suspended: ~~ job_suspended_at sched_susp j t.
Lemma reduction_inductive_step_j_is_backlogged:
susp.backlogged job_arrival original_job_cost next_suspension sched_susp j t.
Lemma reduction_inductive_step_exists_hep_job:
∃ j_hp, arrives_in arr_seq j_hp ∧
scheduled_at sched_susp j_hp t ∧
higher_eq_priority t j_hp j.
Variable j_hp: Job.
Hypothesis H_j_hp_comes_from_sequence: arrives_in arr_seq j_hp.
Hypothesis H_j_hp_is_scheduled: scheduled_at sched_susp j_hp t.
Hypothesis H_higher_or_equal_priority: higher_eq_priority t j_hp j.
Lemma reduction_inductive_step_j_hp_completed_in_new:
completed_by inflated_job_cost sched_new j_hp t.
Lemma reduction_inductive_step_j_hp_completed_in_susp:
completed_by original_job_cost sched_susp j_hp t.
Lemma reduction_inductive_step_contradiction: False.
End ProofByContradiction.
End NotScheduledInSuspensionAware.
Lemma reduction_inductive_step_case2_pending:
job_service_without_suspensions j t.+1 ≤
job_service_with_suspensions j t.+1 + job_cumulative_suspension j t.+1.
End PendingInSuspensionAwareSchedule.
End InductiveStep.
Theorem suspension_oblivious_preserves_service:
∀ j t,
arrives_in arr_seq j →
job_service_without_suspensions j t ≤ job_service_with_suspensions j t
+ job_cumulative_suspension j t.
Corollary suspension_oblivious_preserves_completion:
∀ j t,
arrives_in arr_seq j →
completed_by inflated_job_cost sched_new j t →
completed_by original_job_cost sched_susp j t.
End Service.
End GeneratedScheduleIsValid.
Let schedulable_without_suspensions :=
job_misses_no_deadline job_arrival inflated_job_cost job_deadline sched_new.
Let schedulable_with_suspensions :=
job_misses_no_deadline job_arrival original_job_cost job_deadline sched_susp.
Hypothesis H_schedulable_without_suspensions:
∀ j,
arrives_in arr_seq j →
schedulable_without_suspensions j.
Corollary suspension_oblivious_preserves_schedulability:
∀ j,
arrives_in arr_seq j →
schedulable_with_suspensions j.
End Reduction.
End ReductionToBasicSchedule.