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

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job
               prosa.classic.model.arrival.basic.task_arrival prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.arrival.jitter.job.
Require Import prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.susp.schedule prosa.classic.model.schedule.uni.susp.platform
               prosa.classic.model.schedule.uni.susp.valid_schedule.
Require Import prosa.classic.model.schedule.uni.jitter.valid_schedule.
Require Import prosa.classic.analysis.uni.susp.dynamic.jitter.rta_by_reduction
               prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation
               prosa.classic.analysis.uni.susp.dynamic.jitter.taskset_membership.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module TaskSetRTA.

  Import SporadicTaskset Suspension Priority ValidSuspensionAwareSchedule
         ScheduleWithSuspensions ResponseTime PlatformWithSuspensions
         TaskArrival ValidJitterAwareSchedule RTAByReduction TaskSetMembership.

  Module ts_gen := JitterTaskSetGeneration.
  Module job_susp := Job.
  Module job_jitter := JobWithJitter.

  Section PerTaskAnalysis.

    Context {Task: eqType}.
    Variable task_cost: Task → time.
    Variable task_period: Task → time.
    Variable task_deadline: Task → time.
    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_deadline: Job → time.
    Variable job_task: Job → Task.

    Variable ts: seq Task.
    Hypothesis H_constrained_deadlines:
      constrained_deadline_model task_period task_deadline ts.

    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_sporadic_arrivals:
      sporadic_task_model task_period job_arrival job_task arr_seq.

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

    Hypothesis H_job_deadline_eq_task_deadline:
      ∀ j, arrives_in arr_seq j → job_deadline j = task_deadline (job_task j).

    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.
    Let is_valid_jitter_aware_schedule :=
      valid_jitter_aware_schedule job_arrival arr_seq job_higher_eq_priority.

    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.

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

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

    Hypothesis H_R_le_deadline: R tsk_i ≤ task_deadline tsk_i.

    Let job_cost_positive job_cost :=
      ∀ j, arrives_in arr_seq j → job_cost j > 0.

    Let job_cost_le_task_cost job_cost task_cost :=
      ∀ j,
        arrives_in arr_seq j →
        job_cost j ≤ task_cost (job_task j).

    Let job_jitter_le_task_jitter job_jitter task_jitter :=
      ∀ j,
        arrives_in arr_seq j →
        job_jitter j ≤ task_jitter (job_task j).

    Definition valid_jobs_with_jitter job_cost job_jitter task_cost task_jitter :=
      job_cost_positive job_cost ∧
      job_cost_le_task_cost job_cost task_cost ∧
      job_jitter_le_task_jitter job_jitter task_jitter.

    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_valid_response_time_bound_of_tsk_i:
      ∀ job_cost job_jitter sched,
        valid_jobs_with_jitter job_cost job_jitter inflated_task_cost task_jitter →
        is_valid_jitter_aware_schedule job_cost job_jitter sched →
        is_task_response_time_bound_with job_cost sched tsk_i (R tsk_i).

    Variable job_cost: Job → time.

    Variable sched_susp: schedule Job.
    Hypothesis H_valid_schedule: is_valid_suspension_aware_schedule job_cost sched_susp.

    Hypothesis H_job_cost_positive:
      ∀ 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.

    Theorem valid_response_time_bound_of_tsk_i:
      is_task_response_time_bound_with job_cost sched_susp tsk_i (R tsk_i).

  End PerTaskAnalysis.

End TaskSetRTA.