Library rt.analysis.uni.susp.sustainability.singlecost.reduction_properties

Require Import rt.util.all.
Require Import rt.model.priority rt.model.suspension.
Require Import rt.model.arrival.basic.arrival_sequence.
Require Import rt.model.schedule.uni.response_time.
Require Import rt.model.schedule.uni.susp.suspension_intervals
               rt.model.schedule.uni.susp.schedule
               rt.model.schedule.uni.susp.platform.
Require Import rt.analysis.uni.susp.sustainability.singlecost.reduction.
Require Import rt.model.schedule.uni.transformation.construction.


(* In this file, we prove that the in the generated suspension-aware schedule, 
   the response time of the job whose cost is inflated does not decrease. *)
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.

    (* Consider any job arrival sequence with consistent job arrivals. *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent:
      arrival_times_are_consistent job_arrival arr_seq.

    (* Assume any (schedule-independent) JLDP policy that is reflexive, transitive and total,
       i.e., that indicates "higher-or-equal priority". *)
    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.

    (* Next, consider any suspension-aware schedule of the arrival sequence... *)
    Variable sched_susp: schedule Job.
    Hypothesis H_jobs_come_from_arrival_sequence:
      jobs_come_from_arrival_sequence sched_susp arr_seq.

    (* ...and the associated job suspension times. *)
    Variable job_suspension_duration: job_suspension Job.

    (* Assume that, in this schedule, jobs only execute after they arrive... *)
    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched_susp.

    (* ...and no longer than their execution costs. *)
    Hypothesis H_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched_susp.

    (* Also assume that the schedule is work-conserving if there are non-suspended jobs, ... *)
    Hypothesis H_work_conserving:
      work_conserving job_arrival job_cost job_suspension_duration arr_seq sched_susp.

    (* ...that the schedule respects job priorities... *)
    Hypothesis H_respects_priority:
      respects_JLDP_policy job_arrival job_cost job_suspension_duration arr_seq
                           sched_susp higher_eq_priority.

    (* ...and that suspended jobs are not allowed to be scheduled. *)
    Hypothesis H_respects_self_suspensions:
      respects_self_suspensions job_arrival job_cost job_suspension_duration sched_susp.

    (* Now we prove properties about the reduction. Let j be any job. *)
    Variable j: Job.
    Let arr_j := job_arrival j.

    (* Next, consider any job cost inflation... *)
    Variable inflated_job_cost: Job → time.

    (* ...that does not decrease the cost of job j... *)
    Hypothesis H_cost_of_j_does_not_decrease: inflated_job_cost j ≥ job_cost j.

    (* ...and that preserves the cost of the remaining jobs. *)
    Hypothesis H_inflation_only_for_job_j:
      ∀ any_j,
        any_j != j →
        inflated_job_cost any_j = job_cost any_j.

    (* Recall the schedule we constructed from sched_susp by inflating the cost of job j. *)
    Let sched_susp_highercost := reduction.sched_susp_highercost job_arrival arr_seq higher_eq_priority
                                                  sched_susp job_suspension_duration inflated_job_cost.

    (* For simplicity, we define some local names for the definitions related to both schedules. *)
    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.

    (* In this section, we prove that the new schedule uses its construction function. *)
    Section PropertiesOfScheduleConstruction.

      (* Recall the construction function of the new schedule. *)
      Let build_schedule := reduction.build_schedule job_arrival arr_seq higher_eq_priority
                                               sched_susp job_suspension_duration inflated_job_cost.

      (* By showing that the construction function depends only on the schedule prefix, ... *)
      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.

      (* ...we infer that the new schedule is indeed based on the construction function. *)
      Corollary sched_susp_highercost_uses_construction_function:
        ∀ t,
          sched_susp_highercost t = build_schedule sched_susp_highercost t.

    End PropertiesOfScheduleConstruction.

    (* In this section, we prove that sched_susp_highercost is a valid suspension-aware schedule. *)
    Section ScheduleIsValid.

      (* First, we show that scheduled jobs come from the arrival sequence. *)
      Lemma sched_susp_highercost_jobs_come_from_arrival_sequence:
        jobs_come_from_arrival_sequence sched_susp_highercost arr_seq.

      (* Next, we show that jobs do not execute before their arrival times... *)
      Lemma sched_susp_highercost_jobs_must_arrive_to_execute:
        jobs_must_arrive_to_execute job_arrival sched_susp_highercost.

      (* ...nor longer than their execution costs. *)
      Lemma sched_susp_highercost_completed_jobs_dont_execute:
        completed_jobs_dont_execute inflated_job_cost sched_susp_highercost.

      (* In addition, we prove that the new schedule is work-conserving,... *)
      Lemma sched_susp_highercost_work_conserving:
        work_conserving job_arrival inflated_job_cost job_suspension_duration
                        arr_seq sched_susp_highercost.

      (* ...respects job priorities, ... *)
      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.

      (* ...and does not allow suspended jobs to be scheduled. *)
      Lemma sched_susp_highercost_respects_self_suspensions:
        respects_self_suspensions job_arrival inflated_job_cost
                                  job_suspension_duration sched_susp_highercost.

    End ScheduleIsValid.

    (* In this section, we compare the two schedules to determine they are the same
       while job j has not completed in sched_susp. *)
    Section SchedulingInvariant.

      (* To prove that the schedules are the same, we use induction over time. *)
      Section InductiveStep.

        (* Consider any time t by which job j has not completed in sched_susp. *)
        Variable t: time.
        Hypothesis H_j_has_not_completed: ~~ completed_in_sched_susp j t.

        (* Induction Hypothesis:
           Assume that at every time prior to time t, any job that is scheduled
           in sched_susp is also scheduled in sched_susp_highercost. *)
        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.

        (* Then, let k be any time no later than t. *)
        Variable k: time.
        Hypothesis H_k_before_t: k ≤ t.

        (* First, we prove that jobs complete at time k in sched_susp iff they
           complete in the new schedule. *)
        Lemma sched_susp_highercost_same_completion:
          ∀ any_j,
            completed_in_sched_susp any_j k = completed_in_sched_susp_highercost any_j k.

        (* We also prove the execution patterns of the jobs coincide... *)
        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.

        (* ...and the jobs have the same suspension intervals, ... *)
        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.

        (* ...which implies that jobs suspend at time k in sched_susp iff they suspend
           in the new schedule as well. *)
        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.

        (* Using the lemmas above, we conclude the inductive step by showing that the
           two schedules are the same at time 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.

      (* Using the inductive step above, we prove that before the completion of job j
         in sched_susp, the two schedules are exactly the same. *)
      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.

    (* In this section, we use the scheduling invariant above to compare response-time bounds
       for job j in both schedules. *)
    Section ComparingResponseTimes.

      (* Assume that job j has positive cost. *)
      Hypothesis H_cost_j_positive: job_cost j > 0.

      (* Also assume that the response time of job j in sched_susp is equal to some value r... *)
      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'.

      (* ...and that the response time of j in the new schedule is upper-bounded by some value R. *)
      Variable R: time.
      Hypothesis H_response_time_bound_in_sched_susp_highercost:
        job_response_time_in_sched_susp_highercost_bounded_by j R.

      (* Using the scheduling invariant, we show that job j receives the same service
         in both schedules up to time (arr_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.

      (* Next, since r is an exact response time bound, we show that r <= R... *)
      Lemma sched_susp_highercost_r_le_R: r ≤ R.

      (* ...and also prove that R must be as large as the inflated job cost. *)
      Lemma R_bounds_inflated_cost: R ≥ inflated_job_cost j.

      (* To conclude, we prove that the difference between the response-time bound and the job cost
         is larger in the new schedule. *)
      Theorem sched_susp_highercost_incurs_more_interference:
        r - job_cost j ≤ R - inflated_job_cost j.

    End ComparingResponseTimes.

  End ReductionProperties.

End SustainabilitySingleCostProperties.