Put State inside ProcessorState

It was a parameter but that wasn't of any use, it was just making everything more noisy.

Put State inside ProcessorState
It was a parameter but that wasn't of any use, it was just making everything more noisy.
0b7a65db · Pierre Roux · 6eb9b908 · 0b7a65db · 0b7a65db · 0b7a65db
Commit 0b7a65db authored 3 years ago by Pierre Roux
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -25,8 +25,7 @@ Section Abstract_RTA.
  Context `{JobPreemptable Job}.

  (** Consider any kind of uni-service ideal processor state model. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
  Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
  Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.  
  
@@ -271,7 +270,7 @@ Section Abstract_RTA.
            move: H_busy_interval => [[/andP [GT LT] _] _].
            have ESERV :=
              @j_receives_at_least_run_to_completion_threshold
-                _ _ H1 H2 H3 PState H5 _ _  arr_seq sched tsk interference interfering_workload
+                _ _ H1 H2 H3 PState _ _  arr_seq sched tsk interference interfering_workload
                _ j _ _ _ t1 t2 _ (job_rtct j) _ ((A + F) - optimism). 
            feed_n 7 ESERV; eauto 2.
            specialize (ESERV H3 H4).
@@ -500,7 +499,7 @@ Section Abstract_RTA.
          simpl in IB; rewrite H_equivalent in IB; last by apply ltn_trans with A.
          have ESERV :=
            @j_receives_at_least_run_to_completion_threshold
-              _ _ H1 H2 H3 PState H5 _ _ arr_seq sched tsk
+              _ _ H1 H2 H3 PState _ _ arr_seq sched tsk
              interference interfering_workload _ j _ _ _ t1 t2 _ (job_rtct j) _ (A_sp + F_sp). 
          feed_n 7 ESERV; eauto 2.
          specialize (ESERV H3 H4).
@@ -552,4 +551,4 @@ Section Abstract_RTA.
                   with (j := j) (t1 := t1) (t2 := t2) (A_sp := A1) (F_sp := F1); auto.
  Qed.

-End Abstract_RTA. 
+End Abstract_RTA.
--- a/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -22,8 +22,7 @@ Section AbstractRTADefinitions.
    Context `{JobCost Job}.

    (** Consider any kind of processor state model. *)
-    Context {PState : Type}.
-    Context `{ProcessorState Job PState}.
+    Context {PState : ProcessorState Job}.
    
    (** Consider any arrival sequence... *) 
    Variable arr_seq : arrival_sequence Job.

--- a/analysis/abstract/run_to_completion.v
+++ b/analysis/abstract/run_to_completion.v
@@ -28,8 +28,7 @@ Section AbstractRTARunToCompletionThreshold.
  Context `{JobPreemptable Job}.

  (** Consider any kind of uni-service ideal processor state model. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
  Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
  Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.

@@ -181,7 +180,7 @@ Section AbstractRTARunToCompletionThreshold.
      move => t ES.
      set (job_cost j - job_rtct j) as job_last.
      have LSNP := @job_nonpreemptive_after_run_to_completion_threshold
-                     Job H2 H3 _ _ arr_seq sched _ j _ t.
+                     Job H2 H3 _ arr_seq sched _ j _ t.
      apply negbNE; apply/negP; intros CONTR.
      have SCHED: forall t', t <= t' <= t + job_last -> scheduled_at sched j t'.
      { move => t' /andP [GE LT].

--- a/analysis/definitions/busy_interval.v
+++ b/analysis/definitions/busy_interval.v
@@ -11,8 +11,7 @@ Section BusyIntervalJLFP.
  Context `{JobCost Job}.    

  (** Consider any kind of processor state model. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.  
+  Context {PState : ProcessorState Job}.

  (** Consider any arrival sequence with consistent arrivals ... *)
  Variable arr_seq : arrival_sequence Job.

--- a/analysis/definitions/carry_in.v
+++ b/analysis/definitions/carry_in.v
@@ -18,7 +18,7 @@ Section NoCarryIn.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

  (** ... and the resultant schedule. *)
-  Context {PState : Type} `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
  Variable sched : schedule PState.

  (** There is no carry-in at time [t] iff every job (regardless of priority)

--- a/analysis/definitions/completion_sequence.v
+++ b/analysis/definitions/completion_sequence.v
@@ -11,8 +11,7 @@ Section CompletionSequence.

  (** Consider any kind of jobs with a cost
     and any kind of processor state. *)
-  Context {Job : JobType} `{JobCost Job} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} `{JobCost Job} {PState : ProcessorState Job}.

  (** Consider any job arrival sequence. *)
  Variable arr_seq: arrival_sequence Job.

--- a/analysis/definitions/job_response_time.v
+++ b/analysis/definitions/job_response_time.v
@@ -10,8 +10,7 @@ Section JobResponseTimeExceeds.
  Context `{JobArrival Job}.

  (** ... and any kind of processor state. *)
-  Context `{PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context `{PState : ProcessorState Job}.

  (** Consider any schedule. *)
  Variable sched : schedule PState.

--- a/analysis/definitions/progress.v
+++ b/analysis/definitions/progress.v
@@ -12,8 +12,7 @@ Section Progress.
  Context `{JobCost Job}.

  (** ... and any kind of schedule. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.

  (** For a given job and a given schedule... *)
  Variable sched : schedule PState.

--- a/analysis/definitions/readiness.v
+++ b/analysis/definitions/readiness.v
@@ -12,7 +12,7 @@ Section ReadinessModelProperties.
  Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.

  (** ... and any kind of processor model, ... *)
-  Context {PState: Type} `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.

  (** ... consider a  notion of job readiness. *)
  Variable ReadinessModel : JobReady Job PState.
@@ -46,5 +46,3 @@ Section ReadinessModelProperties.
        ~~ job_preemptable j (service sched j t) -> job_ready sched j t.
  
 End ReadinessModelProperties.
-
-
--- a/analysis/definitions/schedulability.v
+++ b/analysis/definitions/schedulability.v
@@ -18,8 +18,7 @@ Section Task.
  Context `{JobTask Job Task}.

  (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.

  (** Consider any job arrival sequence... *)
  Variable arr_seq: arrival_sequence Job.
@@ -65,8 +64,7 @@ Section Schedulability.
  Context `{JobTask Job Task}.

  (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
  
  (** Consider any job arrival sequence... *)
  Variable arr_seq: arrival_sequence Job.
@@ -115,8 +113,7 @@ Section AllDeadlinesMet.
  Context `{JobDeadline Job}.

  (** ... any given type of processor states. *)
-  Context {PState: eqType}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.

  (** We say that all deadlines are met if every job scheduled at some
     point in the schedule meets its deadline. Note that this is a

--- a/analysis/definitions/schedule_prefix.v
+++ b/analysis/definitions/schedule_prefix.v
@@ -9,7 +9,7 @@ Section PrefixDefinition.
  Context {Job : JobType}.

  (** ... and any kind of processor model, ... *)
-  Context {PState: Type} `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.

  (** ... two schedules share an identical prefix if they are pointwise
          identical (at least) up to a fixed horizon. *)

--- a/analysis/definitions/tardiness.v
+++ b/analysis/definitions/tardiness.v
@@ -18,8 +18,7 @@ Section Tardiness.
  Context `{JobTask Job Task}.

  (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.

  (** Further, consider any job arrival sequence... *)
  Variable arr_seq: arrival_sequence Job.

--- a/analysis/definitions/work_bearing_readiness.v
+++ b/analysis/definitions/work_bearing_readiness.v
@@ -18,11 +18,10 @@ Section WorkBearingReadiness.
  Context {Job : JobType} {Task : TaskType} `{JobArrival Job} `{JobCost Job}.

  (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.

  (** Further, allow for any notion of job readiness. *)
-  Context `{JobReady Job PState}.
+  Context {jr : JobReady Job PState}.

  (** Consider any job arrival sequence, ... *)
  Variable arr_seq : arrival_sequence Job.

--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -39,8 +39,7 @@ End ArrivalPredicates.
 Section Arrived.
  
  (** Consider any kinds of jobs and any kind of processor state. *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} {PState : ProcessorState Job}.

  (** Consider any schedule... *)
  Variable sched : schedule PState.
@@ -49,7 +48,7 @@ Section Arrived.
      notion of readiness. *)
  Context `{JobCost Job}.
  Context `{JobArrival Job}.
-  Context `{JobReady Job PState}.
+  Context {jr : JobReady Job PState}.

  (** First, we note that readiness models are by definition consistent
      w.r.t. [pending]. *)
@@ -57,7 +56,7 @@ Section Arrived.
    forall j t,
      job_ready sched j t -> pending sched j t.
  Proof.
-    move: H5 => [is_ready CONSISTENT].
+    move: jr => [is_ready CONSISTENT].
    move=> j t READY.
    apply CONSISTENT.
    by exact READY.
@@ -345,4 +344,4 @@ Section ArrivalSequencePrefix.

  End ArrivalTimes.

-End ArrivalSequencePrefix. 
+End ArrivalSequencePrefix.
--- a/analysis/facts/behavior/completion.v
+++ b/analysis/facts/behavior/completion.v
@@ -14,8 +14,7 @@ Section CompletionFacts.
  Context `{JobArrival Job}.

  (** ...any kind of processor model,... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.

  (** ...and a given schedule. *)
  Variable sched: schedule PState.
@@ -163,8 +162,7 @@ Section ServiceAndCompletionFacts.
  Context `{JobCost Job}.

  (** ...any kind of processor model,... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.

  (** ...and a given schedule. *)
  Variable sched: schedule PState.
@@ -277,8 +275,7 @@ Section PositiveCost.
  Context `{JobArrival Job}.

  (** ...any kind of processor model,... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.

  (** ...and a given schedule. *)
  Variable sched: schedule PState.
@@ -325,8 +322,7 @@ End PositiveCost.
 Section CompletedJobs.
  
  (** Consider any kinds of jobs and any kind of processor state. *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} {PState : ProcessorState Job}.

  (** Consider any schedule... *)
  Variable sched : schedule PState.
@@ -335,7 +331,7 @@ Section CompletedJobs.
     readiness. *)
  Context `{JobCost Job}.
  Context `{JobArrival Job}.
-  Context `{JobReady Job PState}.
+  Context {jr : JobReady Job PState}.

  (** We observe that a given job is ready only if it is also incomplete... *)
  Lemma ready_implies_incomplete:
@@ -393,7 +389,8 @@ Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_f
 (** Next, we relate the completion of jobs in schedules with identical prefixes. *)
 Section CompletionInTwoSchedules.
  (** Consider any processor model and any type of jobs with costs, arrival times, and a notion of readiness. *)
-  Context {PState: Type} {Job: JobType} `{ProcessorState Job PState} `{JobReady Job PState}.
+  Context {Job: JobType} {PState: ProcessorState Job}.
+  Context {jc : JobCost Job} {ja : JobArrival Job} {jr : JobReady Job PState}.

  (** If two schedules share a common prefix, then (in the prefix) jobs
      complete in one schedule iff they complete in the other. *)
@@ -424,5 +421,3 @@ Section CompletionInTwoSchedules.


 End CompletionInTwoSchedules.
-
-
--- a/analysis/facts/behavior/deadlines.v
+++ b/analysis/facts/behavior/deadlines.v
@@ -10,8 +10,7 @@ Section DeadlineFacts.
  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.

  (** ... any given type of processor states. *)
-  Context {PState: eqType}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.

  (** First, we derive two properties from the fact that a job is incomplete at
      some point in time. *)

--- a/analysis/facts/behavior/service.v
+++ b/analysis/facts/behavior/service.v
@@ -14,8 +14,7 @@ Section Composition.
  
  (** Consider any job type and any processor state. *)
  Context {Job: JobType}.
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.

  (** For any given schedule... *)
  Variable sched: schedule PState.
@@ -137,8 +136,7 @@ Section UnitService.

  (** Consider any job type and any processor state. *)
  Context {Job : JobType}.
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.

  (** Let's consider a unit-service model... *)
  Hypothesis H_unit_service: unit_service_proc_model PState.
@@ -239,8 +237,7 @@ Section Monotonicity.

  (** Consider any job type and any processor model. *)
  Context {Job: JobType}.
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.

  (** Consider any given schedule... *)
  Variable sched: schedule PState.
@@ -264,8 +261,7 @@ End Monotonicity.
 Section RelationToScheduled.

  Context {Job: JobType}.
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.

  (** Consider any given schedule... *)
  Variable sched: schedule PState.
@@ -640,8 +636,7 @@ Section ServiceInTwoSchedules.
  
  (** Consider any job type and any processor model. *)
  Context {Job: JobType}.
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.

  (** Consider any two given schedules... *)
  Variable sched1 sched2: schedule PState.

--- a/analysis/facts/busy_interval/busy_interval.v
+++ b/analysis/facts/busy_interval/busy_interval.v
@@ -40,7 +40,7 @@ Section ExistsBusyIntervalJLFP.
  Context `{JLFP_policy Job}.

  (** Further, allow for any work-bearing notion of job readiness. *)
-  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

  (** For simplicity, let's define some local names. *)
@@ -301,7 +301,7 @@ Section ExistsBusyIntervalJLFP.
      rewrite -{3}[Δ](sum_of_ones t1) exchange_big //=.
      apply/eqP; rewrite eqn_leq; apply/andP; split.
      { rewrite leq_sum // => t' _.
-        have SCH := @service_of_jobs_le_1 _ _ _ _ _ sched predT (arrivals_between 0 (t1 + Δ)).        
+        have SCH := @service_of_jobs_le_1 _ _ _ _ sched predT (arrivals_between 0 (t1 + Δ)).        
        by eapply leq_trans; last apply SCH; eauto using arrivals_uniq with basic_facts. }
      { rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=
                leq_sum // => t' /andP [/andP [LT GT] _]; apply/sum_seq_gt0P.

--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -50,7 +50,7 @@ Section ExistsNoCarryIn.
  Let quiet_time := quiet_time arr_seq sched.

  (** Further, allow for any work-bearing notion of job readiness. *)
-  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
  
  (** Assume that the schedule is work-conserving, ... *)

--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -54,7 +54,7 @@ Section PriorityInversionIsBounded.
    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.

  (** Further, allow for any work-bearing notion of job readiness. *)
-  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

  (** We assume that the schedule is valid and that all jobs come from the arrival sequence. *)
@@ -577,7 +577,7 @@ Section PriorityInversionIsBounded.
              have Fact: exists Δ, t' = t1 + Δ.
              { by exists (t' - t1); apply/eqP; rewrite eq_sym; apply/eqP; rewrite subnKC. }
              move: Fact => [Δ EQ]; subst t'.
-              have NPPJ := @no_intermediate_preemption_point (@service _ _ _ sched jlp (t1 + Δ)).
+              have NPPJ := @no_intermediate_preemption_point (@service _ _ sched jlp (t1 + Δ)).
              apply proj1 in CORR; specialize (CORR jlp ARRs).
              move: CORR => [_ [_ [T _] ]].
              apply T; apply: NPPJ; apply/andP; split.