Library prosa.classic.analysis.uni.susp.dynamic.oblivious.fp_rta

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.arrival_sequence
               prosa.classic.model.priority prosa.classic.model.suspension prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.schedulability.
Require Import prosa.classic.model.schedule.uni.susp.suspension_intervals
               prosa.classic.model.schedule.uni.susp.schedule prosa.classic.model.schedule.uni.susp.platform.
Require Import prosa.classic.analysis.uni.basic.fp_rta_comp.
Require Import prosa.classic.analysis.uni.susp.dynamic.oblivious.reduction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module SuspensionObliviousFP.

  Import Job TaskArrival SporadicTaskset Suspension Priority Schedulability
         PlatformWithSuspensions SuspensionIntervals.
  Export ResponseTimeIterationFP ReductionToBasicSchedule.

  Section ReductionToBasicAnalysis.

    Context {SporadicTask: eqType}.
    Variable task_cost: SporadicTask → time.
    Variable task_period: SporadicTask → time.
    Variable task_deadline: SporadicTask → time.

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

    Variable ts: taskset_of SporadicTask.

    Hypothesis H_valid_task_parameters:
      valid_sporadic_taskset task_cost 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_jobs_from_taskset:
      ∀ j, arrives_in arr_seq j → job_task j \in ts.

    Hypothesis H_valid_job_parameters:
      ∀ j,
        arrives_in arr_seq j →
        valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

    Hypothesis H_sporadic_tasks:
      sporadic_task_model task_period job_arrival job_task arr_seq.

    Variable higher_eq_priority: FP_policy SporadicTask.
    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.

    Variable next_suspension: job_suspension Job.
    Variable task_suspension_bound: SporadicTask → time.
    Hypothesis H_dynamic_suspensions:
      dynamic_suspension_model job_cost job_task next_suspension task_suspension_bound.

    Let inflated_cost := inflated_task_cost task_cost task_suspension_bound.

    Hypothesis H_inflated_cost_le_deadline_and_period:
      ∀ tsk,
        tsk \in ts →
          inflated_cost tsk ≤ task_deadline tsk ∧
          inflated_cost tsk ≤ task_period tsk.

    Section MainProof.

      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 next_suspension arr_seq sched.

      Hypothesis H_respects_priority:
        respects_FP_policy job_arrival job_cost job_task next_suspension arr_seq
                           sched higher_eq_priority.

      Hypothesis H_respects_self_suspensions:
        respects_self_suspensions job_arrival job_cost next_suspension sched.

      Let task_is_schedulable :=
        task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.

      Let claimed_to_be_schedulable :=
        fp_schedulable inflated_cost task_period task_deadline higher_eq_priority.

      Hypothesis H_claimed_schedulable_by_suspension_oblivious_RTA:
        claimed_to_be_schedulable ts.

      Theorem suspension_oblivious_fp_rta_implies_schedulability:
        ∀ tsk,
          tsk \in ts →
          task_is_schedulable tsk.

    End MainProof.

  End ReductionToBasicAnalysis.

End SuspensionObliviousFP.