prosa.classic.analysis.uni.susp.dynamic.jitter.taskset

    Variable ts: seq Task.

    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent:
      arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.

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

    Variable job_cost: Job → time.
    Variable task_cost: Task → time.

    Variable job_suspension_duration: job_suspension Job.
    Variable task_suspension_bound: Task → time.

    Variable higher_eq_priority: FP_policy Task.
    Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
    Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
    Hypothesis H_priority_is_total: FP_is_total_over_task_set higher_eq_priority ts.
    Let job_higher_eq_priority := FP_to_JLDP job_task higher_eq_priority.

    Let is_valid_suspension_aware_schedule :=
      valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
                                      job_suspension_duration.

    Variable sched_susp: schedule Job.
    Hypothesis H_valid_schedule:
      valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
                                      job_suspension_duration job_cost sched_susp.

    Let task_response_time_in_sched_susp_bounded_by :=
      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched_susp.
    Let job_response_time_in_sched_susp_bounded_by :=
      is_response_time_bound_of_job job_arrival job_cost sched_susp.

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

    Variable j: Job.
    Hypothesis H_j_arrives: arrives_in arr_seq j.
    Hypothesis H_job_of_tsk_i: job_task j = tsk_i.

    Let is_task_response_time_bound_with job_cost sched :=
      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.

    Let other_hep_task tsk_other := higher_eq_priority tsk_other tsk_i && (tsk_other != tsk_i ).

    Variable R: Task → time.
    Hypothesis H_valid_response_time_bound_of_hp_tasks_in_all_schedules:
      ∀ job_cost sched,
        is_valid_suspension_aware_schedule job_cost sched →
        ∀ tsk_hp,
          tsk_hp \in ts →
          other_hep_task tsk_hp →
          is_task_response_time_bound_with job_cost sched tsk_hp (R tsk_hp).

    Definition actual_response_time (j_hp: Job) : time :=
      [pick -min r ≤ R (job_task j_hp) |
       job_response_time_in_sched_susp_bounded_by j_hp r ].

    Corollary actual_response_time_is_valid:
      ∀ j_hp,
        arrives_in arr_seq j_hp →
        other_hep_task (job_task j_hp) →
        job_response_time_in_sched_susp_bounded_by j_hp (actual_response_time j_hp).

    Corollary actual_response_time_is_minimum:
      ∀ j_hp r_hp,
        arrives_in arr_seq j_hp →
        other_hep_task (job_task j_hp) →
        job_response_time_in_sched_susp_bounded_by j_hp r_hp →
        actual_response_time j_hp ≤ r_hp.

    Let inflated_job_cost := reduction.inflated_job_cost job_cost job_suspension_duration j.
    Let job_jitter := reduction.job_jitter job_arrival job_task higher_eq_priority job_cost j
                                           actual_response_time.

    Let inflated_task_cost := ts_gen.inflated_task_cost task_cost task_suspension_bound tsk_i.
    Let task_jitter := ts_gen.task_jitter task_cost higher_eq_priority tsk_i R.

    Hypothesis H_positive_costs:
      ∀ j, arrives_in arr_seq j → job_cost j > 0.

    Hypothesis H_job_cost_le_task_cost:
      ∀ j,
        arrives_in arr_seq j →
        job_cost j ≤ task_cost (job_task j).

    Hypothesis H_dynamic_suspensions:
      dynamic_suspension_model job_cost job_task job_suspension_duration task_suspension_bound.

    Section JobCostPositive.

      Lemma ts_membership_inflated_job_cost_positive:
        ∀ j, arrives_in arr_seq j → inflated_job_cost j > 0.

    End JobCostPositive.

    Section JobCostBoundedByTaskCost.

      Lemma ts_membership_inflated_job_cost_le_inflated_task_cost:
        ∀ j,
          arrives_in arr_seq j →
          inflated_job_cost j ≤ inflated_task_cost (job_task j).

    End JobCostBoundedByTaskCost.

    Section JobJitterBoundedByTaskJitter.

      Variable any_j: Job.
      Hypothesis H_any_j_arrives: arrives_in arr_seq any_j.

      Section JitterOfHigherPriorityJobs.

        Hypothesis H_higher_priority: higher_eq_priority (job_task any_j) tsk_i.
        Hypothesis H_different_task: job_task any_j != tsk_i.

        Let higher_cost_wcet j' :=
          if j' == any_j then task_cost (job_task any_j) else job_cost j'.

        Let sched_susp_highercost :=
          sust.sched_susp_highercost job_arrival arr_seq job_higher_eq_priority
                                     sched_susp job_suspension_duration higher_cost_wcet.

        Let task_response_time_in_sched_susp_highercost_bounded_by :=
          is_response_time_bound_of_task job_arrival higher_cost_wcet job_task arr_seq
                                         sched_susp_highercost.

        Remark response_time_bound_in_sched_susp_highercost:
          ∀ tsk_hp,
            tsk_hp \in ts →
            other_hep_task tsk_hp →
            task_response_time_in_sched_susp_highercost_bounded_by tsk_hp (R tsk_hp).

        Lemma ts_membership_difference_in_response_times:
          actual_response_time any_j - job_cost any_j ≤
            R (job_task any_j) - task_cost (job_task any_j).

      End JitterOfHigherPriorityJobs.

      Lemma ts_membership_job_jitter_le_task_jitter:
        job_jitter any_j ≤ task_jitter (job_task any_j).

    End JobJitterBoundedByTaskJitter.

  End ProvingMembership.

End TaskSetMembership.

Library prosa.classic.analysis.uni.susp.dynamic.jitter.taskset_membership