Library prosa.analysis.facts.model.rbf

Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.facts.model.arrival_curves.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.analysis.definitions.schedulability.

Facts about Request Bound Functions (RBFs)

In this file, we prove some lemmas about request bound functions.

RBF is a Bound on Workload

First, we show that a task's RBF is indeed an upper bound on its workload.
Section ProofWorkloadBound.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any arrival sequence with consistent, non-duplicate arrivals, ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... any schedule corresponding to this arrival sequence, ...
  Context {PState : ProcessorState Job}.
  Variable sched : schedule PState.
  Hypothesis H_jobs_come_from_arrival_sequence :
    jobs_come_from_arrival_sequence sched arr_seq.

... and an FP policy that indicates a higher-or-equal priority relation.
  Context `{FP_policy Task}.

Further, consider a task set ts...
  Variable ts : seq Task.

... and let tsk be any task in ts.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

Assume that the job costs are no larger than the task costs ...
  Hypothesis H_valid_job_cost :
    arrivals_have_valid_job_costs arr_seq.

... and that all jobs come from the task set.
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

Let max_arrivals be any arrival bound for task-set ts.
  Context `{MaxArrivals Task}.
  Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.

Next, recall the notions of total workload of jobs...
  Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between arr_seq t1 t2).

... and the workload of jobs of the same task as job j.
  Let task_workload t1 t2 :=
    workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2).

Finally, let us define some local names for clarity.
  Let task_rbf := task_request_bound_function tsk.
  Let total_rbf := total_request_bound_function ts.

In this section, we prove that the workload of all jobs is no larger than the request bound function.
  Section WorkloadIsBoundedByRBF.

Consider any time t and any interval of length Δ.
    Variable t : instant.
    Variable Δ : instant.

First, we show that workload of task tsk is bounded by the number of arrivals of the task times the cost of the task.
    Lemma task_workload_le_num_of_arrivals_times_cost:
      task_workload t (t + Δ)
      ≤ task_cost tsk × number_of_task_arrivals arr_seq tsk t (t + Δ).
    Proof.
      rewrite /task_workload /workload_of_jobs/ number_of_task_arrivals
              /task_arrivals_between -big_filter -sum1_size big_distrr big_filter.
      destruct (task_arrivals_between arr_seq tsk t (t + Δ)) eqn:TASK.
      { unfold task_arrivals_between in TASK.
        by rewrite -big_filter !TASK !big_nil. }
      { rewrite //= big_filter big_seq_cond [in X in _ ≤ X]big_seq_cond.
        apply leq_sum.
        move ⇒ j' /andP [IN TSKj'].
        rewrite muln1.
        move: TSKj' ⇒ /eqP TSKj'; rewrite -TSKj'.
        apply H_valid_job_cost.
        by apply in_arrivals_implies_arrived in IN. }
    Qed.

As a corollary, we prove that workload of task is no larger the than task request bound function.
    Corollary task_workload_le_task_rbf:
      task_workload t (t + Δ) ≤ task_rbf Δ.
    Proof.
      eapply leq_trans; first by apply task_workload_le_num_of_arrivals_times_cost.
      rewrite leq_mul2l; apply/orP; right.
      rewrite -{2}[Δ](addKn t).
      by apply H_is_arrival_bound; last rewrite leq_addr.
    Qed.

Next, we prove that total workload of tasks is no larger than the total request bound function.
    Lemma total_workload_le_total_rbf:
      total_workload t (t + Δ) ≤ total_rbf Δ.
    Proof.
      set l := arrivals_between arr_seq t (t + Δ).
      apply (@leq_trans (\sum_(tsk' <- ts) (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0))).
      { rewrite /total_workload.
        have EXCHANGE := exchange_big_dep predT.
        rewrite EXCHANGE /=; clear EXCHANGE; last by done.
        rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.
        apply leq_sum; move ⇒ j0 /andP [IN0 HP0].
        rewrite big_mkcond (big_rem (job_task j0)) /=.
        rewrite eq_refl; apply leq_addr.
        by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset. }
      apply leq_sum_seq; intros tsk0 INtsk0 HP0.
      apply (@leq_trans (task_cost tsk0 × size (task_arrivals_between arr_seq tsk0 t (t + Δ)))).
      { rewrite -sum1_size big_distrr /= big_filter -/l /workload_of_jobs muln1.
        apply leq_sum_seq ⇒ j0 IN0 /eqP <-.
        apply H_valid_job_cost.
        by apply in_arrivals_implies_arrived in IN0. }
      { rewrite leq_mul2l; apply/orP; right.
        rewrite -{2}[Δ](addKn t).
        by apply H_is_arrival_bound; last rewrite leq_addr. }
    Qed.

Next, we consider any job j of tsk.
    Variable j : Job.
    Hypothesis H_job_of_tsk : job_of_task tsk j.

Consider any general predicate defined on tasks.
    Variable pred : pred Task.

We prove that the sum of job cost of jobs whose corresponding task satisfies the predicate pred is bound by the RBF of these tasks.
    Lemma sum_of_jobs_le_sum_rbf:
      \sum_(j' <- arrivals_between arr_seq t (t + Δ) | pred (job_task j'))
        job_cost j' ≤
        \sum_(tsk' <- ts| pred tsk')
          task_request_bound_function tsk' Δ.
    Proof.
      apply (@leq_trans (\sum_(tsk' <- filter pred ts)
                           (\sum_(j' <- arrivals_between arr_seq t (t + Δ)
                                 | job_task j' == tsk') job_cost j'))).
      - move: (H_job_of_tsk) ⇒ /eqP TSK.
        rewrite [X in _ ≤ X]big_filter.
        set P := fun x ⇒ pred (job_task x).
        rewrite (exchange_big_dep P) //=; last by rewrite /P; move ⇒ ???/eqP→.
        rewrite /P /workload_of_jobs big_seq_cond [X in _ ≤ X]big_seq_cond.
        apply leq_sum ⇒ j0 /andP [IN0 HP0].
        rewrite big_mkcond (big_rem (job_task j0)).
        + by rewrite HP0 andTb eq_refl; apply leq_addr.
        + by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
      - rewrite big_filter.
        apply leq_sum_seq ⇒ tsk0 INtsk0 HP0.
        apply (@leq_trans (task_cost tsk0 × size (task_arrivals_between arr_seq tsk0 t (t + Δ)))).
        + rewrite -sum1_size big_distrr /= big_filter /workload_of_jobs.
          rewrite muln1 /arrivals_between /arrival_sequence.arrivals_between.
          apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.
          by rewrite -EQ; apply H_valid_job_cost; apply in_arrivals_implies_arrived in IN0.
        + rewrite leq_mul2l; apply/orP; right.
          rewrite -{2}[Δ](addKn t).
          by apply H_is_arrival_bound; last by rewrite leq_addr.
    Qed.

  End WorkloadIsBoundedByRBF.

End ProofWorkloadBound.

RBF Properties

In this section, we prove simple properties and identities of RBFs.
Section RequestBoundFunctions.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent:
    consistent_arrival_times arr_seq.

Let tsk be any task.
  Variable tsk : Task.

Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts max_arrival tsk is (1) an arrival bound of tsk, and (2) it is a monotonic function that equals 0 for the empty interval Δ = 0.
  Context `{MaxArrivals Task}.
  Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
  Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).

Let's define some local names for clarity.
  Let task_rbf := task_request_bound_function tsk.

We prove that task_rbf 0 is equal to 0.
  Lemma task_rbf_0_zero:
    task_rbf 0 = 0.
  Proof.
    rewrite /task_rbf /task_request_bound_function.
    apply/eqP; rewrite muln_eq0; apply/orP; right; apply/eqP.
    by move: H_valid_arrival_curve ⇒ [T1 T2].
  Qed.

We prove that task_rbf is monotone.
  Lemma task_rbf_monotone:
    monotone leq task_rbf.
  Proof.
    rewrite /monotone; intros ? ? LE.
    rewrite /task_rbf /task_request_bound_function leq_mul2l.
    apply/orP; right.
    by move: H_valid_arrival_curve ⇒ [_ T]; apply T.
  Qed.

Consider any job j of tsk. This guarantees that there exists at least one job of task tsk.
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_of_tsk : job_of_task tsk j.

Then we prove that task_rbf at ε is greater than or equal to the task's WCET.
  Lemma task_rbf_1_ge_task_cost:
    task_rbf ε ≥ task_cost tsk.
  Proof.
    have ALT: ∀ n, n = 0 ∨ n > 0 by clear; intros n; destruct n; [left | right].
    specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z.
    rewrite leqNgt; apply/negP; intros CONTR.
    move: H_is_arrival_curve ⇒ ARRB.
    specialize (ARRB (job_arrival j) (job_arrival j + ε)).
    feed ARRB; first by rewrite leq_addr.
    move: CONTR; rewrite /task_rbf /task_request_bound_function.
    rewrite -{2}[task_cost tsk]muln1 ltn_mul2l ⇒ /andP [_ CONTR].
    move: CONTR; rewrite -addn1 -[1]add0n leq_add2r leqn0 ⇒ /eqP CONTR.
    move: ARRB; rewrite addKn CONTR leqn0 eqn0Ngt ⇒ /negP T; apply: T.
    rewrite /number_of_task_arrivals -has_predT /task_arrivals_between.
    apply/hasP; ∃ j; last by done.
    rewrite /arrivals_between addn1 big_nat_recl; last by done.
    rewrite big_geq ?cats0 //= mem_filter.
    apply/andP; split; first by done.
    move: H_j_arrives ⇒ [t ARR]; move: (ARR) ⇒ CONS.
    apply H_arrival_times_are_consistent in CONS.
    by rewrite CONS.
  Qed.

As a corollary, we prove that the task_rbf at any point A greater than 0 is no less than the task's WCET.
  Lemma task_rbf_ge_task_cost:
    ∀ A,
      A > 0 →
      task_rbf A ≥ task_cost tsk.
  Proof.
    case ⇒ // A GEQ.
    apply: (leq_trans task_rbf_1_ge_task_cost).
    exact: task_rbf_monotone.
  Qed.

Assume that tsk has a positive cost.
  Hypothesis H_positive_cost : 0 < task_cost tsk.

Then, we prove that task_rbf at ε is greater than 0.
  Lemma task_rbf_epsilon_gt_0 : 0 < task_rbf ε.
  Proof.
    apply leq_trans with (task_cost tsk); first by done.
    by eapply task_rbf_1_ge_task_cost; eauto.
  Qed.

Consider a set of tasks ts containing the task tsk.
  Variable ts : seq Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

Next, we prove that cost of tsk is less than or equal to the total_request_bound_function.
  Lemma task_cost_le_sum_rbf :
    ∀ t,
      t > 0 →
      task_cost tsk ≤ total_request_bound_function ts t.
  Proof.
    move ⇒ t GE.
    destruct t; first by done.
    eapply leq_trans; first by apply task_rbf_1_ge_task_cost; rt_eauto.
    rewrite /total_request_bound_function.
    erewrite big_rem; last by exact H_tsk_in_ts.
    apply leq_trans with (task_request_bound_function tsk t.+1); last by apply leq_addr.
    by apply task_rbf_monotone.
  Qed.

End RequestBoundFunctions.

Monotonicity of the Total RBF

In the following section, we note some trivial facts about the monotonicity of various total RBF variants.
Section TotalRBFMonotonic.

Consider a set of tasks characterized by WCETs and arrival curves.
  Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
  Variable ts : seq Task.
  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.

We observe that the total RBF is monotonically increasing.
  Lemma total_rbf_monotone :
    monotone leq (total_request_bound_function ts).
  Proof.
    apply: sum_leq_mono ⇒ tsk IN.
    by apply task_rbf_monotone; rt_auto.
  Qed.

Furthermore, for any fixed-priority policy, ...
  Context `{FP_policy Task}.

... the total RBF of higher- or equal-priority tasks is also monotonic, ...
  Lemma total_hep_rbf_monotone :
    ∀ tsk,
      monotone leq (total_hep_request_bound_function_FP ts tsk).
  Proof.
    move⇒ tsk.
    apply: sum_leq_mono ⇒ tsk' IN.
    by apply task_rbf_monotone; rt_auto.
  Qed.

... as is the variant that excludes the reference task.
  Lemma total_ohep_rbf_monotone :
    ∀ tsk,
      monotone leq (total_ohep_request_bound_function_FP ts tsk).
  Proof.
    move⇒ tsk.
    apply: sum_leq_mono ⇒ tsk' IN.
    by apply task_rbf_monotone; rt_auto.
  Qed.

End TotalRBFMonotonic.

RBFs Equal to Zero for Duration ε

In the following section, we derive simple properties that follow in the pathological case of an RBF that yields zero for duration ε.
Section DegenerateTotalRBFs.

Consider a set of tasks characterized by WCETs and arrival curves ...
  Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.
  Variable ts : seq Task.

... and any consistent arrival sequence of valid jobs of these tasks.
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job} `{JobCost Job}.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent: consistent_arrival_times arr_seq.
  Hypothesis H_valid_job_cost: arrivals_have_valid_job_costs arr_seq.

Suppose the arrival curves are correct.
  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

Consider any valid schedule corresponding to this arrival sequence.
  Context {PState : ProcessorState Job}.
  Variable sched : schedule PState.
  Hypothesis H_jobs_from_arr_seq : jobs_come_from_arrival_sequence sched arr_seq.

First, we observe that, if a task's RBF is zero for a duration ε, then it trivially has a response-time bound of zero.
  Lemma pathological_rbf_response_time_bound :
    ∀ tsk,
      tsk \in ts →
      task_request_bound_function tsk ε = 0 →
      task_response_time_bound arr_seq sched tsk 0.
  Proof.
    move⇒ tsk IN ZERO j ARR TASK.
    rewrite /job_response_time_bound/completed_by.
    move: ZERO. rewrite /task_request_bound_function ⇒ /eqP.
    rewrite muln_eq0 ⇒ /orP [/eqP COST|/eqP NEVER].
    { apply: leq_trans.
      - by apply: H_valid_job_cost.
      - move: TASK. rewrite /job_of_task ⇒ /eqP →.
        by rewrite COST. }
    { exfalso.
      have: 0 < max_arrivals tsk ε
        by apply: (non_pathological_max_arrivals tsk arr_seq _ j); rt_auto.
      by rewrite NEVER. }
  Qed.

Second, given a fixed-priority policy with reflexive priorities, ...
  Context `{FP_policy Task}.
  Hypothesis H_reflexive : reflexive_priorities.

... if the total RBF of all equal- and higher-priority tasks is zero, then the reference task's response-time bound is also trivially zero.
  Lemma pathological_total_hep_rbf_response_time_bound :
    ∀ tsk,
      tsk \in ts →
      total_hep_request_bound_function_FP ts tsk ε = 0 →
      task_response_time_bound arr_seq sched tsk 0.
  Proof.
    move⇒ tsk IN ZERO j ARR TASK.
    apply: pathological_rbf_response_time_bound; eauto.
    apply /eqP.
    move: ZERO ⇒ /eqP; rewrite sum_nat_eq0_nat ⇒ /allP; apply.
    rewrite mem_filter; apply /andP; split ⇒ //.
    move: (H_reflexive 0 j).
    rewrite /hep_job_at/JLFP_to_JLDP/hep_job/FP_to_JLFP.
    by move: TASK; rewrite /job_of_task ⇒ /eqP →.
  Qed.

Thus we we can prove any response-time bound from such a pathological case, which is useful to eliminate this case in higher-level analyses.
  Corollary pathological_total_hep_rbf_any_bound :
    ∀ tsk,
      tsk \in ts →
      total_hep_request_bound_function_FP ts tsk ε = 0 →
      ∀ R,
        task_response_time_bound arr_seq sched tsk R.
  Proof.
    move⇒ tsk IN ZERO R.
    move: (pathological_total_hep_rbf_response_time_bound tsk IN ZERO).
    rewrite /task_response_time_bound/job_response_time_bound ⇒ COMP j INj TASK.
    apply: completion_monotonic; last by apply: COMP.
    by lia.
  Qed.

End DegenerateTotalRBFs.