Library prosa.classic.analysis.uni.susp.sustainability.allcosts.main_claim

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

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

(* In this file, we use the reduction we derived to show the weak sustainability with
   job costs and varying suspension times in the dynamic suspension model. *)
Module SustainabilityAllCostsProperty.

  Import ScheduleWithSuspensions Suspension Priority SuspensionIntervals
         PlatformWithSuspensions ResponseTime Sustainability
         ValidSuspensionAwareSchedule.

  Module reduction := SustainabilityAllCosts.
  Module reduction_prop := SustainabilityAllCostsProperties.

  Section SustainabilityProperty.

    Context {Task: eqType}.
    Context {Job: eqType}.

    Variable higher_eq_priority: JLDP_policy Job.
    Hypothesis H_priority_reflexive: JLDP_is_reflexive higher_eq_priority.
    Hypothesis H_priority_transitive: JLDP_is_transitive higher_eq_priority.

    Variable job_task: Job → Task.
    Variable task_suspension_bound: Task → duration.

    (* First, we state all properties about suspension, ... *)
    Let satisfies_suspension_properties (params: seq (job_parameter Job)) :=
      dynamic_suspension_model (return_param JOB_COST params) job_task
                               (return_param JOB_SUSPENSION params) task_suspension_bound.

    (* ...all properties of the schedule, ... *)
    Let satisfies_schedule_properties (params: seq (job_parameter Job)) (arr_seq: arrival_sequence Job)
                                      (sched: schedule Job) :=
      let job_arrival := return_param JOB_ARRIVAL params in
      let job_cost := return_param JOB_COST params in
      let job_suspension_duration := return_param JOB_SUSPENSION params in
        jobs_come_from_arrival_sequence sched arr_seq ∧
        jobs_must_arrive_to_execute job_arrival sched ∧
        completed_jobs_dont_execute job_cost sched ∧
        work_conserving job_arrival job_cost job_suspension_duration arr_seq sched ∧
        respects_JLDP_policy job_arrival job_cost job_suspension_duration arr_seq
                             sched higher_eq_priority ∧
        respects_self_suspensions job_arrival job_cost job_suspension_duration sched.

    (* ...and all properties of the arrival sequence. *)
    Let satisfies_arrival_sequence_properties (params: seq (job_parameter Job))
                                              (arr_seq: arrival_sequence Job) :=
      arrival_times_are_consistent (return_param JOB_ARRIVAL params) arr_seq ∧
      JLDP_is_total arr_seq higher_eq_priority.

    (* Then, we define the task model as the combination of such properties. *)
    Let belongs_to_task_model (params: seq (job_parameter Job))
                              (arr_seq: arrival_sequence Job) (sched: schedule Job) :=
      satisfies_arrival_sequence_properties params arr_seq ∧
      satisfies_schedule_properties params arr_seq sched ∧
      satisfies_suspension_properties params.

    (* We use as schedulability property the notion of response-time bound, i.e., we are
       going to show that improving job parameters leads to "no worse response times". *)
    Variable R: time.
    Let response_time_bounded_by_R (params: seq (job_parameter Job)) (sched: schedule Job) (j: Job) :=
      is_response_time_bound_of_job (return_param JOB_ARRIVAL params)
                                    (return_param JOB_COST params) sched j R.

    (* Next, we recall the definition of weakly-sustainable policy with job costs
       and varying suspension times... *)
    Let all_params := [:: JOB_ARRIVAL; JOB_COST; JOB_SUSPENSION].
    Let sustainable_param := JOB_COST.
    Let variable_params := [:: JOB_SUSPENSION].
    Let has_better_sustainable_param (cost cost': Job → time) := ∀ j, cost j ≥ cost' j.

    Let weakly_sustainable_with_job_costs_and_variable_suspension_times :=
      weakly_sustainable all_params response_time_bounded_by_R belongs_to_task_model
                         sustainable_param has_better_sustainable_param variable_params.

    (* ...and prove that it holds for this scheduling policy and task model. *)
    Theorem policy_is_weakly_sustainable:
      weakly_sustainable_with_job_costs_and_variable_suspension_times.

    End SustainabilityProperty.

End SustainabilityAllCostsProperty.