prosa.classic.model.schedule.uni.limited.edf.nonpr_reg.response_time

Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.

  Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
         ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform RBF
         AbstractRTAforEDFwithArrivalCurves BusyIntervalJLFP PriorityInversionIsBounded.

  Section Analysis.

    Context {Task: eqType}.
    Variable task_max_nps task_cost: Task → time.
    Variable task_deadline: Task → time.

    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_max_nps job_cost: Job → time.
    Variable job_task: Job → Task.

    (* For clarity, let's denote the relative deadline of a task as D. *)
    Let D tsk := task_deadline tsk.

    (* The relative deadline of a job is equal to the deadline of the corresponding task. *)
    Let job_relative_deadline j := D (job_task j).

    (* Consider any arrival sequence with consistent, non-duplicate arrivals... *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.

    (* Next, consider any uniprocessor schedule of this arrival sequence...*)
    Variable sched: schedule Job.
    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.

    (* ... where jobs do not execute before their arrival nor after completion. *)
    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.

    (* Assume we have sequential jobs, i.e, jobs from the same
       task execute in the order of their arrival. *)
    Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.

    (* Consider the EDF policy that indicates a higher-or-equal priority relation. *)
    Let higher_eq_priority: JLFP_policy Job := EDF job_arrival job_relative_deadline.

    (* We consider an arbitrary function can_be_preempted which defines
       a preemption model with bounded nonpreemptive segments. *)
    Variable can_be_preempted: Job → time → bool.
    Let preemption_time := preemption_time sched can_be_preempted.
    Hypothesis H_correct_preemption_model:
      correct_preemption_model arr_seq sched can_be_preempted.
    Hypothesis H_model_with_bounded_nonpreemptive_segments:
      model_with_bounded_nonpreemptive_segments
        job_cost job_task arr_seq can_be_preempted job_max_nps task_max_nps.

    (* Next, we assume that the schedule is a work-conserving schedule... *)
    Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.

    (* ... and the schedule respects the policy defined by the
       can_be_preempted function (i.e., bounded nonpreemptive segments). *)
    Hypothesis H_respects_policy:
      respects_JLFP_policy_at_preemption_point
        job_arrival job_cost arr_seq sched can_be_preempted higher_eq_priority.

    (* Consider an arbitrary task set ts. *)
    Variable ts: list Task.

    (* Assume that all jobs come from the task set... *)
    Hypothesis H_all_jobs_from_taskset:
      ∀ j, arrives_in arr_seq j → job_task j \in ts.

    (* ...and the cost of a job cannot be larger than the task cost. *)
    Hypothesis H_job_cost_le_task_cost:
      cost_of_jobs_from_arrival_sequence_le_task_cost
        task_cost job_cost job_task arr_seq.

    (* Let tsk be any task in ts that is to be analyzed. *)
    Variable tsk: Task.
    Hypothesis H_tsk_in_ts: tsk \in ts.

    (* Let max_arrivals be a family of proper 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 delta = 0. *)
    Variable max_arrivals: Task → time → nat.
    Hypothesis H_family_of_proper_arrival_curves:
      family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.

    (* Consider a proper job lock-in service and task lock-in functions, i.e... *)
    Variable job_lock_in_service: Job → time.
    Variable task_lock_in_service: Task → time.

    (* ...we assume that for all jobs in the arrival sequence the lock-in service is
       (1) positive, (2) no bigger than costs of the corresponding jobs, and (3) a job
       becomes nonpreemptive after it reaches its lock-in service... *)
    Hypothesis H_proper_job_lock_in_service:
      proper_job_lock_in_service job_cost arr_seq sched job_lock_in_service.

    (* ...and that task_lock_in_service tsk is (1) no bigger than tsk's cost, (2) for any
       job of task tsk job_lock_in_service is bounded by task_lock_in_service. *)
    Hypothesis H_proper_task_lock_in_service:
      proper_task_lock_in_service
        task_cost job_task arr_seq job_lock_in_service task_lock_in_service tsk.

    (* We introduce as an abbreviation "rbf" for the task request bound function,
       which is defined as task_cost(T) × max_arrivals(T,Δ) for a task T. *)
    Let rbf := task_request_bound_function task_cost max_arrivals.

    (* Next, we introduce task_rbf as an abbreviation for the task
       request bound function of task tsk. *)
    Let task_rbf := rbf tsk.

    (* Using the sum of individual request bound functions, we define the request bound
       function of all tasks (total request bound function). *)
    Let total_rbf := total_request_bound_function task_cost max_arrivals ts.

    (* Next, we define an upper bound on interfering workload received from jobs
       of other tasks with higher-than-or-equal priority. *)
    Let bound_on_total_hep_workload A Δ :=
      \sum_(tsk_o <- ts | tsk_o != tsk )
       rbf tsk_o (minn ((A + ε ) + D tsk - D tsk_o) Δ).

    (* Let's define some local names for clarity. *)
    Let job_pending_at := pending job_arrival job_cost sched.
    Let job_scheduled_at := scheduled_at sched.
    Let job_completed_by := completed_by job_cost sched.
    Let job_backlogged_at := backlogged job_arrival job_cost sched.
    Let arrivals_between := jobs_arrived_between arr_seq.
    Let task_rbf_changes_at A := task_rbf_changes_at task_cost max_arrivals tsk A.
    Let bound_on_total_hep_workload_changes_at :=
      bound_on_total_hep_workload_changes_at task_cost task_deadline ts max_arrivals tsk.
    Let response_time_bounded_by :=
      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
    Let max_length_of_priority_inversion :=
      max_length_of_priority_inversion job_max_nps arr_seq higher_eq_priority.

    (* We also define a bound for the priority inversion caused by jobs with lower priority. *)
    Definition blocking_bound :=
      \max_(tsk_other <- ts | (tsk_other != tsk ) && (D tsk < D tsk_other ))
       (task_max_nps tsk_other - ε ).

    Section PriorityInversionIsBounded.

      (* First, we prove that the maximum length of a priority inversion of job j is
         bounded by the maximum length of a nonpreemptive section of a task with
         lower-priority task (i.e., the blocking term). *)
      Lemma priority_inversion_is_bounded_by_blocking:
        ∀ j t,
          arrives_in arr_seq j →
          job_task j = tsk →
          t ≤ job_arrival j →
          max_length_of_priority_inversion j t ≤ blocking_bound.

      (* Using the lemma above, we prove that the priority inversion of the task is bounded by
         the maximum length of a nonpreemptive section of lower-priority tasks. *)
      Lemma priority_inversion_is_bounded:
        priority_inversion_is_bounded_by
          job_arrival job_cost job_task arr_seq sched higher_eq_priority tsk blocking_bound.

    End PriorityInversionIsBounded.

    Section ResponseTimeBound.

      (* Let L be any positive fixed point of the busy interval recurrence. *)
      Variable L: time.
      Hypothesis H_L_positive: L > 0.
      Hypothesis H_fixed_point: L = total_rbf L.

      (* To reduce the time complexity of the analysis, recall the notion of search space. *)
      Let is_in_search_space A :=
        (A < L ) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A ).

      (* Consider any value R, and assume that for any given arrival offset A in the search space,
         there is a solution of the response-time bound recurrence which is bounded by R. *)
      Variable R: nat.
      Hypothesis H_R_is_maximum:
        ∀ A,
          is_in_search_space A →
          ∃ F ,
            A + F = blocking_bound
                    + (task_rbf (A + ε) - (task_cost tsk - task_lock_in_service tsk ))
                    + bound_on_total_hep_workload A (A + F) ∧
            F + (task_cost tsk - task_lock_in_service tsk ) ≤ R.

      (* Then, using the results for the general RTA for EDF-schedulers, we establish a
         response-time bound for the more concrete model of bounded nonpreemptive segments.
         Note that in case of the general RTA for EDF-schedulers, we just _assume_ that
         the priority inversion is bounded. In this module we provide the preemption model
         with bounded nonpreemptive segments and _prove_ that the priority inversion is
         bounded. *)
      Theorem uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments:
        response_time_bounded_by tsk R.

    End ResponseTimeBound.

  End Analysis.

End RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.

Library prosa.classic.model.schedule.uni.limited.edf.nonpr_reg.response_time_bound

RTA for EDF-schedulers with bounded nonpreemprive segments

Priority inversion is bounded

Response-Time Bound