Library prosa.results.rta.rs.fp.fully_nonpreemptive

Require Export prosa.analysis.facts.readiness.sequential.
Require Export prosa.analysis.abstract.restricted_supply.task_intra_interference_bound.
Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.fp.
Require Export prosa.analysis.abstract.restricted_supply.search_space.fp.
Require Export prosa.analysis.facts.model.task_cost.
Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.

RTA for Fully Non-Preemptive FP Scheduling on Restricted-Supply Uniprocessors

In the following, we derive a response-time analysis for FP schedulers, assuming a workload of sporadic real-time tasks characterized by arbitrary arrival curves executing upon a uniprocessor with arbitrary supply restrictions. To this end, we instantiate the sequential variant of abstract Restricted-Supply Response-Time Analysis (aRSA) as provided in the prosa.analysis.abstract.restricted_supply module.

Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.

Defining the System Model

Before any formal claims can be stated, an initial setup is needed to define the system model under consideration. To this end, we next introduce and define the following notions using Prosa's standard definitions and behavioral semantics:

tasks, jobs, and their parameters,
processor model,
the sequence of job arrivals,
worst-case execution time (WCET) and the absence of self-suspensions,
the task under analysis,
an arbitrary schedule of the task set, and finally,
a supply-bound function.

Tasks and Jobs

Consider any type of tasks, each characterized by a WCET task_cost and an arrival curve max_arrivals, ...

  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{MaxArrivals Task}.

... and any type of jobs associated with these tasks, where each job has a task job_task, a cost job_cost, and an arrival time job_arrival.

  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobCost Job}.
  Context `{JobArrival Job}.

Furthermore, assume that jobs and 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.

Processor Model

Consider any kind of fully-supply-consuming, unit-supply processor state model.

  Context `{PState : ProcessorState Job}.
  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.

The Job Arrival Sequence

Consider any arrival sequence arr_seq with consistent, non-duplicate arrivals.

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

Absence of Self-Suspensions and WCET Compliance

We assume the sequential model of readiness without jitter or self-suspensions, wherein a pending job j is ready as soon as all prior jobs of the same task are complete.

#[local] Instance sequential_readiness : JobReady _ _ :=
sequential_ready_instance arr_seq.

We further require that a job's cost cannot exceed its task's stated WCET.

Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.

The Task Set

We consider an arbitrary task set ts ...

Variable ts : seq Task.

... and assume that all jobs stem from tasks in this task set.

Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

We assume that max_arrivals is a family of valid arrival curves that constrains the arrival sequence arr_seq, i.e., for any task tsk in ts, max_arrival tsk is (1) an arrival bound of tsk, and ...

Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

... (2) a monotonic function that equals 0 for the empty interval delta = 0.

Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.

The Task Under Analysis

Let tsk be any task in ts that is to be analyzed.

Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.

The Schedule

Consider any non-preemptive, work-conserving, valid uniprocessor schedule of the given arrival sequence arr_seq (and hence the given task set ts).

  Variable sched : schedule PState.
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
  Hypothesis H_work_conserving : work_conserving arr_seq sched.
  Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.

Consider an FP policy that indicates a higher-or-equal priority relation, and assume that the relation is reflexive and transitive.

  Context {FP : FP_policy Task}.
  Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
  Hypothesis H_priority_is_transitive : transitive_task_priorities FP.

We assume that the schedule respects the FP scheduling policy.

Hypothesis H_respects_policy_at_preemption_point :
respects_FP_policy_at_preemption_point arr_seq sched FP.

Supply-Bound Function

Assume the minimum amount of supply that any job of task tsk receives is defined by a monotone unit-supply-bound function SBF.

  Context {SBF : SupplyBoundFunction}.
  Hypothesis H_SBF_monotone : sbf_is_monotone SBF.
  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.

We assume that SBF properly characterizes all busy intervals (w.r.t. task tsk) in sched. That is, (1) SBF 0 = 0 and (2) for any duration Δ, at least SBF Δ supply is available in any busy-interval prefix of length Δ.

Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.

Maximum Length of a Busy Interval

In order to apply aRSA, we require a bound on the maximum busy-window length. To this end, let L be any positive solution of the busy-interval "recurrence" (i.e., inequality) SBF L ≥ blocking_bound ts tsk + total_hep_rbf L, as defined below.

As the lemma busy_intervals_are_bounded_rs_fp shows, under FP scheduling, this condition is sufficient to guarantee that the maximum busy-window length is at most L, i.e., the length of any busy interval is bounded by L.

  Definition busy_window_recurrence_solution (L : duration) :=
    L > 0
    ∧ SBF L ≥ blocking_bound ts tsk
              + total_hep_request_bound_function_FP ts tsk L.

Response-Time Bound

Having established all necessary preliminaries, it is finally time to state the claimed response-time bound R.

A value R is a response-time bound if, for any given offset A in the search space, the response-time bound recurrence has a solution F not exceeding A + R.

  Definition rta_recurrence_solution L R :=
    ∀ (A : duration),
      is_in_search_space tsk L A →
      ∃ (F : duration ),
        SBF F ≥ blocking_bound ts tsk
                + (task_request_bound_function tsk (A + ε) - (task_cost tsk - ε ))
                + total_ohep_request_bound_function_FP ts tsk F
        ∧ SBF (A + R) ≥ SBF F + (task_cost tsk - ε )
        ∧ A + R ≥ F.

Finally, using the sequential variant of abstract restricted-supply analysis, we establish that any such R is a sound response-time bound for the concrete model of fully non-preemptive fixed-priority scheduling with arbitrary supply restrictions.

  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.
    move⇒ L [BW_POS BW_FIX] R SOL js ARRs TSKs.
    have VPR : valid_preemption_model arr_seq sched by exact: 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 exact: sequential_readiness_implies_work_bearing_readiness.
    eapply uniprocessor_response_time_bound_restricted_supply_seq with (L := L) ⇒ //.
    - exact: 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: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
      move ⇒ ? ? ? ? [? ?]; split ⇒ //.
      by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
    - 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).
    - move ⇒ A SP; move: (SOL A) ⇒ [].
      + by apply: search_space_sub ⇒ //.
      + move ⇒ F [FIX1 [FIX2 LE]]; ∃ F; split ⇒ //.
        rewrite /task_intra_IBF /task_rtct /fully_nonpreemptive_rtc_threshold /constant.
        split; [rewrite -(leqRW FIX1)| ]; lia.
  Qed.

End RTAforFullyNonPreemptiveFPModelwithArrivalCurves.