Library rt.analysis.uni.susp.sustainability.allcosts.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.valid_schedule
               rt.model.schedule.uni.susp.build_suspension_table
               rt.model.schedule.uni.susp.platform.
Require Import rt.analysis.uni.susp.sustainability.allcosts.reduction.
Require Import rt.model.schedule.uni.transformation.construction.


(* In this file, we prove several properties about the schedule we constructed
   in the sustainability proof. *)
Module SustainabilityAllCostsProperties.

  Import ScheduleWithSuspensions Suspension Priority SuspensionIntervals
         PlatformWithSuspensions ResponseTime ScheduleConstruction
         SuspensionTableConstruction ValidSuspensionAwareSchedule.

  Module reduction := SustainabilityAllCosts.

  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 the job to be analyzed with arrival time arr_j. *)
    Variable j: Job.
    Let arr_j := job_arrival j.

    (* Suppose that we want to prove that the response time of job j in sched_susp
       is upper-bounded by some value R. This allows us to restrict our analysis
       to the finite scheduling window [0, arr_j + R) during the reduction. *)
    Variable R: time.

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

    (* ...in which the cost of every job is no less than in the original schedule. *)
    Hypothesis H_job_costs_do_not_decrease:
      ∀ any_j, inflated_job_cost any_j ≥ job_cost any_j.

    (* Recall the schedule we constructed from sched_susp using these inflated costs. *)
    Let sched_new := reduction.sched_new job_arrival job_cost arr_seq higher_eq_priority
                                         sched_susp inflated_job_cost j R.

    (* Also recall the predicate we defined for a suspended job in the new schedule... *)
    Let suspended_in_sched_new :=
      reduction.suspended_in_sched_new job_arrival job_cost arr_seq higher_eq_priority
                                 sched_susp job_suspension_duration inflated_job_cost j R.

    (* ...and the corresponding suspension table. *)
    Let reduced_suspension_duration :=
      reduction.reduced_suspension_duration job_arrival job_cost arr_seq higher_eq_priority
                                   sched_susp job_suspension_duration inflated_job_cost j R.

    (* For simplicity, let's define some local names. *)
    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_new_bounded_by :=
      is_response_time_bound_of_job job_arrival inflated_job_cost sched_new.
    Let suspended_in_sched_susp :=
      suspended_at job_arrival job_cost job_suspension_duration sched_susp.
    Let job_is_late := reduction.job_is_late job_cost sched_susp inflated_job_cost sched_new.
    Let build_schedule := reduction.build_schedule job_arrival job_cost arr_seq higher_eq_priority
                                                   sched_susp inflated_job_cost j R.
    Let late_or_sched_jobs := reduction.jobs_that_are_late_or_scheduled_in_sched_susp
                                job_arrival job_cost arr_seq sched_susp inflated_job_cost sched_new.
    Let hp_job := reduction.highest_priority_job job_arrival arr_seq higher_eq_priority
                                                 inflated_job_cost sched_new.
    Let hp_late_job := reduction.highest_priority_late_job job_arrival job_cost arr_seq
                                       higher_eq_priority sched_susp inflated_job_cost sched_new.
    Let completed_in_sched_susp := completed_by job_cost sched_susp.
    Let completed_in_sched_new := completed_by inflated_job_cost sched_new.

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

      (* By showing that the construction function depends only on the service, ... *)
      Lemma sched_new_depends_only_on_service:
        ∀ sched1 sched2 t,
          (∀ j, service sched1 j t = service sched2 j t) →
          build_schedule sched1 t = build_schedule sched2 t.

      (* ...we infer that the new schedule is equivalent to the construction function. *)
      Corollary sched_new_uses_construction_function:
        ∀ t,
          sched_new t = build_schedule sched_new t.

    End PropertiesOfScheduleConstruction.

    (* In this section, we prove some properties about the generated schedule that
       only depend on the construction function but not on suspension times. *)
    Section BasicScheduleProperties.

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

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

      (* ...nor longer than their execution costs. *)
      Lemma sched_new_completed_jobs_dont_execute:
        completed_jobs_dont_execute inflated_job_cost sched_new.

    End BasicScheduleProperties.

    (* In this section, we prove some service invariants guaranteed by the new schedule
       up to time (arr_j + R).
       Note that these properties follow directly from the schedule construction and
       do not depend on suspension times. *)
    Section ServiceInvariant.

      (* Let t be any time in the interval [0, arr_j + R]. *)
      Variable t: time.
      Hypothesis H_before_R: t ≤ arr_j + R.

      (* By induction on time, we prove that for any job, the service received up to
         time t in the new schedule is no more than the service received up to time t in
         the original schedule, plus the difference between job costs due to inflation. *)
      Lemma sched_new_service_invariant:
        ∀ any_j,
          service sched_new any_j t
            ≤ service sched_susp any_j t + (inflated_job_cost any_j - job_cost any_j).

      (* From the previous lemma, we conclude that any job that completes in the new
         schedule up to time t must have completed in the original schedule as well. *)
      Corollary sched_new_jobs_complete_later:
        ∀ any_j,
          completed_by inflated_job_cost sched_new any_j t →
          completed_by job_cost sched_susp any_j t.

    End ServiceInvariant.

    (* In order to prove schedule properties that depend on suspension times, we first
       prove some facts about the suspension predicate we defined. *)
    Section SuspensionPredicate.

      (* Let any_j be any job. *)
      Variable any_j: Job.

      (* First, we show that if the suspension predicate holds for any_j at time t,
         then any_j must have arrived... *)
      Lemma suspended_in_sched_new_implies_arrived:
        ∀ t,
          suspended_in_sched_new any_j t → has_arrived job_arrival any_j t.

      (* ...and cannot have completed. *)
      Lemma suspended_in_sched_new_implies_not_completed:
        ∀ t,
          suspended_in_sched_new any_j t → ~~ completed_in_sched_new any_j t.

      (* Next, we show that if the suspension predicate changes from false at time t
         to true at time (t + 1), then any_j must be scheduled at time t. *)
      Lemma executes_before_suspension_in_sched_new:
        ∀ t,
          t < arr_j + R →
          has_arrived job_arrival any_j t →
          ~~ suspended_in_sched_new any_j t →
          suspended_in_sched_new any_j t.+1 →
          scheduled_at sched_new any_j t.

      (* For simplicity, let's call suspension_start the time following the last
         execution of a job. *)
      Let suspension_start := time_after_last_execution job_arrival.

      (* Then, we prove that if any_j is suspended at time t, it does not receive
         any service between time t and the previous beginning of suspension. *)
      Lemma suspended_in_sched_new_no_service_since_execution:
        ∀ t t_mid,
          suspended_in_sched_new any_j t →
          suspension_start sched_new any_j t ≤ t_mid < t →
          service sched_new any_j t ≤ service sched_new any_j t_mid.

      (* Next, we prove that if the suspension predicate holds for any_j at time t,
         then the latest execution of any_j in the new schedule is no earlier than
         its latest execution in the original schedule. *)
      Lemma suspended_in_sched_new_suspension_starts_no_earlier:
        ∀ t,
          has_arrived job_arrival any_j t →
          suspended_in_sched_new any_j t →
          suspension_start sched_susp any_j t ≤ suspension_start sched_new any_j t.

      (* using the previous lemmas, we conclude that the suspension predicate is continuous
         between any suspension point and the last execution of the job. *)
      Lemma suspended_in_sched_new_is_continuous:
        ∀ t t_mid,
          suspended_in_sched_new any_j t →
          suspension_start sched_new any_j t ≤ t_mid < t →
          suspended_in_sched_new any_j t_mid.

    End SuspensionPredicate.

    (* In this section, we prove some properties about the suspension table. *)
    Section SuspensionTable.

      (* First, we show that no job ever suspends after (arr_j + R). *)
      Lemma suspended_in_sched_new_only_inside_window:
        ∀ any_j t,
          arr_j + R ≤ t →
          ~~ suspended_at job_arrival inflated_job_cost reduced_suspension_duration
                          sched_new any_j t.

      (* Next, using the lemmas about the suspension predicate, we show that the suspension
         predicate for the new schedule matches the generated suspension table.
         (see model/schedule/uni/susp/build_suspension_table.v) *)
      Lemma sched_new_suspension_matches:
        ∀ any_j t,
          t < arr_j + R →
          suspended_in_sched_new any_j t =
          suspended_at job_arrival inflated_job_cost reduced_suspension_duration sched_new any_j t.

      (* Recall the definition of cumulative suspension in both schedules. *)
      Let cumulative_suspension_in_sched_susp :=
        cumulative_suspension job_arrival job_cost job_suspension_duration sched_susp.
      Let cumulative_suspension_in_sched_new :=
        cumulative_suspension job_arrival inflated_job_cost reduced_suspension_duration sched_new.

      (* To conclude, we prove that the cumulative suspension in the new schedule is no
         larger than in the original schedule,... *)
      Lemma sched_new_has_shorter_suspension:
        ∀ any_j t,
          cumulative_suspension_in_sched_new any_j t
          ≤ cumulative_suspension_in_sched_susp any_j t.

      (* ... which implies that the total suspension is also no larger. *)
      Corollary sched_new_has_shorter_total_suspension:
        ∀ any_j,
          total_suspension inflated_job_cost reduced_suspension_duration any_j ≤
          total_suspension job_cost job_suspension_duration any_j.

    End SuspensionTable.

    (* Having shown that the suspension table matches the suspension predicate,
       we now analyze the suspension predicate and prove that the generated
       schedule satisfies all the remaining properties. *)
    Section AdditionalScheduleProperties.

      (* First, we show that the new schedule respects self-suspensions. *)
      Lemma sched_new_respects_self_suspensions:
        respects_self_suspensions job_arrival inflated_job_cost reduced_suspension_duration sched_new.

      (* Next, we prove that the new schedule is (suspension-aware) work-conserving... *)
      Lemma sched_new_work_conserving:
        work_conserving job_arrival inflated_job_cost reduced_suspension_duration
                        arr_seq sched_new.

      (* ...and respects job priorities. *)
      Lemma sched_new_respects_policy:
        respects_JLDP_policy job_arrival inflated_job_cost reduced_suspension_duration
                             arr_seq sched_new higher_eq_priority.

    End AdditionalScheduleProperties.

    Section FinalRemarks.

      (* To summarize, we conclude that the new schedule is a valid suspension-aware schedule ...  *)
      Remark sched_new_is_valid:
        valid_suspension_aware_schedule job_arrival arr_seq higher_eq_priority
                                  reduced_suspension_duration inflated_job_cost sched_new.

      (* ...and that if the analyzed job j has response-time bound R in the schedule,
         then it also has response-time bound R in the original schedule. *)
      Remark sched_new_response_time_of_job_j:
        job_response_time_in_sched_new_bounded_by j R →
        job_response_time_in_sched_susp_bounded_by j R.

    End FinalRemarks.

  End ReductionProperties.

End SustainabilityAllCostsProperties.