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.
(* Recall the platform constraints for suspension-oblivious and suspension-aware schedules. *)
Module susp := ScheduleWithSuspensions.
Module susp_oblivious := Platform.
Module susp_aware := PlatformWithSuspensions.
(* In this section, we perform a reduction from a suspension-aware schedule
to a suspension-oblivious schedule, in which jobs have inflated execution costs. *)
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.
(* Let ts be any task set to be analyzed. *)
Variable ts: seq Task.
(* Next, consider any consistent job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
(* ...whose jobs come from task set ts. *)
Hypothesis H_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
(* Consider any JLDP policy that is reflexive, transitive and total, i.e., that
indicates "higher or equal priority". *)
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.
(* Consider the original job and task costs. *)
Variable original_job_cost: Job → time.
Variable original_task_cost: Task → time.
(* Assume that the maximum suspension time of any job is bounded according
to the dynamic suspension model. *)
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.
(* Next, consider any suspension-aware schedule of this arrival sequence. *)
Variable sched_susp: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched_susp arr_seq.
(* Assume that jobs only execute after they arrive... *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched_susp.
(* ...and no longer than their execution costs. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute original_job_cost sched_susp.
(* Also assume that the schedule is work-conserving if there are non-suspended jobs, ... *)
Hypothesis H_work_conserving:
susp_aware.work_conserving job_arrival original_job_cost next_suspension arr_seq sched_susp.
(* ...that the schedule respects job priority... *)
Hypothesis H_respects_priority:
susp_aware.respects_JLDP_policy job_arrival original_job_cost next_suspension
arr_seq sched_susp higher_eq_priority.
(* ...and that suspended jobs are not allowed to be scheduled. *)
Hypothesis H_respects_self_suspensions:
respects_self_suspensions job_arrival original_job_cost next_suspension sched_susp.
(* Now we proceed with the reduction. First, we formalize the inflation of job and task costs. *)
Section CostInflation.
(* Recall the total suspension time of a job in the original schedule. *)
Let job_total_suspension :=
total_suspension original_job_cost next_suspension.
(* To inflate job costs, we just add the total suspension of the job. *)
Definition inflated_job_cost (j: Job) :=
original_job_cost j + job_total_suspension j.
(* Similarly, to inflate task costs, we just add its suspension bound. *)
Definition inflated_task_cost (tsk: Task) :=
original_task_cost tsk + task_suspension_bound tsk.
(* As shown next, this inflation produces job valid parameters. *)
Section NewParametersAreValid.
(* Recall the definition of valid sporadic jobs and tasks. *)
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.
(* If the inflated task costs are no larger than the deadline nor period of each task, ... *)
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.
(* ...then we can prove that job parameters remain valid after the inflation. *)
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.
(* The same applies for task parameters. *)
Lemma suspension_oblivious_task_parameters_remain_valid:
tasks_are_valid original_task_cost → tasks_are_valid inflated_task_cost.
End NewParametersAreValid.
End CostInflation.
(* Now, we are going to generate a suspension-oblivious schedule with the inflated
job costs. For that, we always try to copy the original schedule, as long as that
doesn't break the priority enforcement in the generated schedule. *)
Section ScheduleConstruction.
(* In this section, we define the schedule construction function. *)
Section ConstructionStep.
(* For any time t, suppose that we have generated the schedule prefix in the
interval 0, t). Then, we must define what should be scheduled at time t. *)
Variable sched_prefix: schedule Job.
Variable t: time.
(* First, consider the list of pending jobs at time t in the generated schedule. *)
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].
(* From the list of pending jobs, we take one of the (possibly many) highest-priority
jobs, or None, in case there are no pending jobs. *)
Definition highest_priority_job := seq_min (higher_eq_priority t) pending_jobs.
(* Then, we construct the schedule at time t as follows.
a) If there's a job scheduled in the original schedule at time t that is also a
highest-priority pending job in the generated schedule, copy this job.
b) Else, pick one of the highest priority pending jobs in the generated schedule. *)
Definition build_schedule : option Job :=
(* If there is a highest-priority job j_hp in the generated schedule, ...*)
if highest_priority_job is Some j_hp then
(* ...and there is some job scheduled in the original schedule... *)
if (sched_susp t) is Some j_sched then
(* ...that is a highest-priority pending job,...*)
if job_is_pending j_sched t && higher_eq_priority t j_sched j_hp then
Some j_sched (* ...copy this scheduled job. *)
else
highest_priority_job (* In the remaining cases, just pick the *)
else highest_priority_job (* highest-priority job in the generated schedule. *)
else highest_priority_job.
End ConstructionStep.
(* Next, starting from the empty schedule, ...*)
Let empty_schedule : schedule Job := fun t ⇒ None.
(* ...we use the recursive definition above to construct the suspension-oblivious schedule. *)
Definition sched_new := build_schedule_from_prefixes build_schedule empty_schedule.
(* Then, by showing that the construction function depends only on the previous service, ... *)
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.
(* ...we infer that the generated schedule is indeed based on the construction function. *)
Corollary sched_new_uses_construction_function:
∀ t,
sched_new t = build_schedule sched_new t.
End ScheduleConstruction.
(* Next, we prove that the generated schedule is well-formed. *)
Section GeneratedScheduleIsValid.
(* First, we show that scheduled jobs come from the arrival sequence. *)
Lemma sched_newjobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched_new arr_seq.
(* Next, we show that jobs do not execute before their arrival times... *)
Lemma sched_new_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched_new.
(* ...nor longer than their execution costs. *)
Lemma sched_new_completed_jobs_dont_execute:
completed_jobs_dont_execute inflated_job_cost sched_new.
(* In addition, we prove that the schedule is (suspension-oblivious) work-conserving... *)
Lemma sched_new_work_conserving:
susp_oblivious.work_conserving job_arrival inflated_job_cost arr_seq sched_new.
(* ...and respects job priorities. *)
Lemma sched_new_respects_policy:
susp_oblivious.respects_JLDP_policy job_arrival inflated_job_cost
arr_seq sched_new higher_eq_priority.
(* In addition, due to the copy step in the schedule construction, we show that in case
there are multiple highest-priority jobs, we pick the same job as in the original
schedule. *)
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.
(* To reason about schedulability, we now prove that the generated schedule
preserves the service received by each job. *)
Section Service.
(* Recall the definitions of suspended job, cumulative service and
cumulative suspension time in the suspension-aware schedule. *)
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.
(* Also recall the definition of cumulative service in the generated schedule. *)
Let job_service_without_suspensions := service sched_new.
(* We are going to prove that for any job j, at any time t, the service received by j
in the generated schedule (without suspensions) is no larger than the sum of the
cumulative service plus suspension time in the original schedule (with suspensions).
The proof follows by induction on time. Since the base case is trivial, we focus
on the inductive step. *)
Section InductiveStep.
(* Assume that the claim we want to prove holds for the interval 0, t). *)
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.
(* Now, let j be any job in arrival sequence. We are going to prove that the claim
continues to hold for job j in the interval 0, t + 1). *)
Variable j: Job.
Hypothesis H_comes_from_arrival_sequence: arrives_in arr_seq j.
(* If j has not arrived by time t, then the proof is trivial, ... *)
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.
(* ...so let's assume instead that j has arrived by time t. *)
Hypothesis H_j_has_arrived: has_arrived job_arrival j t.
(* We begin by performing a case analysis on whether j has completed in the
suspension-aware schedule. *)
Section CompletedInSuspensionAwareSchedule.
(* Case 1) If j has completed by time t in the suspension-aware schedule, ... *)
Hypothesis H_j_has_completed:
completed_by original_job_cost sched_susp j t.
(* ...then it follows from the induction hypothesis that the service
received by j is preserved up in the interval 0, t + 1). *)
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.
(* Next, consider the complementary case. *)
Section PendingInSuspensionAwareSchedule.
(* Case 2) Since job j has arrived by time t, let's assume that j has not completed
by time t in the suspension-aware schedule, i.e., j is still pending. *)
Hypothesis H_j_is_pending:
~~ completed_by original_job_cost sched_susp j t.
(* Since we know from the induction hypothesis that the service received by j is
preserved in the interval 0, t), now we only have to consider the state of job j at time t in both schedules. That is, we need to prove the following property: scheduled_at sched_new j t ≤ job_suspended_at sched_susp j t + scheduled_at sched_susp j t. *)
(* If j is not scheduled in the suspension-oblivious schedule, then the claim follows. *)
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.
(* Likewise, if j is scheduled in the suspension-aware schedule, then the claim is also
trivial. *)
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.
(* Having proved the simple cases, let's now move to the harder case. *)
Section NotScheduledInSuspensionAware.
(* Assume that j is scheduled in the suspension-oblivious schedule, but
not in the suspension-aware schedule. *)
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.
(* It remains to show that j is suspended at time t in the suspension-aware schedule.
We are going to prove that by contradiction. *)
Section ProofByContradiction.
(* Assume that j it not suspended at time t in the suspension-aware schedule, ... *)
Hypothesis H_j_is_not_suspended: ~~ job_suspended_at sched_susp j t.
(* ...which implies that j is backlogged at time t in the suspension-aware schedule. *)
Lemma reduction_inductive_step_j_is_backlogged:
susp.backlogged job_arrival original_job_cost next_suspension sched_susp j t.
(* By work conservation, there must be a scheduled job with higher or equal
priority in the suspension-aware schedule. *)
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.
(* Let j_hp be this job with higher-or-equal priority. *)
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.
(* First, note that j and j_hp cannot be the same job, since j is not scheduled
in the suspension-aware schedule at time t. Moreover, since the generated
schedule breaks ties when there are multiple highest-priority jobs (by copying
the original schedule), it follows that the higher-priority job j_hp must have
completed earlier in the suspension-oblivious schedule. *)
Lemma reduction_inductive_step_j_hp_completed_in_new:
completed_by inflated_job_cost sched_new j_hp t.
(* However, recall from the induction hypothesis how the service in the two schedules
are related. From that, we can conclude that j_hp must have completed in the
suspension-aware schedule as well, ... *)
Lemma reduction_inductive_step_j_hp_completed_in_susp:
completed_by original_job_cost sched_susp j_hp t.
(* ...which of course is a contradiction, since we assumed that j_hp was scheduled
in the the suspension-aware schedule at time t. *)
Lemma reduction_inductive_step_contradiction: False.
End ProofByContradiction.
End NotScheduledInSuspensionAware.
(* From the lemmas above, we infer that the claim to be proven holds if job j
is pending in the suspension-aware schedule. *)
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.
(* Using the proof by induction, we show that the service received by any
job j at any time t is preserved in the suspension-aware schedule. *)
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.
(* As a corollary, we show that if a job has completed in the suspension-oblivious
schedule, it must have completed in the suspension-aware schedule as well. *)
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.
(* To conclude, based on the definition of schedulability, ...*)
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.
(* ...we prove that if no job misses a deadline in the suspension-oblivious schedule, ... *)
Hypothesis H_schedulable_without_suspensions:
∀ j,
arrives_in arr_seq j →
schedulable_without_suspensions j.
(* ...then no job misses a deadline in the suspension-aware schedule. *)
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.
(* Recall the platform constraints for suspension-oblivious and suspension-aware schedules. *)
Module susp := ScheduleWithSuspensions.
Module susp_oblivious := Platform.
Module susp_aware := PlatformWithSuspensions.
(* In this section, we perform a reduction from a suspension-aware schedule
to a suspension-oblivious schedule, in which jobs have inflated execution costs. *)
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.
(* Let ts be any task set to be analyzed. *)
Variable ts: seq Task.
(* Next, consider any consistent job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
(* ...whose jobs come from task set ts. *)
Hypothesis H_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
(* Consider any JLDP policy that is reflexive, transitive and total, i.e., that
indicates "higher or equal priority". *)
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.
(* Consider the original job and task costs. *)
Variable original_job_cost: Job → time.
Variable original_task_cost: Task → time.
(* Assume that the maximum suspension time of any job is bounded according
to the dynamic suspension model. *)
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.
(* Next, consider any suspension-aware schedule of this arrival sequence. *)
Variable sched_susp: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched_susp arr_seq.
(* Assume that jobs only execute after they arrive... *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched_susp.
(* ...and no longer than their execution costs. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute original_job_cost sched_susp.
(* Also assume that the schedule is work-conserving if there are non-suspended jobs, ... *)
Hypothesis H_work_conserving:
susp_aware.work_conserving job_arrival original_job_cost next_suspension arr_seq sched_susp.
(* ...that the schedule respects job priority... *)
Hypothesis H_respects_priority:
susp_aware.respects_JLDP_policy job_arrival original_job_cost next_suspension
arr_seq sched_susp higher_eq_priority.
(* ...and that suspended jobs are not allowed to be scheduled. *)
Hypothesis H_respects_self_suspensions:
respects_self_suspensions job_arrival original_job_cost next_suspension sched_susp.
(* Now we proceed with the reduction. First, we formalize the inflation of job and task costs. *)
Section CostInflation.
(* Recall the total suspension time of a job in the original schedule. *)
Let job_total_suspension :=
total_suspension original_job_cost next_suspension.
(* To inflate job costs, we just add the total suspension of the job. *)
Definition inflated_job_cost (j: Job) :=
original_job_cost j + job_total_suspension j.
(* Similarly, to inflate task costs, we just add its suspension bound. *)
Definition inflated_task_cost (tsk: Task) :=
original_task_cost tsk + task_suspension_bound tsk.
(* As shown next, this inflation produces job valid parameters. *)
Section NewParametersAreValid.
(* Recall the definition of valid sporadic jobs and tasks. *)
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.
(* If the inflated task costs are no larger than the deadline nor period of each task, ... *)
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.
(* ...then we can prove that job parameters remain valid after the inflation. *)
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.
(* The same applies for task parameters. *)
Lemma suspension_oblivious_task_parameters_remain_valid:
tasks_are_valid original_task_cost → tasks_are_valid inflated_task_cost.
End NewParametersAreValid.
End CostInflation.
(* Now, we are going to generate a suspension-oblivious schedule with the inflated
job costs. For that, we always try to copy the original schedule, as long as that
doesn't break the priority enforcement in the generated schedule. *)
Section ScheduleConstruction.
(* In this section, we define the schedule construction function. *)
Section ConstructionStep.
(* For any time t, suppose that we have generated the schedule prefix in the
interval 0, t). Then, we must define what should be scheduled at time t. *)
Variable sched_prefix: schedule Job.
Variable t: time.
(* First, consider the list of pending jobs at time t in the generated schedule. *)
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].
(* From the list of pending jobs, we take one of the (possibly many) highest-priority
jobs, or None, in case there are no pending jobs. *)
Definition highest_priority_job := seq_min (higher_eq_priority t) pending_jobs.
(* Then, we construct the schedule at time t as follows.
a) If there's a job scheduled in the original schedule at time t that is also a
highest-priority pending job in the generated schedule, copy this job.
b) Else, pick one of the highest priority pending jobs in the generated schedule. *)
Definition build_schedule : option Job :=
(* If there is a highest-priority job j_hp in the generated schedule, ...*)
if highest_priority_job is Some j_hp then
(* ...and there is some job scheduled in the original schedule... *)
if (sched_susp t) is Some j_sched then
(* ...that is a highest-priority pending job,...*)
if job_is_pending j_sched t && higher_eq_priority t j_sched j_hp then
Some j_sched (* ...copy this scheduled job. *)
else
highest_priority_job (* In the remaining cases, just pick the *)
else highest_priority_job (* highest-priority job in the generated schedule. *)
else highest_priority_job.
End ConstructionStep.
(* Next, starting from the empty schedule, ...*)
Let empty_schedule : schedule Job := fun t ⇒ None.
(* ...we use the recursive definition above to construct the suspension-oblivious schedule. *)
Definition sched_new := build_schedule_from_prefixes build_schedule empty_schedule.
(* Then, by showing that the construction function depends only on the previous service, ... *)
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.
(* ...we infer that the generated schedule is indeed based on the construction function. *)
Corollary sched_new_uses_construction_function:
∀ t,
sched_new t = build_schedule sched_new t.
End ScheduleConstruction.
(* Next, we prove that the generated schedule is well-formed. *)
Section GeneratedScheduleIsValid.
(* First, we show that scheduled jobs come from the arrival sequence. *)
Lemma sched_newjobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched_new arr_seq.
(* Next, we show that jobs do not execute before their arrival times... *)
Lemma sched_new_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched_new.
(* ...nor longer than their execution costs. *)
Lemma sched_new_completed_jobs_dont_execute:
completed_jobs_dont_execute inflated_job_cost sched_new.
(* In addition, we prove that the schedule is (suspension-oblivious) work-conserving... *)
Lemma sched_new_work_conserving:
susp_oblivious.work_conserving job_arrival inflated_job_cost arr_seq sched_new.
(* ...and respects job priorities. *)
Lemma sched_new_respects_policy:
susp_oblivious.respects_JLDP_policy job_arrival inflated_job_cost
arr_seq sched_new higher_eq_priority.
(* In addition, due to the copy step in the schedule construction, we show that in case
there are multiple highest-priority jobs, we pick the same job as in the original
schedule. *)
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.
(* To reason about schedulability, we now prove that the generated schedule
preserves the service received by each job. *)
Section Service.
(* Recall the definitions of suspended job, cumulative service and
cumulative suspension time in the suspension-aware schedule. *)
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.
(* Also recall the definition of cumulative service in the generated schedule. *)
Let job_service_without_suspensions := service sched_new.
(* We are going to prove that for any job j, at any time t, the service received by j
in the generated schedule (without suspensions) is no larger than the sum of the
cumulative service plus suspension time in the original schedule (with suspensions).
The proof follows by induction on time. Since the base case is trivial, we focus
on the inductive step. *)
Section InductiveStep.
(* Assume that the claim we want to prove holds for the interval 0, t). *)
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.
(* Now, let j be any job in arrival sequence. We are going to prove that the claim
continues to hold for job j in the interval 0, t + 1). *)
Variable j: Job.
Hypothesis H_comes_from_arrival_sequence: arrives_in arr_seq j.
(* If j has not arrived by time t, then the proof is trivial, ... *)
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.
(* ...so let's assume instead that j has arrived by time t. *)
Hypothesis H_j_has_arrived: has_arrived job_arrival j t.
(* We begin by performing a case analysis on whether j has completed in the
suspension-aware schedule. *)
Section CompletedInSuspensionAwareSchedule.
(* Case 1) If j has completed by time t in the suspension-aware schedule, ... *)
Hypothesis H_j_has_completed:
completed_by original_job_cost sched_susp j t.
(* ...then it follows from the induction hypothesis that the service
received by j is preserved up in the interval 0, t + 1). *)
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.
(* Next, consider the complementary case. *)
Section PendingInSuspensionAwareSchedule.
(* Case 2) Since job j has arrived by time t, let's assume that j has not completed
by time t in the suspension-aware schedule, i.e., j is still pending. *)
Hypothesis H_j_is_pending:
~~ completed_by original_job_cost sched_susp j t.
(* Since we know from the induction hypothesis that the service received by j is
preserved in the interval 0, t), now we only have to consider the state of job j at time t in both schedules. That is, we need to prove the following property: scheduled_at sched_new j t ≤ job_suspended_at sched_susp j t + scheduled_at sched_susp j t. *)
(* If j is not scheduled in the suspension-oblivious schedule, then the claim follows. *)
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.
(* Likewise, if j is scheduled in the suspension-aware schedule, then the claim is also
trivial. *)
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.
(* Having proved the simple cases, let's now move to the harder case. *)
Section NotScheduledInSuspensionAware.
(* Assume that j is scheduled in the suspension-oblivious schedule, but
not in the suspension-aware schedule. *)
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.
(* It remains to show that j is suspended at time t in the suspension-aware schedule.
We are going to prove that by contradiction. *)
Section ProofByContradiction.
(* Assume that j it not suspended at time t in the suspension-aware schedule, ... *)
Hypothesis H_j_is_not_suspended: ~~ job_suspended_at sched_susp j t.
(* ...which implies that j is backlogged at time t in the suspension-aware schedule. *)
Lemma reduction_inductive_step_j_is_backlogged:
susp.backlogged job_arrival original_job_cost next_suspension sched_susp j t.
(* By work conservation, there must be a scheduled job with higher or equal
priority in the suspension-aware schedule. *)
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.
(* Let j_hp be this job with higher-or-equal priority. *)
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.
(* First, note that j and j_hp cannot be the same job, since j is not scheduled
in the suspension-aware schedule at time t. Moreover, since the generated
schedule breaks ties when there are multiple highest-priority jobs (by copying
the original schedule), it follows that the higher-priority job j_hp must have
completed earlier in the suspension-oblivious schedule. *)
Lemma reduction_inductive_step_j_hp_completed_in_new:
completed_by inflated_job_cost sched_new j_hp t.
(* However, recall from the induction hypothesis how the service in the two schedules
are related. From that, we can conclude that j_hp must have completed in the
suspension-aware schedule as well, ... *)
Lemma reduction_inductive_step_j_hp_completed_in_susp:
completed_by original_job_cost sched_susp j_hp t.
(* ...which of course is a contradiction, since we assumed that j_hp was scheduled
in the the suspension-aware schedule at time t. *)
Lemma reduction_inductive_step_contradiction: False.
End ProofByContradiction.
End NotScheduledInSuspensionAware.
(* From the lemmas above, we infer that the claim to be proven holds if job j
is pending in the suspension-aware schedule. *)
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.
(* Using the proof by induction, we show that the service received by any
job j at any time t is preserved in the suspension-aware schedule. *)
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.
(* As a corollary, we show that if a job has completed in the suspension-oblivious
schedule, it must have completed in the suspension-aware schedule as well. *)
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.
(* To conclude, based on the definition of schedulability, ...*)
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.
(* ...we prove that if no job misses a deadline in the suspension-oblivious schedule, ... *)
Hypothesis H_schedulable_without_suspensions:
∀ j,
arrives_in arr_seq j →
schedulable_without_suspensions j.
(* ...then no job misses a deadline in the suspension-aware schedule. *)
Corollary suspension_oblivious_preserves_schedulability:
∀ j,
arrives_in arr_seq j →
schedulable_with_suspensions j.
End Reduction.
End ReductionToBasicSchedule.