FP: switch from basic readiness to sequential readiness

model/schedule/preemption_time.v

@@ -11,7 +11,8 @@ Require Export prosa.model.preemption.parameter.
     progress of the currently scheduled job.
 
     NB: For legacy reasons, the following definition are currently specific to
-    ideal uniprocessor schedules. Lifting this assumption is future work. *)
+    ideal uniprocessor schedules. Lifting this assumption is future work
+    (https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/76). *)
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require prosa.model.processor.ideal.

results/fixed_priority/rta/bounded_nps.v

@@ -7,9 +7,6 @@ Require Export prosa.results.fixed_priority.rta.bounded_pi.
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
 
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import prosa.model.readiness.basic.
-
 (** * RTA for FP-schedulers with Bounded Non-Preemptive Segments *)
 
 (** In this section we instantiate the Abstract RTA for FP-schedulers
@@ -33,25 +30,37 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.
+  Context `{Arrival : JobArrival Job}.
+  Context `{Cost : JobCost Job}.
+
+  (** Consider an FP policy that indicates a higher-or-equal priority
+      relation, and assume that the relation is reflexive and
+      transitive. *)
+  Context `{FP_policy Task}.
+  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+  Hypothesis H_priority_is_transitive : transitive_priorities.
   
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
   Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
-  (** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
+  (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
   Variable sched : schedule (ideal.processor_state Job).
-  Hypothesis H_jobs_come_from_arrival_sequence:
-    jobs_come_from_arrival_sequence sched arr_seq.
+  
+  (** ... allow for any work-bearing notion of job readiness, ... *)
+  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
+  (** ... and assume that the schedule is valid.  *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** We also assume that jobs do not execute before their arrival or after completion. *)
   Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
   Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
   
   (** In addition, we assume the existence of a function mapping jobs
-      to theirs preemption points ... *)
+      to their preemption points ... *)
   Context `{JobPreemptable Job}.
 
   (** ... and assume that it defines a valid preemption
@@ -59,23 +68,16 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
     valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
 
-  (** Consider an FP policy that indicates a higher-or-equal priority
-      relation, and assume that the relation is reflexive and
-      transitive. *)
-  Context `{FP_policy Task}.
-  Hypothesis H_priority_is_reflexive : reflexive_priorities.
-  Hypothesis H_priority_is_transitive : transitive_priorities.
-  
-  (** Assume we have sequential tasks, i.e, jobs from the same task
-      execute in the order of their arrival. *)
-  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
-
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
   (** ... and the schedule respects the policy defined by the [job_preemptable]
      function (i.e., jobs have bounded non-preemptive segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+
+  (** Assume we have sequential tasks, i.e, jobs from the 
+      same task execute in the order of their arrival. *)
+  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
   
   (** Consider an arbitrary task set ts, ... *)
   Variable ts : list Task.
@@ -166,6 +168,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         arr_seq sched tsk blocking_bound.
     Proof.
       intros j ARR TSK POS t1 t2 PREF.
+      move: H_sched_valid => [CARR MBR].
       case NEQ: (t2 - t1 <= blocking_bound). 
       { apply leq_trans with (t2 - t1); last by done.
         rewrite /cumulative_priority_inversion /is_priority_inversion.

results/fixed_priority/rta/bounded_pi.v

 Require Export prosa.model.schedule.priority_driven.
-Require Export prosa.analysis.facts.busy_interval.busy_interval.
 Require Import prosa.analysis.abstract.ideal_jlfp_rta.
+Require Export prosa.analysis.facts.busy_interval.busy_interval.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
 
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import prosa.model.readiness.basic.
 
 (** * Abstract RTA for FP-schedulers with Bounded Priority Inversion *)
 (** In this module we instantiate the Abstract Response-Time analysis
@@ -34,21 +32,35 @@ Section AbstractRTAforFPwithArrivalCurves.
   (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.
+  Context {Arrival : JobArrival Job}.
+  Context {Cost : JobCost Job}.
   Context `{JobPreemptable Job}.
-
+  
+  (** Consider an FP policy that indicates a higher-or-equal priority relation,
+     and assume that the relation is reflexive. Note that we do not relate 
+     the FP policy with the scheduler. However, we define functions for 
+     Interference and Interfering Workload that actively use the concept of 
+     priorities. We require the FP policy to be reflexive, so a job cannot 
+     cause lower-priority interference (i.e. priority inversion) to itself. *)
+  Context `{FP_policy Task}.
+  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+  
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
   Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
-  
-  (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
+
+  (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
   Variable sched : schedule (ideal.processor_state Job).
-  Hypothesis H_jobs_come_from_arrival_sequence:
-    jobs_come_from_arrival_sequence sched arr_seq.
+  
+  (** ... allow for any work-bearing notion of job readiness, ... *)
+  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** ... and assume that the schedule is valid.  *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
+  (** We also assume that jobs do not execute before their arrival or after completion. *)
   Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
   Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
   
@@ -63,9 +75,9 @@ Section AbstractRTAforFPwithArrivalCurves.
   Hypothesis H_work_conserving : work_conserving_cl.
 
   (** Assume we have sequential tasks, i.e, jobs from the 
-     same task execute in the order of their arrival. *)
+      same task execute in the order of their arrival. *)
   Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
-
+  
   (** Assume that a job cost cannot be larger than a task cost. *)
   Hypothesis H_valid_job_cost:
     arrivals_have_valid_job_costs arr_seq.
@@ -96,15 +108,7 @@ Section AbstractRTAforFPwithArrivalCurves.
      any job of task [tsk] [job_rtct] is bounded by [task_rtct]. *)
   Hypothesis H_valid_run_to_completion_threshold:
     valid_task_run_to_completion_threshold arr_seq tsk.
-  
-  (** Consider an FP policy that indicates a higher-or-equal priority relation,
-     and assume that the relation is reflexive. Note that we do not relate 
-     the FP policy with the scheduler. However, we define functions for 
-     Interference and Interfering Workload that actively use the concept of 
-     priorities. We require the FP policy to be reflexive, so a job cannot 
-     cause lower-priority interference (i.e. priority inversion) to itself. *)
-  Context `{FP_policy Task}.
-  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+
   
   (** For clarity, let's define some local names. *)
   Let job_pending_at := pending sched.
@@ -190,6 +194,7 @@ Section AbstractRTAforFPwithArrivalCurves.
         rewrite negb_or /is_priority_inversion /is_priority_inversion
                 /is_interference_from_another_hep_job.
         move => /andP [HYP1 HYP2].
+        move: H_sched_valid => [CARR MBR].
         case SCHED: (sched t) => [s | ].
         + rewrite SCHED in HYP1, HYP2.
           move: HYP1 HYP2. 
@@ -216,9 +221,11 @@ Section AbstractRTAforFPwithArrivalCurves.
       interference_and_workload_consistent_with_sequential_tasks
         arr_seq sched tsk interference interfering_workload.
     Proof.
-      intros j t1 t2 ARR TSK POS BUSY. 
+      intros j t1 t2 ARR TSK POS BUSY.
+      move: H_sched_valid => [CARR MBR].
       eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto with basic_facts.
-      eapply all_jobs_have_completed_equiv_workload_eq_service; eauto 2; intros s ARRs TSKs.
+      eapply all_jobs_have_completed_equiv_workload_eq_service; eauto with basic_facts.
+      intros s ARRs TSKs.
       move: (BUSY) => [[_ [QT _]] _].
       apply QT.
       - by apply in_arrivals_implies_arrived in ARRs.
@@ -238,6 +245,7 @@ Section AbstractRTAforFPwithArrivalCurves.
       busy_intervals_are_bounded_by arr_seq sched tsk interference interfering_workload L.
     Proof.
       intros j ARR TSK POS.
+      move: H_sched_valid => [CARR MBR].
       edestruct (exists_busy_interval) with (delta := L) as [t1 [t2 [T1 [T2 GGG]]]]; eauto 2.
       { by intros; rewrite {2}H_fixed_point leq_add //; apply total_workload_le_total_rbf'. }
       exists t1, t2; split; first by done.
@@ -263,7 +271,8 @@ Section AbstractRTAforFPwithArrivalCurves.
         arr_seq sched tsk interference interfering_workload (fun t A R => IBF R).
     Proof.
       intros ? ? ? ? ARR TSK ? NCOMPL BUSY; simpl.
-      move: (posnP (@job_cost _ H3 j)) => [ZERO|POS].
+      move: H_sched_valid => [CARR MBR].
+      move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
       { by exfalso; rewrite /completed_by ZERO in  NCOMPL. }
       eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto 2 with basic_facts.
       rewrite /interference; erewrite cumulative_task_interference_split; eauto 2 with basic_facts; last first.
@@ -285,11 +294,10 @@ Section AbstractRTAforFPwithArrivalCurves.
         apply leq_trans with
             (workload_of_jobs
                (fun jhp : Job => (FP_to_JLFP _ _) jhp j && (job_task jhp != job_task j))
-               (arrivals_between arr_seq t1 (t1 + R0))
-            ).
-        { by apply service_of_jobs_le_workload; last apply ideal_proc_model_provides_unit_service.  }
-        { rewrite  /workload_of_jobs /total_ohep_rbf /total_ohep_request_bound_function_FP.
-            by rewrite -TSK; apply total_workload_le_total_rbf.
+               (arrivals_between arr_seq t1 (t1 + R0))).
+        { by apply service_of_jobs_le_workload; first apply ideal_proc_model_provides_unit_service. } 
+        { rewrite /workload_of_jobs /total_ohep_rbf /total_ohep_request_bound_function_FP.
+          by rewrite -TSK; apply total_workload_le_total_rbf.
         }
       }
     Qed.
@@ -359,7 +367,8 @@ Section AbstractRTAforFPwithArrivalCurves.
     response_time_bounded_by tsk R.
   Proof.
     intros js ARRs TSKs.
-    move: (posnP (@job_cost _ H3 js)) => [ZERO|POS].
+    move: H_sched_valid => [CARR MBR].
+    move: (posnP (@job_cost _ Cost js)) => [ZERO|POS].
     { by rewrite /job_response_time_bound /completed_by ZERO. }
     eapply uniprocessor_response_time_bound_seq; eauto 3.
     - by apply instantiated_i_and_w_are_consistent_with_schedule. 

results/fixed_priority/rta/floating_nonpreemptive.v

 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
+Require Export prosa.analysis.facts.readiness.sequential.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
@@ -8,9 +9,9 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
 (** In this module we prove the RTA theorem for floating non-preemptive regions FP model. *)
 
 (** Throughout this file, we assume the FP priority policy, ideal uni-processor 
-    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+    schedules, and the sequential readiness model. *)
 Require Import prosa.model.processor.ideal.
-Require Import prosa.model.readiness.basic.
+Require Import prosa.model.readiness.sequential.
 
 (** Furthermore, we assume the task model with floating non-preemptive regions. *)
 Require Import prosa.model.preemption.limited_preemptive.
@@ -64,13 +65,16 @@ Section RTAforFloatingModelwithArrivalCurves.
   (** Let [tsk] be any task in ts that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
+  
+  (** Recall that we assume sequential readiness. *)
+  Instance sequential_readiness : JobReady _ _ :=
+    sequential_ready_instance arr_seq.
 
-  (** Next, consider any ideal uni-processor schedule with limited preemptions of this arrival sequence ... *)
+  (** Next, consider any valid ideal uni-processor schedule with with
+      limited preemptions of this arrival sequence ... *)
   Variable sched : schedule (ideal.processor_state Job).
-  Hypothesis H_jobs_come_from_arrival_sequence:
-    jobs_come_from_arrival_sequence sched arr_seq.
-  Hypothesis H_schedule_with_limited_preemptions:
-    schedule_respects_preemption_model arr_seq sched.
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+  Hypothesis H_schedule_with_limited_preemptions : schedule_respects_preemption_model arr_seq sched.
   
   (** ... where jobs do not execute before their arrival or after completion. *)
   Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
@@ -81,11 +85,7 @@ Section RTAforFloatingModelwithArrivalCurves.
   Context `{FP_policy Task}.
   Hypothesis H_priority_is_reflexive : reflexive_priorities.
   Hypothesis H_priority_is_transitive : transitive_priorities.
-
-  (** Assume we have sequential tasks, i.e, jobs from the 
-      same task execute in the order of their arrival. *)
-  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
-
+  
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
@@ -153,10 +153,12 @@ Section RTAforFloatingModelwithArrivalCurves.
     move: (LIMJ) => [BEG [END _]].
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.
     all: eauto 2 with basic_facts.
-    intros A SP.
-    rewrite subnn subn0.
-    destruct (H_R_is_maximum _ SP) as [F [EQ LE]].
+    - by apply sequential_readiness_implies_work_bearing_readiness.
+    - by apply sequential_readiness_implies_sequential_tasks.
+    - intros A SP.
+      rewrite subnn subn0.
+      destruct (H_R_is_maximum _ SP) as [F [EQ LE]].
       by exists F; rewrite addn0; split.
   Qed.
-
+           
 End RTAforFloatingModelwithArrivalCurves.

results/fixed_priority/rta/fully_nonpreemptive.v

 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
+Require Export prosa.analysis.facts.readiness.sequential.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
@@ -9,9 +10,9 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
 (** In this module we prove the RTA theorem for the fully non-preemptive FP model. *)
 
 (** Throughout this file, we assume the FP priority policy, ideal uni-processor 
-    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+    schedules, and the sequential readiness model. *)
 Require Import prosa.model.processor.ideal.
-Require Import prosa.model.readiness.basic.
+Require Import prosa.model.readiness.sequential.
 
 (** Furthermore, we assume the fully non-preemptive task model. *)
 Require Import prosa.model.task.preemption.fully_nonpreemptive.
@@ -57,11 +58,14 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
+  (** Recall that we assume sequential readiness. *)
+  Instance sequential_readiness : JobReady _ _ :=
+    sequential_ready_instance arr_seq.
+  
   (** Next, consider any ideal non-preemptive uniprocessor schedule of
       this arrival sequence ... *)
   Variable sched : schedule (ideal.processor_state Job).
-  Hypothesis H_jobs_come_from_arrival_sequence:
-    jobs_come_from_arrival_sequence sched arr_seq.
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
   Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule  sched.
 
   (** ... where jobs do not execute before their arrival or after completion. *)
@@ -74,10 +78,6 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
   Hypothesis H_priority_is_reflexive : reflexive_priorities.
   Hypothesis H_priority_is_transitive : transitive_priorities.
   
-  (** Assume we have sequential tasks, i.e, tasks from the same task
-      execute in the order of their arrival. *)
-  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
-
   (** Next, we assume that the schedule is a work-conserving schedule ... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
@@ -153,7 +153,9 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
     }
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
         (L0 := L).
-    all: eauto 2 with basic_facts. 
+    all: eauto 2 with basic_facts.
+    - by apply sequential_readiness_implies_work_bearing_readiness.
+    - by apply sequential_readiness_implies_sequential_tasks.
   Qed.
 
 End RTAforFullyNonPreemptiveFPModelwithArrivalCurves.

results/fixed_priority/rta/fully_preemptive.v

 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.preemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
+Require Export prosa.analysis.facts.readiness.sequential.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
@@ -9,9 +10,9 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
 (** In this section we prove the RTA theorem for the fully preemptive FP model *)
 
 (** Throughout this file, we assume the FP priority policy, ideal uni-processor 
-    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+    schedules, and the sequential readiness model. *)
 Require Import prosa.model.processor.ideal.
-Require Import prosa.model.readiness.basic.
+Require Import prosa.model.readiness.sequential.
 
 (** Furthermore, we assume the fully preemptive task model. *)
 Require Import prosa.model.task.preemption.fully_preemptive.
@@ -57,8 +58,13 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
+  (** Recall that we assume sequential readiness. *)
+  Instance sequential_readiness : JobReady _ _ :=
+    sequential_ready_instance arr_seq.
+
   (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
   Variable sched : schedule (ideal.processor_state Job).
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
   Hypothesis H_jobs_come_from_arrival_sequence:
     jobs_come_from_arrival_sequence sched arr_seq.
 
@@ -72,10 +78,6 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   Hypothesis H_priority_is_reflexive : reflexive_priorities.
   Hypothesis H_priority_is_transitive : transitive_priorities.
 
-  (** Assume we have sequential tasks, i.e, tasks from the 
-     same task execute in the order of their arrival. *)
-  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
-
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
@@ -139,6 +141,9 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
                /fully_preemptive.fully_preemptive_model subnn big1_eq. } 
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.      
     all: eauto 2 with basic_facts.
+    rewrite /work_bearing_readiness.
+    - by apply sequential_readiness_implies_work_bearing_readiness.
+    - by apply sequential_readiness_implies_sequential_tasks => //.
     - by rewrite BLOCK add0n.
     - move => A /andP [LT NEQ].
       edestruct H_R_is_maximum as [F [FIX BOUND]].

results/fixed_priority/rta/limited_preemptive.v

 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
+Require Export prosa.analysis.facts.readiness.sequential.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
@@ -9,9 +10,9 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
     fixed preemption points. *)
 
 (** Throughout this file, we assume the FP priority policy, ideal uni-processor 
-    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+    schedules, and the sequential readiness model. *)
 Require Import prosa.model.processor.ideal.
-Require Import prosa.model.readiness.basic.
+Require Import prosa.model.readiness.sequential.
 
 (** Furthermore, we assume the task model with fixed preemption points. *)
 Require Import prosa.model.preemption.limited_preemptive.
@@ -65,10 +66,13 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Variable tsk : Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
 
-  (** Next, consider any ideal uni-processor schedule  with limited preemptions of this arrival sequence ... *)
+  (** Recall that we assume sequential readiness. *)
+  Instance sequential_readiness : JobReady _ _ :=
+    sequential_ready_instance arr_seq.
+
+  (** Next, consider any valid ideal uni-processor schedule  with limited preemptions of this arrival sequence ... *)
   Variable sched : schedule (ideal.processor_state Job).
-  Hypothesis H_jobs_come_from_arrival_sequence:
-    jobs_come_from_arrival_sequence sched arr_seq.
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
   Hypothesis H_schedule_respects_preemption_model:
     schedule_respects_preemption_model arr_seq sched.
 
@@ -82,10 +86,6 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Hypothesis H_priority_is_reflexive : reflexive_priorities.
   Hypothesis H_priority_is_transitive : transitive_priorities.
   
-  (** Assume we have sequential tasks, i.e, jobs from the 
-     same task execute in the order of their arrival. *)
-  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
-
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
@@ -160,22 +160,24 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
       with (L0 := L).
     all: eauto 2 with basic_facts.
-    intros A SP.
-    destruct (H_R_is_maximum _ SP) as[FF [EQ1 EQ2]].
-    exists FF; rewrite subKn; first by done. 
-    rewrite /task_last_nonpr_segment  -(leq_add2r 1) subn1 !addn1 prednK; last first.
-    - rewrite /last0 -nth_last.
-      apply HYP3; try by done. 
-      rewrite -(ltn_add2r 1) !addn1 prednK //.
-      move: (number_of_preemption_points_in_task_at_least_two
-               _ _ H_valid_model_with_fixed_preemption_points _ H_tsk_in_ts POSt) => Fact2.
-      move: (Fact2) => Fact3.
+    - by apply sequential_readiness_implies_work_bearing_readiness.
+    - by apply sequential_readiness_implies_sequential_tasks.
+    - intros A SP.
+      destruct (H_R_is_maximum _ SP) as[FF [EQ1 EQ2]].
+      exists FF; rewrite subKn; first by done. 
+      rewrite /task_last_nonpr_segment  -(leq_add2r 1) subn1 !addn1 prednK; last first.
+      + rewrite /last0 -nth_last.
+        apply HYP3; try by done. 
+        rewrite -(ltn_add2r 1) !addn1 prednK //.
+        move: (number_of_preemption_points_in_task_at_least_two
+                 _ _ H_valid_model_with_fixed_preemption_points _ H_tsk_in_ts POSt) => Fact2.
+        move: (Fact2) => Fact3.
         by rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2.
-    - apply leq_trans with (task_max_nonpreemptive_segment tsk).
-      + by apply last_of_seq_le_max_of_seq.
-      + rewrite -END; last by done.
-        apply ltnW; rewrite ltnS; try done.
+      + apply leq_trans with (task_max_nonpreemptive_segment tsk).
+        * by apply last_of_seq_le_max_of_seq.
+        * rewrite -END; last by done.
+          apply ltnW; rewrite ltnS; try done.
           by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
   Qed.
-    
+  
 End RTAforFixedPreemptionPointsModelwithArrivalCurves.