Library prosa.results.rs.exceedance.fully_nonpreemptive_rta

Exceedance-Aware RTA for Fully Non-Preemptive Fixed-Priority Uniprocessor Scheduling

In this file, we state and prove an RTA for ideal uniprocessors with exceedance. We assume a fixed-priority policy and fully non-preemptive tasks.
Section RTA.

Consider tasks characterized by nominal execution times and arbitrary arrival curves, ...
  Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}.

... and their corresponding jobs.
  Context {Job : JobType} `{JobTask Job Task}
          `{JobCost Job} `{JobArrival Job}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

We assume sequential readiness.
   #[local] Instance sequential_readiness : JobReady _ _ :=
    sequential_ready_instance arr_seq.

We assume that all tasks are fully non-preemptive.
  #[local] Existing Instance fully_nonpreemptive_job_model.
  #[local] Existing Instance fully_nonpreemptive_task_model.
  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.

We assume we are given a task set, with valid arrival curves for each task in the task set, and that all jobs in the arrival sequence stem from tasks in the given task set.
Assume we have a valid, nonpreemptive, and work-conserving schedule.
Assume that the FP policy under consideration is reflexive and transitive.
We assume that the schedule respects the FP scheduling policy.
Let us say that e is the bound on the total exceedance ...
  Variable e : work.

... inside any busy interval of a task tsk from the given task set.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

Let us locally recall the exceedance SBF using Instance to make it available to the typeclasses hints database.
  #[local] Instance EPS_SBF_inst : SupplyBoundFunction := eps_sbf e.

Let us formally state that the total exceedance inside the busy window is bounded.
  Hypothesis H_exceedance_in_busy_interval_bounded :
     j t1 t2,
      arrives_in arr_seq j
      job_of_task tsk j
      busy_interval_prefix arr_seq sched j t1 t2
      \sum_(t1 t < t2) is_exceedance_exec (sched t) e.

Let us locally define some abbreviations for clarity.
First, we define the bound on the maximum length of a busy window.
  Definition busy_window_recurrence_solution L :=
    L > e
     L blocking_bound ts tsk + total_hep_rbf L + e.

Then we define the response-time "recurrence" (i.e., set of inequalities) ...
  Definition rta_recurrence_solution L R :=
     (A : duration),
      is_in_search_space tsk L A
       (F : duration),
        A F A + R
         F blocking_bound ts tsk
              + (rbf tsk (A + ε) - (task_cost tsk - ε))
              + total_ohep_rbf F + e
         A + R F + (task_cost tsk - ε) + e.

... and prove that any solution R satisfying this predicate is a bound on the maximum response time of task tsk in sched.
  Theorem uniprocessor_response_time_bound_fully_nonpreemptive_fp :
     (L : duration),
      busy_window_recurrence_solution L
       (R : duration),
        rta_recurrence_solution L R
        task_response_time_bound arr_seq sched tsk R.
  Proof.
    moveL [BW_POS BW_FIX] R SOL js ARRs TSKs.
    have VPR : valid_preemption_model arr_seq sched by apply: valid_fully_nonpreemptive_model.
    have [ZERO|POS] := posnP (job_cost js);
      first by rewrite /job_response_time_bound /completed_by ZERO.
    have READ : work_bearing_readiness arr_seq sched
      by apply: sequential_readiness_implies_work_bearing_readiness.
    have NET: arrivals_have_valid_job_costs arr_seq by done.
    eapply uniprocessor_response_time_bound_restricted_supply_seq with (L := L) ⇒ //.
    - by apply: instantiated_i_and_w_are_coherent_with_schedule ⇒ //=.
    - exact: sequential_readiness_implies_sequential_tasks.
    - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
    - apply: busy_intervals_are_bounded_rs_fp ⇒ //.
      + by apply: instantiated_i_and_w_are_coherent_with_schedule.
      + apply: eps_sbf_is_valid.
        exact: H_exceedance_in_busy_interval_bounded.
      + exact: eps_sbf_is_unit.
      + by move: BW_FIX; rewrite /eps_sbf /total_hep_rbf; lia.
      + by move: BW_FIX; rewrite /EPS_SBF_inst /eps_sbf /total_hep_rbf; lia.
    - apply: valid_pred_sbf_switch_predicate; last by exact: eps_sbf_is_valid.
      move ⇒ ? ? ? ? [? ?]; split ⇒ //.
      by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
    - apply: eps_sbf_is_unit.
    - apply: instantiated_task_intra_interference_is_bounded; eauto 1 ⇒ //; first last.
      + by apply athep_workload_le_total_ohep_rbf.
      + apply: service_inversion_is_bounded ⇒ // ⇒ jo t1 t2 ARRo TSKo BUSYo.
        unshelve rewrite (leqRW (nonpreemptive_segments_bounded_by_blocking _ _ _ _ _ _ _ _ _)) ⇒ //.
        by instantiate (1 := fun _blocking_bound ts tsk).
    - moveA SP; move: (SOL A) ⇒ [].
       + apply: search_space_sub ⇒ //; first lia.
         by apply: non_pathological_max_arrivals =>//; apply H_valid_task_arrival_sequence.
      + moveF [/andP [_ LE] [FIX1 FIX2]]; F; split ⇒ //.
        rewrite /task_intra_IBF /task_rtct /fully_nonpreemptive_rtc_threshold /constant.
        rewrite /EPS_SBF_inst /eps_sbf.
        split; try lia.
        rewrite -/rbf -/total_ohep_rbf.
        by lia.
  Qed.

End RTA.