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

RTA for concrete models

In this module we prove the RTA theorems for (1) fully preemptive EDF model, (2) fully nonpreemptive EDF model, (3) EDF with fixed premption points, and (4) EDF with floating nonpreemptive regions.

Module RTAforConcreteModels.

  Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
         ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
         RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves NonpreemptiveSchedule
         FullyNonPreemptivePlatform FullyPreemptivePlatform AbstractRTAforEDFwithArrivalCurves.

  Section Analysis.

    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).

    Let higher_eq_priority: JLFP_policy Job := EDF job_arrival job_relative_deadline.

    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 ts: list Task.

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

    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 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 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_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.

    Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.

    Let response_time_bounded_by :=
      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
    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 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.

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

RTA for fully preemptive EDF model

In this section we prove the RTA theorem for the fully preemptive EDF model

    Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.

      Hypothesis H_respects_policy:
        respects_JLFP_policy_at_preemption_point
          job_arrival job_cost arr_seq sched
          can_be_preempted_for_fully_preemptive_model higher_eq_priority.

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

      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 = task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) ∧
            F ≤ R.

      Theorem uniprocessor_response_time_bound_fully_preemptive_edf:
        response_time_bounded_by tsk R.

    End RTAforFullyPreemptiveEDFModelwithArrivalCurves.

RTA for fully nonpreemptive EDF model

In this section we prove the RTA theorem for the fully nonpreemptive EDF model.

    Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.

      Hypothesis H_nonpreemptive_sched: is_nonpreemptive_schedule job_cost sched.

      Hypothesis H_respects_policy:
        respects_JLFP_policy_at_preemption_point
          job_arrival job_cost arr_seq sched
          (can_be_preempted_for_fully_nonpreemptive_model job_cost) higher_eq_priority.

      Let blocking_bound :=
        \max_(tsk_other <- ts | (tsk_other != tsk ) && (D tsk_other > D tsk ))
         (task_cost tsk_other - ε).

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

      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 = blocking_bound + (task_rbf (A + ε) - (task_cost tsk - ε))
                    + bound_on_total_hep_workload A (A + F) ∧
            F + (task_cost tsk - ε) ≤ R.

      Theorem uniprocessor_response_time_bound_fully_nonpreemptive_edf:
        response_time_bounded_by tsk R.

    End RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.

RTA for EDF with fixed premption points

In this module we prove a general RTA theorem for EDF-schedulers with fixed preemption points

    Section RTAforFixedPreemptionPointsModelwithArrivalCurves.

      Variable job_preemption_points: Job → seq time.
      Variable task_preemption_points: Task → seq time.
      Hypothesis H_model_with_fixed_preemption_points:
        fixed_preemption_points_model
          task_cost job_cost job_task arr_seq
          job_preemption_points task_preemption_points ts.

      Hypothesis H_schedule_with_limited_preemptions:
        is_schedule_with_limited_preemptions arr_seq job_preemption_points sched.

      Hypothesis H_respects_policy:
        respects_JLFP_policy_at_preemption_point
          job_arrival job_cost arr_seq sched
          (can_be_preempted_for_model_with_limited_preemptions job_preemption_points) higher_eq_priority.

      Let job_max_nps := job_max_nps job_preemption_points.
      Let job_last_nps := job_last_nps job_preemption_points.
      Let task_max_nps := task_max_nps task_preemption_points.
      Let task_last_nps := task_last_nps task_preemption_points.

      Let blocking_bound :=
        \max_(tsk_other <- ts | (tsk_other != tsk ) && (D tsk_other > D tsk ))
         (task_max_nps tsk_other - ε).

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

      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 = blocking_bound
                    + (task_rbf (A + ε) - (task_last_nps tsk - ε))
                    + bound_on_total_hep_workload A (A + F) ∧
            F + (task_last_nps tsk - ε) ≤ R.

      Theorem uniprocessor_response_time_bound_edf_with_fixed_preemption_points:
        response_time_bounded_by tsk R.

    End RTAforFixedPreemptionPointsModelwithArrivalCurves.

RTA for EDF with floating nonpreemptive regions

In this module we prove a general RTA theorem for EDF-schedulers with floating nonpreemptive regions

    Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.

      Variable job_preemption_points: Job → seq time.
      Variable task_max_nps: Task → time.
      Hypothesis H_task_model_with_floating_nonpreemptive_regions:
        model_with_floating_nonpreemptive_regions
          job_cost job_task arr_seq job_preemption_points task_max_nps.

      Hypothesis H_schedule_with_limited_preemptions:
        is_schedule_with_limited_preemptions arr_seq job_preemption_points sched.

      Hypothesis H_respects_policy:
        respects_JLFP_policy_at_preemption_point
          job_arrival job_cost arr_seq sched
          (can_be_preempted_for_model_with_limited_preemptions job_preemption_points) higher_eq_priority.

      Let job_max_nps := job_max_nps job_preemption_points.
      Let job_last_nps := job_last_nps job_preemption_points.

      Definition blocking_bound :=
        \max_(tsk_other <- ts | (tsk_other != tsk ) && (D tsk_other > D tsk ))
         (task_max_nps tsk_other - ε).

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

      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 = blocking_bound + task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) ∧
            F ≤ R.

      Theorem uniprocessor_response_time_bound_edf_with_floating_nonpreemptive_regions:
        response_time_bounded_by tsk R.

    End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.

  End Analysis.

End RTAforConcreteModels.