Polish one file

analysis/facts/busy_interval/busy_interval_rs.v

@@ -5,7 +5,10 @@ Require Export prosa.model.schedule.work_conserving.
 Require Export prosa.analysis.definitions.job_properties.
 Require Export prosa.analysis.definitions.service_inversion.
 Require Export prosa.analysis.facts.behavior.all.
-Require Export prosa.analysis.facts.model.service_of_jobs_rs.
+Require Export prosa.model.aggregate.workload.
+Require Export prosa.model.aggregate.service_of_jobs.
+Require Export prosa.analysis.facts.behavior.completion.
+Require Import prosa.model.processor.restricted_supply.
 
 (** Throughout this file, we assume rs uni-processor schedules. *)
 Require Import prosa.model.processor.restricted_supply.

analysis/facts/busy_interval/priority_inversion.v

@@ -16,6 +16,7 @@ Require Import prosa.model.processor.ideal.
     pending jobs are always ready. *)
 Require Import prosa.model.readiness.basic.
  *)
+Require Export prosa.analysis.definitions.weak_basic_readiness.
 
 (** In preparation of the derivation of the priority inversion bound, we
     establish two basic facts on preemption times. *)
@@ -96,8 +97,8 @@ Section PriorityInversionIsBounded.
   (**  ... 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 any arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
@@ -131,17 +132,13 @@ Section PriorityInversionIsBounded.
      bounded nonpreemptive segments. *)
   Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
     valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
-  
-  Context `{@JobReady Job (ideal.processor_state Job) _ H2 H1}.
 
-  Hypothesis H_job_ready :
-    forall (j : Job) (t : instant),
-      arrives_in arr_seq j ->
-      pending sched j t ->
-      exists (j' : Job),
-        arrives_in arr_seq j' /\
-        job_ready sched j' t /\
-        hep_job j' j.
+  (* TODO: comment *)
+  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+
+  (* TODO: comment *)
+  Hypothesis H_weak_basic_readiness :
+    weak_basic_readiness arr_seq sched.
   
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
@@ -250,7 +247,7 @@ Section PriorityInversionIsBounded.
           - by rewrite /has_arrived.
           - by move: NCOMP'; apply contra, completion_monotonic.
         }
-        apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].
+        apply H_weak_basic_readiness in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].
         have HEP : hep_job j' j by apply (H_priority_is_transitive t j_hp). 
         clear HEP' NCOMP' BEF HP ARR j_hp.
         have BACK: backlogged sched j' t.
@@ -285,7 +282,7 @@ Section PriorityInversionIsBounded.
           }
           have PEND := job_pending_at_arrival sched _ H_job_cost_positive H_jobs_must_arrive_to_execute.
           rewrite ARR in PEND.
-          apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [PENDhp HEPhp]]].
+          apply H_weak_basic_readiness in PEND => //; destruct PEND as [jhp [ARRhp [PENDhp HEPhp]]].
           eapply NOTHP, (H_priority_is_transitive 0); last by apply HEPhp.
           apply (H_respects_policy _ _ t2.-1); auto.
           apply/andP; split; first by done.
@@ -301,7 +298,7 @@ Section PriorityInversionIsBounded.
             - by rewrite /has_arrived ltnW.
             - by move: NOTCOMP'; apply contra, completion_monotonic.
           }          
-          apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].
+          apply H_weak_basic_readiness in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].
           have HEP : hep_job j' j by apply (H_priority_is_transitive t j_hp'). 
           clear ARR HP IN HEP' NOTCOMP' j_hp'.
           have BACK: backlogged sched j' t.

analysis/facts/model/service_of_jobs_rs.v

-Require Export prosa.model.aggregate.workload.
-Require Export prosa.model.aggregate.service_of_jobs.
-Require Export prosa.analysis.facts.behavior.completion.
-Require Import prosa.model.processor.restricted_supply.
-
-(** In this section, we prove some properties about service
-   of sets of jobs for ideal rs-processor model. *)
-Section RestrictedSupplyModelLemmas.
-
-
-  (* TODO: del this file *)
-  
-End RestrictedSupplyModelLemmas.

analysis/facts/readiness/sequential.v

-Require Export prosa.behavior.all.
-Require Export prosa.model.task.sequentiality.
-Require Export prosa.model.priority.classes.
-Require Export prosa.analysis.facts.model.task_arrivals.
-
-Require Export prosa.analysis.definitions.weak_basic_readiness.
-
 Require Export prosa.analysis.definitions.readiness.
-
-
+Require Export prosa.analysis.definitions.weak_basic_readiness.
 Require Export prosa.analysis.facts.behavior.completion.
+Require Export prosa.analysis.facts.model.task_arrivals.
 
-
-
-(* Note that we have readiness in the context *)
+(* TODO: context *)
 Require Export prosa.model.readiness.sequential.
-Print Instances JobReady.
-(* 
-   Output: 
-           sequential_ready_instance :x
-           forall (Job : JobType) (Task : TaskType),
-              JobTask Job Task ->
-              forall (JobArrival Job) (JobCost Job) (PState : Type) (ProcessorState Job PState),
-                 arrival_sequence Job -> 
-                 JobReady Job PState. 
-*)
 
+(* TODO: comment *)
 Section SequentialTasksReadiness.
 
   (** Consider any type of job associated with any type of tasks... *)
@@ -37,38 +19,25 @@ Section SequentialTasksReadiness.
   (** ... and any kind of processor state. *)
   Context {PState : Type}.
   Context `{ProcessorState Job PState}.
-
-  (** Consider any job arrival sequence ... *)
+  
+  (** Consider any arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
-
-  (* ... *)
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  
+  (* ... and any valid schedule of this arrival sequence. *)
   Variable sched : schedule PState.
-  Hypothesis H_todo: consistent_arrival_times arr_seq.
-
-  (* Fails, because Coq cannot find an instance for JobReady *)
-  (* Hypothesis H_todo2 : jobs_must_be_ready_to_execute sched. *)
   
-  (* I think the reason is that Coq cannot quess what is going on with [arr_seq] *)
-  (* So, I'd like to make [test] an instance of JobReady *)
-  Instance test : JobReady Job PState := sequential_ready_instance arr_seq.
-
-  Print Instances JobReady.
-                                     
-  (* Works *)
-  Hypothesis H_todo2: jobs_must_be_ready_to_execute sched.
-
-
-  (* ------------------------------- *) 
-
+  (* TODO: comment *)
+  Instance sequential_ready_instance : JobReady Job PState :=
+    sequential_ready_instance arr_seq.
 
-  
-  Context `{FP_policy Task}.
-  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq. 
   
 
-  (* TODO: name *)
+
+    (* TODO: name *)
   (* TODO: move *)
-  Lemma todo_1:
+  Lemma todo_1 :
     forall j t tsk, 
       (j \in task_arrivals_before arr_seq tsk t) ->
       job_arrival j < t.
@@ -81,7 +50,7 @@ Section SequentialTasksReadiness.
 
   (* TODO: name *)
   (* TODO: move *)
-  Lemma todo_2:
+  Lemma todo_2 :
     forall j t tsk, 
       (j \in task_arrivals_before arr_seq tsk t) ->
       job_task j == tsk.
@@ -90,9 +59,17 @@ Section SequentialTasksReadiness.
     unfold task_arrivals_before, task_arrivals_between in *.
     by move: IN; rewrite mem_filter => /andP [TSK _].
   Qed.
+
   
+  (* TODO: *)
+  Context `{FP_policy Task}.
+  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+  
+
+
   
-  Lemma this_is_valid_sequential_readiness:
+  (* TODO: comment *)
+  Lemma sequential_readiness_implies_weak_basic_readiness : 
     weak_basic_readiness arr_seq sched.
   Proof.
     intros j.
@@ -102,7 +79,8 @@ Section SequentialTasksReadiness.
     { destruct (boolP (job_ready sched j t)) as [READY | NREADY].
       - exists j; repeat split; auto.
         by eapply H_priority_is_reflexive with (t := 0).
-      - move: NREADY; rewrite {1}/job_ready /test /sequential_ready_instance PEND Bool.andb_true_l => /allPn [jhp IN NCOMP].
+      - move: NREADY; rewrite {1}/job_ready /sequential_ready_instance //=
+                              PEND Bool.andb_true_l => /allPn [jhp IN NCOMP].
         apply todo_1 in IN.
         by move: LE; rewrite leqn0 => /eqP EQ; rewrite EQ in IN.
     }
@@ -110,7 +88,8 @@ Section SequentialTasksReadiness.
       destruct (boolP (job_ready sched j t)) as [READY | NREADY].
       - exists j; repeat split; auto. 
         by eapply H_priority_is_reflexive with (t := 0).
-      - move: NREADY; rewrite {1}/job_ready /test /sequential_ready_instance PEND Bool.andb_true_l => /allPn [j' IN NCOMP].
+      - move: NREADY; rewrite {1}/job_ready /sequential_ready_instance //=
+                              PEND Bool.andb_true_l => /allPn [j' IN NCOMP].
         have LE' : job_arrival j' <= k.
         { by apply todo_1 in IN; rewrite -ltnS -EQ. } 
         have ARR' : arrives_in arr_seq j'.
@@ -129,7 +108,7 @@ Section SequentialTasksReadiness.
     }
   Qed.
 
-  Lemma seq_indeed:
+  Lemma sequential_readiness_implies_sequential_tasks :
     sequential_tasks arr_seq sched.
   Proof.
     intros j1 j2 t ARR1 ARR2 SAME LT SCHED.
@@ -138,14 +117,14 @@ Section SequentialTasksReadiness.
       rewrite mem_filter; apply/andP; split; first by done.
       by apply arrived_between_implies_in_arrivals => //.
     } 
-    { by apply H_todo2 in SCHED; rewrite SCHED in NREADY. } 
+    { by apply H_sched_valid  in SCHED; rewrite SCHED in NREADY. } 
   Qed.
 
-  Fact sequential_readiness_nonclairvoyance:
-    nonclairvoyant_readiness test.
+  Fact sequential_readiness_nonclairvoyance :
+    nonclairvoyant_readiness sequential_ready_instance.
   Proof.
     intros sched1 sched2 ? ? ID ? LE.
-    rewrite /job_ready /test //=.
+    rewrite /job_ready /sequential_ready_instance //=.
     erewrite identical_prefix_pending; eauto 2.
     destruct (boolP (pending sched2 j t)) as [_ | _] => //=.
     destruct (boolP (prior_jobs_complete arr_seq sched2 j t)) as [ALL | NOT_ALL]; apply/eqP.

results/fixed_priority/rta/floating_nonpreemptive.v

@@ -159,8 +159,8 @@ Section RTAforFloatingModelwithArrivalCurves.
     move: (LIMJ) => [BEG [END _]].
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.
     all: eauto 2 with basic_facts.
-    - by apply seq_indeed => //.
-    - by apply this_is_valid_sequential_readiness => //.
+    - by apply sequential_readiness_implies_sequential_tasks => //.
+    - by apply sequential_readiness_implies_weak_basic_readiness => //.
     - intros A SP.
       rewrite subnn subn0.
       destruct (H_R_is_maximum _ SP) as [F [EQ LE]].

results/fixed_priority/rta/fully_nonpreemptive.v

@@ -162,8 +162,8 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
         (L0 := L).
     all: eauto 2 with basic_facts.
-    apply seq_indeed => //.
-    apply this_is_valid_sequential_readiness => //.
+    apply sequential_readiness_implies_sequential_tasks => //.
+    apply sequential_readiness_implies_weak_basic_readiness => //.
   Qed.
 
   (* No admitted lemmas *)

results/fixed_priority/rta/fully_preemptive.v

@@ -146,8 +146,8 @@ 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.
-    - by apply seq_indeed => //.
-    - by apply this_is_valid_sequential_readiness => //.
+    - by apply sequential_readiness_implies_sequential_tasks => //.
+    - by apply sequential_readiness_implies_weak_basic_readiness => //.
     - 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

@@ -166,8 +166,8 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
       with (L0 := L).
     all: eauto 2 with basic_facts.
-    - by apply seq_indeed => //.
-    - by apply this_is_valid_sequential_readiness => //.
+    - by apply sequential_readiness_implies_sequential_tasks => //.
+    - by apply sequential_readiness_implies_weak_basic_readiness => //.
     - intros A SP.
       destruct (H_R_is_maximum _ SP) as[FF [EQ1 EQ2]].
       exists FF; rewrite subKn; first by done.