Library prosa.classic.analysis.uni.susp.sustainability.singlecost.reduction_properties

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.response_time.
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.susp.sustainability.singlecost.reduction.
Require Import prosa.classic.model.schedule.uni.transformation.construction.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module SustainabilitySingleCostProperties.

  Import ScheduleWithSuspensions Suspension Priority SuspensionIntervals
         PlatformWithSuspensions ResponseTime ScheduleConstruction.

  Module reduction := SustainabilitySingleCost.

  Section ReductionProperties.

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

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

    Variable higher_eq_priority: JLDP_policy Job.
    Hypothesis H_priority_is_reflexive: JLDP_is_reflexive higher_eq_priority.
    Hypothesis H_priority_is_transitive: JLDP_is_transitive higher_eq_priority.
    Hypothesis H_priority_is_total: JLDP_is_total arr_seq higher_eq_priority.

    Variable sched_susp: schedule Job.
    Hypothesis H_jobs_come_from_arrival_sequence:
      jobs_come_from_arrival_sequence sched_susp arr_seq.

    Variable job_suspension_duration: job_suspension Job.

    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched_susp.

    Hypothesis H_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched_susp.

    Hypothesis H_work_conserving:
      work_conserving job_arrival job_cost job_suspension_duration arr_seq sched_susp.

    Hypothesis H_respects_priority:
      respects_JLDP_policy job_arrival job_cost job_suspension_duration arr_seq
                           sched_susp higher_eq_priority.

    Hypothesis H_respects_self_suspensions:
      respects_self_suspensions job_arrival job_cost job_suspension_duration sched_susp.

    Variable j: Job.
    Let arr_j := job_arrival j.

    Variable inflated_job_cost: Job → time.

    Hypothesis H_cost_of_j_does_not_decrease: inflated_job_cost j ≥ job_cost j.

    Hypothesis H_inflation_only_for_job_j:
      ∀ any_j,
        any_j != j →
        inflated_job_cost any_j = job_cost any_j.

    Let sched_susp_highercost := reduction.sched_susp_highercost job_arrival arr_seq higher_eq_priority
                                                  sched_susp job_suspension_duration inflated_job_cost.

    Let job_response_time_in_sched_susp_bounded_by :=
      is_response_time_bound_of_job job_arrival job_cost sched_susp.
    Let job_response_time_in_sched_susp_highercost_bounded_by :=
      is_response_time_bound_of_job job_arrival inflated_job_cost sched_susp_highercost.
    Let ready_jobs := reduction.ready_jobs job_arrival arr_seq job_suspension_duration
                                           inflated_job_cost sched_susp_highercost.
    Let hp_job := reduction.highest_priority_job job_arrival arr_seq higher_eq_priority
                                   job_suspension_duration inflated_job_cost sched_susp_highercost.
    Let completed_in_sched_susp := completed_by job_cost sched_susp.
    Let completed_in_sched_susp_highercost := completed_by inflated_job_cost sched_susp_highercost.
    Let suspended_in_sched_susp :=
      suspended_at job_arrival job_cost job_suspension_duration sched_susp.
    Let suspended_in_sched_susp_highercost :=
      suspended_at job_arrival inflated_job_cost job_suspension_duration sched_susp_highercost.
    Let service_in_sched_susp := service sched_susp.
    Let service_in_sched_susp_highercost := service sched_susp_highercost.

    Section PropertiesOfScheduleConstruction.

      Let build_schedule := reduction.build_schedule job_arrival arr_seq higher_eq_priority
                                               sched_susp job_suspension_duration inflated_job_cost.

      Lemma sched_susp_highercost_depends_only_on_prefix:
        ∀ sched1 sched2 t,
          (∀ t0, t0 < t → sched1 t0 = sched2 t0) →
          build_schedule sched1 t = build_schedule sched2 t.

      Corollary sched_susp_highercost_uses_construction_function:
        ∀ t,
          sched_susp_highercost t = build_schedule sched_susp_highercost t.

    End PropertiesOfScheduleConstruction.

    Section ScheduleIsValid.

      Lemma sched_susp_highercost_jobs_come_from_arrival_sequence:
        jobs_come_from_arrival_sequence sched_susp_highercost arr_seq.

      Lemma sched_susp_highercost_jobs_must_arrive_to_execute:
        jobs_must_arrive_to_execute job_arrival sched_susp_highercost.

      Lemma sched_susp_highercost_completed_jobs_dont_execute:
        completed_jobs_dont_execute inflated_job_cost sched_susp_highercost.

      Lemma sched_susp_highercost_work_conserving:
        work_conserving job_arrival inflated_job_cost job_suspension_duration
                        arr_seq sched_susp_highercost.

      Lemma sched_susp_highercost_respects_policy:
        respects_JLDP_policy job_arrival inflated_job_cost job_suspension_duration
                             arr_seq sched_susp_highercost higher_eq_priority.

      Lemma sched_susp_highercost_respects_self_suspensions:
        respects_self_suspensions job_arrival inflated_job_cost
                                  job_suspension_duration sched_susp_highercost.

    End ScheduleIsValid.

    Section SchedulingInvariant.

      Section InductiveStep.

        Variable t: time.
        Hypothesis H_j_has_not_completed: ~~ completed_in_sched_susp j t.

        Hypothesis H_schedules_are_the_same:
          ∀ k any_j,
            k < t →
            scheduled_at sched_susp any_j k = scheduled_at sched_susp_highercost any_j k.

        Variable k: time.
        Hypothesis H_k_before_t: k ≤ t.

        Lemma sched_susp_highercost_same_completion:
          ∀ any_j,
            completed_in_sched_susp any_j k = completed_in_sched_susp_highercost any_j k.

        Lemma sched_susp_highercost_same_time_after_last_exec:
          ∀ any_j,
            time_after_last_execution job_arrival sched_susp any_j k =
            time_after_last_execution job_arrival sched_susp_highercost any_j k.

        Lemma sched_susp_highercost_same_suspension_duration:
          ∀ any_j,
            has_arrived job_arrival any_j k →
            suspension_duration job_arrival job_suspension_duration sched_susp any_j k =
            suspension_duration job_arrival job_suspension_duration sched_susp_highercost any_j k.

        Lemma sched_susp_highercost_same_suspension:
          ∀ any_j,
            has_arrived job_arrival any_j k →
            suspended_in_sched_susp any_j k = suspended_in_sched_susp_highercost any_j k.

        Lemma sched_susp_highercost_same_schedule:
          ∀ any_j,
            scheduled_at sched_susp any_j k = scheduled_at sched_susp_highercost any_j k.

      End InductiveStep.

      Lemma scheduled_in_susp_iff_scheduled_in_wcet:
        ∀ t any_j,
          ~~ completed_in_sched_susp j t →
          scheduled_at sched_susp any_j t = scheduled_at sched_susp_highercost any_j t.

    End SchedulingInvariant.

    Section ComparingResponseTimes.

      Hypothesis H_cost_j_positive: job_cost j > 0.

      Variable r: time.
      Hypothesis H_response_time_bound_in_sched_susp:
        job_response_time_in_sched_susp_bounded_by j r.
      Hypothesis H_response_time_bound_is_tight:
        ∀ r', job_response_time_in_sched_susp_bounded_by j r' → r ≤ r'.

      Variable R: time.
      Hypothesis H_response_time_bound_in_sched_susp_highercost:
        job_response_time_in_sched_susp_highercost_bounded_by j R.

      Lemma sched_susp_highercost_same_service_for_j:
        ∀ t,
          t ≤ arr_j + r →
          service_in_sched_susp j t = service_in_sched_susp_highercost j t.

      Lemma sched_susp_highercost_r_le_R: r ≤ R.

      Lemma R_bounds_inflated_cost: R ≥ inflated_job_cost j.

      Theorem sched_susp_highercost_incurs_more_interference:
        r - job_cost j ≤ R - inflated_job_cost j.

    End ComparingResponseTimes.

  End ReductionProperties.

End SustainabilitySingleCostProperties.