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

Abstract RTA for EDF-schedulers

In this module we propose the abstract response-time analysis (RTA) for EDF uniprocessor scheduling of real-time tasks with arbitrary arrival models.

Module AbstractRTAforEDFwithArrivalCurves.

  Import Job ArrivalCurves TaskArrival ScheduleOfTask Priority
         UniprocessorSchedule Workload Service ResponseTime MaxArrivalsWorkloadBound
         BusyIntervalJLFP LimitedPreemptionPlatform RBF Service JLFPInstantiation.

  Section AbstractResponseTimeAnalysisForEDF.

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

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

    Let D tsk := task_deadline tsk.

    Let job_relative_deadline j := D (job_task j).

    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.

    Variable sched: schedule Job.
    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.

    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.

    Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.

    Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.

    Hypothesis H_job_cost_le_task_cost:
      cost_of_jobs_from_arrival_sequence_le_task_cost
        task_cost job_cost job_task arr_seq.

    Variable ts: list Task.

    Hypothesis H_all_jobs_from_taskset:
      ∀ j, arrives_in arr_seq j → job_task j \in ts.

    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.

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

    Variable job_lock_in_service: Job → time.
    Variable task_lock_in_service: Task → time.

    Hypothesis H_proper_job_lock_in_service:
      proper_job_lock_in_service job_cost arr_seq sched job_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.

    Let EDF: JLFP_policy Job := EDF job_arrival job_relative_deadline.

    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_scheduled_at := task_scheduled_at job_task sched.
    Let quiet_time := quiet_time job_arrival job_cost arr_seq sched EDF.
    Let response_time_bounded_by :=
      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
    Let cumulative_task_interference :=
      AbstractSeqRTA.cumul_task_interference job_task arr_seq sched.

    Let rbf := task_request_bound_function task_cost max_arrivals.

    Let task_rbf := rbf tsk.

    Let total_rbf := total_request_bound_function task_cost max_arrivals ts.

    Variable priority_inversion_bound: time.
    Hypothesis H_priority_inversion_is_bounded:
      priority_inversion_is_bounded_by
        job_arrival job_cost job_task arr_seq sched EDF tsk priority_inversion_bound.

    Variable L: time.
    Hypothesis H_L_positive: L > 0.
    Hypothesis H_fixed_point: L = total_rbf L.

    Let bound_on_total_hep_workload A Δ :=
      \sum_(tsk_o <- ts | tsk_o != tsk)
       rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).

    Definition task_rbf_changes_at A := task_rbf A != task_rbf (A + ε).

    Definition bound_on_total_hep_workload_changes_at A :=
       has (fun tsko ⇒
           (tsk != tsko )
             && (rbf tsko (A + D tsk - D tsko )
                     != rbf tsko ((A + ε) + D tsk - D tsko))) ts.

    Let is_in_search_space A :=
      (A < L ) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A ).

    Variable R: nat.
    Hypothesis H_R_is_maximum:
      ∀ A,
        is_in_search_space A →
        ∃ F ,
          A + F = priority_inversion_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.

    Let interference (j: Job) (t: time) :=
      interference sched EDF j t.

    Let interfering_workload (j: Job) (t: time) := interfering_workload job_cost arr_seq sched EDF j t.

    Let IBF A R := priority_inversion_bound + bound_on_total_hep_workload A R.

Filling Out Hypothesis Of Abstract RTA Theorem

In this section we prove that all hypotheses necessary to use the abstract theorem are satisfied.

    Section FillingOutHypothesesOfAbstractRTATheorem.

      Lemma instantiated_i_and_w_are_coherent_with_schedule:
        AbstractRTADefinitions.work_conserving
          job_arrival job_cost job_task arr_seq sched tsk interference interfering_workload.

      Lemma instantiated_interference_and_workload_consistent_with_sequential_jobs:
        AbstractSeqRTA.interference_and_workload_consistent_with_sequential_jobs
          job_arrival job_cost job_task arr_seq sched tsk interference interfering_workload.

      Lemma instantiated_busy_intervals_are_bounded:
        AbstractRTADefinitions.busy_intervals_are_bounded_by
          job_arrival job_cost job_task arr_seq sched tsk interference interfering_workload L.

      Lemma instantiated_task_interference_is_bounded:
        AbstractSeqRTA.task_interference_is_bounded_by
          job_arrival job_cost job_task arr_seq sched tsk interference interfering_workload
          (fun tsk A R ⇒ IBF A R).

      Section SolutionOfResponseTimeReccurenceExists.

        Variable j: Job.
        Hypothesis H_j_arrives: arrives_in arr_seq j.
        Hypothesis H_job_of_tsk: job_task j = tsk.
        Hypothesis H_job_cost_positive: job_cost_positive job_cost j.

        Let total_interference_bound tsk A Δ :=
          task_rbf (A + ε) - task_cost tsk + IBF A Δ.

        Variable A: time.
        Hypothesis H_A_is_in_abstract_search_space:
          AbstractRTAReduction.is_in_search_space tsk L total_interference_bound A.

        Lemma A_is_in_concrete_search_space:
          is_in_search_space A.

        Corollary correct_search_space:
          ∃ F ,
            A + F = task_rbf (A + ε) - (task_cost tsk - task_lock_in_service tsk) + IBF A (A + F) ∧
            F + (task_cost tsk - task_lock_in_service tsk) ≤ R.

      End SolutionOfResponseTimeReccurenceExists.

    End FillingOutHypothesesOfAbstractRTATheorem.

Final Theorem

    Theorem uniprocessor_response_time_bound_edf:
      response_time_bounded_by tsk R.

  End AbstractResponseTimeAnalysisForEDF.

End AbstractRTAforEDFwithArrivalCurves.