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

@@ -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.

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.

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.

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.
 

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.
 

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.
 

analysis/uni/susp/dynamic/jitter/jitter_schedule.v

+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

analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v

+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

analysis/uni/susp/dynamic/jitter/rta_by_reduction.v

+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

analysis/uni/susp/dynamic/jitter/taskset_membership.v

+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

analysis/uni/susp/dynamic/jitter/taskset_rta.v

+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

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.

analysis/uni/susp/sustainability/allcosts/reduction.v

+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

analysis/uni/susp/sustainability/singlecost/reduction.v

+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

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.

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.