From 3f39fe20c14ffbb7ed3de1e5fc513d3beb5e4517 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Tue, 10 Jan 2017 11:29:49 +0100
Subject: [PATCH] Major Commit: Suspension-aware Scheduling
1) Definition of a generic model for job suspensions based on
received service (e.g., job j_1 should suspend for 4ms as
soon as service reaches 5ms).
2) Definition of the dynamic suspension model (i.e., cumulative
suspension of job j_1 <= X).
3) Analysis of suspension-aware scheduling by inflation of job
costs (via schedule reduction). In the literature, this is
called suspension-oblivious analysis.
4) Analysis of suspension-aware scheduling by adjusting job
jitter (via schedule reduction).
5) Proof of (weak) sustainability of job costs under suspension-aware
scheduling. We show that if we increase the costs of all jobs while
reducing their suspension times in a certain way, the response times
of all jobs do not decrease.
This has an important implication regarding worst-case schedules: if
some schedulability analysis already accounts for the fact that job
suspension times can vary from 0 to the task suspension bound, then
it's perfectly safe to assume that jobs execute for their WCET.
6) Proof of sustainability of the cost of a single job under
suspension-aware scheduling. That is, we show that increasing the
cost of a single job does not reduce its own response time.
(Note that this is a very basic result that applies to many
work-conserving, JLFP schedulers. We don't claim anything about
the response time of other jobs.)
---
analysis/uni/basic/fp_rta_comp.v | 2 +-
analysis/uni/basic/fp_rta_theory.v | 2 +-
analysis/uni/basic/workload_bound_fp.v | 2 +-
analysis/uni/jitter/fp_rta_comp.v | 52 +-
analysis/uni/jitter/fp_rta_theory.v | 42 +-
analysis/uni/jitter/workload_bound_fp.v | 44 +-
.../uni/susp/dynamic/jitter/jitter_schedule.v | 162 +++
.../jitter/jitter_schedule_properties.v | 459 ++++++
.../dynamic/jitter/jitter_schedule_service.v | 1283 +++++++++++++++++
.../jitter/jitter_taskset_generation.v | 61 +
.../susp/dynamic/jitter/rta_by_reduction.v | 202 +++
.../susp/dynamic/jitter/taskset_membership.v | 350 +++++
.../uni/susp/dynamic/jitter/taskset_rta.v | 233 +++
analysis/uni/susp/dynamic/oblivious/fp_rta.v | 2 +-
.../susp/sustainability/allcosts/reduction.v | 165 +++
.../allcosts/reduction_properties.v | 891 ++++++++++++
.../sustainability/singlecost/reduction.v | 102 ++
.../singlecost/reduction_properties.v | 741 ++++++++++
implementation/apa/schedule.v | 2 +-
implementation/global/basic/schedule.v | 2 +-
implementation/global/jitter/schedule.v | 2 +-
implementation/uni/basic/schedule.v | 2 +-
implementation/uni/jitter/arrival_sequence.v | 46 +-
implementation/uni/jitter/fp_rta_example.v | 19 +-
implementation/uni/jitter/schedule.v | 2 +-
implementation/uni/susp/schedule.v | 2 +-
model/arrival/basic/arrival_bounds.v | 2 +-
model/arrival/basic/task_arrival.v | 2 +-
model/arrival/jitter/arrival_bounds.v | 2 +-
model/arrival/jitter/task_arrival.v | 2 +-
model/schedule/uni/jitter/valid_schedule.v | 66 +
model/schedule/uni/response_time.v | 52 +-
.../uni/susp/build_suspension_table.v | 264 ++++
model/schedule/uni/susp/last_execution.v | 47 +
.../schedule/uni/susp/suspension_intervals.v | 74 +-
model/schedule/uni/susp/valid_schedule.v | 75 +
36 files changed, 5320 insertions(+), 138 deletions(-)
create mode 100644 analysis/uni/susp/dynamic/jitter/jitter_schedule.v
create mode 100644 analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v
create mode 100644 analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
create mode 100644 analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v
create mode 100644 analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
create mode 100644 analysis/uni/susp/dynamic/jitter/taskset_membership.v
create mode 100644 analysis/uni/susp/dynamic/jitter/taskset_rta.v
create mode 100644 analysis/uni/susp/sustainability/allcosts/reduction.v
create mode 100644 analysis/uni/susp/sustainability/allcosts/reduction_properties.v
create mode 100644 analysis/uni/susp/sustainability/singlecost/reduction.v
create mode 100644 analysis/uni/susp/sustainability/singlecost/reduction_properties.v
create mode 100644 model/schedule/uni/jitter/valid_schedule.v
create mode 100644 model/schedule/uni/susp/build_suspension_table.v
create mode 100644 model/schedule/uni/susp/valid_schedule.v
diff --git a/analysis/uni/basic/fp_rta_comp.v b/analysis/uni/basic/fp_rta_comp.v
index f3740944e..a74f4ef95 100644
--- a/analysis/uni/basic/fp_rta_comp.v
+++ b/analysis/uni/basic/fp_rta_comp.v
@@ -255,7 +255,7 @@ Module ResponseTimeIterationFP.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
- (* Assume any job arrival sequence with consistent, non-duplicate arrivals... *)
+ (* Assume any job arrival sequence with consistent, duplicate-free arrivals... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
diff --git a/analysis/uni/basic/fp_rta_theory.v b/analysis/uni/basic/fp_rta_theory.v
index 7f4e04176..9b5fae2e3 100644
--- a/analysis/uni/basic/fp_rta_theory.v
+++ b/analysis/uni/basic/fp_rta_theory.v
@@ -29,7 +29,7 @@ Module ResponseTimeAnalysisFP.
Variable job_deadline: Job -> time.
Variable job_task: Job -> SporadicTask.
- (* Assume any job arrival sequence with consistent, non-duplicate arrivals... *)
+ (* Assume any job arrival sequence with consistent, duplicate-free arrivals... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
diff --git a/analysis/uni/basic/workload_bound_fp.v b/analysis/uni/basic/workload_bound_fp.v
index 26bede2c4..de92fb980 100644
--- a/analysis/uni/basic/workload_bound_fp.v
+++ b/analysis/uni/basic/workload_bound_fp.v
@@ -160,7 +160,7 @@ Module WorkloadBoundFP.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
- (* Consider any job arrival sequence with consistent, non-duplicate arrivals. *)
+ (* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
diff --git a/analysis/uni/jitter/fp_rta_comp.v b/analysis/uni/jitter/fp_rta_comp.v
index 7b54d24d7..3368541bc 100644
--- a/analysis/uni/jitter/fp_rta_comp.v
+++ b/analysis/uni/jitter/fp_rta_comp.v
@@ -260,13 +260,13 @@ Module ResponseTimeIterationFP.
Variable job_task: Job -> SporadicTask.
(* Consider a task set ts... *)
- Variable ts: taskset_of SporadicTask.
+ Variable ts: seq SporadicTask.
- (* ...where tasks have valid parameters. *)
- Hypothesis H_valid_task_parameters:
- valid_sporadic_taskset task_cost task_period task_deadline ts.
+ (* ...with positive task costs and periods. *)
+ Hypothesis H_positive_costs: forall tsk, tsk \in ts -> task_cost tsk > 0.
+ Hypothesis H_positive_periods: forall tsk, tsk \in ts -> task_period tsk > 0.
- (* Next, consider any job arrival sequence with consistent, non-duplicate arrivals, ... *)
+ (* Next, consider any job arrival sequence with consistent, duplicate-free arrivals, ... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
@@ -276,18 +276,29 @@ Module ResponseTimeIterationFP.
forall j,
arrives_in arr_seq j ->
job_task j \in ts.
+
+ (* ... and satisfy the sporadic task model.*)
+ Hypothesis H_sporadic_tasks:
+ sporadic_task_model task_period job_arrival job_task arr_seq.
- (* ...have valid parameters,...*)
- Hypothesis H_valid_job_parameters:
+ (* Assume that the cost of each job is bounded by the cost of its task,... *)
+ Hypothesis H_job_cost_le_task_cost:
forall j,
arrives_in arr_seq j ->
- valid_sporadic_job_with_jitter task_cost task_deadline task_jitter
- job_cost job_deadline job_jitter job_task j.
+ job_cost j <= task_cost (job_task j).
- (* ... and satisfy the sporadic task model.*)
- Hypothesis H_sporadic_tasks:
- sporadic_task_model task_period job_arrival job_task arr_seq.
+ (* ...the jitter of each job is bounded by the jitter of its task,... *)
+ Hypothesis H_job_jitter_le_task_jitter:
+ forall j,
+ arrives_in arr_seq j ->
+ job_jitter j <= task_jitter (job_task j).
+ (* ...and that job deadlines equal task deadlines. *)
+ Hypothesis H_job_deadline_eq_task_deadline:
+ forall j,
+ arrives_in arr_seq j ->
+ job_deadline j = task_deadline (job_task j).
+
(* Assume any fixed-priority policy... *)
Variable higher_eq_priority: FP_policy SporadicTask.
@@ -329,26 +340,21 @@ Module ResponseTimeIterationFP.
(tsk, R) \In RTA_claimed_bounds ->
response_time_bounded_by tsk (task_jitter tsk + R).
Proof.
- rename H_valid_task_parameters into PARAMS,
- H_valid_job_parameters into JOBPARAMS.
unfold valid_sporadic_job, valid_realtime_job,
valid_sporadic_taskset, is_valid_sporadic_task in *.
unfold RTA_claimed_bounds; intros tsk R.
case SOME: fp_claimed_bounds => [rt_bounds|] IN; last by done.
- move: (PARAMS) => PARAMStsk.
- feed (PARAMStsk tsk);
- [by apply fp_claimed_bounds_from_taskset with (tsk0 := tsk) (R0 := R) in SOME | des].
apply uniprocessor_response_time_bound_fp with
(task_cost0 := task_cost) (task_period0 := task_period)
- (ts0 := ts) (task_deadline0 := task_deadline)
- (job_deadline0 := job_deadline) (job_jitter0 := job_jitter)
+ (ts0 := ts) (job_jitter0 := job_jitter)
(higher_eq_priority0 := higher_eq_priority); try (by done).
{
apply fp_claimed_bounds_gt_zero with (task_cost0 := task_cost)
(task_period0 := task_period) (task_deadline0 := task_deadline)
(higher_eq_priority0 := higher_eq_priority) (ts0 := ts) (task_jitter0 := task_jitter)
(rt_bounds0 := rt_bounds) (tsk0 := tsk); try (by done).
- by intros tsk0 IN0; specialize (PARAMS tsk0 IN0); des.
+ apply H_positive_costs.
+ by eapply fp_claimed_bounds_from_taskset; eauto 1.
}
by apply fp_claimed_bounds_yields_fixed_point with
(task_deadline0 := task_deadline) (rt_bounds0 := rt_bounds).
@@ -370,17 +376,13 @@ Module ResponseTimeIterationFP.
have DL := fp_claimed_bounds_le_deadline task_cost task_period task_deadline
task_jitter higher_eq_priority ts.
have BOUND := fp_analysis_yields_response_time_bounds.
- rename H_test_succeeds into TEST, H_valid_job_parameters into JOBPARAMS.
+ rename H_test_succeeds into TEST.
move:TEST; case TEST:(fp_claimed_bounds _ _ _ _ _) => [rt_bounds|] _//.
intros tsk IN.
move: (RESP rt_bounds TEST tsk IN) => [R INbounds].
specialize (DL rt_bounds TEST tsk R INbounds).
apply task_completes_before_deadline with
(task_deadline0 := task_deadline) (R0 := task_jitter tsk + R); try (by done).
- {
- intros j ARRj; unfold valid_sporadic_job_with_jitter in *.
- by specialize (JOBPARAMS j ARRj); move: JOBPARAMS => [[_ [_ EQ]] _].
- }
by apply BOUND; rewrite /RTA_claimed_bounds TEST.
Qed.
diff --git a/analysis/uni/jitter/fp_rta_theory.v b/analysis/uni/jitter/fp_rta_theory.v
index 645ad7ca3..73069b6f6 100644
--- a/analysis/uni/jitter/fp_rta_theory.v
+++ b/analysis/uni/jitter/fp_rta_theory.v
@@ -30,34 +30,39 @@ Module ResponseTimeAnalysisFP.
Context {Job: eqType}.
Variable job_arrival: Job -> time.
Variable job_cost: Job -> time.
- Variable job_deadline: Job -> time.
Variable job_jitter: Job -> time.
Variable job_task: Job -> SporadicTask.
- (* Consider any job arrival sequence with consistent, non-duplicate arrivals... *)
+ (* Consider any task set ts... *)
+ Variable ts: seq SporadicTask.
+
+ (* ...with positive task periods. *)
+ Hypothesis H_positive_periods: forall tsk, tsk \in ts -> task_period tsk > 0.
+
+ (* Consider any job arrival sequence with consistent, duplicate-free arrivals... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
- (* ... in which jobs arrive sporadically and have valid parameters. *)
+ (* ... in which jobs arrive sporadically,... *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
- Hypothesis H_valid_job_parameters:
+
+ (* ...the cost of each job is bounded by the cost of its task, ... *)
+ Hypothesis H_job_cost_le_task_cost:
forall j,
arrives_in arr_seq j ->
- valid_sporadic_job_with_jitter task_cost task_deadline task_jitter
- job_cost job_deadline job_jitter job_task j.
+ job_cost j <= task_cost (job_task j).
- (* Consider a task set ts where all tasks have valid parameters... *)
- Variable ts: seq SporadicTask.
- Hypothesis H_valid_task_parameters:
- valid_sporadic_taskset task_cost task_period task_deadline ts.
-
- (* ... and assume that all jobs in the arrival sequence come from the task set. *)
- Hypothesis H_all_jobs_from_taskset:
+ (* ...and the jitter of each job is bounded by the jitter of its task. *)
+ Hypothesis H_job_jitter_le_task_jitter:
forall j,
arrives_in arr_seq j ->
- job_task j \in ts.
+ job_jitter j <= task_jitter (job_task j).
+
+ (* Assume that all jobs in the arrival sequence come from the task set. *)
+ Hypothesis H_all_jobs_from_taskset:
+ forall j, arrives_in arr_seq j -> job_task j \in ts.
(* Next, consider any uniprocessor schedule of this arrival sequence... *)
Variable sched: schedule Job.
@@ -105,15 +110,13 @@ Module ResponseTimeAnalysisFP.
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job,
valid_sporadic_taskset, is_valid_sporadic_task in *.
- rename H_response_time_is_fixed_point into FIX,
- H_valid_task_parameters into PARAMS,
- H_valid_job_parameters into JOBPARAMS.
+ rename H_response_time_is_fixed_point into FIX.
intros j IN JOBtsk.
set arr := actual_arrival job_arrival job_jitter.
apply completion_monotonic with (t := arr j + R); try (by done).
{
rewrite -addnA leq_add2l leq_add2r.
- by rewrite -JOBtsk; specialize (JOBPARAMS j IN); des.
+ by rewrite -JOBtsk; apply H_job_jitter_le_task_jitter.
}
set prio := FP_to_JLFP job_task higher_eq_priority.
apply busy_interval_bounds_response_time with (arr_seq0 := arr_seq)
@@ -122,8 +125,7 @@ Module ResponseTimeAnalysisFP.
- by intros x z y; apply H_priority_is_transitive.
intros t.
apply fp_workload_bound_holds with (task_cost0 := task_cost)
- (task_period0 := task_period) (task_deadline0 := task_deadline)
- (job_deadline0 := job_deadline) (task_jitter0 := task_jitter) (ts0 := ts); try (by done).
+ (task_period0 := task_period) (task_jitter0 := task_jitter) (ts0 := ts); try (by done).
by rewrite JOBtsk.
Qed.
diff --git a/analysis/uni/jitter/workload_bound_fp.v b/analysis/uni/jitter/workload_bound_fp.v
index f7379e31b..1e5c93580 100644
--- a/analysis/uni/jitter/workload_bound_fp.v
+++ b/analysis/uni/jitter/workload_bound_fp.v
@@ -155,22 +155,22 @@ Module WorkloadBoundFP.
Context {Task: eqType}.
Variable task_cost: Task -> time.
Variable task_period: Task -> time.
- Variable task_deadline: Task -> time.
Variable task_jitter: Task -> time.
Context {Job: eqType}.
Variable job_arrival: Job -> time.
Variable job_cost: Job -> time.
- Variable job_deadline: Job -> time.
Variable job_jitter: Job -> time.
Variable job_task: Job -> Task.
- (* Let ts be any task set with valid task parameters. *)
+ (* Let ts be any task set... *)
Variable ts: seq Task.
- Hypothesis H_valid_task_parameters:
- valid_sporadic_taskset task_cost task_period task_deadline ts.
+
+ (* ...with positive task periods. *)
+ Hypothesis H_positive_periods:
+ forall tsk, tsk \in ts -> task_period tsk > 0.
- (* Consider any job arrival sequence with consistent, non-duplicate arrivals. *)
+ (* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
@@ -178,18 +178,21 @@ Module WorkloadBoundFP.
(* First, let's define some local names for clarity. *)
Let actual_arrivals := actual_arrivals_between job_arrival job_jitter arr_seq.
- (* Next, assume that all jobs come from the task set ...*)
+ (* Next, assume that all jobs come from the task set, ...*)
Hypothesis H_all_jobs_from_taskset:
+ forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+ (* ...the cost of each job is bounded by the cost of its task, ... *)
+ Hypothesis H_job_cost_le_task_cost:
forall j,
arrives_in arr_seq j ->
- job_task j \in ts.
+ job_cost j <= task_cost (job_task j).
- (* ...and have valid parameters. *)
- Hypothesis H_valid_job_parameters:
+ (* ...and the jitter of each job is bounded by the jitter of its task. *)
+ Hypothesis H_job_jitter_le_task_jitter:
forall j,
arrives_in arr_seq j ->
- valid_sporadic_job_with_jitter task_cost task_deadline task_jitter
- job_cost job_deadline job_jitter job_task j.
+ job_jitter j <= task_jitter (job_task j).
(* Assume that jobs arrived sporadically. *)
Hypothesis H_sporadic_arrivals:
@@ -221,16 +224,13 @@ Module WorkloadBoundFP.
actual_hp_workload t (t + R) <= R.
Proof.
rename H_fixed_point into FIX, H_all_jobs_from_taskset into FROMTS,
- H_valid_job_parameters into JOBPARAMS,
- H_valid_task_parameters into PARAMS,
H_arrival_times_are_consistent into CONS, H_arrival_sequence_is_a_set into SET.
unfold actual_hp_workload, workload_of_higher_or_equal_priority_tasks,
valid_sporadic_job_with_jitter, valid_sporadic_job, valid_realtime_job,
valid_sporadic_taskset, is_valid_sporadic_task in *.
have BOUND := sporadic_task_with_jitter_arrival_bound task_period task_jitter job_arrival
job_jitter job_task arr_seq CONS SET.
- feed_n 2 BOUND; (try by done);
- first by intros j ARRj; specialize (JOBPARAMS j ARRj); des.
+ feed_n 2 BOUND; (try by done).
intro t.
rewrite {2}FIX /workload_bound /total_workload_bound_fp.
set l := actual_arrivals_between job_arrival job_jitter arr_seq t (t + R).
@@ -253,16 +253,12 @@ Module WorkloadBoundFP.
{
rewrite /num_actual_arrivals_of_task -sum1_size big_distrl /= big_filter.
apply leq_sum_seq; move => j1 IN1 /eqP EQ.
- rewrite -EQ mul1n.
- feed (JOBPARAMS j1).
- {
- rewrite mem_filter in IN1; move: IN1 => /andP [_ ARR1].
- by apply in_arrivals_implies_arrived in ARR1.
- }
- by move: JOBPARAMS => [[_ [LE _]] _].
+ rewrite -EQ mul1n; apply H_job_cost_le_task_cost.
+ rewrite mem_filter in IN1; move: IN1 => /andP [_ ARR1].
+ by apply in_arrivals_implies_arrived in ARR1.
}
rewrite /task_workload_bound_FP leq_mul2r; apply/orP; right.
- feed (BOUND t (t + R) tsk0); first by feed (PARAMS tsk0); last by des.
+ feed (BOUND t (t + R) tsk0); first by apply H_positive_periods.
by rewrite -addnA addKn in BOUND.
Qed.
diff --git a/analysis/uni/susp/dynamic/jitter/jitter_schedule.v b/analysis/uni/susp/dynamic/jitter/jitter_schedule.v
new file mode 100644
index 000000000..00494ad4c
--- /dev/null
+++ b/analysis/uni/susp/dynamic/jitter/jitter_schedule.v
@@ -0,0 +1,162 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.schedule.uni.jitter.schedule.
+Require Import rt.model.schedule.uni.transformation.construction.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
+
+(* In this file, we formalize a reduction from a suspension-aware schedule
+ to a jitter-aware schedule. *)
+Module JitterScheduleConstruction.
+
+ Import UniprocessorScheduleWithJitter Suspension Priority ScheduleConstruction.
+
+ Section ConstructingJitterSchedule.
+
+ Context {Task: eqType}.
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_task: Job -> Task.
+
+ (** Basic Setup & Setting*)
+
+ (* Consider any job arrival sequence. *)
+ Variable arr_seq: arrival_sequence Job.
+
+ (* Assume any FP policy and the corresponding job-level priority relation. *)
+ Variable higher_eq_priority: FP_policy Task.
+ Let job_higher_eq_priority := FP_to_JLFP job_task higher_eq_priority.
+
+ (* Consider the original job and task costs from the suspension-aware schedule... *)
+ Variable job_cost: Job -> time.
+ Variable task_cost: Task -> time.
+
+ (* ...and assume that jobs have associated suspension times. *)
+ Variable job_suspension_duration: job_suspension Job.
+
+ (* Next, consider any suspension-aware schedule of the arrival sequence. *)
+ Variable sched_susp: schedule Job.
+
+ (** Definition of the Reduction *)
+
+ (* Now we proceed with the reduction. Let j be the job to be analyzed. *)
+ Variable j: Job.
+
+ (* For simplicity, we give some local names for the parameters of this job... *)
+ Let arr_j := job_arrival j.
+ Let task_of_j := job_task j.
+
+ (* ...and recall the definition of other higher-or-equal-priority tasks. *)
+ Let other_hep_task tsk_other :=
+ higher_eq_priority tsk_other task_of_j && (tsk_other != task_of_j).
+
+ (* Moreover, assume that jobs from higher-priority tasks are associated a response-time bound R. *)
+ Variable R: Job -> time.
+
+ (* Now we are going to redefine the job parameters for the new schedule. *)
+ Section DefiningJobParameters.
+
+ (* First, we inflate job costs with suspension time. *)
+ Section CostInflation.
+
+ (* Recall the total suspension time of a job in the original schedule. *)
+ Let job_total_suspension :=
+ total_suspension job_cost job_suspension_duration.
+
+ (* We inflate job costs as follows.
+ (a) The cost of job j is inflated with its total suspension time.
+ (b) The cost of all other jobs remains unchanged. *)
+ Definition inflated_job_cost (any_j: Job) :=
+ if any_j == j then
+ job_cost any_j + job_total_suspension any_j
+ else
+ job_cost any_j.
+
+ End CostInflation.
+
+ (* Next, we show how to set the job jitter in the new schedule
+ to compensate for the suspension times. *)
+ Section ConvertingSuspensionToJitter.
+
+ (* Let any_j be any job in the new schedule. *)
+ Variable any_j: Job.
+
+ (* First, recall the distance between any_j and job j that is to be analyzed.
+ Note that since we use natural numbers, this distance saturates to 0 if
+ any_j arrives later than j. *)
+ Let distance_to_j := job_arrival j - job_arrival any_j.
+
+ (* Then, we define the actual job jitter in the new schedule as follows.
+ a) For every job of higher-priority tasks (with respect to job j), the jitter is set to
+ the minimum between the distance to j and the term (R any_j - job_cost any_j).
+ b) The remaining jobs have no jitter.
+
+ The intuition behind this formula is that any_j is to be released as close to job j as
+ possible, while not "trespassing" the response-time bound (R any_j) from sched_susp,
+ which is only assumed to be valid for higher-priority tasks. *)
+ Definition job_jitter :=
+ if other_hep_task (job_task any_j) then
+ minn distance_to_j (R any_j - job_cost any_j)
+ else 0.
+
+ End ConvertingSuspensionToJitter.
+
+ End DefiningJobParameters.
+
+ (** Schedule Construction *)
+
+ (* Next we generate a jitter-aware schedule using the job parameters above.
+ For that, we always pick the highest-priority pending job (after jitter) in
+ the new schedule. However, if there are multiple highest-priority jobs, we
+ try not to schedule job j in order to maximize interference. *)
+ Section ScheduleConstruction.
+
+ (* First, 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.
+
+ (* For simplicity, let's define some local names. *)
+ Let job_is_pending := pending job_arrival inflated_job_cost job_jitter sched_prefix.
+ Let actual_job_arrivals_up_to := actual_arrivals_up_to job_arrival job_jitter arr_seq.
+ Let lower_priority j1 j2 := ~~ job_higher_eq_priority j1 j2.
+
+ (* Next, consider the list of pending jobs at time t that are different from j
+ and whose jitter has passed, in the new schedule. *)
+ Definition pending_jobs_other_than_j :=
+ [seq j_other <- actual_job_arrivals_up_to t | job_is_pending j_other t & j_other != j].
+
+ (* From the list of pending jobs, we can return one of the (possibly many)
+ highest-priority jobs, or None, in case there are no pending jobs. *)
+ Definition highest_priority_job_other_than_j :=
+ seq_min job_higher_eq_priority pending_jobs_other_than_j.
+
+ (* Then, we construct the new schedule at time t as follows.
+ a) If job j is pending and the highest-priority job (other than j) has
+ lower priority than j, we have to schedule j.
+ b) Else, if job j is not pending, we pick one of the highest priority pending jobs. *)
+ Definition build_schedule : option Job :=
+ if job_is_pending j t then
+ if highest_priority_job_other_than_j is Some j_hp then
+ if lower_priority j_hp j then
+ Some j
+ else Some j_hp
+ else Some j
+ else highest_priority_job_other_than_j.
+
+ End ConstructionStep.
+
+ (* Finally, starting from the empty schedule, ...*)
+ Let empty_schedule : schedule Job := fun t => None.
+
+ (* ...we use the recursive definition above to construct the jitter-aware schedule. *)
+ Definition sched_jitter := build_schedule_from_prefixes build_schedule empty_schedule.
+
+ End ScheduleConstruction.
+
+ End ConstructingJitterSchedule.
+
+End JitterScheduleConstruction.
\ No newline at end of file
diff --git a/analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v b/analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v
new file mode 100644
index 000000000..67e68044b
--- /dev/null
+++ b/analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v
@@ -0,0 +1,459 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task
+ rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.arrival.jitter.job.
+Require Import rt.model.schedule.uni.schedulability rt.model.schedule.uni.service
+ rt.model.schedule.uni.workload
+ rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.jitter.schedule
+ rt.model.schedule.uni.jitter.valid_schedule
+ rt.model.schedule.uni.jitter.platform.
+Require Import rt.model.schedule.uni.susp.suspension_intervals
+ rt.model.schedule.uni.susp.schedule
+ rt.model.schedule.uni.susp.valid_schedule
+ rt.model.schedule.uni.susp.platform.
+Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule.
+Require Import rt.model.schedule.uni.transformation.construction.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
+
+(* In this file, we prove several properties about the constructed jitter-aware schedule. *)
+Module JitterScheduleProperties.
+
+ Import Job SporadicTaskset Suspension Priority SuspensionIntervals Workload Service
+ UniprocessorScheduleWithJitter Schedulability ResponseTime
+ ScheduleConstruction ValidSuspensionAwareSchedule ValidJitterAwareSchedule.
+
+ Module basic := schedule.UniprocessorSchedule.
+ Module susp := ScheduleWithSuspensions.
+ Module jitter_aware := Platform.
+ Module susp_aware := PlatformWithSuspensions.
+ Module job_jitter := JobWithJitter.
+ Module reduction := JitterScheduleConstruction.
+
+ Section ProvingScheduleProperties.
+
+ Context {Task: eqType}.
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_task: Job -> Task.
+
+ (** Basic Setup & Setting *)
+
+ (* 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:
+ forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+ (* Consider any FP policy that is reflexive, transitive and total. *)
+ Variable higher_eq_priority: FP_policy Task.
+ Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
+ Hypothesis H_priority_is_total: FP_is_total_over_task_set higher_eq_priority ts.
+ Let job_higher_eq_priority := FP_to_JLDP job_task higher_eq_priority.
+
+ (* Consider the original job and task costs from the suspension-aware schedule. *)
+ Variable job_cost: Job -> time.
+ Variable task_cost: Task -> time.
+
+ (* Assume that jobs have associated suspension times. *)
+ Variable job_suspension_duration: job_suspension Job.
+
+ (* Next, consider any valid suspension-aware schedule of this arrival sequence.
+ (Note: see rt.model.schedule.uni.susp.valid_schedule.v for details) *)
+ Variable sched_susp: schedule Job.
+ Hypothesis H_valid_schedule:
+ valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
+ job_suspension_duration job_cost sched_susp.
+
+ (* Finally, recall the definition of a job response-time bound in sched_susp. *)
+ Let job_response_time_in_sched_susp_bounded_by :=
+ is_response_time_bound_of_job job_arrival job_cost sched_susp.
+
+ (** Analysis Setup *)
+
+ (* Now we proceed with the reduction. Let j be the job to be analyzed. *)
+ Variable j: Job.
+ Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
+
+ (* For simplicity, let's give some local names for the parameters of this job... *)
+ Let arr_j := job_arrival j.
+ Let task_of_j := job_task j.
+
+ (* ...and recall the definition of other higher-or-equal-priority tasks. *)
+ Let other_hep_task tsk_other :=
+ higher_eq_priority tsk_other task_of_j && (tsk_other != task_of_j).
+
+ (* Moreover, assume that each job is associated a response-time bound R. *)
+ Variable R: Job -> time.
+
+ (** Instantiation of the Reduction *)
+
+ (* Next, recall the jitter-aware schedule from the reduction. *)
+ Let sched_jitter := reduction.sched_jitter job_arrival job_task arr_seq higher_eq_priority
+ job_cost job_suspension_duration j R.
+ Let inflated_job_cost := reduction.inflated_job_cost job_cost job_suspension_duration j.
+ Let job_jitter := reduction.job_jitter job_arrival job_task higher_eq_priority job_cost j R.
+
+ (** Schedule Construction *)
+
+ (* In this section, we prove that the jitter-aware schedule uses its construction function. *)
+ Section PropertiesOfScheduleConstruction.
+
+ Let build_schedule := reduction.build_schedule job_arrival job_task arr_seq higher_eq_priority
+ job_cost job_suspension_duration j R.
+
+ (* Then, by showing that the construction function depends only on the previous service, ... *)
+ Lemma sched_jitter_depends_only_on_service:
+ forall sched1 sched2 t,
+ (forall j, service sched1 j t = service sched2 j t) ->
+ build_schedule sched1 t = build_schedule sched2 t.
+ Proof.
+ intros sched1 sched2 t ALL.
+ rewrite /build_schedule /reduction.build_schedule /reduction.highest_priority_job_other_than_j.
+ set pend1 := pending _ _ _ sched1.
+ set pend2 := pending _ _ _ sched2.
+ have SAME': forall j, pend1 j t = pend2 j t.
+ {
+ intros j0; rewrite /pend1 /pend2 /pending.
+ case: jitter_has_passed => //=.
+ by rewrite /completed_by ALL.
+ }
+ set pendjobs := reduction.pending_jobs_other_than_j _ _ _ _ _ _ _ _.
+ have SAME: pendjobs sched1 t = pendjobs sched2 t.
+ {
+ apply eq_in_filter; intros j0 IN.
+ rewrite /pending; case: jitter_has_passed => //=.
+ by rewrite /completed_by ALL.
+ }
+ rewrite SAME SAME'; by done.
+ Qed.
+
+ (* ...we infer that the generated schedule is indeed based on the construction function. *)
+ Corollary sched_jitter_uses_construction_function:
+ forall t,
+ sched_jitter t = build_schedule sched_jitter t.
+ Proof.
+ by ins; apply service_dependent_schedule_construction, sched_jitter_depends_only_on_service.
+ Qed.
+
+ End PropertiesOfScheduleConstruction.
+
+ (** Valid Schedule Properties *)
+
+ (* In this section, we prove that sched_jitter is a valid jitter-aware schedule. *)
+ Section ScheduleIsValid.
+
+ (* For simplicity, let's recall some definitions from the schedule construction. *)
+ Let pending_jobs_other_than_j :=
+ reduction.pending_jobs_other_than_j job_arrival job_task arr_seq higher_eq_priority
+ job_cost job_suspension_duration j R sched_jitter.
+ Let hp_job_other_than_j :=
+ reduction.highest_priority_job_other_than_j job_arrival job_task arr_seq higher_eq_priority
+ job_cost job_suspension_duration j R sched_jitter.
+
+ (* Also recall the definition of a valid jitter-aware schedule. *)
+ Let is_valid_jitter_aware_schedule :=
+ valid_jitter_aware_schedule job_arrival arr_seq job_higher_eq_priority
+ inflated_job_cost job_jitter.
+
+ (* First, we show that scheduled jobs come from the arrival sequence. *)
+ Lemma sched_jitter_jobs_come_from_arrival_sequence:
+ jobs_come_from_arrival_sequence sched_jitter arr_seq.
+ Proof.
+ move: H_valid_schedule => [FROM _].
+ move => j0 t /eqP SCHED.
+ rewrite sched_jitter_uses_construction_function /reduction.build_schedule
+ -/hp_job_other_than_j in SCHED.
+ set pending_in_jitter := pending _ _ _ _ in SCHED.
+ destruct (hp_job_other_than_j t) as [j_hp|] eqn:HP; last first.
+ {
+ case PENDj: (pending_in_jitter j t); rewrite PENDj in SCHED; last by done.
+ by case: SCHED => SAME; subst j0.
+ }
+ {
+ have IN: arrives_in arr_seq j_hp.
+ {
+ have IN: j_hp \in pending_jobs_other_than_j t.
+ {
+ rewrite /hp_job_other_than_j /reduction.highest_priority_job_other_than_j in HP.
+ by apply seq_min_in_seq in HP.
+ }
+ rewrite mem_filter in IN; move: IN => /andP [/andP _ IN].
+ rewrite /actual_arrivals_up_to in IN.
+ by apply in_actual_arrivals_between_implies_arrived in IN.
+ }
+ case PENDj: (pending_in_jitter j t); rewrite PENDj in SCHED;
+ first by move: SCHED; case: (~~ _); case => SAME; subst.
+ by case: SCHED => SAME; subst j0.
+ }
+ Qed.
+
+ (* Next, we show that jobs do not execute before their arrival times... *)
+ Lemma sched_jitter_jobs_execute_after_jitter:
+ jobs_execute_after_jitter job_arrival job_jitter sched_jitter.
+ Proof.
+ move => j0 t /eqP SCHED.
+ rewrite sched_jitter_uses_construction_function /reduction.build_schedule
+ -/hp_job_other_than_j in SCHED.
+ set pending_in_jitter := pending _ _ _ _ in SCHED.
+ destruct (hp_job_other_than_j t) as [j_hp|] eqn:HP; last first.
+ {
+ case PENDj: (pending_in_jitter j t); rewrite PENDj in SCHED; last by done.
+ by case: SCHED => SAME; subst j0; move: PENDj => /andP [ARR _].
+ }
+ {
+ have ARR: jitter_has_passed job_arrival job_jitter j_hp t.
+ {
+ have IN: j_hp \in pending_jobs_other_than_j t.
+ {
+ rewrite /hp_job_other_than_j /reduction.highest_priority_job_other_than_j in HP.
+ by apply seq_min_in_seq in HP.
+ }
+ by rewrite mem_filter in IN; move: IN => /andP [/andP [/andP [ARR _] _] _].
+ }
+ case PENDj: (pending_in_jitter j t); rewrite PENDj in SCHED;
+ last by case: SCHED => SAME; subst j0.
+ move: SCHED; case: (~~ _); case => SAME; subst; last by done.
+ by move: PENDj => /andP [ARRj _].
+ }
+ Qed.
+
+ (* ...nor longer than their execution costs. *)
+ Lemma sched_jitter_completed_jobs_dont_execute:
+ completed_jobs_dont_execute inflated_job_cost sched_jitter.
+ Proof.
+ intros j0 t.
+ induction t;
+ first by rewrite /service /service_during big_geq //.
+ rewrite /service /service_during big_nat_recr //=.
+ rewrite leq_eqVlt in IHt; move: IHt => /orP [/eqP EQ | LT]; last first.
+ {
+ apply: leq_trans LT; rewrite -addn1.
+ by apply leq_add; last by apply leq_b1.
+ }
+ rewrite -[inflated_job_cost _]addn0; apply leq_add; first by rewrite -EQ.
+ rewrite leqn0 eqb0 /scheduled_at.
+ rewrite sched_jitter_uses_construction_function /reduction.build_schedule
+ -/hp_job_other_than_j.
+ destruct (hp_job_other_than_j t) as [j_hp|] eqn:HP; last first.
+ {
+ case PENDj: pending; last by done.
+ apply/eqP; case => SAME; subst j0; move: PENDj => /andP [_ NOTCOMPj].
+ by rewrite /completed_by EQ eq_refl in NOTCOMPj.
+ }
+ rewrite /hp_job_other_than_j /reduction.highest_priority_job_other_than_j in HP.
+ apply seq_min_in_seq in HP; rewrite mem_filter /pending /completed_by in HP.
+ move: HP => /andP [/andP [/andP [_ NOTCOMPhp] _] _].
+ case PENDj: pending.
+ {
+ move: PENDj => /andP [_ NOTCOMPj].
+ case: (~~ higher_eq_priority _ _); apply/eqP; case => SAME; subst j0;
+ first by rewrite /completed_by EQ eq_refl in NOTCOMPj.
+ by rewrite EQ eq_refl in NOTCOMPhp.
+ }
+ {
+ apply/eqP; case => SAME; subst j0.
+ by rewrite EQ eq_refl in NOTCOMPhp.
+ }
+ Qed.
+
+ (* In addition, we prove that the schedule is (jitter-aware) work-conserving... *)
+ Lemma sched_jitter_work_conserving:
+ jitter_aware.work_conserving job_arrival inflated_job_cost job_jitter arr_seq sched_jitter.
+ Proof.
+ intros j0 t IN BACK.
+ move: BACK => /andP [PEND NOTSCHED].
+ rewrite /scheduled_at sched_jitter_uses_construction_function
+ /reduction.build_schedule -/hp_job_other_than_j in NOTSCHED *.
+ destruct (hp_job_other_than_j t) as [j_hp|] eqn:HP.
+ {
+ case PENDj: pending; rewrite PENDj in NOTSCHED; last by exists j_hp.
+ by case: (~~ _); [by exists j | by exists j_hp].
+ }
+ {
+ case PENDj: pending; rewrite PENDj in NOTSCHED; first by exists j.
+ rewrite /hp_job_other_than_j /reduction.highest_priority_job_other_than_j in HP.
+ case: (boolP (j0 == j)) => [EQ | NEQ];
+ first by move: EQ => /eqP EQ; subst j0; rewrite PEND in PENDj.
+ have IN0: j0 \in pending_jobs_other_than_j t.
+ {
+ rewrite mem_filter PEND NEQ /=.
+ apply arrived_between_implies_in_actual_arrivals; try (by done).
+ by move: PEND => /andP [ARR _].
+ }
+ move: HP => /eqP HP; rewrite -[_ == _]negbK in HP.
+ exfalso; move: HP => /negP BUG; apply: BUG.
+ by apply seq_min_exists with (x := j0).
+ }
+ Qed.
+
+ (* ...and respects task priorities. *)
+ Lemma sched_jitter_respects_policy:
+ jitter_aware.respects_FP_policy job_arrival inflated_job_cost job_jitter
+ job_task arr_seq sched_jitter higher_eq_priority.
+ Proof.
+ rename H_priority_is_transitive into TRANS, H_priority_is_total into TOTAL,
+ H_priority_is_reflexive into REFL, H_jobs_from_taskset into FROMTS.
+ move => j1 j2 t IN BACK /eqP SCHED.
+ move: BACK => /andP [PEND NOTSCHED].
+ rewrite /scheduled_at sched_jitter_uses_construction_function /reduction.build_schedule
+ -/hp_job_other_than_j in SCHED NOTSCHED *.
+ set pend := pending _ _ _ _ in SCHED NOTSCHED.
+ have ALL: forall j_hi j_lo, hp_job_other_than_j t = Some j_hi ->
+ j_lo \in pending_jobs_other_than_j t ->
+ higher_eq_priority (job_task j_hi) (job_task j_lo).
+ {
+ intros j_hi j_lo SOME INlo; move: SCHED => MIN.
+ rewrite /hp_job_other_than_j /reduction.highest_priority_job_other_than_j in SOME.
+ apply seq_min_computes_min with (y := j_lo) in SOME; try (by done);
+ first by intros x y z; apply TRANS.
+ intros x y; rewrite mem_filter [y \in _]mem_filter /actual_arrivals_up_to.
+ move => /andP [_ INx] /andP [_ INy].
+ rewrite /FP_is_total_over_task_set /total_over_list in TOTAL.
+ by apply/orP; apply TOTAL; apply FROMTS;
+ eapply in_actual_arrivals_between_implies_arrived; eauto 1.
+ }
+ case PENDj: (pend j t); rewrite PENDj in SCHED NOTSCHED.
+ {
+ destruct (hp_job_other_than_j t) as [j_hp|] eqn:HP.
+ {
+ rewrite /FP_to_JLFP /= in SCHED NOTSCHED.
+ case LP: (~~ higher_eq_priority (job_task j_hp) (job_task j));
+ rewrite LP in SCHED NOTSCHED.
+ {
+ case: SCHED => SAME; subst j2.
+ case: (boolP (j1 == j)) => [EQ | NEQ]; first by move: EQ => /eqP EQ; subst j1.
+ apply (TRANS (job_task j_hp)).
+ {
+ have INhp: arrives_in arr_seq j_hp.
+ {
+ rewrite /hp_job_other_than_j /reduction.highest_priority_job_other_than_j in HP.
+ apply seq_min_in_seq in HP.
+ rewrite mem_filter in HP; move: HP => /andP [_ INhp].
+ rewrite /actual_arrivals_up_to in INhp.
+ by apply in_actual_arrivals_before_implies_arrived in INhp.
+ }
+ by exploit (TOTAL (job_task j) (job_task j_hp)); try (by apply FROMTS);
+ move => [HPj | HPhp]; last by rewrite HPhp in LP.
+ }
+ apply ALL; try (by done).
+ move: PEND => /andP [ARR NOTCOMP].
+ rewrite mem_filter /pending ARR NOTCOMP 2!andTb.
+ by apply/andP; split; last by apply arrived_between_implies_in_actual_arrivals.
+ }
+ {
+ case: SCHED => SAME; subst j2.
+ case: (boolP (j1 == j)) => [EQ | NEQ];
+ first by move: EQ => /eqP EQ; subst j1; apply negbT in LP; rewrite negbK in LP.
+ apply ALL; try (by done).
+ move: PEND => /andP [ARR NOTCOMP].
+ rewrite mem_filter /pending ARR NOTCOMP 2!andTb.
+ by apply/andP; split; last by apply arrived_between_implies_in_actual_arrivals.
+ }
+ }
+ {
+ case: SCHED => SAME; subst j2.
+ case: (boolP (j1 == j)) => [EQ | NEQ]; first by move: EQ => /eqP EQ; subst j1.
+ suff NOTNONE: hp_job_other_than_j t != None by rewrite HP in NOTNONE.
+ apply seq_min_exists with (x := j1).
+ move: PEND => /andP [ARR NOTCOMP].
+ rewrite mem_filter /pending ARR NOTCOMP 2!andTb.
+ by apply/andP; split; last by apply arrived_between_implies_in_actual_arrivals.
+ }
+ }
+ {
+ case: (boolP (j1 == j)) => [EQ | NEQ];
+ first by move: EQ => /eqP EQ; subst j1; rewrite -/pend PENDj in PEND.
+ apply ALL; first by done.
+ move: PEND => /andP [ARR NOTCOMP].
+ rewrite mem_filter /pending ARR NOTCOMP 2!andTb.
+ by apply/andP; split; last by apply arrived_between_implies_in_actual_arrivals.
+ }
+ Qed.
+
+ (* From the properties above, we conclude that the generated schedule is valid. *)
+ Corollary sched_jitter_is_valid: is_valid_jitter_aware_schedule sched_jitter.
+ Proof.
+ repeat split.
+ - by apply sched_jitter_jobs_come_from_arrival_sequence.
+ - by apply sched_jitter_jobs_execute_after_jitter.
+ - by apply sched_jitter_completed_jobs_dont_execute.
+ - by apply sched_jitter_work_conserving.
+ - by apply sched_jitter_respects_policy.
+ Qed.
+
+ (* Finally, we show that the generated schedule does not pick job j if
+ there are other pending higher-or-equal-priority jobs. *)
+ Lemma sched_jitter_does_not_pick_j:
+ forall j_hp t,
+ arrives_in arr_seq j_hp ->
+ j_hp != j ->
+ pending job_arrival inflated_job_cost job_jitter sched_jitter j_hp t ->
+ higher_eq_priority (job_task j_hp) (job_task j) ->
+ ~~ scheduled_at sched_jitter j t.
+ Proof.
+ rename H_priority_is_transitive into TRANS, H_priority_is_total into TOTAL,
+ H_jobs_from_taskset into FROMTS.
+ move => j_hp t ARRinhp NEQ PENDhp HP; apply/negP; move => /eqP SCHEDj.
+ rewrite sched_jitter_uses_construction_function /reduction.build_schedule
+ -/hp_job_other_than_j in SCHEDj.
+ set pend := pending _ _ _ _ in SCHEDj.
+ have INhp: j_hp \in pending_jobs_other_than_j t.
+ {
+ rewrite mem_filter PENDhp NEQ /=.
+ apply arrived_between_implies_in_actual_arrivals; try (by done).
+ rewrite /actual_arrival_between /=.
+ by move: PENDhp => /andP [ARRhp _].
+ }
+ case PENDj: (pend j t); rewrite PENDj in SCHEDj.
+ {
+ destruct (hp_job_other_than_j t) as [j_hp'|] eqn:HP'.
+ {
+ have ALL: forall j_lo, j_lo \in pending_jobs_other_than_j t ->
+ higher_eq_priority (job_task j_hp') (job_task j_lo).
+ {
+ intros j_lo INlo; move: HP' => MIN.
+ rewrite /hp_job_other_than_j /reduction.highest_priority_job_other_than_j in MIN.
+ apply seq_min_computes_min with (y := j_lo) in MIN; try (by done);
+ first by intros x y z; apply TRANS.
+ intros x y; rewrite mem_filter [y \in _]mem_filter /actual_arrivals_up_to.
+ move => /andP [_ INx] /andP [_ INy].
+ by apply/orP; apply TOTAL; apply FROMTS;
+ eapply in_actual_arrivals_between_implies_arrived; eauto 1.
+ }
+ case LP: (~~ higher_eq_priority (job_task j_hp') (job_task j)); rewrite LP in SCHEDj.
+ {
+ move: LP => /negP LP; apply: LP.
+ by apply (TRANS (job_task j_hp)); first by apply ALL.
+ }
+ {
+ case: SCHEDj => SAME; subst j_hp'.
+ rewrite /hp_job_other_than_j /reduction.highest_priority_job_other_than_j in HP'.
+ by apply seq_min_in_seq in HP'; rewrite mem_filter eq_refl andbF /= in HP'.
+ }
+ }
+ {
+ suff NOTNONE: hp_job_other_than_j t != None by rewrite HP' in NOTNONE.
+ by apply seq_min_exists with (x := j_hp).
+ }
+ }
+ {
+ rewrite /hp_job_other_than_j /reduction.highest_priority_job_other_than_j in SCHEDj.
+ apply seq_min_in_seq in SCHEDj.
+ by rewrite mem_filter eq_refl andbF in SCHEDj.
+ }
+ Qed.
+
+ End ScheduleIsValid.
+
+ End ProvingScheduleProperties.
+
+End JitterScheduleProperties.
\ No newline at end of file
diff --git a/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v b/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
new file mode 100644
index 000000000..c5d88d837
--- /dev/null
+++ b/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
@@ -0,0 +1,1283 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task
+ rt.model.arrival.basic.task_arrival
+ rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.arrival.jitter.job.
+Require Import rt.model.schedule.uni.schedulability rt.model.schedule.uni.service
+ rt.model.schedule.uni.workload
+ rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.jitter.schedule
+ rt.model.schedule.uni.jitter.platform.
+Require Import rt.model.schedule.uni.susp.suspension_intervals
+ rt.model.schedule.uni.susp.schedule
+ rt.model.schedule.uni.susp.platform
+ rt.model.schedule.uni.susp.valid_schedule.
+Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule
+ rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties.
+Require Import rt.model.schedule.uni.transformation.construction.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
+
+(* In this file, we compare the service received by the analyzed job j after
+ reducing the suspension-aware schedule to a jitter-aware schedule. *)
+Module JitterScheduleService.
+
+ Import Job SporadicTaskset Suspension Priority SuspensionIntervals Workload Service
+ UniprocessorScheduleWithJitter Schedulability ResponseTime TaskArrival
+ ScheduleConstruction ValidSuspensionAwareSchedule.
+
+ Module basic := schedule.UniprocessorSchedule.
+ Module susp := ScheduleWithSuspensions.
+ Module jitter_aware := Platform.
+ Module susp_aware := PlatformWithSuspensions.
+ Module job_jitter := JobWithJitter.
+ Module reduction := JitterScheduleConstruction.
+ Module reduction_prop := JitterScheduleProperties.
+
+ (* We begin by providing the initial setup and definitions in Sections 1 to 5.
+ The main results are proven later in Sections 6-(A) to 6-(C). *)
+ Section ProvingScheduleProperties.
+
+ Context {Task: eqType}.
+ Variable task_cost: Task -> time.
+ Variable task_period: Task -> time.
+ Variable task_deadline: Task -> time.
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
+ Variable job_task: Job -> Task.
+
+ (** 1) Basic Setup & Setting *)
+
+ (* Let ts be any task set. *)
+ Variable ts: seq Task.
+
+ (* Next, consider any consistent, duplicate-free job arrival sequence... *)
+ Variable arr_seq: arrival_sequence Job.
+ Hypothesis H_arrival_times_are_consistent:
+ arrival_times_are_consistent job_arrival arr_seq.
+ Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
+
+ (* ...where all jobs come from task set ts. *)
+ Hypothesis H_jobs_from_taskset:
+ forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+ (* Since we consider real-time tasks, assume that job deadlines are equal to task deadlines. *)
+ Hypothesis H_job_deadlines_equal_task_deadlines:
+ forall j, arrives_in arr_seq j -> job_deadline j = task_deadline (job_task j).
+
+ (* Also assume that tasks have constrained deadlines and that jobs arrive sporadically.
+ (Note: this is required to bound the interference of previous jobs of the analyzed task.) *)
+ Hypothesis H_constrained_deadlines:
+ constrained_deadline_model task_period task_deadline ts.
+ Hypothesis H_sporadic_arrivals:
+ sporadic_task_model task_period job_arrival job_task arr_seq.
+
+ (* Consider any FP policy that is reflexive, transitive and total. *)
+ Variable higher_eq_priority: FP_policy Task.
+ Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
+ Hypothesis H_priority_is_total: FP_is_total_over_task_set higher_eq_priority ts.
+ Let job_higher_eq_priority := FP_to_JLDP job_task higher_eq_priority.
+
+ (* Assume that jobs have associated suspension times. *)
+ Variable job_suspension_duration: job_suspension Job.
+
+ (* Next, consider any valid suspension-aware schedule of this arrival sequence.
+ (Note: see definition in rt.model.schedule.uni.susp.valid_schedule.v) *)
+ Variable sched_susp: schedule Job.
+ Hypothesis H_valid_schedule:
+ valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
+ job_suspension_duration job_cost sched_susp.
+
+ (* Finally, recall the notion of job response-time bound and deadline miss in sched_susp. *)
+ Let job_response_time_in_sched_susp_bounded_by :=
+ is_response_time_bound_of_job job_arrival job_cost sched_susp.
+ Let job_misses_no_deadline_in_sched_susp :=
+ job_misses_no_deadline job_arrival job_cost job_deadline sched_susp.
+
+ (** 2) Analysis Setup *)
+
+ (* Recall that we are going to analyze the response time of some job after
+ applying the reduction to the jitter-aware schedule as defined in
+ rt.analysis.uni.susp.dynamic.jitter.jitter_schedule. *)
+
+ (* Let j be the job to be analyzed. *)
+ Variable j: Job.
+ Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
+ Let arr_j := job_arrival j.
+
+ (* Let R_j be any value that we want to prove to be a response-time bound for job j in sched_susp.
+ Note that in the context of this proof, R_j also delimits the length of the schedules
+ that we are going to analyze, i.e., we only care about the interval [0, arr_j + R_j). *)
+ Variable R_j: time.
+
+ (* Next, recall the definition of higher-or-equal-priority tasks (other than j's task). *)
+ Let other_hep_task tsk_other :=
+ higher_eq_priority tsk_other (job_task j) && (tsk_other != job_task j).
+
+ (* Assume that each job of a higher-or-equal-priority task (other than j's task) is
+ associated a response-time bound R_hp.
+ (Note: this follows from analyzing the higher-priority tasks in a previous step.) *)
+ Variable R_hp: Job -> time.
+ Hypothesis H_bounded_response_time_of_hp_jobs:
+ forall j_hp,
+ arrives_in arr_seq j_hp ->
+ other_hep_task (job_task j_hp) ->
+ job_response_time_in_sched_susp_bounded_by j_hp (R_hp j_hp).
+
+ (* Also assume that all the previous jobs of same task as j do not miss any
+ deadlines in sched_susp.
+ (Note: this is an induction hypothesis that is easily obtained when analyzing the
+ sequence of jobs of the same task.) *)
+ Hypothesis H_no_deadline_misses_for_previous_jobs:
+ forall j0,
+ arrives_in arr_seq j0 ->
+ job_arrival j0 < job_arrival j ->
+ job_task j0 = job_task j ->
+ job_misses_no_deadline_in_sched_susp j0.
+
+ (** 3) Instantiation of the Reduction *)
+
+ (* Having stated all the properties of the suspension-aware schedule, now we recall
+ the construction of the jitter-aware schedule and the corresponding job parameters. *)
+ Let sched_jitter := reduction.sched_jitter job_arrival job_task arr_seq higher_eq_priority
+ job_cost job_suspension_duration j R_hp.
+ Let inflated_job_cost := reduction.inflated_job_cost job_cost job_suspension_duration j.
+ Let job_jitter := reduction.job_jitter job_arrival job_task higher_eq_priority job_cost j R_hp.
+
+ (* By the end of this file, we are going to show that if job j completes by time (arr_j + R_j)
+ in sched_jitter, then it also completes by time (arr_j + R_j) in sched_susp.
+ The argument is based on the fact that the service of higher-or-equal-priority jobs is moved
+ from the interval [0, arr_j) to the interval [arr_j, arr_j + R_j), when we introduce jitter.
+
+ The proofs are structured in the three final sections. In Section 6-A, we prove that
+ sched_jitter provides provides less service for higher-or-equal-priority jobs during [0, arr_j).
+ In Section B, we prove that sched_jitter provides more service for higher-or-equal-priority
+ jobs during [arr_j, arr_j + R). In Section 6-C, we conclude with the main theorem that compares
+ the response time of job j in both schedules. *)
+
+ (** 4) Setup for Next Sections *)
+
+ (* For simplicity, let's define some local names... *)
+ Let actual_job_arrival := actual_arrival job_arrival job_jitter.
+ Let job_arrived_before := arrived_before job_arrival.
+ Let job_has_arrived := has_arrived job_arrival.
+ Let job_has_actually_arrived := jitter_has_passed job_arrival job_jitter.
+ Let job_completed_in_sched_jitter := completed_by inflated_job_cost sched_jitter.
+
+ (* ...and also recall definitions related to the suspension-aware schedule. *)
+ Let job_suspended_at :=
+ suspended_at job_arrival job_cost job_suspension_duration sched_susp.
+ Let job_cumulative_suspension :=
+ cumulative_suspension_during job_arrival job_cost job_suspension_duration sched_susp.
+ Let job_completed_in_sched_susp := completed_by job_cost sched_susp.
+ Let backlogged_in_sched_susp := susp.backlogged job_arrival job_cost
+ job_suspension_duration sched_susp.
+
+ (* Since we'll have to reason about sets of arriving jobs with and without jitter,
+ let's use simpler names for those as well. *)
+ Let arrivals := jobs_arrived_between arr_seq.
+ Let actual_arrivals := actual_arrivals_between job_arrival job_jitter arr_seq.
+
+ (* Because we are dealing with a bounded scheduling window, we also identify all
+ job arrivals (with and without jitter) in the interval [0, arr_j + R_j). *)
+ Let arrivals_before_end_of_interval := arrivals 0 (arr_j + R_j).
+ Let actual_arrivals_before_end_of_interval := actual_arrivals 0 (arr_j + R_j).
+
+ (* Next, by checking jobs priorities, ... *)
+ Let other_higher_eq_priority_job j_hp :=
+ higher_eq_priority (job_task j_hp) (job_task j) && (j_hp != j).
+
+ (* ...we identify the workload of higher-or-equal-priority jobs (other than j)
+ that arrive in any interval [t1, t2), in the original schedule,... *)
+ Definition workload_of_other_hep_jobs_in_sched_susp t1 t2 :=
+ workload_of_jobs job_cost (arrivals t1 t2) other_higher_eq_priority_job.
+
+ (* ... and also the workload of higher-or-equal priority jobs (other than j)
+ with actual arrival time in the interval [t1, t2), in the jitter-aware schedule. *)
+ Definition workload_of_other_hep_jobs_in_sched_jitter t1 t2 :=
+ workload_of_jobs inflated_job_cost (actual_arrivals t1 t2) other_higher_eq_priority_job.
+
+ (* Next, we recall the cumulative service of all higher-or-equal-priority
+ jobs (other than j) that arrived in the interval [0, arr_j + R_j),
+ received in a given interval [t1, t2) in the original schedule. *)
+ Definition service_of_other_hep_jobs_in_sched_susp t1 t2 :=
+ service_of_jobs sched_susp arrivals_before_end_of_interval other_higher_eq_priority_job t1 t2.
+
+ (* Similarly, we recall the cumulative service of all higher-or-equal-priority
+ jobs (other than j) with actual arrival time in the interval [0, arr_j + R_j),
+ received in a given interval [t1, t2) in the jitter-aware schedule. *)
+ Definition service_of_other_hep_jobs_in_sched_jitter t1 t2 :=
+ service_of_jobs sched_jitter actual_arrivals_before_end_of_interval
+ other_higher_eq_priority_job t1 t2.
+
+ (** 5) Auxiliary Lemmas *)
+
+ (* Before moving to the main results, let's prove some auxiliary lemmas about service/workload. *)
+ Section AuxiliaryLemmas.
+
+ (* First, we prove that if all higher-or-equal-priority jobs have completed by
+ some time t in the jitter-aware schedule, then the service received
+ by those jobs up to time t amounts to the requested workload. *)
+ Section ServiceEqualsWorkload.
+
+ (* Let t be any time no later than (arr_j + R_j)... *)
+ Variable t: time.
+ Hypothesis H_before_end_of_interval: t <= arr_j + R_j.
+
+ (* ...in which all higher-or-equal-priority jobs (other than j) have completed. *)
+ Hypothesis H_workload_has_finished:
+ forall j_hp,
+ arrives_in arr_seq j_hp ->
+ actual_arrival_before job_arrival job_jitter j_hp t ->
+ other_higher_eq_priority_job j_hp ->
+ job_completed_in_sched_jitter j_hp t.
+
+ (* Then, the service received by all those jobs in the interval [0, t) amounts to
+ the workload requested by them in the interval [0, t). *)
+ Lemma jitter_reduction_service_equals_workload_in_jitter:
+ service_of_other_hep_jobs_in_sched_jitter 0 t >=
+ workload_of_other_hep_jobs_in_sched_jitter 0 t.
+ Proof.
+ rename H_workload_has_finished into WORK.
+ rewrite /workload_of_other_hep_jobs_in_sched_jitter
+ /workload_of_jobs /service_of_other_hep_jobs_in_sched_jitter
+ /actual_arrivals_before_end_of_interval /actual_arrivals_before.
+ set act := actual_arrivals.
+ set t1 := arr_j; set t2 := arr_j + R_j.
+ set hep := other_higher_eq_priority_job.
+ set Sj := service_during sched_jitter.
+ apply leq_trans with (n := \sum_(j0 <- act 0 t | hep j0) Sj j0 0 t); last first.
+ {
+ rewrite big_mkcond [X in _ <= X]big_mkcond.
+ apply leq_sum_sub_uniq; first by apply actual_arrivals_uniq.
+ intros j0 IN0.
+ by apply actual_arrivals_between_sub with (t3 := 0) (t4 := t).
+ }
+ apply leq_sum_seq; rewrite /act /actual_arrivals; intros j0 IN0 HP0.
+ apply eq_leq; symmetry; apply/eqP.
+ have ARRin: arrives_in arr_seq j0.
+ by apply in_actual_arrivals_between_implies_arrived in IN0.
+ apply in_actual_arrivals_implies_arrived_before in IN0.
+ by apply WORK.
+ Qed.
+
+ End ServiceEqualsWorkload.
+
+ (* Next, we prove a lemma showing that service in the suspension-aware schedule
+ is bounded by the workload. *)
+ Section ServiceBoundedByWorkload.
+
+ (* Consider any time t <= arr_j + R_j. *)
+ Variable t: time.
+ Hypothesis H_before_end_of_interval: t <= arr_j + R_j.
+
+ (* Then, the service of all jobs with higher-or-equal-priority that arrive in
+ the interval [0, arr_j + R_j), received in the interval [0, t), is no
+ larger than the workload of all jobs with higher-or-equal-priority that
+ are released in the interval [0, t), in the suspension-aware schedule. *)
+ Lemma jitter_reduction_service_in_sched_susp_le_workload:
+ service_of_other_hep_jobs_in_sched_susp 0 t <=
+ workload_of_other_hep_jobs_in_sched_susp 0 t.
+ Proof.
+ move: (H_valid_schedule) => [FROMarr [MUSTARRs [COMPs _]]].
+ rename H_before_end_of_interval into LTt.
+ rewrite /workload_of_other_hep_jobs_in_sched_susp /workload_of_jobs
+ /service_of_other_hep_jobs_in_sched_susp /service_of_jobs
+ /arrivals_before_end_of_interval /jobs_arrived_before.
+ set all := arrivals.
+ set t1 := arr_j; set t2 := arr_j + R_j.
+ set hep := other_higher_eq_priority_job.
+ set Ss := service_during sched_susp.
+ apply leq_trans with (n := \sum_(j0 <- all 0 t | hep j0) Ss j0 0 t);
+ last by apply leq_sum; intros j0 _; apply cumulative_service_le_job_cost.
+ rewrite exchange_big [X in _ <= X]exchange_big /=.
+ apply leq_sum_nat; move => t' /= LT' _.
+ apply leq_trans with (n := \sum_(j0 <- all 0 t2 | hep j0 &&
+ (scheduled_at sched_susp j0 t')) 1).
+ {
+ rewrite big_mkcond [X in _ <= X]big_mkcond.
+ rewrite /service_at; apply leq_sum; intros j0 _.
+ by case: hep; case SCHED': scheduled_at.
+ }
+ apply leq_trans with (n := \sum_(j0 <- all 0 t | hep j0 &&
+ (scheduled_at sched_susp j0 t')) 1); last first.
+ {
+ rewrite big_mkcond [X in _ <= X]big_mkcond.
+ rewrite /service_at; apply leq_sum; intros j0 _.
+ by case: hep; case SCHED': scheduled_at.
+ }
+ rewrite -big_filter -[X in _ <= X]big_filter.
+ apply leq_sum_sub_uniq; first by rewrite filter_uniq //; eapply arrivals_uniq; eauto 1.
+ intros j0; rewrite 2!mem_filter; move => /andP [/andP [HP0 SCHED0] IN0].
+ rewrite HP0 SCHED0 /=.
+ have ARRin0: arrives_in arr_seq j0 by apply FROMarr in SCHED0.
+ have ARR0: job_arrival j0 <= t' by apply MUSTARRs.
+ apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival);
+ try (by done).
+ by apply: (leq_ltn_trans _ LT').
+ Qed.
+
+ End ServiceBoundedByWorkload.
+
+ End AuxiliaryLemmas.
+
+ (** ** 6-(A) Less High-Priority Service Before the Arrival of Job j in sched_jitter *)
+
+ (* In this section we prove that before the arrival of job j, the cumulative service
+ received by other higher-or-equal-priority is no larger in the jitter-aware schedule
+ than in the suspension-aware schedule. *)
+ Section LessServiceBeforeArrival.
+
+ (* In fact, we can prove that the service is not larger for each higher-or-equal-priority
+ job in isolation. *)
+ Section LessServiceForEachJob.
+
+ (* Let j_hp be any higher-or-equal-priority job (different from j). *)
+ Variable j_hp: Job.
+ Hypothesis H_arrives: arrives_in arr_seq j_hp.
+ Hypothesis H_higher_or_equal_priority: other_higher_eq_priority_job j_hp.
+
+ (* For simplicity, let's define some local names. *)
+ Let arr_hp := job_arrival j_hp.
+ Let cost_hp := job_cost j_hp.
+ Let Rhp := R_hp j_hp.
+
+ (* Using a series of case analyses, we are going to prove that
+ service sched_jitter j_hp t <= service sched_susp j_hp t. *)
+ Section Case1.
+
+ (* Case 1. Assume that j_hp is a job from the same task as j. *)
+ Hypothesis H_same_task: job_task j_hp = job_task j.
+
+ (* Due to constrained deadlines, we can infer that previous jobs of the same task
+ complete in sched_susp before j arrives. Because these jobs do not have inflated
+ costs, they cannot receive more service in sched_jitter before the arrival of j. *)
+ Lemma jitter_reduction_less_job_service_before_interval_case1:
+ service sched_jitter j_hp arr_j <= service sched_susp j_hp arr_j.
+ Proof.
+ move: (H_valid_schedule) => [_ [MUSTARRs [COMPs _]]].
+ rename H_no_deadline_misses_for_previous_jobs into NOMISS,
+ H_constrained_deadlines into DL, H_jobs_from_taskset into FROM,
+ H_sporadic_arrivals into SPO.
+ move: H_higher_or_equal_priority => /andP [HP NEQ].
+ case (ltnP arr_hp arr_j) => [BEFORE | AFTER]; last first.
+ {
+ rewrite /service /service_during.
+ rewrite (cumulative_service_before_jitter_is_zero job_arrival job_jitter) //;
+ first by eapply reduction_prop.sched_jitter_jobs_execute_after_jitter; eauto 1.
+ move: H_same_task => /eqP SAMEtsk; apply negbF in SAMEtsk.
+ by rewrite /actual_arrival /job_jitter /reduction.job_jitter HP SAMEtsk /= addn0.
+ }
+ apply leq_trans with (n := inflated_job_cost j_hp).
+ {
+ apply cumulative_service_le_job_cost.
+ by apply reduction_prop.sched_jitter_completed_jobs_dont_execute.
+ }
+ rewrite /inflated_job_cost /reduction.inflated_job_cost.
+ apply negbTE in NEQ; rewrite NEQ.
+ apply eq_leq; symmetry; apply/eqP.
+ apply completion_monotonic with (t := arr_hp + job_deadline j_hp);
+ [by done | | by apply NOMISS].
+ rewrite H_job_deadlines_equal_task_deadlines //.
+ apply leq_trans with (n := arr_hp + task_period (job_task j_hp));
+ first by rewrite leq_add2l DL // FROM.
+ apply SPO; try (by done); last by apply ltnW.
+ by intros SAME; subst; rewrite eq_refl in NEQ.
+ Qed.
+
+ End Case1.
+
+ Section Case2.
+
+ (* Case 2. Assume that j_hp is a job from another task,... *)
+ Hypothesis H_different_task: job_task j_hp != job_task j.
+
+ (* ...that is released (with jitter) no earlier than the arrival of j. *)
+ Hypothesis H_released_no_earlier: arr_j <= actual_job_arrival j_hp.
+
+ (* Since j_hp cannot execute in sched_jitter, the claim trivially holds. *)
+ Lemma jitter_reduction_less_job_service_before_interval_case2:
+ service sched_jitter j_hp arr_j <= service sched_susp j_hp arr_j.
+ Proof.
+ rename H_different_task into DIFFtask.
+ move: H_higher_or_equal_priority => /andP [HP NEQ].
+ rewrite /service /service_during.
+ by rewrite (cumulative_service_before_jitter_is_zero job_arrival job_jitter) //;
+ first by eapply reduction_prop.sched_jitter_jobs_execute_after_jitter; eauto 1.
+ Qed.
+
+ End Case2.
+
+ Section Case3.
+
+ (* Case 3. Assume that j_hp is a job from another task,... *)
+ Hypothesis H_different_task: job_task j_hp != job_task j.
+
+ (* ...and that (arr_j - arr_hp < arr_j - cost_hp). *)
+ Hypothesis H_distance_is_smaller:
+ arr_j - arr_hp < Rhp - cost_hp.
+
+ (* By definition, the jitter of j_hp is set so that it arrives after j.
+ Since j_hp cannot execute in sched_jitter, the claim follows trivially. *)
+ Lemma jitter_reduction_less_job_service_before_interval_case3:
+ service sched_jitter j_hp arr_j <= service sched_susp j_hp arr_j.
+ Proof.
+ rename H_higher_or_equal_priority into HEP, H_distance_is_smaller into MIN.
+ move: (HEP) => /andP [HP NEQ].
+ rewrite /service /service_during.
+ rewrite (cumulative_service_before_jitter_is_zero job_arrival job_jitter) //;
+ first by eapply reduction_prop.sched_jitter_jobs_execute_after_jitter; eauto 1.
+ rewrite /actual_arrival /job_jitter /reduction.job_jitter HP H_different_task /=.
+ rewrite /minn MIN.
+ case (leqP (job_arrival j) (job_arrival j_hp)) => [AFTER | BEFORE];
+ first by apply: (leq_trans AFTER); apply leq_addr.
+ by rewrite subnKC; last by apply ltnW.
+ Qed.
+
+ End Case3.
+
+ Section Case4.
+
+ (* Case 4. Assume that j_hp is a job from another task... *)
+ Hypothesis H_different_task: job_task j_hp != job_task j.
+
+ (* ...and that j_hp completes in sched_susp before j arrives. *)
+ Hypothesis H_completes_before_j_arrives: arr_hp + Rhp <= arr_j.
+
+ (* Since j_hp completes early in sched_susp and receives maximum service, it cannot
+ receive more service in sched_jitter before j arrives, thus the claim holds. *)
+ Lemma jitter_reduction_less_job_service_before_interval_case4:
+ service sched_jitter j_hp arr_j <= service sched_susp j_hp arr_j.
+ Proof.
+ rename H_higher_or_equal_priority into HEP,
+ H_bounded_response_time_of_hp_jobs into RESPhp.
+ move: (HEP) => /andP [HP NEQ].
+ apply leq_trans with (n := service sched_susp j_hp (arr_hp + Rhp));
+ last by apply extend_sum.
+ apply leq_trans with (n := cost_hp);
+ last by apply eq_leq; symmetry; apply/eqP; apply RESPhp; last by apply/andP; split.
+ apply leq_trans with (n := inflated_job_cost j_hp);
+ last by rewrite /inflated_job_cost /reduction.inflated_job_cost -[_==_]negbK NEQ.
+ apply cumulative_service_le_job_cost.
+ by apply reduction_prop.sched_jitter_completed_jobs_dont_execute.
+ Qed.
+
+ End Case4.
+
+ Section Case5.
+
+ (* Case 5. Assume that j_hp is a job from another task,... *)
+ Hypothesis H_different_task: job_task j_hp != job_task j.
+
+ (* ...that is released (with jitter) before the arrival of j. *)
+ Hypothesis H_released_before: actual_job_arrival j_hp < arr_j.
+
+ (* Also assume that (arr_j < arr_hp + Rhp) and (Rhp - costhp <= arr_j - arr_hp). *)
+ Hypothesis H_j_hp_completes_after_j_arrives: arr_j < arr_hp + Rhp.
+ Hypothesis H_distance_is_not_smaller: Rhp - cost_hp <= arr_j - arr_hp.
+
+ (* Note that in this case the jitter of job j_hp is set to (Rhp - cost_hp). *)
+ Remark jitter_reduction_jitter_equals_R_minus_cost:
+ job_jitter j_hp = Rhp - cost_hp.
+ Proof.
+ rename H_higher_or_equal_priority into HEP, H_different_task into DIFFtask.
+ move: (HEP) => /andP [HP NEQ].
+ rewrite /job_jitter /reduction.job_jitter HP DIFFtask /= /minn.
+ by rewrite ltnNge H_distance_is_not_smaller /=.
+ Qed.
+
+ (* Since j_hp is released late in sched_jitter with "slack" (Rhp - cost_hp), even
+ if it executes at full speed, it cannot beat sched_susp in terms of service.
+ Therefore, the claim also holds. *)
+ Lemma jitter_reduction_less_job_service_before_interval_case5:
+ service sched_jitter j_hp arr_j <= service sched_susp j_hp arr_j.
+ Proof.
+ move: (H_valid_schedule) => [_ [MUSTARRs [COMPs _]]].
+ have JITdef := jitter_reduction_jitter_equals_R_minus_cost.
+ rename H_higher_or_equal_priority into HEP,
+ H_bounded_response_time_of_hp_jobs into RESPhp.
+ move: (HEP) => /andP [HP NEQ].
+ set arr_hp' := actual_job_arrival j_hp.
+ set cost_hp' := inflated_job_cost j_hp.
+ have JIT: job_jitter j_hp = Rhp - cost_hp by apply JITdef.
+ apply leq_trans with (n := cost_hp - (arr_hp + Rhp - arr_j)); last first.
+ {
+ rewrite /cost_hp leq_subLR.
+ apply leq_trans with (n := service sched_susp j_hp (arr_hp + Rhp));
+ first by apply eq_leq;symmetry;apply/eqP; apply RESPhp; last by apply/andP; split.
+ rewrite /service /service_during.
+ apply leq_trans with (n := \sum_(arr_j <= t' < arr_hp+Rhp)
+ 1 + service sched_susp j_hp arr_j);
+ last by apply leq_add; first by simpl_sum_const.
+ rewrite -> big_cat_nat with (n := arr_j); [simpl | by done | by apply ltnW].
+ by rewrite addnC; apply leq_add; first by apply leq_sum; intros t0 _; apply leq_b1.
+ }
+ {
+ have AFTERj := reduction_prop.sched_jitter_jobs_execute_after_jitter job_arrival
+ job_task arr_seq higher_eq_priority job_cost job_suspension_duration.
+ rewrite /service /service_during.
+ rewrite (ignore_service_before_jitter job_arrival job_jitter) //;
+ [| by eapply AFTERj; eauto 1 | by apply ltnW].
+ apply leq_trans with (n := \sum_(arr_hp' <= t0 < arr_j) 1);
+ first by apply leq_sum; intros t0 _; apply leq_b1.
+ simpl_sum_const; rewrite /arr_hp' /actual_job_arrival /actual_arrival JIT.
+ have LEcost: cost_hp <= Rhp.
+ {
+ apply leq_trans with (n := service sched_susp j_hp (arr_hp + Rhp));
+ first by apply eq_leq;symmetry;apply/eqP;apply RESPhp; last by apply/andP;split.
+ apply leq_trans with (n := \sum_(arr_hp <= t' < arr_hp + Rhp) 1);
+ last by simpl_sum_const; rewrite addKn.
+ rewrite /service /service_during.
+ rewrite (ignore_service_before_arrival job_arrival) //; last by apply leq_addr.
+ by apply leq_sum; intros t0 _; apply leq_b1.
+ }
+ rewrite addnBA; last by done.
+ rewrite subnBA; last by apply: (leq_trans LEcost); apply leq_addl.
+ rewrite subnBA; last by apply ltnW.
+ by apply leq_sub2r; rewrite addnC.
+ }
+ Qed.
+
+ End Case5.
+
+ (** **** Main Claim of Section (A) *)
+
+ (* Using the case analysis above, we conclude that before the arrival of job j,
+ any higher-or-equal-priority job receives no more service in the jitter-aware
+ schedule than in the suspension-aware schedule. *)
+ Lemma jitter_reduction_less_job_service_before_interval:
+ service sched_jitter j_hp arr_j <= service sched_susp j_hp arr_j.
+ Proof.
+ have CASE1 := jitter_reduction_less_job_service_before_interval_case1.
+ have CASE2 := jitter_reduction_less_job_service_before_interval_case2.
+ have CASE3 := jitter_reduction_less_job_service_before_interval_case3.
+ have CASE4 := jitter_reduction_less_job_service_before_interval_case4.
+ have CASE5 := jitter_reduction_less_job_service_before_interval_case5.
+ have AFTERj := reduction_prop.sched_jitter_jobs_execute_after_jitter job_arrival job_task
+ arr_seq higher_eq_priority job_cost job_suspension_duration j _ R_hp.
+ feed AFTERj; try (by done).
+ case (boolP (job_task j_hp == job_task j)) => [/eqP SAME | DIFFtsk]; first by apply CASE1.
+ case (leqP arr_j (actual_job_arrival j_hp)) => [LEarr | GTarr]; first by apply CASE2.
+ case (ltnP (arr_j - arr_hp) (Rhp - cost_hp)) => [LTdiff | GEdiff]; first by apply CASE3.
+ case (leqP (arr_hp + Rhp) arr_j) => [LEarrj | GTarrj]; first by apply CASE4.
+ by apply CASE5.
+ Qed.
+
+ End LessServiceForEachJob.
+
+ (* Since the result about service applies to each individual job, we can prove that
+ it also holds for the cumulative service of all higher-or-equal-priority jobs. *)
+ Corollary jitter_reduction_less_service_before_the_interval:
+ service_of_other_hep_jobs_in_sched_jitter 0 arr_j <=
+ service_of_other_hep_jobs_in_sched_susp 0 arr_j.
+ Proof.
+ rewrite /service_of_other_hep_jobs_in_sched_jitter
+ /service_of_other_hep_jobs_in_sched_susp
+ /actual_arrivals_before_end_of_interval /arrivals_before_end_of_interval
+ /actual_arrivals_before /jobs_arrived_before.
+ set hep := other_higher_eq_priority_job.
+ set Ss := service_during sched_susp.
+ set t2 := arr_j + R_j.
+ apply leq_trans with (n := \sum_(j_hp <- actual_arrivals 0 t2 | hep j_hp) Ss j_hp 0 arr_j).
+ {
+ apply leq_sum_seq; rewrite /actual_arrivals; intros j0 IN0 HEP0.
+ apply jitter_reduction_less_job_service_before_interval; try (by done).
+ by apply in_actual_arrivals_between_implies_arrived in IN0.
+ }
+ {
+ rewrite big_mkcond [X in _ <= X]big_mkcond /actual_arrivals /=.
+ apply leq_sum_sub_uniq; first by apply actual_arrivals_uniq.
+ by intros j0; rewrite !mem_filter /=; move => /andP [_ IN0].
+ }
+ Qed.
+
+ End LessServiceBeforeArrival.
+
+ (** ** 6-(B) More High-Priority Service After the Arrival of Job j in sched_jitter *)
+
+ (* So far, we have shown that the higher-or-equal-priority jobs receives less service
+ in the jitter-aware schedule during [0, arr_j). Recall that our final goal is to show
+ that all this service is actually moved into the interval [arr_j, arr_j + R_j) and
+ converted into interference for the job j being analyzed.
+ In this section, we reason about what happens to high-priority jobs after job j arrives. *)
+ Section MoreServiceAfterArrival.
+
+ (* First, we show that the workload is conserved at every point in the interval
+ [arr_j, arr_j + R_j). *)
+ Section Conservation.
+
+ (* Consider any time t >= arr_j (no earlier than the arrival of j). *)
+ Variable t: time.
+ Hypothesis H_no_earlier_than_j: t >= arr_j.
+
+ (* Then, we prove that every job that arrives up to time t is also released
+ in the jitter-aware schedule up to time t. *)
+ Lemma jitter_reduction_actual_arrival_before_end_of_interval:
+ forall j_hp,
+ other_higher_eq_priority_job j_hp ->
+ job_arrival j_hp <= t ->
+ actual_job_arrival j_hp <= t.
+ Proof.
+ move => j_hp /andP [HP NEQ] ARRhp.
+ set arr_hp := job_arrival j_hp.
+ set cost_hp := job_cost j_hp.
+ rewrite /actual_job_arrival /actual_arrival /job_jitter /reduction.job_jitter HP /=.
+ case: ifP => [NEQtsk | /eqP SAMEtsk]; last by rewrite addn0.
+ case (ltnP (arr_j - arr_hp) (R_hp j_hp - cost_hp)) => [MINl | MINr].
+ {
+ rewrite /minn MINl.
+ case (leqP arr_hp arr_j) => [BEFORE | AFTER]; first by rewrite subnKC //.
+ by apply leq_trans with (n := arr_hp + (arr_hp - arr_hp));
+ [by rewrite leq_add2l leq_sub2r // ltnW | by rewrite subnn addn0].
+ }
+ {
+ rewrite /minn ltnNge MINr /=.
+ apply leq_trans with (n := arr_hp + (arr_j - arr_hp)); first by rewrite leq_add2l.
+ case (leqP arr_hp arr_j) => [BEFORE | AFTER]; first by rewrite subnKC //.
+ by apply leq_trans with (n := arr_hp + (arr_hp - arr_hp));
+ [by rewrite leq_add2l leq_sub2r // ltnW | by rewrite subnn addn0].
+ }
+ Qed.
+
+ (* This implies that the workload is conserved up to time t (inclusive). That is,
+ in the jitter-aware schedule, there's always as much (high-priority) work to be
+ executed as in the original schedule. *)
+ Lemma jitter_reduction_workload_conservation_inside_interval:
+ workload_of_other_hep_jobs_in_sched_susp 0 t.+1 <=
+ workload_of_other_hep_jobs_in_sched_jitter 0 t.+1.
+ Proof.
+ rewrite /workload_of_other_hep_jobs_in_sched_susp
+ /workload_of_other_hep_jobs_in_sched_jitter /workload_of_jobs.
+ set all := arrivals; set act := actual_arrivals.
+ set hep := other_higher_eq_priority_job.
+ apply leq_trans with (n := \sum_(j0 <- all 0 t.+1 | hep j0) inflated_job_cost j0).
+ {
+ apply leq_sum_seq; rewrite /all /arrivals; move => j0 IN0 /andP [_ NEQ].
+ by apply negbTE in NEQ; rewrite /inflated_job_cost /reduction.inflated_job_cost NEQ //.
+ }
+ apply leq_trans with (n := \sum_(j0 <- all 0 t.+1 | hep j0 &&
+ (actual_job_arrival j0 < t.+1)) inflated_job_cost j0); last first.
+ {
+ rewrite -big_filter -[X in _ <= X]big_filter.
+ apply leq_sum_sub_uniq;
+ first by rewrite filter_uniq //; eapply arrivals_uniq; eauto 1.
+ intros j0; rewrite !mem_filter /=.
+ by move => /andP [/andP [HP LT] IN]; rewrite HP LT IN.
+ }
+ rewrite big_mkcond [X in _ <= X]big_mkcond /=.
+ apply leq_sum_seq; intros j0 IN0 _.
+ case HP: hep; simpl; last by done.
+ case: (leqP _ _); last by done.
+ intros BUG; exfalso; rewrite leqNgt in BUG; move: BUG => /negP BUG; apply: BUG.
+ apply jitter_reduction_actual_arrival_before_end_of_interval; try (by done).
+ by eapply in_arrivals_implies_arrived_before in IN0; eauto 1.
+ Qed.
+
+ End Conservation.
+
+ (* Since the higher-or-equal-priority jobs receive no more service in the jitter-aware
+ schedule during [0, arr_j), and because the workload is conserved, we prove next
+ that those jobs receive no less service in the jitter-aware schedule in the interval
+ [arr_j, arr_j + R_j). *)
+ Section MoreServiceInsideTheInterval.
+
+ (* The claim we need to show is presented next. The proof follows by induction on
+ the interval length d:
+ forall d,
+ d <= R_j ->
+ service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d) <=
+ service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d). *)
+
+ (* Since the base case of the induction is trivial, we focus on the inductive step. *)
+ Section InductiveStep.
+
+ (* By strong induction, assume that for a given interval length d < R_j, ... *)
+ Variable d: time.
+ Hypothesis H_d_lt_R: d < R_j.
+
+ (* ...the higher-or-equal-priority jobs (other than j) received as much service in
+ the jitter-aware schedule during [arr_j, arr_j + d) as in the suspension-aware
+ schedule. *)
+ Hypothesis H_induction_hypothesis:
+ service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d) <=
+ service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d).
+
+ (* Now we must prove that the claim continues to hold for interval [arr_j, arr_j + d + 1):
+
+ service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) <=
+ service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1). *)
+
+ (* The proof begins with a case analysis on whether there are pending
+ higher-or-equal-priority jobs at time (arr_j + d) in the jitter-aware schedule. *)
+ Section NoPendingJobs.
+
+ (* Case 1. Assume that all higher-or-equal-priority jobs (other than j) whose jitter
+ has passed by time (arr_j + d) are already complete at time (arr_j + d)
+ in the jitter-aware schedule. *)
+ Hypothesis H_all_jobs_completed_in_sched_jitter:
+ forall j_hp,
+ arrives_in arr_seq j_hp ->
+ other_higher_eq_priority_job j_hp ->
+ job_has_actually_arrived j_hp (arr_j + d) ->
+ job_completed_in_sched_jitter j_hp (arr_j + d).
+
+ (* First, we show that the service received in the suspension-aware schedule
+ during [arr_j, arr_j + d + 1) is bounded by the difference between the
+ requested workload and the service received prior to the arrival of job j. *)
+ Lemma jitter_reduction_convert_service_to_workload:
+ service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) <=
+ workload_of_other_hep_jobs_in_sched_susp 0 (arr_j + d + 1)
+ - service_of_other_hep_jobs_in_sched_susp 0 arr_j.
+ Proof.
+ have LEWORKs := jitter_reduction_service_in_sched_susp_le_workload.
+ rewrite /service_of_other_hep_jobs_in_sched_jitter
+ /actual_arrivals_before_end_of_interval /actual_arrivals_before.
+ rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs
+ /arrivals_before_end_of_interval /jobs_arrived_before.
+ set all := arrivals; set act := actual_arrivals.
+ set hep := other_higher_eq_priority_job.
+ set Ss := service_during sched_susp.
+ set Sj := service_during sched_jitter.
+ set SCHs := scheduled_at sched_susp.
+ set SCHj := scheduled_at sched_jitter.
+ set SUSP := job_cumulative_suspension.
+ set Wj := workload_of_other_hep_jobs_in_sched_jitter.
+ set Ws := workload_of_other_hep_jobs_in_sched_susp.
+ set t1 := arr_j.
+ set t2 := arr_j + R_j.
+ rewrite exchange_big [X in _ <= _ - X]exchange_big /= /service_at.
+ rewrite -/SCHs -/SCHj addnS addn0.
+ set TSs := fun a b => \sum_(a <= t0 < b)
+ \sum_(j_hp <- all 0 t2 | hep j_hp) SCHs j_hp t0.
+ set TSj := fun a b => \sum_(a <= t0 < b)
+ \sum_(j_hp <- act 0 t2 | hep j_hp) SCHj j_hp t0.
+ rewrite -/(TSs t1 (t1 + d).+1) -/(TSs 0 t1).
+ rewrite subh3 //; last first.
+ {
+ apply leq_trans with (n := TSs 0 (t1 + d).+1).
+ {
+ apply extend_sum; try (by done).
+ by apply leq_trans with (n := t1 + d); first by apply leq_addr.
+ }
+ rewrite /TSs exchange_big /=.
+ by apply LEWORKs.
+ }
+ rewrite addnC -big_cat_nat //=;
+ last by apply leq_trans with (n := t1 + d); first by apply leq_addr.
+ by rewrite exchange_big; apply LEWORKs; rewrite ltn_add2l.
+ Qed.
+
+ (* Because of workload conservation, we show that the workload in the suspension-aware
+ schedule is bounded by the workload in the jitter-aware schedule. *)
+ Lemma jitter_reduction_compare_workload:
+ workload_of_other_hep_jobs_in_sched_susp 0 (arr_j + d + 1)
+ - service_of_other_hep_jobs_in_sched_susp 0 arr_j
+ <= workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
+ - service_of_other_hep_jobs_in_sched_susp 0 arr_j.
+ Proof.
+ have CONS := jitter_reduction_workload_conservation_inside_interval.
+ rewrite /service_of_other_hep_jobs_in_sched_jitter
+ /actual_arrivals_before_end_of_interval /actual_arrivals_before.
+ rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs
+ /arrivals_before_end_of_interval /jobs_arrived_before.
+ set all := arrivals; set act := actual_arrivals.
+ set hep := other_higher_eq_priority_job.
+ set Ss := service_during sched_susp.
+ set Sj := service_during sched_jitter.
+ set SCHs := scheduled_at sched_susp.
+ set SCHj := scheduled_at sched_jitter.
+ set SUSP := job_cumulative_suspension.
+ set Wj := workload_of_other_hep_jobs_in_sched_jitter.
+ set Ws := workload_of_other_hep_jobs_in_sched_susp.
+ set t1 := arr_j.
+ set t2 := arr_j + R_j.
+ rewrite exchange_big /= /service_at.
+ rewrite -/SCHs -/SCHj addnS addn0.
+ set TSs := fun a b => \sum_(a <= t0 < b)
+ \sum_(j_hp <- all 0 t2 | hep j_hp) SCHs j_hp t0.
+ set TSj := fun a b => \sum_(a <= t0 < b)
+ \sum_(j_hp <- act 0 t2 | hep j_hp) SCHj j_hp t0.
+ rewrite -/(TSs t1 (t1 + d).+1) -/(TSs 0 t1).
+ apply leq_trans with (n := Ws 0 (t1 + d).+1 - TSs 0 t1); first by done.
+ by rewrite leq_sub2r //; apply CONS, leq_addr.
+ Qed.
+
+ (* Since the higher-or-equal-priority jobs received less service in the
+ jitter-aware schedule in the interval [0, arr_j), we can compare the
+ service in the two schedules. *)
+ Lemma jitter_reduction_compare_service:
+ workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
+ - service_of_other_hep_jobs_in_sched_susp 0 arr_j
+ <= workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
+ - service_of_other_hep_jobs_in_sched_jitter 0 arr_j.
+ Proof.
+ have LEserv := jitter_reduction_less_service_before_the_interval.
+ rewrite /service_of_other_hep_jobs_in_sched_jitter
+ /actual_arrivals_before_end_of_interval /actual_arrivals_before.
+ rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs
+ /arrivals_before_end_of_interval /jobs_arrived_before.
+ set all := arrivals; set act := actual_arrivals.
+ set hep := other_higher_eq_priority_job.
+ set Ss := service_during sched_susp.
+ set Sj := service_during sched_jitter.
+ set SCHs := scheduled_at sched_susp.
+ set SCHj := scheduled_at sched_jitter.
+ set SUSP := job_cumulative_suspension.
+ set Wj := workload_of_other_hep_jobs_in_sched_jitter.
+ set Ws := workload_of_other_hep_jobs_in_sched_susp.
+ set t1 := arr_j.
+ set t2 := arr_j + R_j.
+ rewrite exchange_big [X in _ <= _ - X]exchange_big /= /service_at.
+ rewrite -/SCHs -/SCHj addnS addn0.
+ set TSs := fun a b => \sum_(a <= t0 < b)
+ \sum_(j_hp <- all 0 t2 | hep j_hp) SCHs j_hp t0.
+ set TSj := fun a b => \sum_(a <= t0 < b)
+ \sum_(j_hp <- act 0 t2 | hep j_hp) SCHj j_hp t0.
+ rewrite -/(TSs t1 (t1 + d).+1) -/(TSs 0 t1).
+ rewrite leq_sub2l //.
+ rewrite /TSj /TSs exchange_big [X in _ <= X]exchange_big /=.
+ by apply LEserv.
+ Qed.
+
+ (* Having inferred that the difference between the workload and service is that
+ large in the jitter-aware schedule, we can convert this difference back to
+ service received in the interval [arr_j, arr_j + d + 1] in sched_jitter. *)
+ Lemma jitter_reduction_convert_workload_to_service:
+ workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1) -
+ service_of_other_hep_jobs_in_sched_jitter 0 arr_j <=
+ service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).
+ Proof.
+ have EQWORKj := jitter_reduction_service_equals_workload_in_jitter.
+ rename H_all_jobs_completed_in_sched_jitter into ALL.
+ rewrite /service_of_other_hep_jobs_in_sched_jitter
+ /actual_arrivals_before_end_of_interval /actual_arrivals_before.
+ rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs
+ /arrivals_before_end_of_interval /jobs_arrived_before.
+ set all := arrivals; set act := actual_arrivals.
+ set hep := other_higher_eq_priority_job.
+ set Ss := service_during sched_susp.
+ set Sj := service_during sched_jitter.
+ set SCHs := scheduled_at sched_susp.
+ set SCHj := scheduled_at sched_jitter.
+ set SUSP := job_cumulative_suspension.
+ set Wj := workload_of_other_hep_jobs_in_sched_jitter.
+ set Ws := workload_of_other_hep_jobs_in_sched_susp.
+ set t1 := arr_j.
+ set t2 := arr_j + R_j.
+ rewrite exchange_big [X in _ <= X]exchange_big /= /service_at.
+ rewrite -/SCHs -/SCHj addnS addn0.
+ set TSs := fun a b => \sum_(a <= t0 < b)
+ \sum_(j_hp <- all 0 t2 | hep j_hp) SCHs j_hp t0.
+ set TSj := fun a b => \sum_(a <= t0 < b)
+ \sum_(j_hp <- act 0 t2 | hep j_hp) SCHj j_hp t0.
+ rewrite -/(TSj t1 (t1 + d).+1) -/(TSj 0 t1).
+ rewrite leq_subLR -big_cat_nat //=;
+ last by apply leq_trans with (n := t1 + d); first by apply leq_addr.
+ rewrite exchange_big /=.
+ feed (EQWORKj (t1 + d).+1); first by rewrite ltn_add2l.
+ apply EQWORKj.
+ intros j0 ARRin0 ARR0 HEP0; specialize (ALL j0 ARRin0 HEP0 ARR0).
+ by apply completion_monotonic with (t := t1 + d);
+ first by apply reduction_prop.sched_jitter_completed_jobs_dont_execute.
+ Qed.
+
+ (* By combining each inequality above in sequence, we complete the induction
+ step for Case 1. *)
+ Lemma jitter_reduction_inductive_step_case1:
+ service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) <=
+ service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).
+ Proof.
+ apply: (leq_trans jitter_reduction_convert_service_to_workload).
+ apply: (leq_trans jitter_reduction_compare_workload).
+ apply: (leq_trans jitter_reduction_compare_service).
+ by apply: (leq_trans jitter_reduction_convert_workload_to_service).
+ Qed.
+
+ End NoPendingJobs.
+
+ Section ThereArePendingJobs.
+
+ (* Case 2. Assume that there are higher-or-equal-priority jobs (other than j) whose
+ jitter has passed by time (arr_j + d) that are still pending at time
+ (arr_j + d) in the jitter-aware schedule. *)
+ Hypothesis H_there_are_pending_jobs_in_sched_jitter:
+ exists j_hp,
+ arrives_in arr_seq j_hp /\
+ other_higher_eq_priority_job j_hp /\
+ job_has_actually_arrived j_hp (arr_j + d) /\
+ ~~ job_completed_in_sched_jitter j_hp (arr_j + d).
+
+ (* By the induction hypothesis, the higher-or-equal-priority jobs received
+ as much service in the jitter-aware schedule as in the suspension-aware
+ schedule in the interval [arr_j, arr_j + d). Therefore, it only remains
+ to show that:
+
+ service_of_other_hep_jobs_in_sched_susp (arr_j + d) (arr_j + d + 1) <=
+ service_of_other_hep_jobs_in_sched_jitter (arr_j + d) (arr_j + d + 1). *)
+
+ (* Because the LHS in the inequality above cannot be larger than 1 (single point),
+ it suffices to show that there is a higher-or-equal-priority job (different from j)
+ scheduled at time (arr_j + d) in the jitter-aware schedule. That follows
+ from two facts:
+ (a) The jitter-aware schedule is work-conserving and enforces priorities.
+ Therefore, even if the job j_hp in the hypothesis above is not scheduled,
+ there will always be a job with higher-or-equal-priority being scheduled.
+ (b) If there is at least one higher-or-equal-priority pending job, by the
+ additional property we embedded in the schedule construction, we avoid
+ scheduling job j (see lemma sched_jitter_does_not_pick_j). *)
+ Lemma jitter_reduction_inductive_step_case2:
+ service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) <=
+ service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).
+ Proof.
+ have RESPj := reduction_prop.sched_jitter_respects_policy job_arrival job_task ts
+ arr_seq _ _ higher_eq_priority _ _ _ job_cost job_suspension_duration j _ R_hp.
+ feed_n 6 RESPj; try (by done).
+ unfold reduction_prop.jitter_aware.respects_FP_policy in RESPj.
+ have NOTj := reduction_prop.sched_jitter_does_not_pick_j job_arrival job_task ts arr_seq
+ _ _ higher_eq_priority _ _ job_cost job_suspension_duration j R_hp.
+ feed_n 4 NOTj; try (by done).
+ have WORKj := reduction_prop.sched_jitter_work_conserving job_arrival job_task arr_seq _
+ higher_eq_priority job_cost job_suspension_duration j R_hp.
+ feed WORKj; first by done.
+ have AFTERj := reduction_prop.sched_jitter_jobs_execute_after_jitter job_arrival job_task
+ arr_seq higher_eq_priority job_cost job_suspension_duration j _ R_hp.
+ feed AFTERj; try (by done).
+ set sched_j := reduction_prop.reduction.sched_jitter _ _ _ _ _ _ _ _ in AFTERj NOTj
+ WORKj RESPj.
+ set inf_cost := reduction_prop.reduction.inflated_job_cost _ _ _ in NOTj WORKj
+ AFTERj RESPj.
+ set job_jit := reduction_prop.reduction.job_jitter _ _ _ _ _ _ in AFTERj NOTj
+ WORKj RESPj.
+ rename H_priority_is_transitive into TRANS, H_induction_hypothesis into IH,
+ H_there_are_pending_jobs_in_sched_jitter into HASj.
+ rewrite /service_of_other_hep_jobs_in_sched_jitter
+ /actual_arrivals_before_end_of_interval /actual_arrivals_before.
+ rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs
+ /arrivals_before_end_of_interval /jobs_arrived_before.
+ set all := arrivals; set act := actual_arrivals.
+ set hep := other_higher_eq_priority_job.
+ set Ss := service_during sched_susp.
+ set Sj := service_during sched_jitter.
+ set SCHs := scheduled_at sched_susp.
+ set SCHj := scheduled_at sched_jitter.
+ set SUSP := job_cumulative_suspension.
+ set Wj := workload_of_other_hep_jobs_in_sched_jitter.
+ set Ws := workload_of_other_hep_jobs_in_sched_susp.
+ set t1 := arr_j.
+ set t2 := arr_j + R_j.
+ rewrite exchange_big [X in _ <= X]exchange_big /=.
+ rewrite addnS /service_at addn0.
+ rewrite big_nat_recr ?leq_addr // big_nat_recr ?leq_addr //=.
+ apply leq_add;
+ first by rewrite exchange_big [X in _ <= X]exchange_big; apply IH.
+ case (boolP (has (fun j0 => hep j0 && scheduled_at sched_susp j0 (t1 + d))
+ (all 0 t2))) => [HASs | ALLs]; last first.
+ {
+ rewrite -all_predC in ALLs; move: ALLs => /allP ALLs.
+ rewrite big_seq_cond big1 //.
+ move => j0 /andP [IN0 HP0]; apply/eqP; rewrite eqb0.
+ by specialize (ALLs j0 IN0); rewrite /= HP0 /= in ALLs.
+ }
+ move: HASs => /hasP [j0 IN0 /andP [HP0 SCHED0]].
+ rewrite big_mkcond (bigD1_seq j0) /=; [| by done | by eapply arrivals_uniq; eauto 1].
+ rewrite HP0 SCHED0 big1 //; last first.
+ {
+ intros j1 NEQ; case: (hep j1); last by done.
+ apply/eqP; rewrite eqb0; apply/negP; intro SCHED1.
+ apply (only_one_job_scheduled _ j1) in SCHED0; last by done.
+ by rewrite SCHED0 eq_refl in NEQ.
+ }
+ rewrite addn0.
+ move: HASj => [j1 [ARRin1 [HEP1 [IN1 NOTCOMP1]]]].
+ move: (HEP1) => /andP [HP1 NEQ1].
+ rewrite /act /actual_arrivals in IN1.
+ case (boolP (scheduled_at sched_jitter j1 (t1+d))) => [SCHED1 | NOTSCHED1].
+ {
+ rewrite (big_rem j1) /=; first by rewrite /hep HEP1 SCHED1.
+ apply arrived_between_implies_in_actual_arrivals; try (by done).
+ rewrite /actual_arrival_between /=.
+ by apply leq_ltn_trans with (n := arr_j + d); last by rewrite ltn_add2l.
+ }
+ have BACK1: backlogged job_arrival inflated_job_cost job_jitter sched_jitter j1 (t1+d).
+ by repeat (apply/andP; split); try (by done).
+ move: (BACK1) (BACK1) => SCHED2 PRIO2.
+ apply WORKj in SCHED2; try (by done).
+ move: SCHED2 => [j2 SCHED2].
+ apply RESPj with (j_hp := j2) in PRIO2; try (by done).
+ have ARRin2: arrives_in arr_seq j2.
+ {
+ rewrite /sched_j in SCHED2.
+ by apply reduction_prop.sched_jitter_jobs_come_from_arrival_sequence with
+ (sched_susp0 := sched_susp) in SCHED2.
+ }
+ have HP2: hep j2.
+ {
+ apply/andP; split; first by apply (TRANS (job_task j1)).
+ apply/eqP; intro SAME; subst j2.
+ move: BACK1 => /andP [PEND1 _].
+ by specialize (NOTj j1 (t1+d) ARRin1 NEQ1 PEND1 HP1); rewrite SCHED2 in NOTj.
+ }
+ have IN2: j2 \in act 0 t2.
+ {
+ apply arrived_between_implies_in_actual_arrivals; try (by done).
+ rewrite /actual_arrival_between /=.
+ apply leq_ltn_trans with (n := t1+d); last by rewrite ltn_add2l.
+ by apply AFTERj.
+ }
+ by rewrite (big_rem j2) //= HP2 SCHED2.
+ Qed.
+
+ End ThereArePendingJobs.
+
+ End InductiveStep.
+
+ (** **** Main Claim of Section (B) *)
+
+ (* Using the proof by induction above, we conclude that, for any interval length
+ d <= R_j, the service received by higher-or-equal-priority jobs (other than j)
+ in the interval [arr_j, arr_j + d) in the jitter-aware schedule is as large as
+ the corresponding service in the suspension-aware schedule. *)
+ Lemma jitter_reduction_more_service_inside_the_interval:
+ forall d,
+ d <= R_j ->
+ service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d) <=
+ service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d).
+ Proof.
+ have CASE1 := jitter_reduction_inductive_step_case1.
+ have CASE2 := jitter_reduction_inductive_step_case2.
+ set all := arrivals; set act := actual_arrivals.
+ set hep := other_higher_eq_priority_job.
+ rename H_priority_is_transitive into TRANS.
+ induction d.
+ {
+ rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs.
+ by intros _; rewrite exchange_big /= addn0 big_geq.
+ }
+ intros LTR; feed (IHd); first by apply ltnW.
+ rewrite -addn1 addnA.
+ case (boolP (has (fun j0 => hep j0 && job_has_actually_arrived j0 (arr_j + d)
+ && ~~ completed_by inflated_job_cost sched_jitter j0 (arr_j + d))
+ (act 0 (arr_j + R_j)))) => [HASj | ALLj]; last first.
+ {
+ apply CASE1; try (by done).
+ rewrite -all_predC in ALLj; move: ALLj => /allP ALLj.
+ intros j0 ARRin0 HEP0 ARR0.
+ feed (ALLj j0).
+ {
+ apply arrived_between_implies_in_actual_arrivals; try (by done).
+ rewrite /actual_arrival_between /=.
+ by apply leq_ltn_trans with (n := arr_j + d); last by rewrite ltn_add2l.
+ }
+ by rewrite /= /hep HEP0 ARR0 /= negbK in ALLj.
+ }
+ {
+ apply (CASE2 _ LTR IHd).
+ move: HASj => /hasP [j0 IN0 /andP [/andP [HP0 ARR0] NOTCOMP0]].
+ exists j0; repeat (split); try (by done).
+ rewrite /act /actual_arrivals in IN0.
+ by apply in_actual_arrivals_between_implies_arrived in IN0.
+ }
+ Qed.
+
+ End MoreServiceInsideTheInterval.
+
+ End MoreServiceAfterArrival.
+
+ (** ** 6-(C) Conclusion: Comparing Response Times of Job j *)
+
+ (* In this section, we prove that the generated schedule is "worse" for job j.
+ More precisely, job j receives no more service in the jitter-aware schedule
+ than the cumulative service and suspension time in the original schedule. *)
+ Section JitterAwareScheduleIsWorse.
+
+ (* Recall the definition of job response-time bound in sched_jitter. *)
+ Let job_response_time_in_sched_jitter_bounded_by :=
+ is_response_time_bound_of_job job_arrival inflated_job_cost sched_jitter.
+
+ (* From this point, we are going to analyze both schedules up to time (arr_j + R_j) and
+ compare the service received by job j. At the end, we are going to prove that R_j is
+ also a response-time bound for job j in the suspension-aware schedule sched_susp. *)
+
+ (* First, we show that the service received by job j in the interval [arr_j, arr_j + R_j)
+ is always bounded by the difference between the interval length R_j and the service
+ received by the other higher-or-equal-priority jobs in the same interval. *)
+ Lemma jitter_reduction_service_jitter:
+ service_during sched_jitter j arr_j (arr_j + R_j) <=
+ R_j - service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + R_j).
+ Proof.
+ have ARRj := reduction_prop.sched_jitter_jobs_come_from_arrival_sequence job_arrival job_task
+ arr_seq higher_eq_priority job_cost job_suspension_duration sched_susp _ j _ R_hp.
+ feed_n 2 ARRj; try done.
+ have AFTERj := reduction_prop.sched_jitter_jobs_execute_after_jitter job_arrival job_task
+ arr_seq higher_eq_priority job_cost job_suspension_duration j _ R_hp.
+ feed AFTERj; try done.
+ set Sj := service_during sched_jitter j arr_j.
+ set Shp := service_of_other_hep_jobs_in_sched_jitter arr_j.
+ rewrite subh3 //; last first.
+ {
+ rewrite /Shp /service_of_other_hep_jobs_in_sched_jitter.
+ rewrite -[X in _ <= X](addKn arr_j).
+ by apply service_of_jobs_le_delta, actual_arrivals_uniq.
+ }
+ apply leq_trans with (n := \sum_(arr_j <= t < arr_j + R_j) 1);
+ last by simpl_sum_const; rewrite addKn.
+ rewrite /Sj /Shp /service_of_other_hep_jobs_in_sched_jitter /service_of_jobs
+ /service_during.
+ rewrite exchange_big -big_split /=.
+ apply leq_sum_nat; move => i /andP [GEi LTi] _.
+ destruct (sched_jitter i) as [j'|] eqn:SCHED;
+ last by rewrite /service_at /scheduled_at SCHED /= add0n; simpl_sum_const.
+ case (boolP ((j' == j) || ~~ higher_eq_priority (job_task j') (job_task j))).
+ {
+ intros OR; rewrite big1; first by rewrite addn0 leq_b1.
+ intros j_hp HP; rewrite /other_higher_eq_priority_job in HP.
+ apply/eqP; rewrite eqb0; apply contraT; rewrite negbK; move => /eqP SCHED'.
+ rewrite SCHED in SCHED'; case: SCHED' => SAME; subst j_hp.
+ move: OR => /orP [/eqP EQ | NOTHP]; subst; first by rewrite eq_refl andbF in HP.
+ by apply negbTE in NOTHP; rewrite NOTHP /= in HP.
+ }
+ {
+ rewrite negb_or negbK; move => /andP [NEQ HP].
+ rewrite -[1]add0n; apply leq_add.
+ {
+ rewrite leqn0 eqb0; apply/negP; intro SCHED'.
+ apply only_one_job_scheduled with (j1 := j') in SCHED'; [subst | by apply/eqP].
+ by rewrite eq_refl in NEQ.
+ }
+ {
+ move: SCHED => /eqP SCHED.
+ have IN: arrives_in arr_seq j' by apply ARRj in SCHED.
+ have ARR: actual_arrival_before job_arrival job_jitter j' (arr_j + R_j).
+ by apply AFTERj in SCHED; apply: (leq_ltn_trans _ LTi).
+ rewrite big_mkcond (bigD1_seq j') /=; first last.
+ - by eapply actual_arrivals_uniq; eauto 1.
+ - by eapply arrived_between_implies_in_actual_arrivals.
+ rewrite /other_higher_eq_priority_job HP NEQ /=.
+ move: SCHED => /eqP SCHED.
+ rewrite /service_at /scheduled_at SCHED eq_refl.
+ rewrite big1 //; intros j_other NEQother.
+ case: ifP => HPother; last by done.
+ apply/eqP; rewrite eqb0; apply/eqP; case => SAME; subst j_other.
+ by rewrite eq_refl in NEQother.
+ }
+ }
+ Qed.
+
+ (* Next, since we want to infer that job j is schedulable in the suspension-aware
+ schedule if it is schedulable in the jitter-aware schedule, we can assume by
+ contrapositive that job j has not completed by time (arr_j + R_j) in
+ the suspension-aware schedule. *)
+ Section JobNotCompleted.
+
+ (* Assume that j has not completed by (arr_j + R_j) in the suspension-aware schedule. *)
+ Hypothesis H_j_not_completed:
+ ~~ job_completed_in_sched_susp j (arr_j + R_j).
+
+ (* Then, we can prove that the difference between the interval length and
+ the service received by the other higher-or-equal-priority jobs during
+ [arr_j, arr_j + R_j) in the suspension-aware schedule is bounded by
+ the cumulative service and suspension time of job j. *)
+ Lemma jitter_reduction_service_susp:
+ R_j - service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + R_j) <=
+ service_during sched_susp j arr_j (arr_j + R_j) +
+ job_cumulative_suspension j arr_j (arr_j + R_j).
+ Proof.
+ move: (H_valid_schedule) => [FROM [ARRIVE [COMPs [WORK [PRIO _]]]]].
+ rename H_j_not_completed into NOTCOMP.
+ rewrite leq_subLR -big_split /=.
+ rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs.
+ rewrite exchange_big -big_split /=.
+ apply leq_trans with (n := \sum_(arr_j <= t < arr_j + R_j) 1);
+ first by simpl_sum_const; rewrite addKn.
+ apply leq_sum_nat; move => i /andP [GEi LTi] _.
+ rewrite -/job_suspended_at /service_at.
+ case: (boolP (job_suspended_at _ _)) => [SUSP | NOTSUSP];
+ [by rewrite addnA leq_addl | rewrite addn0].
+ case: (boolP (scheduled_at _ _ _)) => [SCHED | NOTSCHED];
+ [by rewrite leq_addl | rewrite addn0].
+ have BACK: susp.backlogged job_arrival job_cost job_suspension_duration sched_susp j i.
+ {
+ repeat (apply/andP; split); try (by done).
+ apply/negP; intro COMP.
+ move: NOTCOMP => /negP NOTCOMP; apply: NOTCOMP.
+ by apply completion_monotonic with (t := i); try (by done); apply ltnW.
+ }
+ move: (BACK) => SCHED; apply WORK in SCHED; last by done.
+ move: SCHED => [j_hp SCHEDhp].
+ have NEQ: j_hp != j by apply/eqP => SAME; subst; rewrite SCHEDhp in NOTSCHED.
+ have HP: higher_eq_priority (job_task j_hp) (job_task j) by apply PRIO with (t := i).
+ rewrite (big_rem j_hp) /other_higher_eq_priority_job /=; last first.
+ {
+ have IN: arrives_in arr_seq j_hp by apply FROM in SCHEDhp.
+ apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival);
+ try (by done).
+ by apply: (leq_trans _ LTi); apply ARRIVE.
+ }
+ by rewrite HP NEQ SCHEDhp /=.
+ Qed.
+
+ (* Since the higher-or-equal-priority jobs receive more service during
+ [arr_j, arr_j + R_j) in the jitter-aware schedule and produce more
+ interference, it follows that job j cannot receive as much service
+ in the jitter-aware schedule as in the suspension-aware schedule. *)
+ Lemma jitter_reduction_less_service_for_job_j:
+ service_during sched_jitter j arr_j (arr_j + R_j) <=
+ service_during sched_susp j arr_j (arr_j + R_j)
+ + job_cumulative_suspension j arr_j (arr_j + R_j).
+ Proof.
+ apply: (leq_trans jitter_reduction_service_jitter).
+ apply: (leq_trans _ jitter_reduction_service_susp).
+ by apply leq_sub2l, jitter_reduction_more_service_inside_the_interval.
+ Qed.
+
+ End JobNotCompleted.
+
+ (** **** Main Claim of Section (C) *)
+
+ (* Suppose that the response time of job j is bounded by R_j in sched_jitter. *)
+ Hypothesis H_response_time_of_j_in_sched_jitter:
+ job_response_time_in_sched_jitter_bounded_by j R_j.
+
+ (* Then, using the lemmas above, we conclude that the response time of job j in sched_susp
+ is also bounded by R_j. *)
+ Corollary jitter_reduction_job_j_completes_no_later:
+ job_response_time_in_sched_susp_bounded_by j R_j.
+ Proof.
+ move: (H_valid_schedule) => [_ [MUSTARRs [COMPs [WORK [PRIO SELF]]]]].
+ rename H_response_time_of_j_in_sched_jitter into COMPj.
+ apply contraT; intro NOTCOMPs.
+ suff NOTCOMPj: ~~ job_response_time_in_sched_jitter_bounded_by j R_j;
+ [by rewrite COMPj in NOTCOMPj | clear COMPj].
+ have LESS := jitter_reduction_less_service_for_job_j NOTCOMPs.
+ rewrite neq_ltn; apply/orP; left.
+ rewrite /inflated_job_cost /reduction.inflated_job_cost eq_refl.
+ apply leq_ltn_trans with (n := service_during sched_jitter j arr_j (arr_j + R_j)).
+ {
+ rewrite /service /service_during.
+ rewrite (ignore_service_before_arrival job_arrival) ?leq_addr //.
+ apply jobs_with_jitter_must_arrive_to_execute with (job_jitter0 := job_jitter).
+ by apply reduction_prop.sched_jitter_jobs_execute_after_jitter.
+ }
+ apply: (leq_ltn_trans LESS).
+ rewrite -addn1 -addnA [_ + 1]addnC addnA; apply leq_add.
+ {
+ rewrite addn1; apply contraT; rewrite -leqNgt; intro LE.
+ exfalso; move: NOTCOMPs => /negP NOTCOMPs; apply: NOTCOMPs.
+ rewrite /job_response_time_in_sched_susp_bounded_by /is_response_time_bound_of_job.
+ rewrite /completed_by eqn_leq; apply/andP; split;
+ first by apply cumulative_service_le_job_cost.
+ apply: (leq_trans LE).
+ rewrite /service /service_during.
+ by rewrite [X in _ <= X](ignore_service_before_arrival job_arrival) ?leq_addr.
+ }
+ by apply cumulative_suspension_le_total_suspension.
+ Qed.
+
+ End JitterAwareScheduleIsWorse.
+
+ End ProvingScheduleProperties.
+
+End JitterScheduleService.
\ No newline at end of file
diff --git a/analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v b/analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v
new file mode 100644
index 000000000..4500ed1c1
--- /dev/null
+++ b/analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v
@@ -0,0 +1,61 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.schedule.uni.jitter.schedule.
+Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
+
+(* In this file we construct a jitter-aware task set that contains the
+ jitter-aware schedule generated in the reduction. *)
+Module JitterTaskSetGeneration.
+
+ Import UniprocessorScheduleWithJitter Suspension Priority
+ JitterScheduleConstruction.
+
+ Section GeneratingTaskset.
+
+ Context {Task: eqType}.
+
+ (** Analysis Setup *)
+
+ (* Let ts be the original, suspension-aware task set. *)
+ Variable ts: seq Task.
+
+ (* Assume that tasks have cost and suspension bound. *)
+ Variable original_task_cost: Task -> time.
+ Variable task_suspension_bound: Task -> time.
+
+ (* Consider any FP policy that is reflexive, transitive and total, i.e., that
+ indicates "higher-or-equal priority". *)
+ Variable higher_eq_priority: FP_policy Task.
+
+ (* Let tsk_i be any task to be analyzed... *)
+ Variable tsk_i: Task.
+
+ (* ...and recall the definition of higher-or-equal-priority tasks (other than tsk_i). *)
+ Let other_hep_task tsk_other := higher_eq_priority tsk_other tsk_i && (tsk_other != tsk_i).
+
+ (** Definition of Jitter-Aware Task Parameters *)
+
+ (* We are going to define next a jitter-aware task set that models the jitter-aware
+ schedule that we constructed in the reduction. *)
+
+ (* First, using the task suspension bounds, we inflate the cost of the analyzed task
+ in a suspension-oblivious manner. *)
+ Definition inflated_task_cost (tsk: Task) :=
+ if tsk == tsk_i then
+ original_task_cost tsk + task_suspension_bound tsk
+ else original_task_cost tsk.
+
+ (* Next, assuming that higher-priority tasks have a valid response-time bound R,... *)
+ Variable R: Task -> time.
+
+ (* ...we define the task jitter as follows. *)
+ Definition task_jitter (tsk: Task) :=
+ if other_hep_task tsk then
+ R tsk - original_task_cost tsk
+ else 0.
+
+ End GeneratingTaskset.
+
+End JitterTaskSetGeneration.
\ No newline at end of file
diff --git a/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v b/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
new file mode 100644
index 000000000..21ebe100f
--- /dev/null
+++ b/analysis/uni/susp/dynamic/jitter/rta_by_reduction.v
@@ -0,0 +1,202 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task
+ rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task_arrival.
+Require Import rt.model.arrival.jitter.job.
+Require Import rt.model.schedule.uni.schedulability rt.model.schedule.uni.service
+ rt.model.schedule.uni.workload
+ rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.jitter.schedule
+ rt.model.schedule.uni.jitter.platform.
+Require Import rt.model.schedule.uni.susp.suspension_intervals
+ rt.model.schedule.uni.susp.schedule
+ rt.model.schedule.uni.susp.valid_schedule
+ rt.model.schedule.uni.susp.platform.
+Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule
+ rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties
+ rt.analysis.uni.susp.dynamic.jitter.jitter_schedule_service
+ rt.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+(* In this file, we determine task response-time bounds in suspension-aware
+ schedules using a reduction to jitter-aware schedules. *)
+Module RTAByReduction.
+
+ Import TaskArrival SporadicTaskset Suspension Priority Workload Service Schedulability
+ UniprocessorScheduleWithJitter ResponseTime SuspensionIntervals ValidSuspensionAwareSchedule.
+
+ Module susp_aware := PlatformWithSuspensions.
+ Module reduction := JitterScheduleConstruction.
+ Module reduction_prop := JitterScheduleProperties.
+ Module reduction_serv := JitterScheduleService.
+ Module ts_gen := JitterTaskSetGeneration.
+
+ Section ComparingResponseTimeBounds.
+
+ 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.
+
+ (** Basic Setup & Setting *)
+
+ (* Let ts be any task set with constrained deadlines. *)
+ Variable ts: seq Task.
+ Hypothesis H_constrained_deadlines:
+ constrained_deadline_model task_period task_deadline ts.
+
+ (* Consider any consistent, duplicate-free job arrival sequence... *)
+ Variable arr_seq: arrival_sequence Job.
+ Hypothesis H_arrival_times_are_consistent:
+ arrival_times_are_consistent job_arrival arr_seq.
+ Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
+
+ (* ...with sporadic arrivals... *)
+ Hypothesis H_sporadic_arrivals:
+ sporadic_task_model task_period job_arrival job_task arr_seq.
+
+ (* ...and in which all jobs come from task set ts. *)
+ Hypothesis H_jobs_from_taskset:
+ forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+ (* Since we consider real-time tasks, assume that job deadlines are equal to task deadlines. *)
+ Hypothesis H_job_deadlines_equal_task_deadlines:
+ forall j, arrives_in arr_seq j -> job_deadline j = task_deadline (job_task j).
+
+ (* Consider any FP policy that is reflexive, transitive and total.
+ Note that the policy does not depend on the schedule. *)
+ Variable higher_eq_priority: FP_policy Task.
+ Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
+ Hypothesis H_priority_is_total: FP_is_total_over_task_set higher_eq_priority ts.
+ Let job_higher_eq_priority := FP_to_JLDP job_task higher_eq_priority.
+
+ (* Assume that jobs and tasks have associated costs... *)
+ Variable job_cost: Job -> time.
+ Variable task_cost: Task -> time.
+
+ (* ...and suspension times. *)
+ Variable job_suspension_duration: job_suspension Job.
+ Variable task_suspension_bound: Task -> time.
+
+ (* Assume that jobs have positive cost. *)
+ Hypothesis H_positive_costs:
+ forall j, arrives_in arr_seq j -> job_cost j > 0.
+
+ (* Next, consider any valid suspension-aware schedule of this arrival sequence.
+ (Note: see rt.model.schedule.uni.susp.valid_schedule.v for details) *)
+ Variable sched_susp: schedule Job.
+ Hypothesis H_valid_schedule:
+ valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
+ job_suspension_duration job_cost sched_susp.
+
+ (** Analysis Setup *)
+
+ (* Now we proceed with the proof. Let tsk be the task to be analyzed. *)
+ Variable tsk: Task.
+ Hypothesis H_tsk_in_ts: tsk \in ts.
+
+ (* For simplicity, let's define some local names. *)
+ Let other_hep_task tsk_other :=
+ higher_eq_priority tsk_other tsk && (tsk_other != tsk).
+ Let task_response_time_in_sched_susp_bounded_by :=
+ is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched_susp.
+ Let job_response_time_in_sched_susp_bounded_by :=
+ is_response_time_bound_of_job job_arrival job_cost sched_susp.
+ Let completed_in_sched_susp_by := completed_by job_cost sched_susp.
+ Let job_misses_no_deadline_in_sched_susp :=
+ job_misses_no_deadline job_arrival job_cost job_deadline sched_susp.
+
+ (* Assume that each task is associated a value R... *)
+ Variable R: Task -> time.
+
+ (* ...that bounds the response-time of all tasks with higher-or-equal priority
+ (other than tsk) in the suspension-aware schedule sched_susp. *)
+ Hypothesis H_valid_response_time_bound_of_hp_tasks:
+ forall tsk_hp,
+ tsk_hp \in ts ->
+ other_hep_task tsk_hp ->
+ task_response_time_in_sched_susp_bounded_by tsk_hp (R tsk_hp).
+
+ (* The existence of those response-time bounds implies that we can compute the actual
+ response times of the higher-priority jobs in sched_susp. *)
+ Definition actual_response_time (j_hp: Job) : time :=
+ [pick-min r <= R (job_task j_hp) |
+ job_response_time_in_sched_susp_bounded_by j_hp r].
+
+ (* Next, let j be any job of tsk... *)
+ Variable j: Job.
+ Hypothesis H_j_arrives: arrives_in arr_seq j.
+ Hypothesis H_job_of_tsk: job_task j = tsk.
+
+ (* ...and assume that all the previous jobs of same task do not miss any
+ deadlines in sched_susp. *)
+ Hypothesis H_no_deadline_misses_for_previous_jobs:
+ forall j0,
+ arrives_in arr_seq j0 ->
+ job_arrival j0 < job_arrival j ->
+ job_task j0 = job_task j ->
+ job_misses_no_deadline_in_sched_susp j0.
+
+ (** Instantiation of the Reduction *)
+
+ (* First, recall the parameters of the jitter-aware task set. *)
+ Let inflated_task_cost := ts_gen.inflated_task_cost task_cost task_suspension_bound tsk.
+ Let task_jitter := ts_gen.task_jitter task_cost higher_eq_priority tsk.
+
+ (* Then, using the actual response times of higher-priority jobs as parameters, we construct
+ the jitter-aware schedule from sched_susp. *)
+ Let sched_jitter := reduction.sched_jitter job_arrival job_task arr_seq higher_eq_priority
+ job_cost job_suspension_duration j actual_response_time.
+
+ (* Next, recall the corresponding job parameters... *)
+ Let inflated_job_cost := reduction.inflated_job_cost job_cost job_suspension_duration j.
+ Let job_jitter := reduction.job_jitter job_arrival job_task higher_eq_priority job_cost j
+ actual_response_time.
+
+ (* ...and the definition of job response-time bound in sched_jitter. *)
+ Let job_response_time_in_sched_jitter_bounded_by :=
+ is_response_time_bound_of_job job_arrival inflated_job_cost sched_jitter.
+
+ (** Central Hypothesis *)
+
+ (* Assume that using some jitter-aware RTA, we determine that
+ (R tsk) is a response-time bound for tsk in sched_jitter. *)
+ Hypothesis H_valid_response_time_bound_in_sched_jitter:
+ job_response_time_in_sched_jitter_bounded_by j (R tsk).
+
+ (** **** Main Claim *)
+
+ (* Then, we use the properties of the reduction to prove that (R tsk) is also a
+ response-time bound for tsk in the original schedule sched_susp. *)
+ Theorem valid_response_time_bound_in_sched_susp:
+ job_response_time_in_sched_susp_bounded_by j (R tsk).
+ Proof.
+ rename H_priority_is_reflexive into REFL, H_priority_is_transitive into TRANS,
+ H_priority_is_total into TOT, H_jobs_from_taskset into FROM,
+ H_valid_response_time_bound_of_hp_tasks into RESPhp,
+ H_valid_response_time_bound_in_sched_jitter into RESPj.
+ rewrite -H_job_of_tsk /job_response_time_in_sched_susp_bounded_by.
+ apply reduction_serv.jitter_reduction_job_j_completes_no_later with (job_task0 := job_task)
+ (ts0 := ts) (arr_seq0 := arr_seq) (higher_eq_priority0 := higher_eq_priority)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (job_deadline0 := job_deadline)
+ (job_suspension_duration0 := job_suspension_duration) (R_hp := actual_response_time);
+ try (by done).
+ {
+ intros j_hp ARRhp OTHERhp.
+ rewrite /actual_response_time.
+ apply pick_min_holds; last by intros r RESP _.
+ exists (Ordinal (ltnSn (R (job_task j_hp)))).
+ by apply RESPhp; try (by done); [by apply FROM | rewrite /other_hep_task -H_job_of_tsk].
+ }
+ {
+ by rewrite /is_response_time_bound_of_job H_job_of_tsk; apply RESPj.
+ }
+ Qed.
+
+ End ComparingResponseTimeBounds.
+
+End RTAByReduction.
\ No newline at end of file
diff --git a/analysis/uni/susp/dynamic/jitter/taskset_membership.v b/analysis/uni/susp/dynamic/jitter/taskset_membership.v
new file mode 100644
index 000000000..40a2fb460
--- /dev/null
+++ b/analysis/uni/susp/dynamic/jitter/taskset_membership.v
@@ -0,0 +1,350 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job
+ rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.arrival.jitter.job.
+Require Import rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.susp.schedule
+ rt.model.schedule.uni.susp.platform
+ rt.model.schedule.uni.susp.valid_schedule.
+Require Import rt.analysis.uni.susp.dynamic.jitter.jitter_schedule
+ rt.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation.
+Require Import rt.analysis.uni.susp.sustainability.singlecost.reduction
+ rt.analysis.uni.susp.sustainability.singlecost.reduction_properties.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(* In this file we prove that the jitter-aware schedule sched_jitter used in the
+ reduction is an instance of the jitter-aware task set that we analyze. *)
+Module TaskSetMembership.
+
+ Import SporadicTaskset Suspension Priority ValidSuspensionAwareSchedule
+ ScheduleWithSuspensions ResponseTime PlatformWithSuspensions.
+
+ Module reduction := JitterScheduleConstruction.
+ Module ts_gen := JitterTaskSetGeneration.
+ Module sust := SustainabilitySingleCost.
+ Module sust_prop := SustainabilitySingleCostProperties.
+ Module valid_sched := ValidSuspensionAwareSchedule.
+ Module job_susp := Job.
+ Module job_jitter := JobWithJitter.
+
+ Section ProvingMembership.
+
+ 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.
+
+ (** Basic Setup & Setting*)
+
+ (* Let ts be any suspension-aware task set. *)
+ Variable ts: seq Task.
+
+ (* Consider any job arrival sequence with consistent, duplicate-free arrivals... *)
+ Variable arr_seq: arrival_sequence Job.
+ Hypothesis H_arrival_times_are_consistent:
+ arrival_times_are_consistent job_arrival arr_seq.
+ Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
+
+ (* ...where jobs come from the task set. *)
+ Hypothesis H_jobs_come_from_taskset:
+ forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+ (* ...and the associated job and task costs. *)
+ Variable job_cost: Job -> time.
+ Variable task_cost: Task -> time.
+
+ (* Assume that jobs and tasks have associated suspension times. *)
+ Variable job_suspension_duration: job_suspension Job.
+ Variable task_suspension_bound: Task -> time.
+
+ (* Assume any FP policy that is reflexive, transitive and total... *)
+ Variable higher_eq_priority: FP_policy Task.
+ Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
+ Hypothesis H_priority_is_total: FP_is_total_over_task_set higher_eq_priority ts.
+ Let job_higher_eq_priority := FP_to_JLDP job_task higher_eq_priority.
+
+ (* Recall the definition of a valid suspension-aware schedule. *)
+ Let is_valid_suspension_aware_schedule :=
+ valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
+ job_suspension_duration.
+
+ (* Next, consider any valid suspension-aware schedule of this arrival sequence.
+ (Note: see rt.model.schedule.uni.susp.valid_schedule.v for details) *)
+ Variable sched_susp: schedule Job.
+ Hypothesis H_valid_schedule:
+ valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
+ job_suspension_duration job_cost sched_susp.
+
+ (* Recall the definition of response-time bounds in sched_susp. *)
+ Let task_response_time_in_sched_susp_bounded_by :=
+ is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched_susp.
+ Let job_response_time_in_sched_susp_bounded_by :=
+ is_response_time_bound_of_job job_arrival job_cost sched_susp.
+
+ (** Analysis Setup *)
+
+ (* Let tsk_i be any task to be analyzed... *)
+ Variable tsk_i: Task.
+ Hypothesis H_tsk_in_ts: tsk_i \in ts.
+
+ (* ...and let j be any job of this task. *)
+ Variable j: Job.
+ Hypothesis H_j_arrives: arrives_in arr_seq j.
+ Hypothesis H_job_of_tsk_i: job_task j = tsk_i.
+
+ (* Also recall the definition of task response-time bound with any job cost and schedule... *)
+ Let is_task_response_time_bound_with job_cost sched :=
+ is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
+
+ (* ...and the definition of higher-or-equal-priority tasks (other than tsk_i). *)
+ Let other_hep_task tsk_other := higher_eq_priority tsk_other tsk_i && (tsk_other != tsk_i).
+
+ (* Next, assume that for each of those higher-or-equal-priority tasks (other than tsk_i),
+ we know a response-time bound R that is valid across all suspension-aware schedules of ts. *)
+ Variable R: Task -> time.
+ Hypothesis H_valid_response_time_bound_of_hp_tasks_in_all_schedules:
+ forall job_cost sched,
+ is_valid_suspension_aware_schedule job_cost sched ->
+ forall tsk_hp,
+ tsk_hp \in ts ->
+ other_hep_task tsk_hp ->
+ is_task_response_time_bound_with job_cost sched tsk_hp (R tsk_hp).
+
+ (* The existence of response-time bounds across all schedules implies that we can find
+ actual response times of the higher-priority jobs in sched_susp... *)
+ Definition actual_response_time (j_hp: Job) : time :=
+ [pick-min r <= R (job_task j_hp) |
+ job_response_time_in_sched_susp_bounded_by j_hp r].
+
+ (* ...and show that they are valid... *)
+ Corollary actual_response_time_is_valid:
+ forall j_hp,
+ arrives_in arr_seq j_hp ->
+ other_hep_task (job_task j_hp) ->
+ job_response_time_in_sched_susp_bounded_by j_hp (actual_response_time j_hp).
+ Proof.
+ rename H_valid_response_time_bound_of_hp_tasks_in_all_schedules into RESPhp,
+ H_jobs_come_from_taskset into FROM.
+ intros j_hp ARRhp HP.
+ rewrite /actual_response_time.
+ apply pick_min_holds; last by done.
+ exists (Ordinal (ltnSn (R (job_task j_hp)))). simpl.
+ by apply RESPhp; try (by done); first by apply FROM.
+ Qed.
+
+ (* ...and tight. *)
+ Corollary actual_response_time_is_minimum:
+ forall j_hp r_hp,
+ arrives_in arr_seq j_hp ->
+ other_hep_task (job_task j_hp) ->
+ job_response_time_in_sched_susp_bounded_by j_hp r_hp ->
+ actual_response_time j_hp <= r_hp.
+ Proof.
+ rename H_valid_response_time_bound_of_hp_tasks_in_all_schedules into RESPhp,
+ H_jobs_come_from_taskset into FROM.
+ intros j_hp r_hp ARRhp HP RESP.
+ case (leqP r_hp (R (job_task j_hp))) => [LT | GE].
+ {
+ rewrite /actual_response_time.
+ apply pick_min_holds;
+ last by intros x RESPx _ MINx; rewrite -ltnS in LT; apply (MINx (Ordinal LT)).
+ exists (Ordinal (ltnSn (R (job_task j_hp)))).
+ by apply RESPhp; try (by done); first by apply FROM.
+ }
+ {
+ apply leq_trans with (n := (R (job_task j_hp))); last by apply ltnW.
+ rewrite -ltnS /actual_response_time.
+ apply pick_min_ltn.
+ exists (Ordinal (ltnSn (R (job_task j_hp)))). simpl.
+ by apply RESPhp; try (by done); first by apply FROM.
+ }
+ Qed.
+
+ (** Instantiation of the Reduction *)
+
+ (* Using the actual response time of higher-priority jobs as a parameter, we construct
+ the jitter-aware schedule from sched_susp. *)
+ Let inflated_job_cost := reduction.inflated_job_cost job_cost job_suspension_duration j.
+ Let job_jitter := reduction.job_jitter job_arrival job_task higher_eq_priority job_cost j
+ actual_response_time.
+
+ (* We also recall the parameters of the generated jitter-aware task set. *)
+ Let inflated_task_cost := ts_gen.inflated_task_cost task_cost task_suspension_bound tsk_i.
+ Let task_jitter := ts_gen.task_jitter task_cost higher_eq_priority tsk_i R.
+
+ (** Proof of Task Set Membership *)
+
+ (* Now we proceed with the main claim. We are going to show that the job parameters in the
+ jitter-aware schedule sched_susp are an instance of the task set parameters. *)
+
+ (* Assume that the original costs are positive... *)
+ Hypothesis H_positive_costs:
+ forall j, arrives_in arr_seq j -> job_cost j > 0.
+
+ (* ...and no larger than the task costs. *)
+ Hypothesis H_job_cost_le_task_cost:
+ forall j,
+ arrives_in arr_seq j ->
+ job_cost j <= task_cost (job_task j).
+
+ (* Also assume that job suspension times are bounded by the task suspension bounds. *)
+ Hypothesis H_dynamic_suspensions:
+ dynamic_suspension_model job_cost job_task job_suspension_duration task_suspension_bound.
+
+ (* We begin by showing that the inflated job costs remain positive... *)
+ Section JobCostPositive.
+
+ Lemma ts_membership_inflated_job_cost_positive:
+ forall j, arrives_in arr_seq j -> inflated_job_cost j > 0.
+ Proof.
+ intros j0 ARR0.
+ apply leq_trans with (n := job_cost j0); first by apply H_positive_costs.
+ rewrite /inflated_job_cost /reduction.inflated_job_cost.
+ by case: ifP => _; first by apply leq_addr.
+ Qed.
+
+ End JobCostPositive.
+
+ (* ...and no larger than the inflated task costs. *)
+ Section JobCostBoundedByTaskCost.
+
+ Lemma ts_membership_inflated_job_cost_le_inflated_task_cost:
+ forall j,
+ arrives_in arr_seq j ->
+ inflated_job_cost j <= inflated_task_cost (job_task j).
+ Proof.
+ intros j' ARR'.
+ rewrite /inflated_job_cost /inflated_task_cost /reduction.inflated_job_cost
+ /ts_gen.inflated_task_cost.
+ case: ifP => [/eqP SAME | NEQ]; subst.
+ {
+ rewrite eq_refl; apply leq_add; last by apply H_dynamic_suspensions.
+ by apply H_job_cost_le_task_cost.
+ }
+ case: ifP => [SAMEtsk | DIFFtsk]; last by apply H_job_cost_le_task_cost.
+ apply leq_trans with (n := task_cost (job_task j')); last by apply leq_addr.
+ by apply H_job_cost_le_task_cost.
+ Qed.
+
+ End JobCostBoundedByTaskCost.
+
+ (* Finally, we show that the job jitter in sched_susp is upper-bounded by the task jitter.
+ This only concerns higher-priority jobs, which are assigned non-zero jitter to
+ compensate suspension times. *)
+ Section JobJitterBoundedByTaskJitter.
+
+ (* Let any_j be any job from the arrival sequence. *)
+ Variable any_j: Job.
+ Hypothesis H_any_j_arrives: arrives_in arr_seq any_j.
+
+ (* Since most parts of the proof are trivial, we focus on the more complicated case
+ of higher-priority jobs. *)
+ Section JitterOfHigherPriorityJobs.
+
+ (* Suppose that any_j is a higher-or-equal-priority job from some task other than tsk_i. *)
+ Hypothesis H_higher_priority: higher_eq_priority (job_task any_j) tsk_i.
+ Hypothesis H_different_task: job_task any_j != tsk_i.
+
+ (* Recall that we want to prove that job_jitter any_j <= task_jitter (job_task any_j).
+ By definition, this amounts to showing that:
+ actual_response_time any_j - job_cost any_j <=
+ R (job_task any_j) - task_cost (job_task any_j). *)
+
+ (* The proof follows by a sustainability argument based on the following reduction. *)
+
+ (* By inflating the cost of any_j to its worst-case execution time...*)
+ Let higher_cost_wcet j' :=
+ if j' == any_j then task_cost (job_task any_j) else job_cost j'.
+
+ (* ...we construct a new suspension-aware schedule sched_susp_highercost where the response
+ time of any_j is as large as in the original schedule sched_susp.
+ (For more details, see analysis/uni/susp/sustainability/cost. ) *)
+ Let sched_susp_highercost :=
+ sust.sched_susp_highercost job_arrival arr_seq job_higher_eq_priority
+ sched_susp job_suspension_duration higher_cost_wcet.
+
+ (* Next, recall the definition of task response-time bounds in sched_susp_highercost. *)
+ Let task_response_time_in_sched_susp_highercost_bounded_by :=
+ is_response_time_bound_of_task job_arrival higher_cost_wcet job_task arr_seq
+ sched_susp_highercost.
+
+ (* Since the response-time bounds R are valid across all suspension-aware schedules
+ of task set ts, they are also valid in sched_susp_higher_cost. *)
+ Remark response_time_bound_in_sched_susp_highercost:
+ forall tsk_hp,
+ tsk_hp \in ts ->
+ other_hep_task tsk_hp ->
+ task_response_time_in_sched_susp_highercost_bounded_by tsk_hp (R tsk_hp).
+ Proof.
+ rename H_valid_response_time_bound_of_hp_tasks_in_all_schedules into RESPhp,
+ H_jobs_come_from_taskset into FROM, H_valid_schedule into VALID.
+ split_conj VALID.
+ feed (RESPhp higher_cost_wcet sched_susp_highercost).
+ {
+ repeat split.
+ - by apply sust_prop.sched_susp_highercost_jobs_come_from_arrival_sequence.
+ - by apply sust_prop.sched_susp_highercost_jobs_must_arrive_to_execute.
+ - by apply sust_prop.sched_susp_highercost_completed_jobs_dont_execute.
+ - by apply sust_prop.sched_susp_highercost_work_conserving.
+ - apply sust_prop.sched_susp_highercost_respects_policy; try (by done).
+ -- by intros t j1 j2 j3; apply H_priority_is_transitive.
+ -- by intros j1 j2 t ARR1 ARR2; apply/orP; apply H_priority_is_total; apply FROM.
+ - by apply sust_prop.sched_susp_highercost_respects_self_suspensions.
+ }
+ by intros tsk_hp IN Ohp; by apply RESPhp.
+ Qed.
+
+ (* Finally, by comparing the two schedules, we prove that the difference between the
+ actual response time and job cost is bounded by the difference between the
+ response-time bound and the task cost. *)
+ Lemma ts_membership_difference_in_response_times:
+ actual_response_time any_j - job_cost any_j <=
+ R (job_task any_j) - task_cost (job_task any_j).
+ Proof.
+ have VALIDr := actual_response_time_is_valid.
+ have MINr := actual_response_time_is_minimum.
+ have RESPhp := response_time_bound_in_sched_susp_highercost.
+ rename H_jobs_come_from_taskset into FROM, H_valid_schedule into VALIDSCHED.
+ split_conj VALIDSCHED.
+ apply leq_trans with (n := R (job_task any_j) - higher_cost_wcet any_j);
+ last by apply leq_sub2l; rewrite /higher_cost_wcet eq_refl.
+ apply sust_prop.sched_susp_highercost_incurs_more_interference with
+ (job_arrival0 := job_arrival) (arr_seq0 := arr_seq) (sched_susp0 := sched_susp)
+ (higher_eq_priority0:=job_higher_eq_priority)
+ (job_suspension_duration0 := job_suspension_duration); try (by done).
+ - by intros t j1; apply H_priority_is_reflexive.
+ - by rewrite /higher_cost_wcet eq_refl; apply H_job_cost_le_task_cost.
+ - by move => j' NEQ; apply negbTE in NEQ; rewrite /higher_cost_wcet NEQ.
+ - by apply H_positive_costs.
+ - by apply VALIDr; try (by done); apply/andP; split.
+ - by intros r' RESP; apply MINr; try (by done); first by apply/andP; split.
+ - by apply RESPhp; try (by done); [apply FROM | apply/andP; split].
+ Qed.
+
+ End JitterOfHigherPriorityJobs.
+
+ (* Using the lemmas above, we conclude that the job jitter parameter is
+ upper-bounded by the task jitter for any job in the arrival sequence. *)
+ Lemma ts_membership_job_jitter_le_task_jitter:
+ job_jitter any_j <= task_jitter (job_task any_j).
+ Proof.
+ have DIFF := ts_membership_difference_in_response_times.
+ rewrite /job_jitter /task_jitter /reduction.job_jitter /ts_gen.task_jitter H_job_of_tsk_i.
+ case: ifP => // /andP [HP' NEQ].
+ rewrite /minn; case: ifP => [LTdist | GEdist]; last by apply DIFF.
+ case (leqP (job_arrival j) (job_arrival any_j)) => [AFTER | BEFORE];
+ first by apply leq_trans with (n := 0); first rewrite leqn0 subn_eq0.
+ apply leq_trans with (n := actual_response_time any_j - job_cost any_j); first by apply ltnW.
+ by apply DIFF.
+ Qed.
+
+ End JobJitterBoundedByTaskJitter.
+
+ End ProvingMembership.
+
+End TaskSetMembership.
\ No newline at end of file
diff --git a/analysis/uni/susp/dynamic/jitter/taskset_rta.v b/analysis/uni/susp/dynamic/jitter/taskset_rta.v
new file mode 100644
index 000000000..400d139f5
--- /dev/null
+++ b/analysis/uni/susp/dynamic/jitter/taskset_rta.v
@@ -0,0 +1,233 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job
+ rt.model.arrival.basic.task_arrival rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.arrival.jitter.job.
+Require Import rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.susp.schedule rt.model.schedule.uni.susp.platform
+ rt.model.schedule.uni.susp.valid_schedule.
+Require Import rt.model.schedule.uni.jitter.valid_schedule.
+Require Import rt.analysis.uni.susp.dynamic.jitter.rta_by_reduction
+ rt.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation
+ rt.analysis.uni.susp.dynamic.jitter.taskset_membership.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(* In this file we use the reduction to jitter-aware schedule to analyze
+ individual tasks using RTA. *)
+Module TaskSetRTA.
+
+ Import SporadicTaskset Suspension Priority ValidSuspensionAwareSchedule
+ ScheduleWithSuspensions ResponseTime PlatformWithSuspensions
+ TaskArrival ValidJitterAwareSchedule RTAByReduction TaskSetMembership.
+
+ Module ts_gen := JitterTaskSetGeneration.
+ Module job_susp := Job.
+ Module job_jitter := JobWithJitter.
+
+ (* In this section, we are going to assume we have obtained response-time
+ bounds for high-priority tasks and then use the reduction to infer a
+ response-time bound for a particular task. *)
+ Section PerTaskAnalysis.
+
+ Context {Task: eqType}.
+ Variable task_cost: Task -> time.
+ 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.
+
+ (** Basic Setup & Setting*)
+
+ (* Let ts be any task set with constrained deadlines. *)
+ Variable ts: seq Task.
+ Hypothesis H_constrained_deadlines:
+ constrained_deadline_model task_period task_deadline ts.
+
+ (* Consider any consistent, duplicate-free job arrival sequence... *)
+ Variable arr_seq: arrival_sequence Job.
+ Hypothesis H_arrival_times_are_consistent:
+ arrival_times_are_consistent job_arrival arr_seq.
+ Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
+
+ (* ...with sporadic arrivals... *)
+ Hypothesis H_sporadic_arrivals:
+ sporadic_task_model task_period job_arrival job_task arr_seq.
+
+ (* ...and in which all jobs come from the task set. *)
+ Hypothesis H_jobs_come_from_taskset:
+ forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+ (* Assume that job deadlines equal task deadlines. *)
+ Hypothesis H_job_deadline_eq_task_deadline:
+ forall j, arrives_in arr_seq j -> job_deadline j = task_deadline (job_task j).
+
+ (* Consider any job suspension times and task suspension bound. *)
+ Variable job_suspension_duration: job_suspension Job.
+ Variable task_suspension_bound: Task -> time.
+
+ (* Assume any FP policy that is reflexive, transitive and total. *)
+ Variable higher_eq_priority: FP_policy Task.
+ Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
+ Hypothesis H_priority_is_total: FP_is_total_over_task_set higher_eq_priority ts.
+ Let job_higher_eq_priority := FP_to_JLDP job_task higher_eq_priority.
+
+ (* Recall the definition of a valid suspension-aware and jitter-aware schedules. *)
+ Let is_valid_suspension_aware_schedule :=
+ valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
+ job_suspension_duration.
+ Let is_valid_jitter_aware_schedule :=
+ valid_jitter_aware_schedule job_arrival arr_seq job_higher_eq_priority.
+
+ (* Also recall the definition of task response-time bound for given job cost and schedule. *)
+ Let is_task_response_time_bound_with job_cost sched :=
+ is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
+
+ (** Analysis Setup *)
+
+ (* Let tsk_i be any task to be analyzed. *)
+ Variable tsk_i: Task.
+ Hypothesis H_tsk_in_ts: tsk_i \in ts.
+
+ (* Recall the definition of higher-or-equal-priority tasks (other than tsk_i). *)
+ Let other_hep_task tsk_other := higher_eq_priority tsk_other tsk_i && (tsk_other != tsk_i).
+
+ (* Next, assume that for each of those higher-or-equal-priority tasks (other than tsk_i),
+ we know a response-time bound R that is valid across all suspension-aware schedules of ts. *)
+ Variable R: Task -> time.
+ Hypothesis H_valid_response_time_bound_of_hp_tasks_in_all_schedules:
+ forall job_cost sched,
+ is_valid_suspension_aware_schedule job_cost sched ->
+ forall tsk_hp,
+ tsk_hp \in ts ->
+ other_hep_task tsk_hp ->
+ is_task_response_time_bound_with job_cost sched tsk_hp (R tsk_hp).
+
+ (* Since this analysis is for constrained deadlines, also assume that
+ (R tsk_i) is no larger than the deadline of tsk_i. *)
+ Hypothesis H_R_le_deadline: R tsk_i <= task_deadline tsk_i.
+
+ (** Recall: Properties of Valid Jitter-Aware Jobs *)
+
+ (* Recall that a valid jitter-aware schedule must have positive job costs,... *)
+ Let job_cost_positive job_cost :=
+ forall j, arrives_in arr_seq j -> job_cost j > 0.
+
+ (* ...job costs that are no larger than the task costs... *)
+ Let job_cost_le_task_cost job_cost task_cost :=
+ forall j,
+ arrives_in arr_seq j ->
+ job_cost j <= task_cost (job_task j).
+
+ (* ...and job jitter no larger than the task jitter. *)
+ Let job_jitter_le_task_jitter job_jitter task_jitter :=
+ forall j,
+ arrives_in arr_seq j ->
+ job_jitter j <= task_jitter (job_task j).
+
+ (* This is summarized in the following predicate. *)
+ Definition valid_jobs_with_jitter job_cost job_jitter task_cost task_jitter :=
+ job_cost_positive job_cost /\
+ job_cost_le_task_cost job_cost task_cost /\
+ job_jitter_le_task_jitter job_jitter task_jitter.
+
+ (** Conclusion: Response-time Bound for Task tsk_i *)
+
+ (* Recall the parameters of the generated jitter-aware task set. *)
+ Let inflated_task_cost := ts_gen.inflated_task_cost task_cost task_suspension_bound tsk_i.
+ Let task_jitter := ts_gen.task_jitter task_cost higher_eq_priority tsk_i R.
+
+ (* By using a jitter-aware RTA, assume that we proved that (R tsk_i) is a valid
+ response-time bound for task tsk_i in any jitter-aware schedule of the same
+ arrival sequence. *)
+ Hypothesis H_valid_response_time_bound_of_tsk_i:
+ forall job_cost job_jitter sched,
+ valid_jobs_with_jitter job_cost job_jitter inflated_task_cost task_jitter ->
+ is_valid_jitter_aware_schedule job_cost job_jitter sched ->
+ is_task_response_time_bound_with job_cost sched tsk_i (R tsk_i).
+
+ (* Next, consider any job cost function... *)
+ Variable job_cost: Job -> time.
+
+ (* ...and let sched_susp be any valid suspension-aware schedule with those job costs. *)
+ Variable sched_susp: schedule Job.
+ Hypothesis H_valid_schedule: is_valid_suspension_aware_schedule job_cost sched_susp.
+
+ (* Assume that the job costs are positive... *)
+ Hypothesis H_job_cost_positive:
+ forall j, arrives_in arr_seq j -> job_cost j > 0.
+
+ (* ...and no larger than the task costs. *)
+ Hypothesis H_job_cost_le_task_cost:
+ forall j,
+ arrives_in arr_seq j ->
+ job_cost j <= task_cost (job_task j).
+
+ (* Also assume that job suspension times are bounded by the task suspension bounds. *)
+ Hypothesis H_dynamic_suspensions:
+ dynamic_suspension_model job_cost job_task job_suspension_duration task_suspension_bound.
+
+ (* Using the reduction to a jitter-aware schedule, we conclude that (R tsk_i) must
+ also be a response-time bound for task tsk_i in the suspension-aware schedule. *)
+ Theorem valid_response_time_bound_of_tsk_i:
+ is_task_response_time_bound_with job_cost sched_susp tsk_i (R tsk_i).
+ Proof.
+ unfold is_task_response_time_bound_with,
+ is_response_time_bound_of_task, is_response_time_bound_of_job in *.
+ rename H_valid_response_time_bound_of_hp_tasks_in_all_schedules into RESPhp,
+ H_valid_response_time_bound_of_tsk_i into RESPi.
+
+ move: (H_valid_schedule) => [_ [_ [COMP _]]].
+ intros j ARRj JOBtsk.
+
+ (* First, rewrite the claim in terms of the *absolute* response-time bound (arrival + R) *)
+ remember (job_arrival j + R tsk_i) as ctime.
+
+ (* Now, we apply strong induction on the absolute response-time bound. *)
+ generalize dependent j.
+ induction ctime as [ctime IH] using strong_ind.
+
+ intros j ARRj JOBtsk EQc; subst ctime.
+
+ (* First, let's simplify the induction hypothesis. *)
+ have BEFOREok:
+ forall j0,
+ arrives_in arr_seq j0 ->
+ job_task j0 = tsk_i ->
+ job_arrival j0 < job_arrival j ->
+ completed_by job_cost sched_susp j0 (job_arrival j0 + R tsk_i);
+ [by ins; apply IH; try (by done); rewrite ltn_add2r | clear IH].
+ set actual_response_time :=
+ actual_response_time job_arrival job_task job_cost sched_susp R.
+ set inflated_job_cost :=
+ reduction.inflated_job_cost job_cost job_suspension_duration.
+ set job_jitter := reduction.job_jitter job_arrival job_task
+ higher_eq_priority job_cost j actual_response_time.
+ apply valid_response_time_bound_in_sched_susp with
+ (task_period0 := task_period) (task_deadline0 := task_deadline)
+ (job_deadline0 := job_deadline) (job_task0 := job_task) (ts0 := ts)
+ (arr_seq0 := arr_seq) (higher_eq_priority0 := higher_eq_priority)
+ (job_suspension_duration0:=job_suspension_duration); try (by done).
+ - by intros tsk_hp IN OHEP j'; apply RESPhp.
+ {
+ intros j0 ARR0 LT0 JOB0.
+ apply completion_monotonic with (t := job_arrival j0 + R tsk_i);
+ [by done | | by apply BEFOREok; rewrite // -JOBtsk].
+ by rewrite leq_add2l H_job_deadline_eq_task_deadline // JOB0 JOBtsk.
+ }
+ {
+ apply RESPi with (job_jitter := job_jitter); try (by done);
+ last by eapply reduction_prop.sched_jitter_is_valid; eauto 1.
+ repeat split; intros j' ARR.
+ - by eapply ts_membership_inflated_job_cost_positive; eauto 1.
+ - by eapply ts_membership_inflated_job_cost_le_inflated_task_cost;
+ eauto 1.
+ - by eapply ts_membership_job_jitter_le_task_jitter; eauto 1.
+ }
+ Qed.
+
+ End PerTaskAnalysis.
+
+End TaskSetRTA.
\ No newline at end of file
diff --git a/analysis/uni/susp/dynamic/oblivious/fp_rta.v b/analysis/uni/susp/dynamic/oblivious/fp_rta.v
index 6aba2b662..d6c9c4943 100644
--- a/analysis/uni/susp/dynamic/oblivious/fp_rta.v
+++ b/analysis/uni/susp/dynamic/oblivious/fp_rta.v
@@ -39,7 +39,7 @@ Module SuspensionObliviousFP.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
- (* Next, consider any job arrival sequence with consistent, non-duplicate arrivals,... *)
+ (* Next, consider any job arrival sequence with consistent, duplicate-free arrivals,... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
diff --git a/analysis/uni/susp/sustainability/allcosts/reduction.v b/analysis/uni/susp/sustainability/allcosts/reduction.v
new file mode 100644
index 000000000..220ee451a
--- /dev/null
+++ b/analysis/uni/susp/sustainability/allcosts/reduction.v
@@ -0,0 +1,165 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.schedule.uni.susp.schedule
+ rt.model.schedule.uni.susp.platform
+ rt.model.schedule.uni.susp.build_suspension_table.
+Require Import rt.model.schedule.uni.transformation.construction.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq bigop fintype.
+
+(* In this file, we prove that uniprocessor suspension-aware scheduling is
+ sustainable with job costs under the dynamic suspension model. *)
+Module SustainabilityAllCosts.
+
+ Import ScheduleWithSuspensions Suspension Priority PlatformWithSuspensions
+ ScheduleConstruction SuspensionTableConstruction.
+
+ Section Reduction.
+
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_cost: Job -> time.
+
+ (** Basic Setup & Setting *)
+
+ (* Consider any job arrival sequence... *)
+ Variable arr_seq: arrival_sequence Job.
+
+ (* ...and assume any (schedule-independent) job-level priorities. *)
+ Variable higher_eq_priority: JLDP_policy Job.
+
+ (* Next, consider any suspension-aware schedule of the arrival sequence... *)
+ Variable sched_susp: schedule Job.
+
+ (* ...and the associated job suspension durations. *)
+ Variable job_suspension_duration: job_suspension Job.
+
+ (** Definition of the Reduction *)
+
+ (* Now we proceed with the reduction.
+ Let inflated_job_cost denote any job cost inflation, i.e., the cost of
+ every job is as large as in the original schedule. *)
+ Variable inflated_job_cost: Job -> time.
+
+ (* To simplify the analysis, instead of observing an infinite schedule, we
+ focus on the finite window delimited by the job we want to analyze.
+ Let's call this job j, with arrival time arr_j, ... *)
+ Variable j: Job.
+ Let arr_j := job_arrival j.
+
+ (* ...and suppose that we want to prove that the response time of j in sched_susp
+ is upper-bounded by some value R.
+ In the analysis, we only need to focus on the schedule prefix [0, arr_j + R). *)
+ Variable R: time.
+
+ (* In this sustainability proof, we must construct a new schedule with the inflated
+ job costs that is no "better" for job j than the original schedule.
+ Since we also modify the suspension durations, the construction is divided in
+ two parts: (A) Schedule Construction, and (B) Definition of Suspension Times. *)
+
+ (** (A) Schedule Construction *)
+ Section ScheduleConstruction.
+
+ (* Let's begin by defining the schedule construction function. *)
+ Section ConstructionStep.
+
+ (* For any time t, suppose that we have generated the schedule prefix [0, t).
+ Then, we must define what should be scheduled at time t. *)
+ Variable sched_prefix: schedule Job.
+ Variable t: time.
+
+ (* Consider the set of jobs that arrived up to time t. *)
+ Let arrivals := jobs_arrived_up_to arr_seq t.
+
+ (* Recall whether a job is pending in the new schedule. *)
+ Let job_is_pending := pending job_arrival inflated_job_cost sched_prefix.
+
+ (* Also, let's denote as late any job whose service in the new schedule is strictly
+ less than the service in sched_susp plus the difference between job costs. *)
+ Definition job_is_late any_j t :=
+ service sched_prefix any_j t
+ < service sched_susp any_j t + (inflated_job_cost any_j - job_cost any_j).
+
+ (* In order not to have to prove complex properties about the entire schedule,
+ we split the construction for the schedule prefix [0, arr_j + R) and for the
+ suffix [arr_j + R, ...). *)
+
+ (** (A.1) The prefix is built in a way that prevents jobs from getting late. *)
+ Section Prefix.
+
+ (* Consider the list of pending jobs in the new schedule that are either late
+ or scheduled in sched_susp.
+ (Note that when there are no late jobs, we pick the jobs that are scheduled
+ in sched_susp so that the suspension times remain consistent.) *)
+ Definition jobs_that_are_late_or_scheduled_in_sched_susp :=
+ [seq any_j <- arrivals | job_is_pending any_j t &&
+ (job_is_late any_j t || scheduled_at sched_susp any_j t)].
+
+ (* From that list, we take one of the (possibly many) highest-priority jobs,
+ or None, in case there are no late jobs and sched_susp is idle. *)
+ Definition highest_priority_late_job :=
+ seq_min (higher_eq_priority t) jobs_that_are_late_or_scheduled_in_sched_susp.
+
+ End Prefix.
+
+ (** (A.2) In the suffix, we just pick the highest-priority pending job
+ so that the schedule constraints are satisfied. *)
+ Section Suffix.
+
+ (* From the list of pending jobs in the new schedule, ... *)
+ Definition pending_jobs :=
+ [seq any_j <- arrivals | job_is_pending any_j t ].
+
+ (* ...let's take one of the (possibly many) highest-priority jobs. *)
+ Definition highest_priority_job :=
+ seq_min (higher_eq_priority t) pending_jobs.
+
+ End Suffix.
+
+ (** (A.3) In the end, we just combine the prefix and suffix schedules. *)
+ Definition build_schedule :=
+ if t < arr_j + R then
+ highest_priority_late_job (* PREFIX (see A.1) *)
+ else
+ highest_priority_job. (* SUFFIX (see A.2) *)
+
+ End ConstructionStep.
+
+ (* To conclude, starting from the empty schedule, ...*)
+ Let empty_schedule : schedule Job := fun t => None.
+
+ (* ...we use the recursive definition above to construct the new schedule. *)
+ Definition sched_new :=
+ build_schedule_from_prefixes build_schedule empty_schedule.
+
+ End ScheduleConstruction.
+
+ (** (B) Definition of Suspension Times *)
+
+ (* Having decided when jobs should be scheduled, we now define when they should suspend
+ so that the schedule properties remain consistent. *)
+ Section DefiningSuspension.
+
+ (* Recall the definition of a suspended job in sched_susp. *)
+ Let job_is_suspended_in_sched_susp :=
+ suspended_at job_arrival job_cost job_suspension_duration sched_susp.
+
+ (* Based on the notion of a "late" job from the schedule construction, we say that a
+ job is suspended at time t in sched_new iff:
+ (a) time t precedes arr_j + R (i.e., suspensions only occur in the prefix),
+ (b) the job is suspended in sched_susp at time t, and
+ (c) the job is not late in sched_new at time t. *)
+ Definition suspended_in_sched_new (any_j: Job) (t: time) :=
+ (t < arr_j + R) && job_is_suspended_in_sched_susp any_j t
+ && ~~ job_is_late sched_new any_j t.
+
+ (* Next, using this suspension predicate, we build a table of suspension durations
+ that is valid up to time (arr_j + R).
+ For more details, see model/schedule/uni/susp/build_suspension_table. *)
+ Definition reduced_suspension_duration :=
+ build_suspension_duration sched_new (arr_j + R) suspended_in_sched_new.
+
+ End DefiningSuspension.
+
+ End Reduction.
+
+End SustainabilityAllCosts.
\ No newline at end of file
diff --git a/analysis/uni/susp/sustainability/allcosts/reduction_properties.v b/analysis/uni/susp/sustainability/allcosts/reduction_properties.v
new file mode 100644
index 000000000..506e5b834
--- /dev/null
+++ b/analysis/uni/susp/sustainability/allcosts/reduction_properties.v
@@ -0,0 +1,891 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.susp.suspension_intervals
+ rt.model.schedule.uni.susp.schedule
+ rt.model.schedule.uni.susp.valid_schedule
+ rt.model.schedule.uni.susp.build_suspension_table
+ rt.model.schedule.uni.susp.platform.
+Require Import rt.analysis.uni.susp.sustainability.allcosts.reduction.
+Require Import rt.model.schedule.uni.transformation.construction.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(* In this file, we prove several properties about the schedule we constructed
+ in the sustainability proof. *)
+Module SustainabilityAllCostsProperties.
+
+ Import ScheduleWithSuspensions Suspension Priority SuspensionIntervals
+ PlatformWithSuspensions ResponseTime ScheduleConstruction
+ SuspensionTableConstruction ValidSuspensionAwareSchedule.
+
+ Module reduction := SustainabilityAllCosts.
+
+ Section ReductionProperties.
+
+ Context {Task: eqType}.
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_cost: Job -> time.
+
+ (** Basic Setup & Setting*)
+
+ (* Consider any job arrival sequence with consistent job arrivals. *)
+ Variable arr_seq: arrival_sequence Job.
+ Hypothesis H_arrival_times_are_consistent:
+ arrival_times_are_consistent job_arrival arr_seq.
+
+ (* Assume any (schedule-independent) 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.
+
+ (* Next, consider any suspension-aware schedule of the arrival sequence... *)
+ Variable sched_susp: schedule Job.
+ Hypothesis H_jobs_come_from_arrival_sequence:
+ jobs_come_from_arrival_sequence sched_susp arr_seq.
+
+ (* ...and the associated job suspension times. *)
+ Variable job_suspension_duration: job_suspension Job.
+
+ (* Assume that, in this schedule, 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 job_cost sched_susp.
+
+ (* Also assume that the schedule is work-conserving if there are non-suspended jobs, ... *)
+ Hypothesis H_work_conserving:
+ work_conserving job_arrival job_cost job_suspension_duration arr_seq sched_susp.
+
+ (* ...that the schedule respects job priorities... *)
+ Hypothesis H_respects_priority:
+ respects_JLDP_policy job_arrival job_cost job_suspension_duration 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 job_cost job_suspension_duration sched_susp.
+
+ (** Reduction Setup *)
+
+ (* Now we prove properties about the reduction.
+ Let j be the job to be analyzed with arrival time arr_j. *)
+ Variable j: Job.
+ Let arr_j := job_arrival j.
+
+ (* Suppose that we want to prove that the response time of job j in sched_susp
+ is upper-bounded by some value R. This allows us to restrict our analysis
+ to the finite scheduling window [0, arr_j + R) during the reduction. *)
+ Variable R: time.
+
+ (* Next, consider any job cost inflation... *)
+ Variable inflated_job_cost: Job -> time.
+
+ (* ...in which the cost of every job is no less than in the original schedule. *)
+ Hypothesis H_job_costs_do_not_decrease:
+ forall any_j, inflated_job_cost any_j >= job_cost any_j.
+
+ (* Recall the schedule we constructed from sched_susp using these inflated costs. *)
+ Let sched_new := reduction.sched_new job_arrival job_cost arr_seq higher_eq_priority
+ sched_susp inflated_job_cost j R.
+
+ (* Also recall the predicate we defined for a suspended job in the new schedule... *)
+ Let suspended_in_sched_new :=
+ reduction.suspended_in_sched_new job_arrival job_cost arr_seq higher_eq_priority
+ sched_susp job_suspension_duration inflated_job_cost j R.
+
+ (* ...and the corresponding suspension table. *)
+ Let reduced_suspension_duration :=
+ reduction.reduced_suspension_duration job_arrival job_cost arr_seq higher_eq_priority
+ sched_susp job_suspension_duration inflated_job_cost j R.
+
+ (* For simplicity, let's define some local names. *)
+ Let job_response_time_in_sched_susp_bounded_by :=
+ is_response_time_bound_of_job job_arrival job_cost sched_susp.
+ Let job_response_time_in_sched_new_bounded_by :=
+ is_response_time_bound_of_job job_arrival inflated_job_cost sched_new.
+ Let suspended_in_sched_susp :=
+ suspended_at job_arrival job_cost job_suspension_duration sched_susp.
+ Let job_is_late := reduction.job_is_late job_cost sched_susp inflated_job_cost sched_new.
+ Let build_schedule := reduction.build_schedule job_arrival job_cost arr_seq higher_eq_priority
+ sched_susp inflated_job_cost j R.
+ Let late_or_sched_jobs := reduction.jobs_that_are_late_or_scheduled_in_sched_susp
+ job_arrival job_cost arr_seq sched_susp inflated_job_cost sched_new.
+ Let hp_job := reduction.highest_priority_job job_arrival arr_seq higher_eq_priority
+ inflated_job_cost sched_new.
+ Let hp_late_job := reduction.highest_priority_late_job job_arrival job_cost arr_seq
+ higher_eq_priority sched_susp inflated_job_cost sched_new.
+ Let completed_in_sched_susp := completed_by job_cost sched_susp.
+ Let completed_in_sched_new := completed_by inflated_job_cost sched_new.
+
+ (** Properties of the Schedule Construction *)
+
+ (* In this section, we prove that the new schedule is equivalent to its construction function. *)
+ Section PropertiesOfScheduleConstruction.
+
+ (* By showing that the construction function depends only on the service, ... *)
+ Lemma sched_new_depends_only_on_service:
+ forall sched1 sched2 t,
+ (forall j, service sched1 j t = service sched2 j t) ->
+ build_schedule sched1 t = build_schedule sched2 t.
+ Proof.
+ intros sched1 sched2 t SAME.
+ rewrite /build_schedule /reduction.build_schedule.
+ case: (_ < _).
+ {
+ rewrite /reduction.highest_priority_late_job; f_equal.
+ apply eq_in_filter; intros j0 IN0; f_equal;
+ first by rewrite /pending /completed_by SAME.
+ by f_equal; rewrite /reduction.job_is_late SAME.
+ }
+ {
+ rewrite /reduction.highest_priority_job; f_equal.
+ apply eq_in_filter; intros j0 IN0.
+ by rewrite /pending /completed_by SAME.
+ }
+ Qed.
+
+ (* ...we infer that the new schedule is equivalent to the construction function. *)
+ Corollary sched_new_uses_construction_function:
+ forall t,
+ sched_new t = build_schedule sched_new t.
+ Proof.
+ by ins; apply service_dependent_schedule_construction,
+ sched_new_depends_only_on_service.
+ Qed.
+
+ End PropertiesOfScheduleConstruction.
+
+ (** Basic Properties of the Generated Schedule *)
+
+ (* In this section, we prove some properties about the generated schedule that
+ only depend on the construction function but not on suspension times. *)
+ Section BasicScheduleProperties.
+
+ (* First, we show that scheduled jobs come from the arrival sequence. *)
+ Lemma sched_new_jobs_come_from_arrival_sequence:
+ jobs_come_from_arrival_sequence sched_new arr_seq.
+ Proof.
+ move => j0 t /eqP SCHEDn.
+ rewrite /scheduled_at sched_new_uses_construction_function in SCHEDn.
+ rewrite /build_schedule /reduction.build_schedule in SCHEDn.
+ case (ltnP t (arr_j + R)) => [LT | GE].
+ {
+ rewrite LT /reduction.highest_priority_late_job in SCHEDn;
+ apply seq_min_in_seq in SCHEDn.
+ rewrite mem_filter in SCHEDn.
+ move: SCHEDn => /andP [_ IN].
+ by eapply in_arrivals_implies_arrived; eauto 1.
+ }
+ {
+ rewrite ltnNge GE /= in SCHEDn.
+ rewrite /reduction.highest_priority_job in SCHEDn; apply seq_min_in_seq in SCHEDn.
+ rewrite mem_filter in SCHEDn.
+ move: SCHEDn => /andP [_ IN].
+ by eapply in_arrivals_implies_arrived; eauto 1.
+ }
+ Qed.
+
+ (* 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.
+ Proof.
+ move => j0 t /eqP SCHEDn.
+ rewrite /scheduled_at sched_new_uses_construction_function in SCHEDn.
+ rewrite /build_schedule /reduction.build_schedule in SCHEDn.
+ case (ltnP t (arr_j + R)) => [LT | GE].
+ {
+ rewrite LT /reduction.highest_priority_late_job in SCHEDn;
+ apply seq_min_in_seq in SCHEDn.
+ rewrite mem_filter in SCHEDn.
+ by move: SCHEDn => /andP [/andP [/andP [ARR _] _] _].
+ }
+ {
+ rewrite ltnNge GE /= in SCHEDn.
+ rewrite /reduction.highest_priority_job in SCHEDn; apply seq_min_in_seq in SCHEDn.
+ rewrite mem_filter in SCHEDn.
+ by move: SCHEDn => /andP [/andP [ARR _] _].
+ }
+ Qed.
+
+ (* ...nor longer than their execution costs. *)
+ Lemma sched_new_completed_jobs_dont_execute:
+ completed_jobs_dont_execute inflated_job_cost sched_new.
+ Proof.
+ intros j0 t.
+ induction t;
+ first by rewrite /service /service_during big_geq //.
+ rewrite /service /service_during big_nat_recr //=.
+ rewrite leq_eqVlt in IHt; move: IHt => /orP [/eqP EQ | LT]; last first.
+ {
+ apply: leq_trans LT; rewrite -addn1.
+ by apply leq_add; last by apply leq_b1.
+ }
+ rewrite -[inflated_job_cost _]addn0; apply leq_add; first by rewrite -EQ.
+ rewrite leqn0 eqb0 /scheduled_at.
+ rewrite sched_new_uses_construction_function /build_schedule
+ /reduction.build_schedule.
+ case: (_ < _); rewrite /reduction.highest_priority_job
+ /reduction.highest_priority_late_job.
+ {
+ apply/eqP; intro SCHEDn.
+ apply seq_min_in_seq in SCHEDn.
+ rewrite mem_filter in SCHEDn.
+ move: SCHEDn => /andP [/andP [/andP [_ NOTCOMP] _] _].
+ by rewrite /completed_by EQ eq_refl in NOTCOMP.
+ }
+ {
+ apply/eqP; intro SCHEDn.
+ apply seq_min_in_seq in SCHEDn.
+ rewrite mem_filter in SCHEDn.
+ move: SCHEDn => /andP [/andP [_ NOTCOMP] _].
+ by rewrite /completed_by EQ eq_refl in NOTCOMP.
+ }
+ Qed.
+
+ End BasicScheduleProperties.
+
+ (** Service Invariants *)
+
+ (* In this section, we prove some service invariants guaranteed by the new schedule
+ up to time (arr_j + R).
+ Note that these properties follow directly from the schedule construction and
+ do not depend on suspension times. *)
+ Section ServiceInvariant.
+
+ (* Let t be any time in the interval [0, arr_j + R]. *)
+ Variable t: time.
+ Hypothesis H_before_R: t <= arr_j + R.
+
+ (* By induction on time, we prove that for any job, the service received up to
+ time t in the new schedule is no more than the service received up to time t in
+ the original schedule, plus the difference between job costs due to inflation. *)
+ Lemma sched_new_service_invariant:
+ forall any_j,
+ service sched_new any_j t
+ <= service sched_susp any_j t + (inflated_job_cost any_j - job_cost any_j).
+ Proof.
+ rename H_priority_is_total into TOTAL, H_priority_is_transitive into TRANS,
+ H_respects_priority into PRIO, H_work_conserving into WORK.
+ rename t into t', H_before_R into BEFORE.
+ move: t' BEFORE.
+ induction t';
+ first by intros _ j0; rewrite /service /service_during big_geq.
+ intros LTr; feed IHt'; first by apply ltnW.
+ intros j0.
+ case (boolP (scheduled_at sched_new j0 t')) => [SCHEDn| NOTSCHEDn]; last first.
+ {
+ apply negbTE in NOTSCHEDn.
+ rewrite /service /service_during big_nat_recr //=.
+ rewrite /service_at NOTSCHEDn addn0.
+ apply: (leq_trans (IHt' j0)).
+ by rewrite leq_add2r extend_sum.
+ }
+ move: (SCHEDn) => IN.
+ rewrite /scheduled_at sched_new_uses_construction_function in IN.
+ rewrite /build_schedule /reduction.build_schedule LTr in IN; move: IN => /eqP IN.
+ rewrite /reduction.highest_priority_late_job in IN.
+ apply seq_min_in_seq in IN; rewrite mem_filter in IN.
+ move: IN => /andP [/andP [PEND OR] IN].
+ move: OR => /orP [LT | SCHEDs].
+ {
+ apply leq_trans with (n := service sched_new j0 t' + 1);
+ first by rewrite /service/service_during big_nat_recr // leq_add ?leq_b1.
+ rewrite addn1.
+ by apply: (leq_trans LT); rewrite leq_add2r extend_sum.
+ }
+ {
+ rewrite /service /service_during big_nat_recr // big_nat_recr //=.
+ rewrite /service_at SCHEDn SCHEDs -addnA [1 + _]addnC addnA leq_add2r.
+ by apply IHt'.
+ }
+ Qed.
+
+ (* From the previous lemma, we conclude that any job that completes in the new
+ schedule up to time t must have completed in the original schedule as well. *)
+ Corollary sched_new_jobs_complete_later:
+ forall any_j,
+ completed_by inflated_job_cost sched_new any_j t ->
+ completed_by job_cost sched_susp any_j t.
+ Proof.
+ intros j0 COMPn.
+ rewrite /completed_by eqn_leq; apply/andP; split;
+ first by apply cumulative_service_le_job_cost.
+ rewrite -(leq_add2r (inflated_job_cost j0 - job_cost j0)).
+ rewrite subnKC; last by eauto 1.
+ move: COMPn => /eqP {1}<-.
+ by apply sched_new_service_invariant.
+ Qed.
+
+ End ServiceInvariant.
+
+ (** Properties of the Suspension Predicate *)
+
+ (* In order to prove schedule properties that depend on suspension times, we first
+ prove some facts about the suspension predicate we defined. *)
+ Section SuspensionPredicate.
+
+ (* Let any_j be any job. *)
+ Variable any_j: Job.
+
+ (* First, we show that if the suspension predicate holds for any_j at time t,
+ then any_j must have arrived... *)
+ Lemma suspended_in_sched_new_implies_arrived:
+ forall t,
+ suspended_in_sched_new any_j t -> has_arrived job_arrival any_j t.
+ Proof.
+ rename any_j into j0.
+ move => t /andP [/andP [LT SUSPs] _].
+ by eapply suspended_implies_arrived; eauto 1.
+ Qed.
+
+ (* ...and cannot have completed. *)
+ Lemma suspended_in_sched_new_implies_not_completed:
+ forall t,
+ suspended_in_sched_new any_j t -> ~~ completed_in_sched_new any_j t.
+ Proof.
+ rename any_j into j0.
+ move => t /andP [/andP [LT SUSPs] _].
+ apply/negP; intro COMPn.
+ apply suspended_implies_not_completed in SUSPs.
+ apply sched_new_jobs_complete_later in COMPn; last by apply ltnW.
+ by rewrite COMPn in SUSPs.
+ Qed.
+
+ (* Next, we show that if the suspension predicate changes from false at time t
+ to true at time (t + 1), then any_j must be scheduled at time t. *)
+ Lemma executes_before_suspension_in_sched_new:
+ forall t,
+ t < arr_j + R ->
+ has_arrived job_arrival any_j t ->
+ ~~ suspended_in_sched_new any_j t ->
+ suspended_in_sched_new any_j t.+1 ->
+ scheduled_at sched_new any_j t.
+ Proof.
+ rename any_j into j0.
+ intros t LTr ARR NOTSUSPn SUSPn'.
+ rewrite negb_and LTr /= negbK -/suspended_in_sched_susp -/job_is_late in NOTSUSPn.
+ move: NOTSUSPn => /orP [NOTSUSPs | LATE]; last first.
+ {
+ apply contraT; intro NOTSCHEDn.
+ move: SUSPn' => /andP [_ NOTLATE].
+ rewrite /job_is_late /reduction.job_is_late -leqNgt -/sched_new in LATE NOTLATE.
+ have GT: service sched_new j0 t < service sched_new j0 t.+1.
+ {
+ apply: (leq_trans LATE); apply: (leq_trans _ NOTLATE).
+ by rewrite leq_add2r extend_sum.
+ }
+ rewrite /service/service_during big_nat_recr// -addn1 leq_add2l in GT.
+ rewrite lt0n eqb0 negbK in GT.
+ by rewrite GT in NOTSCHEDn.
+ }
+ move: (SUSPn') => /andP [/andP [_ SUSPs'] NOTLATE'].
+ rewrite -/suspended_in_sched_susp in SUSPs'.
+ rewrite /reduction.job_is_late -/sched_new -leqNgt in NOTLATE'.
+ apply contraT; intro NOTSCHEDn.
+ have SAME: service sched_new j0 t.+1 = service sched_new j0 t.
+ {
+ apply negbTE in NOTSCHEDn.
+ by rewrite /service /service_during big_nat_recr //= /service_at NOTSCHEDn.
+ }
+ rewrite SAME {SAME} in NOTLATE'.
+ have INV := sched_new_service_invariant t (ltnW LTr) j0.
+ have SCHEDs: ~~ scheduled_at sched_susp j0 t.
+ {
+ apply contraT; rewrite negbK; intro SCHEDs.
+ have BUG: service sched_susp j0 t + 1 <= service sched_susp j0 t.
+ {
+ rewrite -(leq_add2r (inflated_job_cost j0 - job_cost j0)).
+ apply: (leq_trans _ INV); apply: (leq_trans _ NOTLATE').
+ rewrite leq_add2r.
+ by rewrite /service /service_during big_nat_recr //= /service_at SCHEDs.
+ }
+ by rewrite addn1 ltnn in BUG.
+ }
+ suff BUG: scheduled_at sched_susp j0 t by rewrite BUG in SCHEDs.
+ by eapply executes_before_suspension; eauto 1.
+ Qed.
+
+ (* For simplicity, let's call suspension_start the time following the last
+ execution of a job. *)
+ Let suspension_start := time_after_last_execution job_arrival.
+
+ (* Then, we prove that if any_j is suspended at time t, it does not receive
+ any service between time t and the previous beginning of suspension. *)
+ Lemma suspended_in_sched_new_no_service_since_execution:
+ forall t t_mid,
+ suspended_in_sched_new any_j t ->
+ suspension_start sched_new any_j t <= t_mid < t ->
+ service sched_new any_j t <= service sched_new any_j t_mid.
+ Proof.
+ have BEFORE := executes_before_suspension_in_sched_new.
+ rename any_j into j0.
+ induction t; first by intros t_susp _; rewrite ltn0 andbF.
+ move => t_mid SUSPn' /andP [GE LT].
+ move: (SUSPn') => /andP [/andP [LTr' SUSPs'] _].
+ have LTr: t < arr_j + R by apply: (ltn_trans _ LTr').
+ have ARR: has_arrived job_arrival j0 t.+1.
+ by apply suspended_implies_arrived in SUSPs'.
+ rewrite /has_arrived leq_eqVlt in ARR; move: ARR => /orP [/eqP EQ | ARR].
+ {
+ rewrite /service /service_during.
+ rewrite (cumulative_service_before_job_arrival_zero job_arrival) ?EQ //.
+ by apply sched_new_jobs_must_arrive_to_execute.
+ }
+ case (boolP (scheduled_at sched_new j0 t)) => [SCHEDn | NOTSCHEDn]; last first.
+ {
+ apply leq_trans with (n := service sched_new j0 t).
+ {
+ apply negbTE in NOTSCHEDn; rewrite /service/service_during.
+ by rewrite big_nat_recr //= /service_at NOTSCHEDn addn0.
+ }
+ case (boolP (t_mid == t)) => [/eqP EQ | DIFF]; first by subst.
+ apply IHt.
+ {
+ apply contraT; intro NOTSUSPn.
+ suff SCHEDn: scheduled_at sched_new j0 t by rewrite SCHEDn in NOTSCHEDn.
+ by apply BEFORE.
+ }
+ apply/andP; split.
+ {
+ apply: (leq_trans _ GE); apply last_execution_monotonic; last by done.
+ by apply sched_new_jobs_must_arrive_to_execute.
+ }
+ by rewrite ltn_neqAle -ltnS LT andbT.
+ }
+ set start := suspension_start sched_new.
+ apply leq_trans with (n := service sched_new j0 (start j0 t.+1));
+ last by apply extend_sum.
+ apply extend_sum; first by done.
+ rewrite /start /suspension_start /time_after_last_execution.
+ have EX: [exists t0:'I_t.+1, scheduled_at sched_new j0 t0].
+ by apply/existsP; exists (Ordinal (ltnSn t)).
+ rewrite EX -addn1 leq_add2r addn1.
+ have GEt := @leq_bigmax_cond _ (fun x:'I_t.+1 => scheduled_at sched_new j0 x)
+ id (Ordinal (ltnSn t)).
+ by apply GEt.
+ Qed.
+
+ (* Next, we prove that if the suspension predicate holds for any_j at time t,
+ then the latest execution of any_j in the new schedule is no earlier than
+ its latest execution in the original schedule. *)
+ Lemma suspended_in_sched_new_suspension_starts_no_earlier:
+ forall t,
+ has_arrived job_arrival any_j t ->
+ suspended_in_sched_new any_j t ->
+ suspension_start sched_susp any_j t <= suspension_start sched_new any_j t.
+ Proof.
+ have BEFORE := executes_before_suspension_in_sched_new.
+ rename any_j into j0.
+ induction t.
+ {
+ intros ARR SUSPs; apply leq_trans with (n := 0); last by done.
+ rewrite /suspension_start /time_after_last_execution.
+ have NOTEX: [exists t0: 'I_0, scheduled_at sched_susp j0 t0] = false.
+ by apply negbTE; rewrite negb_exists; apply/forallP; intros [x LT0].
+ by rewrite NOTEX {NOTEX}.
+ }
+ {
+ intros ARR SUSPn'.
+ move: (SUSPn') => /andP [/andP [LTr _] _].
+ have LTr': t < arr_j + R by apply: (ltn_trans _ LTr).
+ rewrite /has_arrived leq_eqVlt in ARR; move: ARR => /orP [/eqP EQ | ARR].
+ {
+ have LAST := last_execution_after_arrival.
+ rewrite /suspension_start /has_arrived in LAST *.
+ apply leq_trans with (n := job_arrival j0);
+ last by apply LAST, sched_new_jobs_must_arrive_to_execute.
+ rewrite /time_after_last_execution.
+ suff NOTEX: [exists t0: 'I_t.+1, scheduled_at sched_susp j0 t0] = false
+ by rewrite NOTEX.
+ apply negbTE; rewrite negb_exists; apply/forallP; intros t0.
+ apply/negP; intro SCHED0.
+ apply H_jobs_must_arrive_to_execute in SCHED0.
+ suff BUG: t0 < t0 by rewrite ltnn in BUG.
+ by apply: (leq_trans _ SCHED0); rewrite EQ.
+ }
+ rewrite ltnS in ARR.
+ case (boolP (suspended_in_sched_new j0 t)) => [SUSPn | NOTSUSPn].
+ {
+ apply leq_trans with (n := suspension_start sched_new j0 t); last first.
+ {
+ apply last_execution_monotonic; last by done.
+ by apply sched_new_jobs_must_arrive_to_execute.
+ }
+ apply leq_trans with (n := suspension_start sched_susp j0 t); [|by apply IHt].
+ apply eq_leq, same_service_implies_same_last_execution.
+ rewrite /service /service_during big_nat_recr //= /service_at.
+ case (boolP (scheduled_at sched_susp j0 t)); last by done.
+ intros SCHEDs; apply H_respects_self_suspensions in SCHEDs.
+ by move: SUSPn => /andP [/andP [_ SUSPs] _].
+ }
+ move: (SUSPn') => /andP [/andP [_ SUSPs']] _.
+ have SCHEDn := BEFORE t LTr' ARR NOTSUSPn SUSPn'.
+ apply leq_trans with (n := t.+1);
+ first by move: SUSPs' => /andP [_ /andP [LE _]].
+ rewrite /suspension_start /time_after_last_execution.
+ have EX: [exists t0:'I_t.+1, scheduled_at sched_new j0 t0].
+ by apply/existsP; exists (Ordinal (ltnSn t)).
+ rewrite EX -addn1 leq_add2r addn1.
+ have GE := @leq_bigmax_cond _ (fun x:'I_t.+1 => scheduled_at sched_new j0 x)
+ id (Ordinal (ltnSn t)).
+ by apply GE.
+ }
+ Qed.
+
+ (* using the previous lemmas, we conclude that the suspension predicate is continuous
+ between any suspension point and the last execution of the job. *)
+ Lemma suspended_in_sched_new_is_continuous:
+ forall t t_mid,
+ suspended_in_sched_new any_j t ->
+ suspension_start sched_new any_j t <= t_mid < t ->
+ suspended_in_sched_new any_j t_mid.
+ Proof.
+ have NOSERV := suspended_in_sched_new_no_service_since_execution.
+ have NOEARLIER := suspended_in_sched_new_suspension_starts_no_earlier.
+ rename any_j into j0; intros t.
+ induction t_mid as [k IH] using strong_ind.
+ have INV := sched_new_service_invariant.
+ move => SUSPn /andP [GE LT].
+ move: (SUSPn) => /andP [/andP [LTr SUSPt] NOTLATEt].
+ rewrite -/job_is_late in NOTLATEt.
+ apply/andP; split; last first.
+ {
+ rewrite /reduction.job_is_late -/sched_new -2!leqNgt in NOTLATEt *.
+ feed (INV t); [by apply ltnW | specialize (INV j0)].
+ set Sn := service sched_new in INV NOTLATEt *.
+ set Ss := service sched_susp in INV NOTLATEt *.
+ set cost0 := job_cost j0 in INV NOTLATEt *.
+ set cost0' := inflated_job_cost j0 in INV NOTLATEt *.
+ have SAME: Sn j0 t = Ss j0 t + (cost0' - cost0).
+ by apply/eqP; rewrite eqn_leq; apply/andP.
+ clear INV.
+ apply leq_trans with (n := Ss j0 t + (cost0' - cost0));
+ first by rewrite leq_add2r; apply extend_sum; last by apply ltnW.
+ rewrite -SAME {SAME}.
+ by apply NOSERV; rewrite ?SUSPn ?LTr ?SUSPt ?GE ?LT.
+ }
+ apply/andP; split; first by apply: (ltn_trans _ LTr).
+ apply suspended_in_suspension_interval with (t0 := t); try done.
+ {
+ apply/negP; intro COMPmid.
+ apply suspended_implies_not_completed in SUSPt.
+ suff BUG: completed_by job_cost sched_susp j0 t by rewrite BUG in SUSPt.
+ by apply completion_monotonic with (t0 := k); [| by apply ltnW |].
+ }
+ apply/andP; split;
+ last by apply: (ltn_trans LT); move: SUSPt => /andP [_ /andP [_ GTt]].
+ apply: (leq_trans _ GE).
+ apply NOEARLIER; try done.
+ by apply suspended_implies_arrived in SUSPt.
+ Qed.
+
+ End SuspensionPredicate.
+
+ (** Properties of the Suspension Table *)
+
+ (* In this section, we prove some properties about the suspension table. *)
+ Section SuspensionTable.
+
+ (* First, we show that no job ever suspends after (arr_j + R). *)
+ Lemma suspended_in_sched_new_only_inside_window:
+ forall any_j t,
+ arr_j + R <= t ->
+ ~~ suspended_at job_arrival inflated_job_cost reduced_suspension_duration
+ sched_new any_j t.
+ Proof.
+ intros any_j t LE.
+ case (boolP (has_arrived job_arrival any_j t)) => [ARR | NOTARR]; last first.
+ {
+ apply/negP; intro SUSP.
+ apply suspended_implies_arrived in SUSP;
+ last by apply sched_new_jobs_must_arrive_to_execute.
+ by rewrite SUSP in NOTARR.
+ }
+ apply suspension_duration_no_suspension_after_t_max; try done;
+ first by apply sched_new_jobs_must_arrive_to_execute.
+ intros j0 t0 LT.
+ rewrite /reduction.suspended_in_sched_new LT /=.
+ move => /andP [SUSPs _].
+ by apply suspended_implies_arrived in SUSPs.
+ Qed.
+
+ (* Next, using the lemmas about the suspension predicate, we show that the suspension
+ predicate for the new schedule matches the generated suspension table.
+ (see model/schedule/uni/susp/build_suspension_table.v) *)
+ Lemma sched_new_suspension_matches:
+ forall any_j t,
+ t < arr_j + R ->
+ suspended_in_sched_new any_j t =
+ suspended_at job_arrival inflated_job_cost reduced_suspension_duration sched_new any_j t.
+ Proof.
+ apply suspension_duration_matches_predicate_up_to_t_max;
+ first by apply sched_new_jobs_must_arrive_to_execute.
+ - by intros j0 t LT SUSP; apply suspended_in_sched_new_implies_arrived.
+ - by intros j0 t LT SUSP; apply suspended_in_sched_new_implies_not_completed.
+ - by intros j0 t LT SUSP; apply suspended_in_sched_new_is_continuous.
+ Qed.
+
+ (* Recall the definition of cumulative suspension in both schedules. *)
+ Let cumulative_suspension_in_sched_susp :=
+ cumulative_suspension job_arrival job_cost job_suspension_duration sched_susp.
+ Let cumulative_suspension_in_sched_new :=
+ cumulative_suspension job_arrival inflated_job_cost reduced_suspension_duration sched_new.
+
+ (* To conclude, we prove that the suspension durations in the new schedule are no
+ longer than in the original schedule. *)
+ Lemma sched_new_has_shorter_suspensions:
+ forall any_j t,
+ cumulative_suspension_in_sched_new any_j t
+ <= cumulative_suspension_in_sched_susp any_j t.
+ Proof.
+ intros j0 t.
+ apply leq_sum; intros i _.
+ case (ltnP i (arr_j + R)) => [LTr | GEr].
+ {
+ rewrite -sched_new_suspension_matches //.
+ rewrite /suspended_in_sched_new /reduction.suspended_in_sched_new.
+ rewrite LTr /=.
+ by case: (X in (_ && X)); rewrite ?andbT ?andbF.
+ }
+ {
+ apply leq_trans with (n := 0); last by done.
+ rewrite leqn0 eqb0.
+ case (boolP (has_arrived job_arrival j0 i)) => [ARR | NOTARR];
+ first by apply suspended_in_sched_new_only_inside_window.
+ apply/negP; intro SUSPn.
+ apply suspended_implies_arrived in SUSPn; first by rewrite SUSPn in NOTARR.
+ by apply sched_new_jobs_must_arrive_to_execute.
+ }
+ Qed.
+
+ End SuspensionTable.
+
+ (** Suspension-Related Schedule Properties *)
+
+ (* Having shown that the suspension table matches the suspension predicate,
+ we now analyze the suspension predicate and prove that the generated
+ schedule satisfies all the remaining properties. *)
+ Section AdditionalScheduleProperties.
+
+ (* First, we show that the new schedule respects self-suspensions. *)
+ Lemma sched_new_respects_self_suspensions:
+ respects_self_suspensions job_arrival inflated_job_cost reduced_suspension_duration sched_new.
+ Proof.
+ move => j0 t /eqP SCHEDn; apply/negP.
+ case (ltnP t (arr_j + R)) => [LTr | GEr];
+ last by apply suspended_in_sched_new_only_inside_window.
+ rewrite -sched_new_suspension_matches /suspended_in_sched_new //.
+ rewrite negb_and negbK.
+ rewrite /scheduled_at sched_new_uses_construction_function in SCHEDn.
+ rewrite /build_schedule /reduction.build_schedule in SCHEDn.
+ case (ltnP t (arr_j + R)) => [LT | GE]; last by rewrite ltnNge GE.
+ rewrite LT /reduction.highest_priority_late_job in SCHEDn.
+ apply seq_min_in_seq in SCHEDn.
+ rewrite mem_filter in SCHEDn.
+ move: SCHEDn => /andP [/andP [PEND OR] _].
+ move: OR => /orP [SERV | SCHED]; first by rewrite SERV orbT.
+ apply/orP; left.
+ rewrite negb_and; apply/orP; right.
+ by apply/negP; apply H_respects_self_suspensions.
+ Qed.
+
+ (* Next, we prove that the new schedule is (suspension-aware) work-conserving... *)
+ Lemma sched_new_work_conserving:
+ work_conserving job_arrival inflated_job_cost reduced_suspension_duration
+ arr_seq sched_new.
+ Proof.
+ have COMPnew := sched_new_completed_jobs_dont_execute.
+ have MATCH := sched_new_suspension_matches.
+ rename H_work_conserving into WORKs, H_respects_priority into PRIOs.
+ intros j0 t IN BACK.
+ move: BACK => /andP [/andP[PEND NOTSCHED] NOTSUSP].
+ rewrite /scheduled_at sched_new_uses_construction_function in NOTSCHED *.
+ rewrite /build_schedule /reduction.build_schedule in NOTSCHED *.
+ case: (ltnP t (arr_j + R)) => [BEFORE | AFTER]; last first.
+ {
+ clear NOTSUSP; rewrite ltnNge AFTER /= in NOTSCHED.
+ rewrite -/hp_job in NOTSCHED *.
+ destruct (hp_job t) eqn:SCHEDn; first by exists s.
+ exfalso; clear NOTSCHED.
+ suff NOTNONE: hp_job t != None by rewrite SCHEDn in NOTNONE.
+ move: (PEND) => /andP [ARR NOTCOMPn].
+ have IN0: j0 \in jobs_arrived_up_to arr_seq t.
+ by eapply arrived_between_implies_in_arrivals; eauto 1.
+ apply seq_min_exists with (x := j0).
+ by rewrite mem_filter PEND IN0.
+ }
+ rewrite -MATCH // in NOTSUSP.
+ rewrite /suspended_in_sched_new negb_and negbK in NOTSUSP.
+ rewrite BEFORE /= in NOTSUSP NOTSCHED.
+ rewrite -/hp_late_job in NOTSCHED *.
+ destruct (hp_late_job t) eqn:SCHEDn; first by exists s.
+ exfalso; clear NOTSCHED.
+ suff NOTNONE: hp_late_job t != None by rewrite SCHEDn in NOTNONE.
+ move: (PEND) => /andP [ARR NOTCOMPn].
+ have IN0: j0 \in jobs_arrived_up_to arr_seq t.
+ by eapply arrived_between_implies_in_arrivals; eauto 1.
+ move: NOTSUSP => /orP [NOTSUSPs | LT]; last first.
+ {
+ clear SCHEDn; apply seq_min_exists with (x := j0).
+ by rewrite mem_filter PEND IN0 andbT LT.
+ }
+ case (boolP (completed_by job_cost sched_susp j0 t)) => [COMPs | NOTCOMPs].
+ {
+ clear SCHEDn; apply seq_min_exists with (x := j0).
+ rewrite mem_filter PEND IN0 andbT /=.
+ apply/orP; left.
+ apply leq_trans with (n := job_cost j0 + (inflated_job_cost j0 - job_cost j0));
+ last by move: COMPs => /eqP <-; rewrite leq_add2r.
+ rewrite subnKC; last by apply H_job_costs_do_not_decrease.
+ by rewrite ltn_neqAle; apply/andP; split;
+ last by apply sched_new_completed_jobs_dont_execute.
+ }
+ case (boolP (scheduled_at sched_susp j0 t)) => [SCHEDs | NOTSCHEDs].
+ {
+ clear SCHEDn; apply seq_min_exists with (x := j0).
+ by rewrite mem_filter PEND IN0 andbT SCHEDs orbT.
+ }
+ feed (WORKs j0 t IN); first by repeat (apply/andP; split).
+ move: WORKs => [j_hp SCHEDhp].
+ clear SCHEDn; apply seq_min_exists with (x := j_hp).
+ have ARRhp: has_arrived job_arrival j_hp t.
+ by apply H_jobs_must_arrive_to_execute.
+ have ARRINhp: arrives_in arr_seq j_hp.
+ by eapply H_jobs_come_from_arrival_sequence; eauto 1.
+ have INhp: j_hp \in jobs_arrived_up_to arr_seq t.
+ by eapply arrived_between_implies_in_arrivals; eauto 1.
+ rewrite mem_filter INhp andbT SCHEDhp orbT andbT.
+ apply/andP; split; first by done.
+ apply contraT; rewrite negbK; intro COMPhpN.
+ have COMPhpS: completed_by job_cost sched_susp j_hp t.
+ by apply sched_new_jobs_complete_later; first by apply ltnW.
+ by apply completed_implies_not_scheduled in COMPhpS;
+ first by rewrite SCHEDhp in COMPhpS.
+ Qed.
+
+ (* ...and respects job priorities. *)
+ Lemma sched_new_respects_policy:
+ respects_JLDP_policy job_arrival inflated_job_cost reduced_suspension_duration
+ arr_seq sched_new higher_eq_priority.
+ Proof.
+ have MATCH := sched_new_suspension_matches.
+ rename H_priority_is_transitive into TRANS, H_priority_is_total into TOTAL,
+ H_priority_is_reflexive into REFL, H_work_conserving into WORKs,
+ H_respects_priority into PRIOs.
+ move => j1 j2 t ARRin BACK /eqP SCHED.
+ move: BACK => /andP [/andP [PEND NOTSCHED] NOTSUSPn].
+ rewrite /scheduled_at sched_new_uses_construction_function /build_schedule
+ /reduction.build_schedule in SCHED NOTSCHED *.
+ case: (ltnP t (arr_j + R)) => [BEFORE | AFTER]; last first.
+ {
+ rewrite ltnNge AFTER /= in SCHED NOTSCHED.
+ rewrite /reduction.highest_priority_job in SCHED NOTSCHED.
+ set jobs := reduction.pending_jobs _ _ _ _ _ in SCHED NOTSCHED.
+ have IN: j1 \in jobs.
+ {
+ rewrite mem_filter PEND /=.
+ move: PEND => /andP [ARR _].
+ by eapply arrived_between_implies_in_arrivals; eauto 1.
+ }
+ apply seq_min_computes_min with (y := j1) in SCHED; try (by done).
+ by intros x y; rewrite 2!mem_filter; move => /andP [_ INx] /andP [_ INy];
+ apply TOTAL; eapply in_arrivals_implies_arrived; eauto 2.
+ }
+ rewrite BEFORE in SCHED NOTSCHED.
+ rewrite /reduction.highest_priority_late_job in SCHED NOTSCHED.
+ set jobs := _ sched_new t in SCHED NOTSCHED.
+ rewrite -MATCH // negb_and negbK in NOTSUSPn.
+ have TOT: forall x y, x \in jobs -> y \in jobs ->
+ higher_eq_priority t x y || higher_eq_priority t y x.
+ {
+ intros x y INx INy; rewrite 2!mem_filter in INx INy.
+ move: INx INy => /andP [_ INx] /andP [_ INy].
+ by apply TOTAL; eapply in_arrivals_implies_arrived; eauto 1.
+ }
+ have ARR1: has_arrived job_arrival j1 t by move: PEND => /andP [ARR _].
+ have IN1: j1 \in jobs_arrived_up_to arr_seq t.
+ by eapply arrived_between_implies_in_arrivals; eauto 1.
+ move: NOTSUSPn => /orP [NOTSUSPs | LT]; last first.
+ {
+ apply seq_min_computes_min with (l := jobs); try done.
+ by rewrite mem_filter IN1 andbT PEND LT.
+ }
+ rewrite BEFORE /= in NOTSUSPs.
+ case (boolP (scheduled_at sched_susp j1 t)) => [SCHEDs | NOTSCHEDs].
+ {
+ apply seq_min_computes_min with (l := jobs); try done.
+ by rewrite mem_filter IN1 andbT PEND SCHEDs orbT.
+ }
+ case (boolP (completed_by job_cost sched_susp j1 t)) => [COMPs | NOTCOMPs].
+ {
+ apply seq_min_computes_min with (l := jobs); try (by done).
+ rewrite mem_filter PEND /= IN1 andbT.
+ apply/orP; left.
+ rewrite /reduction.job_is_late.
+ move: COMPs => /eqP ->; rewrite subnKC; last by eauto 1.
+ move: PEND => /andP [_ NOTCOMP].
+ rewrite ltn_neqAle; apply/andP; split; first by done.
+ apply cumulative_service_le_job_cost.
+ by apply sched_new_completed_jobs_dont_execute.
+ }
+ feed (WORKs j1 t ARRin); first by repeat (apply/andP; split).
+ move: WORKs => [j_hp SCHEDhp].
+ apply: (TRANS _ j_hp);
+ last by apply PRIOs; try done; repeat (apply/andP; split).
+ have ARRhp: has_arrived job_arrival j_hp t.
+ by apply H_jobs_must_arrive_to_execute.
+ have ARRINhp: arrives_in arr_seq j_hp.
+ by eapply H_jobs_come_from_arrival_sequence; eauto 1.
+ have INhp: j_hp \in jobs_arrived_up_to arr_seq t.
+ by eapply arrived_between_implies_in_arrivals; eauto 1.
+ apply seq_min_computes_min with (l := jobs); try done.
+ rewrite mem_filter INhp andbT SCHEDhp orbT andbT.
+ apply/andP; split; first by done.
+ apply contraT; rewrite negbK; intro COMPhpN.
+ have COMPhpS: completed_by job_cost sched_susp j_hp t.
+ by apply sched_new_jobs_complete_later; first by apply ltnW.
+ by apply completed_implies_not_scheduled in COMPhpS;
+ first by rewrite SCHEDhp in COMPhpS.
+ Qed.
+
+ End AdditionalScheduleProperties.
+
+ (** Final Remarks *)
+
+ Section FinalRemarks.
+
+ (* To summarize, we conclude that the new schedule is a valid suspension-aware schedule ... *)
+ Remark sched_new_is_valid:
+ valid_suspension_aware_schedule job_arrival arr_seq higher_eq_priority
+ reduced_suspension_duration inflated_job_cost sched_new.
+ Proof.
+ repeat split.
+ - by apply sched_new_jobs_come_from_arrival_sequence.
+ - by apply sched_new_jobs_must_arrive_to_execute.
+ - by apply sched_new_completed_jobs_dont_execute.
+ - by apply sched_new_work_conserving.
+ - by apply sched_new_respects_policy.
+ - by apply sched_new_respects_self_suspensions.
+ Qed.
+
+ (* ...and that if the analyzed job j has response-time bound R in the schedule,
+ then it also has response-time bound R in the original schedule. *)
+ Remark sched_new_response_time_of_job_j:
+ job_response_time_in_sched_new_bounded_by j R ->
+ job_response_time_in_sched_susp_bounded_by j R.
+ Proof.
+ by apply sched_new_jobs_complete_later.
+ Qed.
+
+ End FinalRemarks.
+
+ End ReductionProperties.
+
+End SustainabilityAllCostsProperties.
\ No newline at end of file
diff --git a/analysis/uni/susp/sustainability/singlecost/reduction.v b/analysis/uni/susp/sustainability/singlecost/reduction.v
new file mode 100644
index 000000000..ace08f94e
--- /dev/null
+++ b/analysis/uni/susp/sustainability/singlecost/reduction.v
@@ -0,0 +1,102 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.schedule.uni.susp.schedule.
+Require Import rt.model.schedule.uni.transformation.construction.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
+
+(* In this file, we propose a reduction that converts a suspension-aware
+ schedule to another suspension-aware schedule where the cost of a certain
+ job is inflated and its response time does not decrease. *)
+Module SustainabilitySingleCost.
+
+ Import ScheduleWithSuspensions Suspension Priority ScheduleConstruction.
+
+ Section Reduction.
+
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_cost: Job -> time.
+
+ (** Basic Setup & Setting*)
+
+ (* Consider any job arrival sequence... *)
+ Variable arr_seq: arrival_sequence Job.
+
+ (* ...and assume any (schedule-independent) JLDP policy. *)
+ Variable higher_eq_priority: JLDP_policy Job.
+
+ (* Next, consider any suspension-aware schedule of the arrival sequence... *)
+ Variable sched_susp: schedule Job.
+
+ (* ...and the associated job suspension times. *)
+ Variable job_suspension_duration: job_suspension Job.
+
+ (** Definition of the Reduction *)
+
+ (* Now we proceed with the reduction. Let j be the job to be analyzed. *)
+ Variable j: Job.
+
+ (* Next, consider any job cost inflation that does not decrease the cost of job j
+ and that preserves the cost of the remaining jobs. *)
+ Variable inflated_job_cost: Job -> time.
+
+ (** Schedule Construction *)
+
+ (* We are going to construct a new schedule that copies the original suspension-aware
+ schedule and tries to preserve the service received by job j, until the time when
+ it completes in the original schedule. *)
+ Section ScheduleConstruction.
+
+ (* First, 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.
+
+ (* For simplicity, let's define some local names. *)
+ Let job_is_pending := pending job_arrival inflated_job_cost sched_prefix.
+ Let job_is_suspended :=
+ suspended_at job_arrival inflated_job_cost job_suspension_duration sched_prefix.
+ Let actual_job_arrivals_up_to := jobs_arrived_up_to arr_seq.
+
+ (* Recall that a job is ready in the new schedule iff it is pending and not suspended. *)
+ Let job_is_ready j t := job_is_pending j t && ~~ job_is_suspended j t.
+
+ (* Then, consider the list of ready jobs at time t in the new schedule. *)
+ Definition ready_jobs :=
+ [seq j_other <- actual_job_arrivals_up_to t | job_is_ready j_other t].
+
+ (* From the list of ready jobs, we take one of the (possibly many)
+ highest-priority jobs, or None, in case there are no ready jobs. *)
+ Definition highest_priority_job := seq_min (higher_eq_priority t) ready_jobs.
+
+ (* Then, we construct the new schedule at time t as follows.
+ a) If the currently scheduled job in sched_susp is ready to execute in the new schedule
+ and has highest priority, pick that job.
+ b) Else, pick one of the highest priority ready jobs in the new schedule. *)
+ Definition build_schedule : option Job :=
+ if highest_priority_job is Some j_hp then
+ if sched_susp t is Some j_in_susp then
+ if job_is_ready j_in_susp t && higher_eq_priority t j_in_susp j_hp then
+ Some j_in_susp
+ else
+ Some j_hp
+ else Some j_hp
+ else None.
+
+ End ConstructionStep.
+
+ (* To conclude, starting from the empty schedule, ...*)
+ Let empty_schedule : schedule Job := fun t => None.
+
+ (* ...we use the recursive definition above to construct the new schedule. *)
+ Definition sched_susp_highercost :=
+ build_schedule_from_prefixes build_schedule empty_schedule.
+
+ End ScheduleConstruction.
+
+ End Reduction.
+
+End SustainabilitySingleCost.
\ No newline at end of file
diff --git a/analysis/uni/susp/sustainability/singlecost/reduction_properties.v b/analysis/uni/susp/sustainability/singlecost/reduction_properties.v
new file mode 100644
index 000000000..1389856cc
--- /dev/null
+++ b/analysis/uni/susp/sustainability/singlecost/reduction_properties.v
@@ -0,0 +1,741 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.susp.suspension_intervals
+ rt.model.schedule.uni.susp.schedule
+ rt.model.schedule.uni.susp.platform.
+Require Import rt.analysis.uni.susp.sustainability.singlecost.reduction.
+Require Import rt.model.schedule.uni.transformation.construction.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(* In this file, we prove that the in the generated suspension-aware schedule,
+ the response time of the job whose cost is inflated does not decrease. *)
+Module SustainabilitySingleCostProperties.
+
+ Import ScheduleWithSuspensions Suspension Priority SuspensionIntervals
+ PlatformWithSuspensions ResponseTime ScheduleConstruction.
+
+ Module reduction := SustainabilitySingleCost.
+
+ Section ReductionProperties.
+
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_cost: Job -> time.
+
+ (** Basic Setup & Setting*)
+
+ (* Consider any job arrival sequence with consistent job arrivals. *)
+ Variable arr_seq: arrival_sequence Job.
+ Hypothesis H_arrival_times_are_consistent:
+ arrival_times_are_consistent job_arrival arr_seq.
+
+ (* Assume any (schedule-independent) 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.
+
+ (* Next, consider any suspension-aware schedule of the arrival sequence... *)
+ Variable sched_susp: schedule Job.
+ Hypothesis H_jobs_come_from_arrival_sequence:
+ jobs_come_from_arrival_sequence sched_susp arr_seq.
+
+ (* ...and the associated job suspension times. *)
+ Variable job_suspension_duration: job_suspension Job.
+
+ (* Assume that, in this schedule, 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 job_cost sched_susp.
+
+ (* Also assume that the schedule is work-conserving if there are non-suspended jobs, ... *)
+ Hypothesis H_work_conserving:
+ work_conserving job_arrival job_cost job_suspension_duration arr_seq sched_susp.
+
+ (* ...that the schedule respects job priorities... *)
+ Hypothesis H_respects_priority:
+ respects_JLDP_policy job_arrival job_cost job_suspension_duration 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 job_cost job_suspension_duration sched_susp.
+
+ (** Reduction Setup *)
+
+ (* Now we prove properties about the reduction. Let j be any job. *)
+ Variable j: Job.
+ Let arr_j := job_arrival j.
+
+ (* Next, consider any job cost inflation... *)
+ Variable inflated_job_cost: Job -> time.
+
+ (* ...that does not decrease the cost of job j... *)
+ Hypothesis H_cost_of_j_does_not_decrease: inflated_job_cost j >= job_cost j.
+
+ (* ...and that preserves the cost of the remaining jobs. *)
+ Hypothesis H_inflation_only_for_job_j:
+ forall any_j,
+ any_j != j ->
+ inflated_job_cost any_j = job_cost any_j.
+
+ (* Recall the schedule we constructed from sched_susp by inflating the cost of job j. *)
+ Let sched_susp_highercost := reduction.sched_susp_highercost job_arrival arr_seq higher_eq_priority
+ sched_susp job_suspension_duration inflated_job_cost.
+
+ (* For simplicity, we define some local names for the definitions related to both schedules. *)
+ Let job_response_time_in_sched_susp_bounded_by :=
+ is_response_time_bound_of_job job_arrival job_cost sched_susp.
+ Let job_response_time_in_sched_susp_highercost_bounded_by :=
+ is_response_time_bound_of_job job_arrival inflated_job_cost sched_susp_highercost.
+ Let ready_jobs := reduction.ready_jobs job_arrival arr_seq job_suspension_duration
+ inflated_job_cost sched_susp_highercost.
+ Let hp_job := reduction.highest_priority_job job_arrival arr_seq higher_eq_priority
+ job_suspension_duration inflated_job_cost sched_susp_highercost.
+ Let completed_in_sched_susp := completed_by job_cost sched_susp.
+ Let completed_in_sched_susp_highercost := completed_by inflated_job_cost sched_susp_highercost.
+ Let suspended_in_sched_susp :=
+ suspended_at job_arrival job_cost job_suspension_duration sched_susp.
+ Let suspended_in_sched_susp_highercost :=
+ suspended_at job_arrival inflated_job_cost job_suspension_duration sched_susp_highercost.
+ Let service_in_sched_susp := service sched_susp.
+ Let service_in_sched_susp_highercost := service sched_susp_highercost.
+
+ (** Properties of the Schedule Construction *)
+
+ (* In this section, we prove that the new schedule uses its construction function. *)
+ Section PropertiesOfScheduleConstruction.
+
+ (* Recall the construction function of the new schedule. *)
+ Let build_schedule := reduction.build_schedule job_arrival arr_seq higher_eq_priority
+ sched_susp job_suspension_duration inflated_job_cost.
+
+ (* By showing that the construction function depends only on the schedule prefix, ... *)
+ Lemma sched_susp_highercost_depends_only_on_prefix:
+ forall sched1 sched2 t,
+ (forall t0, t0 < t -> sched1 t0 = sched2 t0) ->
+ build_schedule sched1 t = build_schedule sched2 t.
+ Proof.
+ intros sched1 sched2 t ALL.
+ rewrite /build_schedule /reduction.build_schedule /reduction.highest_priority_job.
+ have COMP: forall j, completed_by inflated_job_cost sched1 j t =
+ completed_by inflated_job_cost sched2 j t.
+ {
+ intros j0; rewrite /completed_by; f_equal.
+ apply eq_big_nat; move => i /= LTi.
+ by rewrite /service_at /scheduled_at ALL.
+ }
+ set pend1 := pending _ _ sched1.
+ set pend2 := pending _ _ sched2.
+ set susp1 := suspended_at _ _ _ sched1.
+ set susp2 := suspended_at _ _ _ sched2.
+ have SAME: forall j, pend1 j t = pend2 j t.
+ {
+ intros j0; rewrite /pend1 /pend2 /pending.
+ by case: has_arrived => //=; rewrite COMP.
+ }
+ set readyjobs := reduction.ready_jobs _ _ _ _.
+ have EX: forall j0, [exists t0: 'I_t, scheduled_at sched1 j0 t0] =
+ [exists t0: 'I_t, scheduled_at sched2 j0 t0].
+ {
+ intros j0; apply/idP/idP.
+ - by move => /existsP [t0 SCHED]; apply/existsP; exists t0; rewrite /scheduled_at -ALL.
+ - by move => /existsP [t0 SCHED]; apply/existsP; exists t0; rewrite /scheduled_at ALL.
+ }
+ have BEG: forall j0, time_after_last_execution job_arrival sched1 j0 t =
+ time_after_last_execution job_arrival sched2 j0 t.
+ {
+ intros j0; rewrite /time_after_last_execution EX.
+ case: ifP => _; last by done.
+ by f_equal; apply eq_bigl; intros t0; rewrite /scheduled_at ALL.
+ }
+ have SUSP: forall j0, has_arrived job_arrival j0 t ->
+ suspension_duration job_arrival job_suspension_duration sched1 j0 t =
+ suspension_duration job_arrival job_suspension_duration sched2 j0 t.
+ {
+ intros j0 ARR0; rewrite /suspension_duration BEG; f_equal.
+ rewrite /service /service_during big_nat_cond [in RHS]big_nat_cond.
+ apply congr_big; try (by done).
+ move => i /= /andP [LTi _].
+ rewrite /service_at /scheduled_at ALL //.
+ apply: (leq_trans LTi).
+ by apply last_execution_bounded_by_identity.
+ }
+ have SAMEsusp: forall j0, has_arrived job_arrival j0 t -> susp1 j0 t = susp2 j0 t.
+ by intros j0 ARR0; rewrite /susp1 /susp2 /suspended_at COMP BEG SUSP.
+ have SAMEready: readyjobs sched1 t = readyjobs sched2 t.
+ {
+ apply eq_in_filter; intros j0 IN.
+ rewrite -/pend1 -/pend2 SAME; f_equal.
+ rewrite /suspended_at COMP BEG SUSP; first by done.
+ by rewrite /has_arrived -ltnS; eapply in_arrivals_implies_arrived_before; eauto 1.
+ }
+ rewrite SAMEready; desf; try (by done); rewrite SAME SAMEsusp in Heq1; try (by done);
+ by apply H_jobs_must_arrive_to_execute; apply/eqP.
+ Qed.
+
+ (* ...we infer that the new schedule is indeed based on the construction function. *)
+ Corollary sched_susp_highercost_uses_construction_function:
+ forall t,
+ sched_susp_highercost t = build_schedule sched_susp_highercost t.
+ Proof.
+ by ins; apply prefix_dependent_schedule_construction,
+ sched_susp_highercost_depends_only_on_prefix.
+ Qed.
+
+ End PropertiesOfScheduleConstruction.
+
+ (** Basic Properties of the Generated Schedule *)
+
+ (* In this section, we prove that sched_susp_highercost is a valid suspension-aware schedule. *)
+ Section ScheduleIsValid.
+
+ (* First, we show that scheduled jobs come from the arrival sequence. *)
+ Lemma sched_susp_highercost_jobs_come_from_arrival_sequence:
+ jobs_come_from_arrival_sequence sched_susp_highercost arr_seq.
+ Proof.
+ rename H_jobs_come_from_arrival_sequence into FROM.
+ move => j0 t /eqP SCHED.
+ rewrite sched_susp_highercost_uses_construction_function /reduction.build_schedule
+ -/hp_job in SCHED.
+ destruct (hp_job t) as [j_hp|] eqn:HP; last by done.
+ have IN: j_hp \in ready_jobs t.
+ by rewrite /hp_job /reduction.highest_priority_job in HP; apply seq_min_in_seq in HP.
+ have ARRhp: arrives_in arr_seq j_hp.
+ {
+ rewrite mem_filter in IN; move: IN => /andP [/andP _ IN].
+ by apply in_arrivals_implies_arrived in IN.
+ }
+ destruct (sched_susp t) eqn:SCHEDs; last by case: SCHED => SAME; subst.
+ move: SCHEDs => /eqP SCHEDs; apply FROM in SCHEDs.
+ case: SCHED; case: ifP; first by move => /andP [PEND _]; case => <-.
+ by move => NOTPEND; case => <-.
+ Qed.
+
+ (* Next, we show that jobs do not execute before their arrival times... *)
+ Lemma sched_susp_highercost_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute job_arrival sched_susp_highercost.
+ Proof.
+ have FUNC := sched_susp_highercost_uses_construction_function.
+ rename H_jobs_must_arrive_to_execute into MUST.
+ move => j0 t /eqP SCHED.
+ rewrite FUNC /reduction.build_schedule -/hp_job in SCHED.
+ destruct (hp_job t) as [j_hp|] eqn:HP; last by done.
+ have IN: j_hp \in ready_jobs t.
+ by rewrite /hp_job /reduction.highest_priority_job in HP; apply seq_min_in_seq in HP.
+ have ARRhp: has_arrived job_arrival j_hp t.
+ {
+ rewrite mem_filter in IN; move: IN => /andP [/andP _ IN].
+ by eapply in_arrivals_implies_arrived_before in IN; eauto.
+ }
+ destruct (sched_susp t) eqn:SCHEDs; last by case: SCHED => SAME; subst.
+ case: SCHED; case: ifP;
+ first by move => /andP [PEND _]; case => <-; apply MUST; apply/eqP.
+ by move => NOTPEND; case => <-.
+ Qed.
+
+ (* ...nor longer than their execution costs. *)
+ Lemma sched_susp_highercost_completed_jobs_dont_execute:
+ completed_jobs_dont_execute inflated_job_cost sched_susp_highercost.
+ Proof.
+ intros j0 t.
+ induction t;
+ first by rewrite /service /service_during big_geq //.
+ rewrite /service /service_during big_nat_recr //=.
+ rewrite leq_eqVlt in IHt; move: IHt => /orP [/eqP EQ | LT]; last first.
+ {
+ apply: leq_trans LT; rewrite -addn1.
+ by apply leq_add; last by apply leq_b1.
+ }
+ rewrite -[inflated_job_cost _]addn0; apply leq_add; first by rewrite -EQ.
+ rewrite leqn0 eqb0 /scheduled_at.
+ rewrite sched_susp_highercost_uses_construction_function /reduction.build_schedule
+ -/hp_job.
+ destruct (hp_job t) as [j_hp|] eqn:HP; last by done.
+ have IN: j_hp \in ready_jobs t.
+ by rewrite /hp_job /reduction.highest_priority_job in HP; apply seq_min_in_seq in HP.
+ have PENDhp: pending job_arrival inflated_job_cost sched_susp_highercost j_hp t.
+ {
+ rewrite mem_filter in IN; move: IN => /andP [/andP [PEND _] IN].
+ by eapply in_arrivals_implies_arrived_before in IN; eauto.
+ }
+ destruct (sched_susp t) eqn:SCHEDs; last first.
+ {
+ apply/eqP; case => SAME; subst j0.
+ suff NOTPEND: ~~ pending job_arrival inflated_job_cost sched_susp_highercost j_hp t.
+ by rewrite PENDhp in NOTPEND.
+ by rewrite /pending negb_and; apply/orP; right; rewrite negbK; apply/eqP.
+ }
+ {
+ case: ifP => [PEND | NOTPEND]; apply/eqP; case => SAME; subst j0;
+ last by move: PENDhp => /andP [_ NC]; rewrite /completed_by EQ eq_refl in NC.
+ move: PEND => /andP [/andP [/andP [_ NC] _] _].
+ by rewrite /completed_by EQ eq_refl in NC.
+ }
+ Qed.
+
+ (* In addition, we prove that the new schedule is work-conserving,... *)
+ Lemma sched_susp_highercost_work_conserving:
+ work_conserving job_arrival inflated_job_cost job_suspension_duration
+ arr_seq sched_susp_highercost.
+ Proof.
+ intros j0 t IN BACK.
+ move: BACK => /andP [/andP[PEND NOTSCHED] NOTSUSP].
+ rewrite /scheduled_at sched_susp_highercost_uses_construction_function
+ /reduction.build_schedule -/hp_job in NOTSCHED *.
+ destruct (hp_job) as [j_hp|] eqn:HP.
+ {
+ destruct (sched_susp t) eqn:SCHEDs; last by exists j_hp.
+ by case: ifP; intros _; [exists s | exists j_hp].
+ }
+ {
+ have IN0: j0 \in ready_jobs t.
+ {
+ rewrite mem_filter PEND NOTSUSP /=.
+ eapply arrived_between_implies_in_arrivals; eauto 1.
+ by move: PEND => /andP [ARR _].
+ }
+ suff NOTNONE: hp_job t != None by rewrite HP in NOTNONE.
+ by apply seq_min_exists with (x := j0).
+ }
+ Qed.
+
+ (* ...respects job priorities, ... *)
+ Lemma sched_susp_highercost_respects_policy:
+ respects_JLDP_policy job_arrival inflated_job_cost job_suspension_duration
+ arr_seq sched_susp_highercost higher_eq_priority.
+ Proof.
+ rename H_priority_is_transitive into TRANS, H_priority_is_total into TOTAL,
+ H_priority_is_reflexive into REFL.
+ move => j1 j2 t IN BACK /eqP SCHED.
+ move: BACK => /andP [/andP [PEND NOTSCHED] NOTSUSP].
+ rewrite /scheduled_at sched_susp_highercost_uses_construction_function /reduction.build_schedule
+ -/hp_job in SCHED NOTSCHED *.
+ set pend := pending _ _ _ in SCHED NOTSCHED.
+ have ALL: forall j_hi j_lo, hp_job t = Some j_hi ->
+ j_lo \in ready_jobs t ->
+ higher_eq_priority t j_hi j_lo.
+ {
+ intros j_hi j_lo SOME INlo; move: SCHED => MIN.
+ rewrite /hp_job /reduction.highest_priority_job in SOME.
+ apply seq_min_computes_min with (y := j_lo) in SOME; try (by done).
+ intros x y; rewrite mem_filter [y \in _]mem_filter /jobs_arrived_up_to.
+ move => /andP [_ INx] /andP [_ INy].
+ by apply TOTAL; eapply in_arrivals_implies_arrived; eauto 1.
+ }
+ destruct (hp_job t) as [j_hp |] eqn:HP; last by done.
+ have HIGHER: higher_eq_priority t j_hp j1.
+ {
+ apply ALL; first by done.
+ move: PEND => /andP [ARR NOTCOMP].
+ rewrite mem_filter /pending ARR NOTCOMP NOTSUSP /=.
+ by eapply arrived_between_implies_in_arrivals; eauto 1.
+ }
+ destruct (sched_susp t) eqn:SCHEDs; last by case: SCHED => SAME; subst j2.
+ move: SCHED; case: ifP => [/andP[ PENDs HPs] | NOTPENDs]; case => SAME; subst;
+ first by apply (TRANS t (j_hp)).
+ apply ALL; first by done.
+ move: PEND => /andP [ARR NOTCOMP].
+ rewrite mem_filter /pending ARR NOTCOMP NOTSUSP /=.
+ by eapply arrived_between_implies_in_arrivals; eauto 1.
+ Qed.
+
+ (* ...and does not allow suspended jobs to be scheduled. *)
+ Lemma sched_susp_highercost_respects_self_suspensions:
+ respects_self_suspensions job_arrival inflated_job_cost
+ job_suspension_duration sched_susp_highercost.
+ Proof.
+ rename H_respects_self_suspensions into SELF.
+ move => j0 t /eqP SCHED SUSP.
+ set suspended := suspended_at _ _ _ _ in SUSP.
+ rewrite sched_susp_highercost_uses_construction_function /reduction.build_schedule
+ -/hp_job in SCHED.
+ destruct (hp_job t) as [j_hp|] eqn:HP; last by done.
+ have IN: j_hp \in ready_jobs t.
+ by rewrite /hp_job /reduction.highest_priority_job in HP; apply seq_min_in_seq in HP.
+ have NOTSUSP: ~~ suspended j_hp t.
+ {
+ by rewrite mem_filter in IN; move: IN => /andP [/andP [_ NOTs] _].
+ }
+ destruct (sched_susp t) eqn:SCHEDs;
+ last by case: SCHED => SAME; subst; rewrite SUSP in NOTSUSP.
+ case: SCHED; case: ifP; last by move => _; case => SAME; subst; rewrite SUSP in NOTSUSP.
+ move: SCHEDs; move => /eqP SCHEDs /andP [/andP [PEND NOTSUSPs] _]; case => SAME; subst.
+ by rewrite -/suspended SUSP in NOTSUSPs.
+ Qed.
+
+ End ScheduleIsValid.
+
+ (** Scheduling Invariant *)
+
+ (* In this section, we compare the two schedules to determine they are the same
+ while job j has not completed in sched_susp. *)
+ Section SchedulingInvariant.
+
+ (* To prove that the schedules are the same, we use induction over time. *)
+ Section InductiveStep.
+
+ (* Consider any time t by which job j has not completed in sched_susp. *)
+ Variable t: time.
+ Hypothesis H_j_has_not_completed: ~~ completed_in_sched_susp j t.
+
+ (* Induction Hypothesis:
+ Assume that at every time prior to time t, any job that is scheduled
+ in sched_susp is also scheduled in sched_susp_highercost. *)
+ Hypothesis H_schedules_are_the_same:
+ forall k any_j,
+ k < t ->
+ scheduled_at sched_susp any_j k = scheduled_at sched_susp_highercost any_j k.
+
+ (* Then, let k be any time no later than t. *)
+ Variable k: time.
+ Hypothesis H_k_before_t: k <= t.
+
+ (* First, we prove that jobs complete at time k in sched_susp iff they
+ complete in the new schedule. *)
+ Lemma sched_susp_highercost_same_completion:
+ forall any_j,
+ completed_in_sched_susp any_j k = completed_in_sched_susp_highercost any_j k.
+ Proof.
+ rename H_j_has_not_completed into NOTCOMPj,
+ H_schedules_are_the_same into IH, H_cost_of_j_does_not_decrease into COSTj,
+ H_inflation_only_for_job_j into COSTother.
+ have COMPLETIONw := sched_susp_highercost_completed_jobs_dont_execute.
+ rewrite /completed_in_sched_susp/completed_in_sched_susp_highercost
+ /completed_by in NOTCOMPj *.
+ intros any_j; apply/idP/idP.
+ {
+ intros COMPs.
+ case (boolP (any_j == j)) => [/eqP EQ | NEQ]; subst.
+ {
+ suff BUG: service sched_susp j t == job_cost j by rewrite BUG in NOTCOMPj.
+ by apply completion_monotonic with (t0 := k); try (by done); apply ltnW.
+ }
+ rewrite COSTother //; move: COMPs => /eqP <-.
+ apply/eqP; rewrite /service /service_during big_nat_cond [X in _=X]big_nat_cond.
+ apply eq_bigr; move => i /= /andP [LT _].
+ by rewrite /service_at IH //; apply: (leq_trans LT).
+ }
+ {
+ intros COMPw.
+ rewrite eqn_leq; apply/andP; split;
+ first by apply cumulative_service_le_job_cost.
+ apply leq_trans with (n := inflated_job_cost any_j);
+ first by case (boolP (any_j==j)) => [/eqP EQ | NEQ]; subst; rewrite ?COSTj ?COSTother.
+ move: COMPw => /eqP <-.
+ apply leq_sum_nat; move => i /= LT _.
+ by rewrite /service_at IH //; apply: (leq_trans LT).
+ }
+ Qed.
+
+ (* We also prove the execution patterns of the jobs coincide... *)
+ Lemma sched_susp_highercost_same_time_after_last_exec:
+ forall any_j,
+ time_after_last_execution job_arrival sched_susp any_j k =
+ time_after_last_execution job_arrival sched_susp_highercost any_j k.
+ Proof.
+ rename H_schedules_are_the_same into IH.
+ intros any_j; rewrite /time_after_last_execution.
+ have EXsame: [exists t0:'I_k, scheduled_at sched_susp any_j t0] =
+ [exists t0:'I_k, scheduled_at sched_susp_highercost any_j t0].
+ {
+ by apply/idP/idP; move => /existsP [t0 LT0];
+ apply/existsP; exists t0; rewrite ?IH//-?IH//; apply leq_trans with (n := k).
+ }
+ rewrite EXsame {EXsame}; case: ifP => [EX | _]; last by done.
+ f_equal; apply eq_bigl; intros i; rewrite IH //.
+ by apply leq_trans with (n := k).
+ Qed.
+
+ (* ...and the jobs have the same suspension intervals, ... *)
+ Lemma sched_susp_highercost_same_suspension_duration:
+ forall any_j,
+ has_arrived job_arrival any_j k ->
+ suspension_duration job_arrival job_suspension_duration sched_susp any_j k =
+ suspension_duration job_arrival job_suspension_duration sched_susp_highercost any_j k.
+ Proof.
+ intros any_j ARR.
+ rewrite /suspension_duration /service /service_during; f_equal.
+ rewrite sched_susp_highercost_same_time_after_last_exec.
+ rewrite big_nat_cond [X in _ = X]big_nat_cond; apply eq_bigr.
+ move => i /= /andP [LT _].
+ rewrite /service_at H_schedules_are_the_same //.
+ apply leq_trans with (n := k); last by done.
+ apply: (leq_trans LT).
+ by apply last_execution_bounded_by_identity.
+ Qed.
+
+ (* ...which implies that jobs suspend at time k in sched_susp iff they suspend
+ in the new schedule as well. *)
+ Lemma sched_susp_highercost_same_suspension:
+ forall any_j,
+ has_arrived job_arrival any_j k ->
+ suspended_in_sched_susp any_j k = suspended_in_sched_susp_highercost any_j k.
+ Proof.
+ intros any_j ARR.
+ rewrite /suspended_in_sched_susp /suspended_in_sched_susp_highercost /suspended_at.
+ rewrite -/completed_in_sched_susp_highercost -sched_susp_highercost_same_completion.
+ rewrite sched_susp_highercost_same_time_after_last_exec.
+ by rewrite sched_susp_highercost_same_suspension_duration.
+ Qed.
+
+ (* Using the lemmas above, we conclude the inductive step by showing that the
+ two schedules are the same at time k. *)
+ Lemma sched_susp_highercost_same_schedule:
+ forall any_j,
+ scheduled_at sched_susp any_j k = scheduled_at sched_susp_highercost any_j k.
+ Proof.
+ have FUNC := sched_susp_highercost_uses_construction_function.
+ have SELFw := sched_susp_highercost_respects_self_suspensions.
+ have COMPLETIONw := sched_susp_highercost_completed_jobs_dont_execute.
+ have LEMMAcomp := sched_susp_highercost_same_completion.
+ have LEMMAsusp := sched_susp_highercost_same_suspension.
+ rename H_jobs_must_arrive_to_execute into MUSTARR,
+ H_cost_of_j_does_not_decrease into HIGHER,
+ H_inflation_only_for_job_j into SAME,
+ H_respects_self_suspensions into SELFs,
+ H_work_conserving into WORKs, H_priority_is_reflexive into REFL,
+ H_respects_priority into PRIOs.
+ rewrite /service_in_sched_susp /service_in_sched_susp_highercost /service /service_during.
+ suff EQsched: sched_susp k = sched_susp_highercost k by rewrite /scheduled_at EQsched.
+ rewrite /scheduled_at FUNC /reduction.build_schedule -/hp_job.
+ destruct (hp_job k) as [j_hp|] eqn:HP; last first.
+ {
+ destruct (sched_susp k) as [j_s|] eqn:SCHEDs; last by done.
+ suff NOTNONE: hp_job k != None by rewrite HP in NOTNONE.
+ apply seq_min_exists with (x := j_s).
+ have NOTCOMPs: ~~ completed_in_sched_susp j_s k.
+ {
+ apply/negP; intros COMP'.
+ apply completed_implies_not_scheduled in COMP'; try (by done).
+ by rewrite /scheduled_at SCHEDs eq_refl in COMP'.
+ }
+ have ARR: has_arrived job_arrival j_s k by apply MUSTARR; apply/eqP.
+ have NOTCOMPw: ~~ completed_by inflated_job_cost sched_susp_highercost j_s k.
+ by rewrite -/completed_in_sched_susp_highercost -LEMMAcomp //.
+ have NOTSUSPs: ~~ suspended_in_sched_susp j_s k by apply/negP; apply SELFs; apply/eqP.
+ have NOTSUSPw: ~~ suspended_in_sched_susp_highercost j_s k by rewrite -LEMMAsusp //.
+ have ARRw: j_s \in jobs_arrived_up_to arr_seq k.
+ {
+ eapply arrived_between_implies_in_arrivals; eauto 1.
+ by apply H_jobs_come_from_arrival_sequence with (t := k); apply/eqP.
+ }
+ by rewrite mem_filter; repeat (apply/andP; split).
+ }
+ {
+ have IN: j_hp \in ready_jobs k.
+ by apply seq_min_in_seq with (rel := higher_eq_priority k).
+ rewrite mem_filter in IN; move: IN => /andP [/andP [/andP [ARRhp NOTCOMPhp] NOTSUSP] IN].
+ have ARRINhp: arrives_in arr_seq j_hp by apply in_arrivals_implies_arrived in IN.
+ destruct (sched_susp k) as [j_s|] eqn:SCHEDs.
+ {
+ case: ifP => // NOTPEND.
+ have PENDw: pending job_arrival inflated_job_cost sched_susp_highercost j_s k.
+ {
+ apply/andP; split; first by apply MUSTARR; apply/eqP.
+ rewrite -/completed_in_sched_susp_highercost -LEMMAcomp //.
+ apply/negP; intros COMPs.
+ apply completed_implies_not_scheduled in COMPs; try (by done).
+ by rewrite /scheduled_at SCHEDs eq_refl in COMPs.
+ }
+ have ARRs: has_arrived job_arrival j_s k by apply MUSTARR; apply/eqP.
+ have NOTSUSPs: ~~ suspended_in_sched_susp j_s k by apply/negP; apply SELFs; apply/eqP.
+ have NOTSUSPw: ~~ suspended_in_sched_susp_highercost j_s k by rewrite -LEMMAsusp.
+ rewrite -/suspended_in_sched_susp_highercost PENDw NOTSUSPw /= in NOTPEND.
+ suff PRIOINV: higher_eq_priority k j_s j_hp by rewrite PRIOINV in NOTPEND.
+ apply PRIOs; try (by done); last by apply/eqP.
+ have NOTCOMPhp': ~~ completed_by job_cost sched_susp j_hp k.
+ by rewrite -/completed_in_sched_susp LEMMAcomp.
+ have NOTSCHEDhp: ~~ scheduled_at sched_susp j_hp k.
+ {
+ apply/negP; intro SCHEDs'.
+ apply only_one_job_scheduled with (j1 := j_s) in SCHEDs'; subst; last by apply/eqP.
+ suff BUG: higher_eq_priority k j_hp j_hp by rewrite BUG in NOTPEND.
+ by apply REFL.
+ }
+ have NOTSUSPhp: ~~ suspended_in_sched_susp j_hp k by rewrite LEMMAsusp.
+ by repeat (apply/andP; split).
+ }
+ {
+ have NOTCOMPhp': ~~ completed_by job_cost sched_susp j_hp k.
+ by rewrite -/completed_in_sched_susp LEMMAcomp.
+ have NOTSCHEDhp: ~~ scheduled_at sched_susp j_hp k by rewrite /scheduled_at SCHEDs.
+ have NOTSUSPhp: ~~ suspended_in_sched_susp j_hp k by rewrite LEMMAsusp.
+ feed (WORKs j_hp k ARRINhp); first by repeat (apply/andP; split).
+ move: WORKs => [j_x SCHEDx].
+ by rewrite /scheduled_at SCHEDs in SCHEDx.
+ }
+ }
+ Qed.
+
+ End InductiveStep.
+
+ (* Using the inductive step above, we prove that before the completion of job j
+ in sched_susp, the two schedules are exactly the same. *)
+ Lemma scheduled_in_susp_iff_scheduled_in_wcet:
+ forall t any_j,
+ ~~ completed_in_sched_susp j t ->
+ scheduled_at sched_susp any_j t = scheduled_at sched_susp_highercost any_j t.
+ Proof.
+ have LEMMAsched := sched_susp_highercost_same_schedule.
+ induction t as [t IHtmp] using strong_ind.
+ intros j' NOTCOMP.
+ suff IH: forall k any_j, k < t ->
+ scheduled_at sched_susp any_j k = scheduled_at sched_susp_highercost any_j k.
+ by apply LEMMAsched with (t := t).
+ intros k any_j LT; apply IHtmp; first by done.
+ apply/negP; intro COMPk.
+ suff COMPt: completed_in_sched_susp j t by rewrite COMPt in NOTCOMP.
+ by apply completion_monotonic with (t0 := k); [| apply ltnW|].
+ Qed.
+
+ End SchedulingInvariant.
+
+ (** Comparison of Response-time Bounds *)
+
+ (* In this section, we use the scheduling invariant above to compare response-time bounds
+ for job j in both schedules. *)
+ Section ComparingResponseTimes.
+
+ (* Assume that job j has positive cost. *)
+ Hypothesis H_cost_j_positive: job_cost j > 0.
+
+ (* Also assume that the response time of job j in sched_susp is equal to some value r... *)
+ Variable r: time.
+ Hypothesis H_response_time_bound_in_sched_susp:
+ job_response_time_in_sched_susp_bounded_by j r.
+ Hypothesis H_response_time_bound_is_tight:
+ forall r', job_response_time_in_sched_susp_bounded_by j r' -> r <= r'.
+
+ (* ...and that the response time of j in the new schedule is upper-bounded by some value R. *)
+ Variable R: time.
+ Hypothesis H_response_time_bound_in_sched_susp_highercost:
+ job_response_time_in_sched_susp_highercost_bounded_by j R.
+
+ (* Using the scheduling invariant, we show that job j receives the same service
+ in both schedules up to time (arr_j + r). *)
+ Lemma sched_susp_highercost_same_service_for_j:
+ forall t,
+ t <= arr_j + r ->
+ service_in_sched_susp j t = service_in_sched_susp_highercost j t.
+ Proof.
+ rename H_response_time_bound_is_tight into TIGHT.
+ have IFF := scheduled_in_susp_iff_scheduled_in_wcet.
+ rewrite /service_in_sched_susp /service_in_sched_susp_highercost /service /service_during.
+ induction t; first by intros _; rewrite big_geq // big_geq.
+ intros LT.
+ feed IHt; first by apply ltnW.
+ rewrite big_nat_recr // big_nat_recr //=.
+ f_equal; first by done.
+ rewrite /service_at IFF; first by done.
+ apply/negP; intro COMPt.
+ suff BUG: t >= arr_j + r by rewrite leqNgt LT in BUG.
+ have AFTER: arr_j <= t.
+ {
+ apply contraT; rewrite -ltnNge; intro BEFORE.
+ suff BUG: ~~ completed_in_sched_susp j t by rewrite COMPt in BUG.
+ rewrite /completed_in_sched_susp /completed_by /service /service_during.
+ rewrite (cumulative_service_before_job_arrival_zero job_arrival) //; last by apply ltnW.
+ by rewrite eq_sym -lt0n.
+ }
+ rewrite -[t](addKn arr_j) -addnBA //.
+ rewrite leq_add2l; apply TIGHT.
+ rewrite /job_response_time_in_sched_susp_bounded_by /is_response_time_bound_of_job.
+ by rewrite subnKC.
+ Qed.
+
+ (* Next, since r is an exact response time bound, we show that r <= R... *)
+ Lemma sched_susp_highercost_r_le_R: r <= R.
+ Proof.
+ have SAME := sched_susp_highercost_same_service_for_j.
+ rename H_response_time_bound_in_sched_susp_highercost into RESPw,
+ H_response_time_bound_in_sched_susp into RESPs,
+ H_response_time_bound_is_tight into TIGHT,
+ H_cost_of_j_does_not_decrease into COSTj.
+ unfold job_response_time_in_sched_susp_bounded_by, service_in_sched_susp_highercost,
+ job_response_time_in_sched_susp_highercost_bounded_by, service_in_sched_susp,
+ is_response_time_bound_of_job, completed_by, service in *.
+ set Sw := service_during sched_susp_highercost in RESPw RESPs TIGHT SAME.
+ set Ss := service_during sched_susp in RESPs TIGHT SAME.
+ apply contraT; rewrite -ltnNge; intros LT.
+ suff BUG: job_cost j > inflated_job_cost j by rewrite ltnNge COSTj in BUG.
+ move: RESPw RESPs => /eqP RESPw /eqP RESPs; rewrite -RESPw -RESPs.
+ rewrite /Ss /service_during.
+ rewrite -> big_cat_nat with (n := arr_j + R);
+ [simpl | by done | by rewrite leq_add2l ltnW].
+ rewrite -addn1; apply leq_add;
+ first by rewrite -SAME; [apply leqnn | rewrite leq_add2l ltnW].
+ rewrite lt0n; apply/eqP; intro ZERO.
+ suff BUG: R >= r by rewrite leqNgt LT in BUG.
+ apply TIGHT.
+ rewrite -(eqn_add2r 0) -{2}ZERO addn0.
+ rewrite -big_cat_nat //=; last by rewrite leq_add2l ltnW.
+ by rewrite -RESPs.
+ Qed.
+
+ (* ...and also prove that R must be as large as the inflated job cost. *)
+ Lemma R_bounds_inflated_cost: R >= inflated_job_cost j.
+ Proof.
+ apply leq_trans with (n := service sched_susp_highercost j (arr_j + R));
+ first by apply eq_leq; symmetry; apply/eqP.
+ rewrite /service /service_during.
+ rewrite (ignore_service_before_arrival job_arrival) //; first last.
+ - by apply leq_addr.
+ - by apply sched_susp_highercost_jobs_must_arrive_to_execute.
+ by apply cumulative_service_le_delta.
+ Qed.
+
+ (* To conclude, we prove that the difference between the response-time bound and the job cost
+ is larger in the new schedule. *)
+ Theorem sched_susp_highercost_incurs_more_interference:
+ r - job_cost j <= R - inflated_job_cost j.
+ Proof.
+ have GECOST := R_bounds_inflated_cost.
+ have LEQ := sched_susp_highercost_r_le_R.
+ have SAME := sched_susp_highercost_same_service_for_j.
+ rename H_response_time_bound_in_sched_susp into RESPs,
+ H_response_time_bound_in_sched_susp_highercost into RESPw.
+ rewrite leq_subLR.
+ rewrite addnBA; last by apply GECOST.
+ apply leq_trans with (n := service_in_sched_susp j (arr_j + r) + R
+ - service_in_sched_susp_highercost j (arr_j + R));
+ last by apply leq_sub; [rewrite leq_add2r|]; apply eq_leq; [|symmetry]; apply/eqP.
+ rewrite addnC.
+ rewrite /service_in_sched_susp /service_in_sched_susp_highercost /service
+ /service_during in SAME *.
+ rewrite -> big_cat_nat with (n := arr_j+r) (p := arr_j+R);
+ [simpl | by done | by rewrite leq_add2l].
+ feed (SAME (arr_j + r)); first by apply leqnn.
+ rewrite -/(service_during sched_susp_highercost _ _ _)
+ -/(service_during sched_susp_highercost _ _ _)
+ -/(service_during sched_susp _ _ _) in SAME *.
+ set Ss := service_during sched_susp in SAME *; set Sw := service_during sched_susp_highercost.
+ rewrite -subnBA;
+ last by apply leq_trans with (n := Sw j 0 (arr_j + r)); [rewrite SAME | apply leq_addr].
+ rewrite addnC -addnBA; last by rewrite SAME.
+ apply leq_trans with (n := R - (Sw j (arr_j + r) (arr_j + R) + 0));
+ last by rewrite leq_sub2l // leq_add2l; apply eq_leq; apply/eqP; rewrite subn_eq0 SAME.
+ rewrite addn0 subh3 //; last first.
+ {
+ apply leq_trans with (n := Sw j arr_j (arr_j+R)); last by apply cumulative_service_le_delta.
+ by apply extend_sum; first by apply leq_addr.
+ }
+ {
+ apply leq_trans with (n := r + \sum_(arr_j+r<=t<arr_j+R) 1);
+ first by rewrite leq_add2l; apply leq_sum; intros t _; apply leq_b1.
+ by simpl_sum_const; rewrite subnDl subnKC.
+ }
+ Qed.
+
+ End ComparingResponseTimes.
+
+ End ReductionProperties.
+
+End SustainabilitySingleCostProperties.
\ No newline at end of file
diff --git a/implementation/apa/schedule.v b/implementation/apa/schedule.v
index 263da8fd8..486e6f026 100644
--- a/implementation/apa/schedule.v
+++ b/implementation/apa/schedule.v
@@ -146,7 +146,7 @@ Module ConcreteScheduler.
(* Let alpha be an affinity associated with each task. *)
Variable alpha: task_affinity sporadic_task num_cpus.
- (* Let arr_seq be any job arrival sequence with consistent, non-duplicate arrivals. *)
+ (* Let arr_seq be any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
diff --git a/implementation/global/basic/schedule.v b/implementation/global/basic/schedule.v
index ab0715841..9e8eded3f 100644
--- a/implementation/global/basic/schedule.v
+++ b/implementation/global/basic/schedule.v
@@ -95,7 +95,7 @@ Module ConcreteScheduler.
Variable num_cpus: nat.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
- (* Let arr_seq be any job arrival sequence with consistent, non-duplicate arrivals. *)
+ (* Let arr_seq be any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
diff --git a/implementation/global/jitter/schedule.v b/implementation/global/jitter/schedule.v
index eb8c0cc29..47ab16a7c 100644
--- a/implementation/global/jitter/schedule.v
+++ b/implementation/global/jitter/schedule.v
@@ -98,7 +98,7 @@ Module ConcreteScheduler.
Variable num_cpus: nat.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
- (* Let arr_seq be any job arrival sequence with consistent, non-duplicate arrivals. *)
+ (* Let arr_seq be any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
diff --git a/implementation/uni/basic/schedule.v b/implementation/uni/basic/schedule.v
index 8b77cdd23..742c5d25d 100644
--- a/implementation/uni/basic/schedule.v
+++ b/implementation/uni/basic/schedule.v
@@ -89,7 +89,7 @@ Module ConcreteScheduler.
Variable job_arrival: Job -> time.
Variable job_cost: Job -> time.
- (* Let arr_seq be any job arrival sequence with consistent, non-duplicate arrivals. *)
+ (* Let arr_seq be any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
diff --git a/implementation/uni/jitter/arrival_sequence.v b/implementation/uni/jitter/arrival_sequence.v
index 3f3eb9db4..b88bf013f 100644
--- a/implementation/uni/jitter/arrival_sequence.v
+++ b/implementation/uni/jitter/arrival_sequence.v
@@ -30,9 +30,7 @@ Module ConcreteArrivalSequence.
(* Let ts be any concrete task set with valid parameters. *)
Variable ts: concrete_taskset.
- Hypothesis H_valid_task_parameters:
- valid_sporadic_taskset task_cost task_period task_deadline ts.
-
+
(* Regarding the periodic arrival sequence built from ts, we prove that...*)
Let arr_seq := periodic_arrival_sequence ts.
@@ -58,22 +56,6 @@ Module ConcreteArrivalSequence.
by unfold add_job in *; desf.
Qed.
- (* ..., jobs have valid parameters, ... *)
- Theorem periodic_arrivals_valid_job_parameters:
- forall j,
- arrives_in arr_seq j ->
- valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
- Proof.
- rename H_valid_task_parameters into PARAMS.
- unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
- move => j [t ARRj].
- rewrite mem_pmap in ARRj; move: ARRj => /mapP [tsk IN SOME].
- unfold add_job in SOME; desf.
- specialize (PARAMS tsk IN); des.
- unfold valid_sporadic_job, valid_realtime_job, job_cost_positive.
- by repeat split; try (by done); apply leqnn.
- Qed.
-
(* ... job arrivals satisfy the sporadic task model, ... *)
Theorem periodic_arrivals_are_sporadic:
sporadic_task_model task_period job_arrival job_task arr_seq.
@@ -105,7 +87,31 @@ Module ConcreteArrivalSequence.
apply (pmap_uniq) with (g := job_task); last by destruct ts.
by unfold add_job, ocancel; intro tsk; desf.
Qed.
-
+
+ (* We also show that job costs are bounded by task costs... *)
+ Theorem periodic_arrivals_job_cost_le_task_cost:
+ forall j,
+ arrives_in arr_seq j ->
+ job_cost j <= task_cost (job_task j).
+ Proof.
+ intros j [t ARRj].
+ rewrite mem_pmap in ARRj.
+ move: ARRj => /mapP [tsk_j INj SOMEj].
+ by unfold add_job in SOMEj; desf.
+ Qed.
+
+ (* ...and that job deadlines equal task deadlines. *)
+ Theorem periodic_arrivals_job_deadline_eq_task_deadline:
+ forall j,
+ arrives_in arr_seq j ->
+ job_deadline j = task_deadline (job_task j).
+ Proof.
+ intros j [t ARRj].
+ rewrite mem_pmap in ARRj.
+ move: ARRj => /mapP [tsk_j INj SOMEj].
+ by unfold add_job in SOMEj; desf.
+ Qed.
+
End Proofs.
End ConcreteArrivalSequence.
\ No newline at end of file
diff --git a/implementation/uni/jitter/fp_rta_example.v b/implementation/uni/jitter/fp_rta_example.v
index 1482a0c17..161f6f891 100644
--- a/implementation/uni/jitter/fp_rta_example.v
+++ b/implementation/uni/jitter/fp_rta_example.v
@@ -33,9 +33,15 @@ Module ResponseTimeAnalysisFP.
Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.
(* ...which can be shown to have valid parameters. *)
- Fact ts_has_valid_parameters:
- valid_sporadic_taskset task_cost task_period task_deadline ts.
+ Remark ts_has_positive_costs:
+ forall tsk, tsk \in ts -> task_cost tsk > 0.
Proof.
+ intros tsk IN.
+ by repeat (move: IN => /orP [/eqP EQ | IN]; subst; compute); by done.
+ Qed.
+ Remark ts_has_positive_periods:
+ forall tsk, tsk \in ts -> task_period tsk > 0.
+ Proof.
intros tsk IN.
repeat (move: IN => /orP [/eqP EQ | IN]; subst; compute); by done.
Qed.
@@ -146,18 +152,19 @@ Module ResponseTimeAnalysisFP.
Proof.
rename H_jitter_is_bounded into JIT.
intros tsk IN.
- have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
- have TSVALID := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline) (ts0 := ts)
(higher_eq_priority0 := RM task_period) (job_jitter0 := job_jitter)
(task_jitter := task_jitter); try (by done).
+ - by apply ts_has_positive_costs.
+ - by apply ts_has_positive_periods.
- by apply periodic_arrivals_are_consistent.
- - by apply periodic_arrivals_is_a_set.
+ - - apply periodic_arrivals_is_a_set.
- by apply periodic_arrivals_all_jobs_from_taskset.
- - by intros j ARRj; specialize (VALID j ARRj); des; repeat split; try (apply JIT).
- by apply periodic_arrivals_are_sporadic.
+ - by apply periodic_arrivals_job_cost_le_task_cost.
+ - by apply periodic_arrivals_job_deadline_eq_task_deadline.
- by apply RM_is_reflexive.
- by apply RM_is_transitive.
- by apply scheduler_jobs_come_from_arrival_sequence.
diff --git a/implementation/uni/jitter/schedule.v b/implementation/uni/jitter/schedule.v
index 273b2f067..d4581e2c0 100644
--- a/implementation/uni/jitter/schedule.v
+++ b/implementation/uni/jitter/schedule.v
@@ -90,7 +90,7 @@ Module ConcreteScheduler.
Variable job_cost: Job -> time.
Variable job_jitter: Job -> time.
- (* Assume any job arrival sequence with consistent, non-duplicate arrivals. *)
+ (* Assume any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
diff --git a/implementation/uni/susp/schedule.v b/implementation/uni/susp/schedule.v
index ae9088610..bdcdc0eef 100644
--- a/implementation/uni/susp/schedule.v
+++ b/implementation/uni/susp/schedule.v
@@ -135,7 +135,7 @@ Module ConcreteScheduler.
Variable job_arrival: Job -> time.
Variable job_cost: Job -> time.
- (* Assume any job arrival sequence with consistent, non-duplicate arrivals... *)
+ (* Assume any job arrival sequence with consistent, duplicate-free arrivals... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
diff --git a/model/arrival/basic/arrival_bounds.v b/model/arrival/basic/arrival_bounds.v
index 0cfbb40c8..1f7797bbc 100644
--- a/model/arrival/basic/arrival_bounds.v
+++ b/model/arrival/basic/arrival_bounds.v
@@ -19,7 +19,7 @@ Module ArrivalBounds.
Variable job_cost: Job -> time.
Variable job_task: Job -> Task.
- (* Consider any job arrival sequence with consistent, non-duplicate arrivals. *)
+ (* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
diff --git a/model/arrival/basic/task_arrival.v b/model/arrival/basic/task_arrival.v
index a55fa51a6..d9cb85399 100644
--- a/model/arrival/basic/task_arrival.v
+++ b/model/arrival/basic/task_arrival.v
@@ -72,7 +72,7 @@ Module TaskArrival.
Variable job_arrival: Job -> time.
Variable job_task: Job -> Task.
- (* Consider any arrival sequence with consistent, non-duplicate arrivals, ... *)
+ (* Consider any arrival sequence with consistent, duplicate-free arrivals, ... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_consistent_arrivals: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
diff --git a/model/arrival/jitter/arrival_bounds.v b/model/arrival/jitter/arrival_bounds.v
index 6828eb9dd..65de91276 100644
--- a/model/arrival/jitter/arrival_bounds.v
+++ b/model/arrival/jitter/arrival_bounds.v
@@ -24,7 +24,7 @@ Module ArrivalBounds.
Variable job_jitter: Job -> time.
Variable job_task: Job -> Task.
- (* Consider any job arrival sequence with consistent, non-duplicate arrivals... *)
+ (* Consider any job arrival sequence with consistent, duplicate-free arrivals... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
diff --git a/model/arrival/jitter/task_arrival.v b/model/arrival/jitter/task_arrival.v
index f92439414..cc27dc598 100644
--- a/model/arrival/jitter/task_arrival.v
+++ b/model/arrival/jitter/task_arrival.v
@@ -54,7 +54,7 @@ Module TaskArrivalWithJitter.
Variable job_jitter: Job -> time.
Variable job_task: Job -> Task.
- (* Consider any arrival sequence with consistent, non-duplicate arrivals, ... *)
+ (* Consider any arrival sequence with consistent, duplicate-free arrivals, ... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_consistent_arrivals: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
diff --git a/model/schedule/uni/jitter/valid_schedule.v b/model/schedule/uni/jitter/valid_schedule.v
new file mode 100644
index 000000000..46c8be09d
--- /dev/null
+++ b/model/schedule/uni/jitter/valid_schedule.v
@@ -0,0 +1,66 @@
+Require Import rt.util.all.
+Require Import rt.model.priority.
+Require Import rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.schedule.uni.jitter.schedule
+ rt.model.schedule.uni.jitter.platform.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(* In this file, we construct a predicate that defines a valid jitter-aware schedule
+ of a given task set. *)
+Module ValidJitterAwareSchedule.
+
+ Import UniprocessorScheduleWithJitter Priority Platform.
+
+ (** Basic Setup & Setting*)
+ Section DefiningValidSchedule.
+
+ Context {Task: eqType}.
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_task: Job -> Task.
+
+ (* Consider any job arrival sequence. *)
+ Variable arr_seq: arrival_sequence Job.
+
+ (* Assume any given job-level policy. *)
+ Variable higher_eq_priority: JLDP_policy Job.
+
+ (** Definition of the Jitter-Aware Schedule *)
+
+ (* Consider any job cost and job jitter functions. *)
+ Variable job_cost: Job -> time.
+ Variable job_jitter: Job -> time.
+
+ (* Let sched be any schedule. *)
+ Variable sched: schedule Job.
+
+ (* For sched to denote a valid jitter-aware schedule of ts, the following properties must hold. *)
+
+ (* 1) All scheduled jobs must come from the arrival sequence. *)
+ Let H1_jobs_come_from_arrival_sequence := jobs_come_from_arrival_sequence sched arr_seq.
+
+ (* 2) Jobs only execute after the jitter has passed. *)
+ Let H2_jobs_execute_after_jitter := jobs_execute_after_jitter job_arrival job_jitter sched.
+
+ (* 3) Jobs do not execute for longer than their costs. *)
+ Let H3_completed_jobs_dont_execute := completed_jobs_dont_execute job_cost sched.
+
+ (* 4) The schedule is work-conserving. *)
+ Let H4_work_conserving := work_conserving job_arrival job_cost job_jitter arr_seq sched.
+
+ (* 5) The schedule respects task priorities. *)
+ Let H5_respects_priority :=
+ respects_JLDP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.
+
+ (* All these properties can be combined into the following predicate. *)
+ Definition valid_jitter_aware_schedule :=
+ H1_jobs_come_from_arrival_sequence /\
+ H2_jobs_execute_after_jitter /\
+ H3_completed_jobs_dont_execute /\
+ H4_work_conserving /\
+ H5_respects_priority.
+
+ End DefiningValidSchedule.
+
+End ValidJitterAwareSchedule.
\ No newline at end of file
diff --git a/model/schedule/uni/response_time.v b/model/schedule/uni/response_time.v
index 49799fa77..4e18a8a92 100644
--- a/model/schedule/uni/response_time.v
+++ b/model/schedule/uni/response_time.v
@@ -7,7 +7,7 @@ Module ResponseTime.
Import UniprocessorSchedule SporadicTaskset TaskArrival.
- (* In this section, we define the notion of a response-time bound. *)
+ (* In this section, we define the notion of response-time bound. *)
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
@@ -22,23 +22,40 @@ Module ResponseTime.
(* ...and any uniprocessor schedule of these jobs. *)
Variable sched: schedule Job.
- (* Let tsk be any task that is to be analyzed. *)
- Variable tsk: sporadic_task.
-
(* For simplicity, let's define some local names. *)
Let job_has_completed_by := completed_by job_cost sched.
- (* Then, we say that R is a response-time bound of tsk in this schedule ... *)
- Variable R: time.
-
- (* ... iff any job j of tsk in this arrival sequence has
- completed by (job_arrival j + R). *)
- Definition is_response_time_bound_of_task :=
- forall j,
- arrives_in arr_seq j ->
- job_task j = tsk ->
- job_has_completed_by j (job_arrival j + R).
-
+ Section Job.
+
+ (* Given any job j, ... *)
+ Variable j: Job.
+
+ (* ...we say that R is a response-time bound of j in this schedule ... *)
+ Variable R: time.
+
+ (* ... iff j completes by (job_arrival j + R). *)
+ Definition is_response_time_bound_of_job := job_has_completed_by j (job_arrival j + R).
+
+ End Job.
+
+ Section Task.
+
+ (* Let tsk be any task that is to be analyzed. *)
+ Variable tsk: sporadic_task.
+
+ (* Then, we say that R is a response-time bound of tsk in this schedule ... *)
+ Variable R: time.
+
+ (* ... iff any job j of tsk in this arrival sequence has
+ completed by (job_arrival j + R). *)
+ Definition is_response_time_bound_of_task :=
+ forall j,
+ arrives_in arr_seq j ->
+ job_task j = tsk ->
+ is_response_time_bound_of_job j R.
+
+ End Task.
+
End ResponseTimeBound.
(* In this section, we prove some basic lemmas about response-time bounds. *)
@@ -61,7 +78,7 @@ Module ResponseTime.
completed_jobs_dont_execute job_cost sched.
(* For simplicity, let's define some local names. *)
- Let job_has_completed_by := completed_by job_cost sched.
+ Let response_time_bounded_by := is_response_time_bound_of_job job_arrival job_cost sched.
(* We begin by proving lemmas about job response-time bounds. *)
Section SpecificJob.
@@ -71,8 +88,7 @@ Module ResponseTime.
(* ...with response-time bound R. *)
Variable R: time.
- Hypothesis response_time_bound:
- job_has_completed_by j (job_arrival j + R).
+ Hypothesis response_time_bound: response_time_bounded_by j R.
(* Then, the service received by j at any time t' after its response time is 0. *)
Lemma service_after_job_rt_zero :
diff --git a/model/schedule/uni/susp/build_suspension_table.v b/model/schedule/uni/susp/build_suspension_table.v
new file mode 100644
index 000000000..0e7a1411c
--- /dev/null
+++ b/model/schedule/uni/susp/build_suspension_table.v
@@ -0,0 +1,264 @@
+Require Import rt.util.all.
+Require Import rt.model.suspension.
+Require Import rt.model.schedule.uni.susp.schedule.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq bigop fintype.
+
+(* In this file, we take any predicate that defines whether a job
+ is suspended at time t and build a table of suspension durations
+ that is valid up to time t. *)
+Module SuspensionTableConstruction.
+
+ Import ScheduleWithSuspensions Suspension.
+
+ Section BuildingSuspensionTable.
+
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_cost: Job -> time.
+
+ (** Basic Setup & Setting *)
+
+ (* Consider any job arrival sequence... *)
+ Variable arr_seq: arrival_sequence Job.
+
+ (* ...and any schedule of this arrival sequence... *)
+ Variable sched: schedule Job.
+
+ (* ...in which jobs must arrive to execute. *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute job_arrival sched.
+
+ (* Recall the instant following the last execution of a job, which
+ indicates the start of the latest suspension interval. *)
+ Let start_of_latest_suspension :=
+ time_after_last_execution job_arrival sched.
+
+ (* For simplicity, let's also define some local names. *)
+ Let job_completed_by := completed_by job_cost sched.
+
+ (** Construction of Suspension Table *)
+
+ (* We are going to construct a suspension table that is valid up to time t_max. *)
+ Variable t_max: time.
+
+ (* First, consider any predicate that indicates whether a job is suspended at time t. *)
+ Variable job_suspended_at: Job -> time -> bool.
+
+ (* Assume that this predicate only holds for jobs that have arrived... *)
+ Hypothesis H_arrived:
+ forall j t,
+ t < t_max ->
+ job_suspended_at j t ->
+ has_arrived job_arrival j t.
+
+ (* ...and that have not yet completed. *)
+ Hypothesis H_not_completed:
+ forall j t,
+ t < t_max ->
+ job_suspended_at j t ->
+ ~~ job_completed_by j t.
+
+ (* Assume that this predicate divides the timeline into continuous
+ suspension intervals, for any given amount of received service. *)
+ Hypothesis H_continuous_suspension:
+ forall j t t_susp,
+ t < t_max ->
+ job_suspended_at j t ->
+ start_of_latest_suspension j t <= t_susp < t ->
+ job_suspended_at j t_susp.
+
+ (* Then, we can construct a suspension table for the given suspension
+ predicate as follows. *)
+ Definition build_suspension_duration (j: Job) (s: time) :=
+ \sum_(0 <= t < t_max | service sched j t == s) job_suspended_at j t.
+
+ (* In order to prove that the suspension table matches the given predicate,
+ let's first prove some helper lemmas. *)
+ Section HelperLemmas.
+
+ (* First, we show that for any job j suspended at time t, the cumulative suspension
+ time before the beginning of the suspension is zero. *)
+ Lemma not_suspended_before_suspension_start:
+ forall j t,
+ t < t_max ->
+ job_suspended_at j t ->
+ let susp_start := start_of_latest_suspension j t in
+ let S := service sched j in
+ \sum_(0 <= i < susp_start | S i == S susp_start) job_suspended_at j i = 0.
+ Proof.
+ rename H_arrived into ARR, H_not_completed into COMPLETED,
+ H_continuous_suspension into CONT.
+ intros j t LTmax SUSPt X1 X2; rewrite /X1 /X2; clear X1 X2.
+ set ex := start_of_latest_suspension.
+ set S := service sched.
+ rewrite big_nat_cond big1 ?add0n //.
+ move => i /= /andP [LTex /eqP SAME].
+ apply/eqP; rewrite eqb0; apply/negP; intro SUSPi.
+ suff BUG: S j i != S j (ex j t) by rewrite SAME eq_refl in BUG.
+ rewrite neq_ltn; apply/orP; left.
+ rewrite /S/ex (same_service_since_last_execution job_arrival) //.
+ eapply less_service_before_start_of_suspension; last by apply LTex.
+ apply ARR; last by done.
+ apply ltn_trans with (n := ex j t); first by done.
+ apply leq_ltn_trans with (n := t); last by done.
+ by apply last_execution_bounded_by_identity, ARR.
+ Qed.
+
+ (* Next, we prove that after time t_max, no job suspends according to the table. *)
+ Lemma suspension_duration_no_suspension_after_t_max:
+ forall j t,
+ has_arrived job_arrival j t ->
+ t_max <= t ->
+ ~~ suspended_at job_arrival job_cost build_suspension_duration sched j t.
+ Proof.
+ have ZERO := not_suspended_before_suspension_start.
+ rename H_arrived into ARR.
+ intros j t ARRt GEmax.
+ rewrite /suspended_at negb_and; apply/orP; right.
+ rewrite negb_and -leqNgt; apply/orP; right.
+ rewrite /suspension_duration /build_suspension_duration.
+ set ex := _ job_arrival _.
+ set S := service sched.
+ set susp_at := job_suspended_at.
+ case (ltnP (ex j t) t_max) => [LT | GE].
+ {
+ apply leq_trans with (n := t_max); last by done.
+ rewrite big_mkcond /=.
+ rewrite -> big_cat_nat with (n := ex j t); [simpl | by done | by apply ltnW].
+ rewrite big_nat_cond big1 ?add0n.
+ {
+ apply leq_trans with (n := ex j t + \sum_(ex j t <= i < t_max) 1);
+ last by simpl_sum_const; rewrite subnKC // ltnW.
+ by rewrite leq_add2l; apply leq_sum; intros i _; case: ifP => //_; apply leq_b1.
+ }
+ move => /= i /andP [LTex _]; case: ifP => /eqP SERV; last by done.
+ apply/eqP; rewrite eqb0; apply/negP; intro SUSPi.
+ suff BUG: S j i != S j (ex j t) by rewrite SERV eq_refl in BUG.
+ rewrite neq_ltn; apply/orP; left.
+ rewrite /S/ex same_service_since_last_execution //.
+ eapply less_service_before_start_of_suspension; last by apply LTex.
+ by apply ARR; first by apply:(ltn_trans LTex).
+ }
+ {
+ rewrite big_nat_cond big1 ?addn0;
+ first by apply last_execution_bounded_by_identity.
+ move => /= i /andP [LTmax /eqP SERV].
+ apply/eqP; rewrite eqb0; apply/negP; intro SUSPi.
+ suff BUG: S j i != S j (ex j t) by rewrite SERV eq_refl in BUG.
+ rewrite neq_ltn; apply/orP; left.
+ rewrite /S/ex same_service_since_last_execution //.
+ eapply less_service_before_start_of_suspension; first by apply ARR.
+ by apply: (leq_trans LTmax); apply GE.
+ }
+ Qed.
+
+ End HelperLemmas.
+
+ (* Using the lemmas above, we prove that up to time t_max, the constructed suspension
+ table matches the given suspension predicate. *)
+ Lemma suspension_duration_matches_predicate_up_to_t_max:
+ forall j t,
+ t < t_max ->
+ job_suspended_at j t =
+ suspended_at job_arrival job_cost build_suspension_duration sched j t.
+ Proof.
+ have ZERO := not_suspended_before_suspension_start.
+ rename H_arrived into ARR, H_not_completed into COMPLETED,
+ H_continuous_suspension into CONT.
+ intros j t LEmax.
+ apply/idP/idP.
+ {
+ intros SUSPt.
+ set ex := time_after_last_execution job_arrival sched.
+ set S := service sched.
+ set susp_at := job_suspended_at.
+ have LEt: ex j t <= t.
+ by apply last_execution_bounded_by_identity, ARR.
+ apply/andP; split; first by apply COMPLETED.
+ apply/andP; split; first by done.
+ rewrite /suspension_duration /build_suspension_duration.
+ rewrite -/ex -/S -/susp_at.
+ apply leq_trans with (n := ex j t + \sum_(ex j t <= t0 < t.+1) 1);
+ first by simpl_sum_const; rewrite subnKC // ltnW // ltnS.
+ rewrite leq_add2l.
+ rewrite -> big_cat_nat with (m := 0) (n := ex j t); rewrite //=;
+ last by apply leq_trans with (n := t); last by apply ltnW.
+ rewrite ZERO // add0n.
+ apply leq_trans with (n := \sum_(ex j t<= i <t.+1|S j i==S j (ex j t)) susp_at j i);
+ last by rewrite big_mkcond [X in _ <= X]big_mkcond /= extend_sum.
+ rewrite [X in _ <= X]big_mkcond /=.
+ apply leq_sum_nat; move => i /andP [GE LT] _.
+ have SAMEserv: S j i == S j (ex j t).
+ {
+ rewrite ltnS in LT.
+ rewrite eqn_leq; apply/andP; split; last by apply extend_sum.
+ by rewrite /S/ex same_service_since_last_execution ?extend_sum.
+ }
+ rewrite SAMEserv lt0n eqb0 negbK.
+ rewrite ltnS leq_eqVlt in LT.
+ move: LT => /orP [/eqP EQ | LT]; subst; first by done.
+ by apply CONT with (t := t); try (apply/andP; split).
+ }
+ {
+ move => /andP [NOTCOMP /andP [GE LT]].
+ rewrite /suspension_duration /build_suspension_duration in LT.
+ set S := service sched in LT.
+ set susp_at := job_suspended_at in LT *.
+ set ex := _ job_arrival _ in GE LT.
+ rewrite -> big_cat_nat with (m := 0) (n := ex j t) in LT; rewrite //= in LT;
+ last by apply leq_trans with (n := t); last by apply ltnW.
+ rewrite big_nat_cond big1 ?add0n in LT; last first.
+ {
+ move => i /= /andP [LTex /eqP SAME].
+ apply/eqP; rewrite eqb0; apply/negP; intro SUSPi.
+ suff BUG: S j i != S j (ex j t) by rewrite SAME eq_refl in BUG.
+ rewrite neq_ltn; apply/orP; left.
+ rewrite /S/ex same_service_since_last_execution //.
+ eapply less_service_before_start_of_suspension; last by apply LTex.
+ by apply ARR; first by apply:(ltn_trans LTex); apply:(leq_ltn_trans _ LEmax).
+ }
+ case (boolP ([exists t0:'I_t_max,(S j t0==S j (ex j t))&&susp_at j t0]));last first.
+ {
+ rewrite negb_exists; move => /forallP ALL.
+ rewrite big_nat_cond big1 in LT; first by rewrite addn0 ltnNge GE in LT.
+ move => i /andP [/andP [_ LTmax] EQ].
+ specialize (ALL (Ordinal LTmax)).
+ by rewrite EQ /= in ALL; apply/eqP; rewrite eqb0.
+ }
+ move => /existsP [t0 /andP [/eqP EQ SUSP0]].
+ have MAX := @arg_maxP _ t0 (fun x=>(S j x == S j (ex j t)) && susp_at j x) id.
+ feed MAX; simpl in MAX; first by rewrite EQ eq_refl SUSP0.
+ move: MAX => [m /andP [/eqP EQserv SUSPm] ALL]; clear EQ SUSP0 t0.
+ case (ltnP t m) => [LTm | GEm].
+ {
+ apply CONT with (t := m); try done; apply/andP; split; last by done.
+ rewrite /start_of_latest_suspension.
+ rewrite (same_service_implies_same_last_execution _ _ _ _ t); first by done.
+ rewrite -/S EQserv /S /ex /start_of_latest_suspension.
+ by rewrite same_service_since_last_execution.
+ }
+ rewrite leq_eqVlt in GEm; move: GEm => /orP [/eqP EQm | GTm]; subst; first by done.
+ apply contraT; intro NOTSUSP.
+ set SUM := (X in _ < _ + X) in LT.
+ suff BUG: t >= ex j t + SUM by rewrite leqNgt LT in BUG.
+ rewrite /SUM in LT *; clear SUM LT.
+ apply leq_trans with (n := ex j t + (t - ex j t)); last by rewrite subnKC.
+ rewrite leq_add2l.
+ rewrite -> big_cat_nat with (n := t); rewrite //=; last by apply ltnW.
+ rewrite [X in _ + X <= _]big_nat_cond [X in _ + X <= _]big1 ?addn0.
+ {
+ apply leq_trans with (n := \sum_(ex j t <= i < t) 1); last by simpl_sum_const.
+ by rewrite big_mkcond; apply leq_sum; intros i _; case: ifP => // _; apply leq_b1.
+ }
+ move => i /andP [/andP [GEi LTi] /eqP SERVi].
+ apply/eqP; rewrite eqb0; apply/negP; intro SUSPi.
+ specialize (ALL (Ordinal LTi)); rewrite /= in ALL.
+ feed ALL; first by rewrite SERVi eq_refl SUSPi.
+ suff BUG: m >= t by rewrite leqNgt GTm in BUG.
+ by apply: (leq_trans GEi).
+ }
+ Qed.
+
+ End BuildingSuspensionTable.
+
+End SuspensionTableConstruction.
\ No newline at end of file
diff --git a/model/schedule/uni/susp/last_execution.v b/model/schedule/uni/susp/last_execution.v
index bf1c65f82..5c3f4979b 100644
--- a/model/schedule/uni/susp/last_execution.v
+++ b/model/schedule/uni/susp/last_execution.v
@@ -356,6 +356,53 @@ Module LastExecution.
Qed.
End ExistsIntermediateExecution.
+
+ (* In this section we prove that before the last execution the job
+ must have received strictly less service. *)
+ Section LessServiceBeforeLastExecution.
+
+ (* Let t be any time... *)
+ Variable t: time.
+
+ (* ...and consider any earlier time t0 no earlier than the arrival of job j... *)
+ Variable t0: time.
+ Hypothesis H_no_earlier_than_arrival: has_arrived job_arrival j t0.
+
+ (* ...and before the last execution of job j (with respect to time t). *)
+ Hypothesis H_before_last_execution: t0 < time_after_last_execution j t.
+
+ (* Then, we can prove that the service received by j before time t0
+ is strictly less than the service received by j before time t. *)
+ Lemma less_service_before_start_of_suspension:
+ service sched j t0 < service sched j t.
+ Proof.
+ rename H_no_earlier_than_arrival into ARR, H_before_last_execution into LT.
+ set ex := time_after_last_execution in LT.
+ set S := service sched.
+ case EX:([exists t0:'I_t, scheduled_at sched j t0]); last first.
+ {
+ rewrite /ex /time_after_last_execution EX in LT.
+ apply leq_trans with (p := t0) in LT; last by done.
+ by rewrite ltnn in LT.
+ }
+ {
+ rewrite /ex /time_after_last_execution EX in LT.
+ set m := (X in _ < X + 1) in LT.
+ apply leq_ltn_trans with (n := S j m);
+ first by rewrite -/m addn1 ltnS in LT; apply extend_sum.
+ move: EX => /existsP [t' SCHED'].
+ have LTt: m < t by apply bigmax_ltn_ord with (i0 := t').
+ rewrite /S /service /service_during.
+ rewrite -> big_cat_nat with (p := t) (n := m); [simpl | by done | by apply ltnW].
+ rewrite -addn1 leq_add2l; destruct t; first by done.
+ rewrite big_nat_recl //.
+ apply leq_trans with (n := scheduled_at sched j m); last by apply leq_addr.
+ rewrite lt0n eqb0 negbK.
+ by apply bigmax_pred with (i0 := t').
+ }
+ Qed.
+
+ End LessServiceBeforeLastExecution.
End Lemmas.
diff --git a/model/schedule/uni/susp/suspension_intervals.v b/model/schedule/uni/susp/suspension_intervals.v
index 1222b486b..6177442ac 100644
--- a/model/schedule/uni/susp/suspension_intervals.v
+++ b/model/schedule/uni/susp/suspension_intervals.v
@@ -44,7 +44,7 @@ Module SuspensionIntervals.
(Note that suspension_start can return time t itself.) *)
Let suspension_start := time_after_last_execution job_arrival sched j t.
- (* Next, using the service received by j in the interval [0, suspension_start), ... *)
+ (* Next, using the service received by j in the interval [0, suspension_start),...*)
Let current_service := service sched j suspension_start.
(* ... we recall the duration of the suspension expected for job j after having
@@ -151,7 +151,8 @@ Module SuspensionIntervals.
case: (boolP (completed_by _ _ _ _)) => [COMP | NOTCOMP];
first by apply completed_implies_not_scheduled in COMP;
first by rewrite SCHED' in COMP.
- rewrite andTb (same_service_implies_same_last_execution _ _ _ _ suspension_start) //.
+ rewrite andTb (same_service_implies_same_last_execution _ _ _ _
+ suspension_start) //.
rewrite /suspension_start last_execution_idempotent //.
apply/andP; split; first by apply leq_addr.
by rewrite ltn_add2l.
@@ -289,19 +290,20 @@ Module SuspensionIntervals.
total_suspension_of_j, total_suspension.
intros t1 t2.
apply leq_trans with (n := \sum_(0 <= s < job_cost j)
- \sum_(t1 <= t < t2 | service sched j t == s) suspended_at j t).
+ \sum_(t1 <= t < t2 | service sched j t == s) suspended_at j t).
{
rewrite (exchange_big_dep_nat (fun x => true)) //=.
apply leq_sum; intros s _.
destruct (boolP (suspended_at j s)) as [SUSP | NOTSUSP]; last by done.
rewrite (big_rem (service sched j s)); first by rewrite eq_refl.
rewrite mem_index_iota; apply/andP; split; first by done.
- rewrite ltn_neqAle; apply/andP; split; last by apply cumulative_service_le_job_cost.
+ rewrite ltn_neqAle; apply/andP; split;
+ last by apply cumulative_service_le_job_cost.
by apply suspended_implies_not_completed in SUSP.
}
{
apply leq_sum_nat; move => s /andP [_ LT] _.
- destruct (boolP [exists t: 'I_t2, (t >= t1) && (service sched j t == s)]) as [EX | ALL];
+ destruct (boolP [exists t:'I_t2, (t>=t1)&& (service sched j t==s)]) as [EX|ALL];
last first.
{
rewrite negb_exists in ALL; move: ALL => /forallP ALL.
@@ -374,13 +376,13 @@ Module SuspensionIntervals.
Proof.
rename H_j_has_completed into COMP, H_jobs_must_arrive_to_execute into ARR.
have EARLIER := exists_last_execution_with_smaller_service job_arrival
- job_cost sched ARR j t COMP.
+ job_cost sched ARR j t COMP.
apply/eqP; rewrite eqn_leq; apply/andP; split;
first by apply cumulative_suspension_le_total_suspension.
rewrite /total_suspension /cumulative_suspension /cumulative_suspension_during.
move: COMP => /eqP COMP.
apply leq_trans with (n := \sum_(0 <= s < job_cost j)
- \sum_(0 <= t0 < t | service sched j t0 == s) suspended_at j t0);
+ \sum_(0 <= t0 < t | service sched j t0 == s) suspended_at j t0);
last first.
{
rewrite (exchange_big_dep_nat (fun x => true)) //=.
@@ -409,7 +411,7 @@ Module SuspensionIntervals.
move: (EARLIER s LTs) => [t' EQ'].
apply leq_trans with (n := \sum_(0 <= t0 < t | (service sched j t0 == s) &&
- (b t' <= t0 < b t' + n (service sched j (b t')))) 1); last first.
+ (b t' <= t0 < b t' + n (service sched j (b t')))) 1); last first.
{
rewrite big_mkcond [\sum_(_ <= _ < _ | _ == s)_]big_mkcond.
apply leq_sum_nat; move => i /andP [_ LTi] _.
@@ -421,10 +423,11 @@ Module SuspensionIntervals.
by apply: (leq_ltn_trans _ LTs); apply eq_leq; apply/eqP.
}
{
- apply leq_trans with (n := \sum_(b t' <= t0 < b t' + n (service sched j (b t')) |
- (0 <= t0 < t) && (service sched j t0 == s)) 1).
+ apply leq_trans with (n := \sum_(b t'<= t0< b t'+ n (service sched j (b t')) |
+ (0 <= t0 < t) && (service sched j t0 == s)) 1).
{
- apply leq_trans with (n := \sum_(b t' <= t0 < b t' + n (service sched j (b t'))) 1);
+ apply leq_trans with (n := \sum_(b t' <= t0 < b t'
+ + n (service sched j (b t'))) 1);
first by simpl_sum_const; rewrite addKn -EQ'.
rewrite [in X in _ <= X]big_mkcond /=.
apply leq_sum_nat; move => i /andP [LEi GTi] _.
@@ -463,6 +466,55 @@ Module SuspensionIntervals.
End SuspendsForTotalSuspension.
+ (* In this section, we prove that a job executes just before it starts suspending. *)
+ Section ExecutionBeforeSuspension.
+
+ (* Assume that jobs do not execute before they arrive... *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute job_arrival sched.
+
+ (* ...and nor after completion. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost sched.
+
+ (* Assume that the schedule respects self-suspensions. *)
+ Hypothesis H_respects_self_suspensions: respects_self_suspensions.
+
+ (* Let j be any job... *)
+ Variable j: Job.
+
+ (* ...that has arrived by some time t. *)
+ Variable t: time.
+ Hypothesis H_arrived: has_arrived job_arrival j t.
+
+ (* If job j is not suspended at time t, but starts to suspend at time t + 1, ... *)
+ Hypothesis H_not_suspended_at_t: ~~ suspended_at j t.
+ Hypothesis H_begins_suspension: suspended_at j t.+1.
+
+ (* ...then j must be scheduled at time t. *)
+ Lemma executes_before_suspension:
+ scheduled_at sched j t.
+ Proof.
+ rename H_not_suspended_at_t into NOTSUSPs, H_begins_suspension into SUSPs'.
+ move: SUSPs' => /andP [NOTCOMP' /andP [GE LT]].
+ apply contraT; intro NOTSCHED.
+ suff BUG: suspended_at j t by rewrite BUG in NOTSUSPs.
+ apply suspended_in_suspension_interval with (t := t.+1); try done.
+ {
+ apply contraT; rewrite negbK; intro COMP.
+ suff COMP': completed_by job_cost sched j t.+1 by rewrite COMP' in NOTCOMP'.
+ by apply completion_monotonic with (t0 := t).
+ }
+ apply/andP; split; last by apply: (leq_ltn_trans _ LT).
+ apply leq_trans with (n := time_after_last_execution job_arrival sched j t);
+ last by apply last_execution_bounded_by_identity.
+ apply eq_leq, same_service_implies_same_last_execution.
+ rewrite /service /service_during big_nat_recr //= /service_at.
+ by apply negbTE in NOTSCHED; rewrite NOTSCHED.
+ Qed.
+
+ End ExecutionBeforeSuspension.
+
End Lemmas.
End DefiningSuspensionIntervals.
diff --git a/model/schedule/uni/susp/valid_schedule.v b/model/schedule/uni/susp/valid_schedule.v
new file mode 100644
index 000000000..2ce70a272
--- /dev/null
+++ b/model/schedule/uni/susp/valid_schedule.v
@@ -0,0 +1,75 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.schedule.uni.susp.schedule
+ rt.model.schedule.uni.susp.platform.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(* In this file, we construct a predicate that defines a valid suspension-aware schedule. *)
+Module ValidSuspensionAwareSchedule.
+
+ Import ScheduleWithSuspensions Suspension Priority PlatformWithSuspensions.
+
+ (** Basic Setup & Setting*)
+ Section DefiningValidSchedule.
+
+ Context {Task: eqType}.
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_task: Job -> Task.
+
+ (* Consider any job arrival sequence. *)
+ Variable arr_seq: arrival_sequence Job.
+
+ (* Assume any given job-level policy... *)
+ Variable higher_eq_priority: JLDP_policy Job.
+
+ (* ...and job suspension times. *)
+ Variable job_suspension_duration: job_suspension Job.
+
+ (** Definition of the Suspension-Aware Schedule *)
+
+ (* Let job_cost denote any job cost function... *)
+ Variable job_cost: Job -> time.
+
+ (* ...and let sched_susp be any schedule. *)
+ Variable sched_susp: schedule Job.
+
+ (* For sched_susp to denote a valid suspension-aware schedule,
+ the following properties must be satisfied. *)
+
+ (* 1) All scheduled jobs must come from the arrival sequence. *)
+ Let H1_jobs_come_from_arrival_sequence := jobs_come_from_arrival_sequence sched_susp arr_seq.
+
+ (* 2) Jobs only execute after they arrive. *)
+ Let H2_jobs_must_arrive_to_execute := jobs_must_arrive_to_execute job_arrival sched_susp.
+
+ (* 3) Jobs do not execute for longer than their costs. *)
+ Let H3_completed_jobs_dont_execute := completed_jobs_dont_execute job_cost sched_susp.
+
+ (* 4) The schedule is work-conserving if there are non-suspended jobs. *)
+ Let H4_work_conserving :=
+ work_conserving job_arrival job_cost job_suspension_duration arr_seq sched_susp.
+
+ (* 5) The schedule respects task priorities. *)
+ Let H5_respects_priority :=
+ respects_JLDP_policy job_arrival job_cost job_suspension_duration arr_seq
+ sched_susp higher_eq_priority.
+
+ (* 6) Suspended jobs are not allowed to be schedule. *)
+ Let H6_respects_self_suspensions :=
+ respects_self_suspensions job_arrival job_cost job_suspension_duration sched_susp.
+
+ (* All these properties can be combined into the following predicate. *)
+ Definition valid_suspension_aware_schedule :=
+ H1_jobs_come_from_arrival_sequence /\
+ H2_jobs_must_arrive_to_execute /\
+ H3_completed_jobs_dont_execute /\
+ H4_work_conserving /\
+ H5_respects_priority /\
+ H6_respects_self_suspensions.
+
+ End DefiningValidSchedule.
+
+End ValidSuspensionAwareSchedule.
\ No newline at end of file
--
GitLab