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

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task
               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.schedulability prosa.classic.model.schedule.uni.service
               prosa.classic.model.schedule.uni.workload
               prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.jitter.schedule
               prosa.classic.model.schedule.uni.jitter.platform.
Require Import prosa.classic.model.schedule.uni.susp.suspension_intervals
               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.analysis.uni.susp.dynamic.jitter.jitter_schedule
               prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties.
Require Import prosa.classic.model.schedule.uni.transformation.construction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.

Module JitterScheduleService.

  Import Job SporadicTaskset Suspension Priority SuspensionIntervals Workload Service
         UniprocessorScheduleWithJitter Schedulability ResponseTime TaskArrival
         ScheduleConstruction ValidSuspensionAwareSchedule.

  Module basic := schedule.UniprocessorSchedule.
  Module susp := ScheduleWithSuspensions.
  Module jitter_aware := Platform.
  Module susp_aware := PlatformWithSuspensions.
  Module job_jitter := JobWithJitter.
  Module reduction := JitterScheduleConstruction.
  Module reduction_prop := JitterScheduleProperties.

  Section ProvingScheduleProperties.

    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_cost: Job → time.
    Variable job_deadline: Job → time.
    Variable job_task: Job → Task.

    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_from_taskset:
      ∀ j, arrives_in arr_seq j → job_task j \in ts.

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

    Hypothesis H_constrained_deadlines:
      constrained_deadline_model task_period task_deadline ts.
    Hypothesis H_sporadic_arrivals:
      sporadic_task_model task_period job_arrival job_task arr_seq.

    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.

    Variable job_suspension_duration: job_suspension Job.

    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 job_response_time_in_sched_susp_bounded_by :=
      is_response_time_bound_of_job job_arrival job_cost sched_susp.
    Let job_misses_no_deadline_in_sched_susp :=
      job_misses_no_deadline job_arrival job_cost job_deadline sched_susp.

    Variable j: Job.
    Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
    Let arr_j := job_arrival j.

    Variable R_j: time.

    Let other_hep_task tsk_other :=
      higher_eq_priority tsk_other (job_task j) && (tsk_other != job_task j).

    Variable R_hp: Job → time.
    Hypothesis H_bounded_response_time_of_hp_jobs:
      ∀ 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 (R_hp j_hp).

    Hypothesis H_no_deadline_misses_for_previous_jobs:
      ∀ j0,
        arrives_in arr_seq j0 →
        job_arrival j0 < job_arrival j →
        job_task j0 = job_task j →
        job_misses_no_deadline_in_sched_susp j0.

    Let sched_jitter := reduction.sched_jitter job_arrival job_task arr_seq higher_eq_priority
                                               job_cost job_suspension_duration j 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 R_hp.

    Let actual_job_arrival := actual_arrival job_arrival job_jitter.
    Let job_arrived_before := arrived_before job_arrival.
    Let job_has_arrived := has_arrived job_arrival.
    Let job_has_actually_arrived := jitter_has_passed job_arrival job_jitter.
    Let job_completed_in_sched_jitter := completed_by inflated_job_cost sched_jitter.

    Let job_suspended_at :=
      suspended_at job_arrival job_cost job_suspension_duration sched_susp.
    Let job_cumulative_suspension :=
      cumulative_suspension_during job_arrival job_cost job_suspension_duration sched_susp.
    Let job_completed_in_sched_susp := completed_by job_cost sched_susp.
    Let backlogged_in_sched_susp := susp.backlogged job_arrival job_cost
                                                    job_suspension_duration sched_susp.

    Let arrivals := jobs_arrived_between arr_seq.
    Let actual_arrivals := actual_arrivals_between job_arrival job_jitter arr_seq.

    Let arrivals_before_end_of_interval := arrivals 0 (arr_j + R_j).
    Let actual_arrivals_before_end_of_interval := actual_arrivals 0 (arr_j + R_j).

    Let other_higher_eq_priority_job j_hp :=
      higher_eq_priority (job_task j_hp) (job_task j) && (j_hp != j).

    Definition workload_of_other_hep_jobs_in_sched_susp t1 t2 :=
      workload_of_jobs job_cost (arrivals t1 t2) other_higher_eq_priority_job.

    Definition workload_of_other_hep_jobs_in_sched_jitter t1 t2 :=
      workload_of_jobs inflated_job_cost (actual_arrivals t1 t2) other_higher_eq_priority_job.

    Definition service_of_other_hep_jobs_in_sched_susp t1 t2 :=
      service_of_jobs sched_susp arrivals_before_end_of_interval other_higher_eq_priority_job t1 t2.

    Definition service_of_other_hep_jobs_in_sched_jitter t1 t2 :=
      service_of_jobs sched_jitter actual_arrivals_before_end_of_interval
                      other_higher_eq_priority_job t1 t2.

    Section AuxiliaryLemmas.

      Section ServiceEqualsWorkload.

        Variable t: time.
        Hypothesis H_before_end_of_interval: t ≤ arr_j + R_j.

        Hypothesis H_workload_has_finished:
          ∀ j_hp,
            arrives_in arr_seq j_hp →
            actual_arrival_before job_arrival job_jitter j_hp t →
            other_higher_eq_priority_job j_hp →
            job_completed_in_sched_jitter j_hp t.

        Lemma jitter_reduction_service_equals_workload_in_jitter:
          service_of_other_hep_jobs_in_sched_jitter 0 t ≥
          workload_of_other_hep_jobs_in_sched_jitter 0 t.

      End ServiceEqualsWorkload.

      Section ServiceBoundedByWorkload.

        Variable t: time.
        Hypothesis H_before_end_of_interval: t ≤ arr_j + R_j.

        Lemma jitter_reduction_service_in_sched_susp_le_workload:
          service_of_other_hep_jobs_in_sched_susp 0 t ≤
          workload_of_other_hep_jobs_in_sched_susp 0 t.

      End ServiceBoundedByWorkload.

    End AuxiliaryLemmas.

    Section LessServiceBeforeArrival.

      Section LessServiceForEachJob.

          Variable j_hp: Job.
          Hypothesis H_arrives: arrives_in arr_seq j_hp.
          Hypothesis H_higher_or_equal_priority: other_higher_eq_priority_job j_hp.

          Let arr_hp := job_arrival j_hp.
          Let cost_hp := job_cost j_hp.
          Let Rhp := R_hp j_hp.

          Section Case1.

            Hypothesis H_same_task: job_task j_hp = job_task j.

            Lemma jitter_reduction_less_job_service_before_interval_case1:
              service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

          End Case1.

          Section Case2.

            Hypothesis H_different_task: job_task j_hp != job_task j.

            Hypothesis H_released_no_earlier: arr_j ≤ actual_job_arrival j_hp.

            Lemma jitter_reduction_less_job_service_before_interval_case2:
              service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

          End Case2.

          Section Case3.

            Hypothesis H_different_task: job_task j_hp != job_task j.

            Hypothesis H_distance_is_smaller:
              arr_j - arr_hp < Rhp - cost_hp.

            Lemma jitter_reduction_less_job_service_before_interval_case3:
              service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

          End Case3.

          Section Case4.

            Hypothesis H_different_task: job_task j_hp != job_task j.

            Hypothesis H_completes_before_j_arrives: arr_hp + Rhp ≤ arr_j.

            Lemma jitter_reduction_less_job_service_before_interval_case4:
              service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

          End Case4.

          Section Case5.

            Hypothesis H_different_task: job_task j_hp != job_task j.

            Hypothesis H_released_before: actual_job_arrival j_hp < arr_j.

            Hypothesis H_j_hp_completes_after_j_arrives: arr_j < arr_hp + Rhp.
            Hypothesis H_distance_is_not_smaller: Rhp - cost_hp ≤ arr_j - arr_hp.

            Remark jitter_reduction_jitter_equals_R_minus_cost:
              job_jitter j_hp = Rhp - cost_hp.

            Lemma jitter_reduction_less_job_service_before_interval_case5:
              service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

          End Case5.

          Lemma jitter_reduction_less_job_service_before_interval:
            service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.

      End LessServiceForEachJob.

      Corollary jitter_reduction_less_service_before_the_interval:
        service_of_other_hep_jobs_in_sched_jitter 0 arr_j ≤
        service_of_other_hep_jobs_in_sched_susp 0 arr_j.

    End LessServiceBeforeArrival.

    Section MoreServiceAfterArrival.

      Section Conservation.

        Variable t: time.
        Hypothesis H_no_earlier_than_j: t ≥ arr_j.

        Lemma jitter_reduction_actual_arrival_before_end_of_interval:
          ∀ j_hp,
            other_higher_eq_priority_job j_hp →
            job_arrival j_hp ≤ t →
            actual_job_arrival j_hp ≤ t.

        Lemma jitter_reduction_workload_conservation_inside_interval:
            workload_of_other_hep_jobs_in_sched_susp 0 t.+1 ≤
            workload_of_other_hep_jobs_in_sched_jitter 0 t.+1.

      End Conservation.

      Section MoreServiceInsideTheInterval.


        Section InductiveStep.

          Variable d: time.
          Hypothesis H_d_lt_R: d < R_j.

          Hypothesis H_induction_hypothesis:
            service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d) ≤
            service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d).


          Section NoPendingJobs.

            Hypothesis H_all_jobs_completed_in_sched_jitter:
              ∀ j_hp,
                arrives_in arr_seq j_hp →
                other_higher_eq_priority_job j_hp →
                job_has_actually_arrived j_hp (arr_j + d) →
                job_completed_in_sched_jitter j_hp (arr_j + d).

            Lemma jitter_reduction_convert_service_to_workload:
              service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) ≤
                workload_of_other_hep_jobs_in_sched_susp 0 (arr_j + d + 1)
                - service_of_other_hep_jobs_in_sched_susp 0 arr_j.

            Lemma jitter_reduction_compare_workload:
                  workload_of_other_hep_jobs_in_sched_susp 0 (arr_j + d + 1)
                          - service_of_other_hep_jobs_in_sched_susp 0 arr_j
               ≤ workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
                          - service_of_other_hep_jobs_in_sched_susp 0 arr_j.

            Lemma jitter_reduction_compare_service:
                  workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
                          - service_of_other_hep_jobs_in_sched_susp 0 arr_j
               ≤ workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
                         - service_of_other_hep_jobs_in_sched_jitter 0 arr_j.

            Lemma jitter_reduction_convert_workload_to_service:
              workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1) -
                service_of_other_hep_jobs_in_sched_jitter 0 arr_j ≤
              service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).

            Lemma jitter_reduction_inductive_step_case1:
                service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) ≤
                service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).

          End NoPendingJobs.

          Section ThereArePendingJobs.

            Hypothesis H_there_are_pending_jobs_in_sched_jitter:
              ∃ j_hp,
                arrives_in arr_seq j_hp ∧
                other_higher_eq_priority_job j_hp ∧
                job_has_actually_arrived j_hp (arr_j + d) ∧
                ~~ job_completed_in_sched_jitter j_hp (arr_j + d).


            Lemma jitter_reduction_inductive_step_case2:
              service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) ≤
              service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).

          End ThereArePendingJobs.

        End InductiveStep.

        Lemma jitter_reduction_more_service_inside_the_interval:
          ∀ d,
            d ≤ R_j →
            service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d) ≤
            service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d).

      End MoreServiceInsideTheInterval.

    End MoreServiceAfterArrival.

    Section JitterAwareScheduleIsWorse.

      Let job_response_time_in_sched_jitter_bounded_by :=
        is_response_time_bound_of_job job_arrival inflated_job_cost sched_jitter.


      Lemma jitter_reduction_service_jitter:
        service_during sched_jitter j arr_j (arr_j + R_j) ≤
        R_j - service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + R_j).

      Section JobNotCompleted.

        Hypothesis H_j_not_completed:
          ~~ job_completed_in_sched_susp j (arr_j + R_j).

        Lemma jitter_reduction_service_susp:
          R_j - service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + R_j) ≤
          service_during sched_susp j arr_j (arr_j + R_j) +
          job_cumulative_suspension j arr_j (arr_j + R_j).

        Lemma jitter_reduction_less_service_for_job_j:
          service_during sched_jitter j arr_j (arr_j + R_j) ≤
          service_during sched_susp j arr_j (arr_j + R_j)
          + job_cumulative_suspension j arr_j (arr_j + R_j).

      End JobNotCompleted.

      Hypothesis H_response_time_of_j_in_sched_jitter:
        job_response_time_in_sched_jitter_bounded_by j R_j.

      Corollary jitter_reduction_job_j_completes_no_later:
        job_response_time_in_sched_susp_bounded_by j R_j.

    End JitterAwareScheduleIsWorse.

  End ProvingScheduleProperties.

End JitterScheduleService.